InvariantChecker.scala 6.4 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
package de.tum.workflows.toz3

Christian Müller's avatar
Christian Müller committed
3
import java.util.HashMap
Christian Müller's avatar
Christian Müller committed
4

Christian Müller's avatar
Christian Müller committed
5
6
7
import scala.annotation.tailrec

// labeled directed edge
Christian Müller's avatar
Christian Müller committed
8
9
10
import com.microsoft.z3.Context
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
11
12
13
14
15
16

import de.tum.workflows.Encoding
import de.tum.workflows.Implicits._
import de.tum.workflows.Preconditions
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
testing    
Christian Müller committed
17
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
18
import de.tum.workflows.ltl.FOTransformers
Christian Müller's avatar
Christian Müller committed
19
20

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

Christian Müller's avatar
Christian Müller committed
22
  val TIMEOUT = 60000 // in milliseconds
Christian Müller's avatar
checker    
Christian Müller committed
23
24
25
26
27
28

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

30
31
32
33
    //    val qe = ctx.mkTactic("qe")
    //    val default = ctx.mkTactic("smt")
    //    val t = ctx.andThen(qe, default)
    //    val s = ctx.mkSolver(t)
34

Christian Müller's avatar
testing    
Christian Müller committed
35
    val s = ctx.mkSolver()
Christian Müller's avatar
Christian Müller committed
36
37
38
    
    // Can only check universal things
    val neg = Neg(f).simplify()
39
40

    // univfree is now in E*, so can be solved as SAT Problem
Christian Müller's avatar
Christian Müller committed
41
    val stripped = FormulaFunctions.stripQuantifiers(neg)
42
43

    // val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
Christian Müller's avatar
Christian Müller committed
44
    val satform = FOTransformers.eliminatePredicates(stripped)
45

Christian Müller's avatar
testing    
Christian Müller committed
46
    // Checking QFree
47
    s.add(Z3QFree.translate(satform, ctx))
Christian Müller's avatar
checker    
Christian Müller committed
48
49
50
51
52
53
54

    // Send to z3
    val c = s.check()
    if (c == Status.UNKNOWN) {
      logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
    }
    if (c == Status.SATISFIABLE) {
55
      logger.info(s"Z3 status satisfiable")
56
      //      logger.info(s"${s.getModel()}")
Christian Müller's avatar
checker    
Christian Müller committed
57
58
    }
    (c, s)
Christian Müller's avatar
Christian Müller committed
59
  }
Christian Müller's avatar
checker    
Christian Müller committed
60

61
  def checkBlockInvariant(sig: Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
Christian Müller's avatar
Christian Müller committed
62
    val precond = Preconditions.abstractPrecondition(post, b, stubborn)
63

Christian Müller's avatar
Christian Müller committed
64
    // TODO: do we do this here?
65
    val firstprecond = if (isfirst) {
Christian Müller's avatar
Christian Müller committed
66
67
      precond.assumeEmpty(sig.preds.map(_.name).toList)
    } else { precond }
68
69
70
71
72
73
74
75

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

    val f = Implies(pre, firstprecond)

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

76
77
    checkOnZ3(f.simplify())
  }
78

79
80
81
82
83
84
  def checkInvariantFP(w: Workflow, inv: Formula, stubborn: Boolean) = {
    val graph = Encoding.toGraph(w)
    type Node = graph.NodeT
    type Edge = graph.EdgeT

    @tailrec
Christian Müller's avatar
Christian Müller committed
85
    def checkInvariantRec(labels: Map[Node, Formula], proven: Set[Edge]): (Boolean, Map[Node, Formula], Set[Edge]) = {
86
87
88
89

      // check if done, i.e. all edges proven
      val toProve = (graph.edges -- proven)
      if (toProve.isEmpty) {
Christian Müller's avatar
Christian Müller committed
90
        logger.info("Everything proven. Terminating.")
Christian Müller's avatar
Christian Müller committed
91
        (true, labels, proven)
92
93
94
95
96
97
98
99
      } else {

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

        // try to prove
        val pre = labels(next._1)
        val post = labels(next._2)
Christian Müller's avatar
Christian Müller committed
100
101
        val isfirst = !next._1.hasPredecessors
        val (status, solver) = checkBlockInvariant(w.sig, next, pre, post, stubborn, isfirst)
102
103
104

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
105
106
          // --> safe, continue with larger proven set.
          logger.info(s"Proven inductiveness for (${next._1} -> ${next._2}).")
107
108
109
110
111
          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
Christian Müller's avatar
Christian Müller committed
112
113
          // never relabel initial node
          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
114
            val newinv = And(labels(next._1), Preconditions.abstractPrecondition(post, next, stubborn)).simplify()
Christian Müller's avatar
Christian Müller committed
115
            
Christian Müller's avatar
Christian Müller committed
116
            val (status2, solver2) = checkOnZ3(Implies(newinv, False))
Christian Müller's avatar
Christian Müller committed
117
            
Christian Müller's avatar
Christian Müller committed
118
119
120
121
122
            val nostrangebindings = FormulaFunctions.checkBindings(newinv)
            if (!nostrangebindings) {
              logger.error("New invariant binds variables more than once")
              logger.error(s"Invariant would be $newinv")
            }
Christian Müller's avatar
Christian Müller committed
123
124
125
126
127
128
129
  
            val newlabels = labels.updated(next._1, newinv)
            val invalidated = proven.filter(_._2 == next._1)
            
            val newproven = (proven -- invalidated) + next
  
            if (status2 == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
130
              // Negation of newinv still sat, newinv does not imply false)
Christian Müller's avatar
Christian Müller committed
131
132
133
134
135
136
              logger.info(s"Relabeling ${next._1}. Continuing.")
              checkInvariantRec(newlabels, newproven)
            } else {
              logger.info(s"New invariant for ${next._1} not satisfiable. Terminating.")
              (false, newlabels, newproven)
            }
137
          } else {
Christian Müller's avatar
Christian Müller committed
138
139
            logger.info("Would have to relabel initial node. Terminating.")
            (false, labels, proven)
140
141
142
          }
        }
      }
143
144
    }

Christian Müller's avatar
Christian Müller committed
145
146
    // create labelling - FIXME: maybe use inv only for last
    val labels = (for (n <- graph.nodes) yield { n -> inv }).toMap
Christian Müller's avatar
Christian Müller committed
147
    val (result, afterlabels, proven) = checkInvariantRec(labels, Set())
148

Christian Müller's avatar
Christian Müller committed
149
    val dot = Encoding.toDot(graph)(afterlabels.map(t => (t._1, t._2.pretty())), proven)
150
    (result, dot)
151
  }
Christian Müller's avatar
Christian Müller committed
152
  
153
  def checkInvariantOnce(w: Workflow, inv: Formula, stubborn: Boolean) = {
Christian Müller's avatar
checker    
Christian Müller committed
154

Christian Müller's avatar
Christian Müller committed
155
156
    // Build graph
    val graph = Encoding.toGraph(w)
Christian Müller's avatar
checker    
Christian Müller committed
157

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

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

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

167
168
169
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
170

171
      val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
172

Christian Müller's avatar
Christian Müller committed
173
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
174
175
176
        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
177
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
178
179
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
180
181
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
182
183
184
185
186
187
        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
188

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