InvariantChecker.scala 7.47 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
6
7
8
9
package de.tum.workflows.toz3

import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Implicits._
import de.tum.workflows.WorkflowParser
import de.tum.workflows.Encoding
import de.tum.workflows.Preconditions
Christian Müller's avatar
Christian Müller committed
10
11
import de.tum.workflows.foltl.Properties.T1
import de.tum.workflows.foltl.Properties.T2
Christian Müller's avatar
Christian Müller committed
12
13
14
15
16
17
18

import scalax.collection.edge.LDiEdge // labeled directed edge
import com.microsoft.z3.Context
import java.util.HashMap
import org.omg.CORBA.TIMEOUT
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
19
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
testing    
Christian Müller committed
20
import de.tum.workflows.foltl.FormulaFunctions
21
22
23
import scalax.collection.Graph
import de.tum.workflows.Encoding.WorkflowGraph
import scala.annotation.tailrec
Christian Müller's avatar
Christian Müller committed
24
25

object InvariantChecker extends LazyLogging {
Christian Müller's avatar
checker    
Christian Müller committed
26

Christian Müller's avatar
Christian Müller committed
27
  val TIMEOUT = 60000 // in milliseconds
Christian Müller's avatar
checker    
Christian Müller committed
28
29
30
31
32
33

  def checkOnZ3(f: Formula) = {
    // Set up Z3
    val cfg = new HashMap[String, String]()
    cfg.put("timeout", TIMEOUT.toString())
    val ctx = new Context(cfg)
34

35
36
37
38
    //    val qe = ctx.mkTactic("qe")
    //    val default = ctx.mkTactic("smt")
    //    val t = ctx.andThen(qe, default)
    //    val s = ctx.mkSolver(t)
39

Christian Müller's avatar
testing    
Christian Müller committed
40
    val s = ctx.mkSolver()
Christian Müller's avatar
checker    
Christian Müller committed
41

42
43
44
45
46
47
48
49
50
51
52
53
54
    // Make QFree - will work for any A* or A*E* formula
    val tocheck = Neg(f).simplify()
    if (!tocheck.isBS()) {
      logger.error(s"Not in BS: ${tocheck.pretty}")
    }
    val univfree = LTL.instantiateUniversals(tocheck)

    // univfree is now in E*, so can be solved as SAT Problem
    val stripped = FormulaFunctions.stripQuantifiers(univfree)

    // val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
    val satform = LTL.eliminatePredicates(stripped)

Christian Müller's avatar
testing    
Christian Müller committed
55
    // Checking QFree
56
    s.add(Z3QFree.translate(satform, ctx))
Christian Müller's avatar
checker    
Christian Müller committed
57
58
59
60
61
62
63

    // Send to z3
    val c = s.check()
    if (c == Status.UNKNOWN) {
      logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
    }
    if (c == Status.SATISFIABLE) {
64
      logger.info(s"Z3 status satisfiable")
65
      //      logger.info(s"${s.getModel()}")
Christian Müller's avatar
checker    
Christian Müller committed
66
67
    }
    (c, s)
Christian Müller's avatar
Christian Müller committed
68
  }
Christian Müller's avatar
checker    
Christian Müller committed
69

70
  def checkBlockInvariant(sig: Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
71
72
73
74
75
76
77
78
    val precond = Preconditions.weakestPrecondition(post, b)

    // Stubborn agents -> remove trace variable from choice predicate
    val stubprecond = if (stubborn) {
      precond.everywhere {
        case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
      }
    } else precond
79

Christian Müller's avatar
Christian Müller committed
80
    // TODO: do we do this here?
81
82
83
84
85
86
87
88
89
90
91
    val firstprecond = if (isfirst) {
      stubprecond.assumeEmpty(sig.preds.map(_.name).toList)
    } else { stubprecond }

    //      val test1 = inv.toPrenex()
    //      val test2 = stubprecond.toPrenex()

    val f = Implies(pre, firstprecond)

    logger.info(s"Checking invariant implication for $b")

92
93
    checkOnZ3(f.simplify())
  }
94

95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
  def checkInvariantFP(w: Workflow, inv: Formula, stubborn: Boolean) = {
    val graph = Encoding.toGraph(w)
    type Node = graph.NodeT
    type Edge = graph.EdgeT

    @tailrec
    def checkInvariantRec(labels: Map[Node, Formula], proven: Set[Edge]): Option[Map[Node, Formula]] = {

      // check if done, i.e. all edges proven
      val toProve = (graph.edges -- proven)
      if (toProve.isEmpty) {
        Some(labels)
      } else {

        // take one edge to prove
        val next = toProve.head

        // try to prove
        val pre = labels(next._1)
        val post = labels(next._2)
        val (status, solver) = checkBlockInvariant(w.sig, next, pre, post, stubborn, next._1.hasPredecessors)

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
          // --> safe, continue with larger proven set
          checkInvariantRec(labels, proven + next)
        } else {
          // Negation of implication sat
          // --> unsafe, relabel incoming node, invalidate all proven guarantees for that node
          // check if relabelled invariant still satisfiable
          val newinv = And(labels(next._1), Preconditions.weakestPrecondition(post, next))
          val (status2, solver2) = checkOnZ3(newinv)

          val newlabels = labels.updated(next._1, newinv)
          val newproven = proven.filterNot(_._1 == next._1)

          if (status2 == Status.UNSATISFIABLE) {
            // Negation of newinv still unsat, newinv still sat
            checkInvariantRec(newlabels, newproven)
          } else {
            None
          }
        }
      }
139
140
    }

141
142
143
    // create labelling
    val labels = (for (n <- graph.nodes) yield { n -> inv }) toMap
    val result = checkInvariantRec(labels, Set())
144

145
    val dot = Encoding.toDot(graph, labels.map(t => (t._1, t._2.pretty())))
146

147
    (result, dot)
148
149
  }

150
  def checkInvariantOnce(w: Workflow, inv: Formula, stubborn: Boolean) = {
Christian Müller's avatar
checker    
Christian Müller committed
151

Christian Müller's avatar
Christian Müller committed
152
153
    // Build graph
    val graph = Encoding.toGraph(w)
Christian Müller's avatar
checker    
Christian Müller committed
154

Christian Müller's avatar
Christian Müller committed
155
    val msg = new StringBuilder()
156
    msg ++= s"Trying to prove safe with invariant:\n\n${inv.pretty()}\n\n"
Christian Müller's avatar
checker    
Christian Müller committed
157

158
    // Check all edges
Christian Müller's avatar
Christian Müller committed
159
    val list = for (e <- graph.edges) yield {
Christian Müller's avatar
checker    
Christian Müller committed
160

Christian Müller's avatar
Christian Müller committed
161
      // Check I -> WP[w](inv)
Christian Müller's avatar
checker    
Christian Müller committed
162
      val b: SimpleBlock = e
163

164
165
166
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
167

168
      val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
169

Christian Müller's avatar
Christian Müller committed
170
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
171
172
173
        msg ++= s"Possibly unsafe: Block may not uphold invariant:\n\n${e.label}\n\n"
        if (res == Status.SATISFIABLE) {
          msg ++= "Satisfying model:\n"
Christian Müller's avatar
Christian Müller committed
174
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
175
176
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
177
178
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
179
180
181
182
183
184
        logger.info(s"Could not prove invariant $inv")
        logger.info(s"Z3 status $res")
        logger.info(s"Block ${e.label} may not uphold it")
      }
      res == Status.UNSATISFIABLE
    }
Christian Müller's avatar
checker    
Christian Müller committed
185

Christian Müller's avatar
Christian Müller committed
186
187
    val safe = list.reduceLeft(_ && _)
    if (safe) {
188
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
189
      logger.info(s"Workflow $w\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
190
    }
Christian Müller's avatar
Christian Müller committed
191
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
192
  }
Christian Müller's avatar
checker    
Christian Müller committed
193
194

  def genEq(f: Fun, p: List[Var]) = {
Christian Müller's avatar
Christian Müller committed
195
196
197
    val newf = f.parallelRename(f.params, p)
    Eq(newf.in(T1), newf.in(T2))
  }
Christian Müller's avatar
checker    
Christian Müller committed
198
199

  def invariantNoninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
200
    val agent = spec.target.params(0)
Christian Müller's avatar
checker    
Christian Müller committed
201
202

    val premise = And.make(for ((o, t) <- spec.declass) yield {
203
      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
Christian Müller's avatar
Christian Müller committed
204
      Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
Christian Müller's avatar
Christian Müller committed
205
    })
Christian Müller's avatar
checker    
Christian Müller committed
206

Christian Müller's avatar
Christian Müller committed
207
208
    val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
      val quant = r.params.drop(1)
Christian Müller's avatar
checker    
Christian Müller committed
209
      Forall(quant, genEq(r, agent :: quant))
Christian Müller's avatar
Christian Müller committed
210
    })
Christian Müller's avatar
checker    
Christian Müller committed
211

Christian Müller's avatar
Christian Müller committed
212
    Forall(agent, premise  conclusion).simplify()
Christian Müller's avatar
Christian Müller committed
213
  }
Christian Müller's avatar
checker    
Christian Müller committed
214

215
216
217
218
  def invariantNoninterStubbornBS(spec: Spec) = {
    val agent = spec.target.params(0)

    val premise = for ((o, t) <- spec.declass) yield {
219
      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2)
220
221
222
223
224
225
226
227
228
229
230
231
      (o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
    }
    val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles

    val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
      val quant = r.params.drop(1)
      Forall(quant, genEq(r, agent :: quant))
    })

    Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
  }

Christian Müller's avatar
Christian Müller committed
232
233
234
235
236
237
  def invariantAllEqual(spec: Spec) = {
    And.make(for (r <- spec.w.sig.preds.toList) yield {
      Forall(r.params, genEq(r, r.params))
    })
  }

Christian Müller's avatar
Christian Müller committed
238
}