InvariantChecker.scala 7.69 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
import de.tum.workflows.Utils
Christian Müller's avatar
Christian Müller committed
20
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
21
22

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

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

  def checkOnZ3(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
27
    
Christian Müller's avatar
Christian Müller committed
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
    val (time, res) = Utils.time {
      // Set up Z3
      val cfg = new HashMap[String, String]()
      cfg.put("timeout", TIMEOUT.toString())
      val ctx = new Context(cfg)
  
      //    val qe = ctx.mkTactic("qe")
      //    val default = ctx.mkTactic("smt")
      //    val t = ctx.andThen(qe, default)
      //    val s = ctx.mkSolver(t)
  
      val s = ctx.mkSolver()
      
      // Can only check universal things
      val neg = Neg(f).simplify()
  
      // univfree is now in E*, so can be solved as SAT Problem
      val stripped = FormulaFunctions.stripQuantifiers(neg)
  
      // val prefix = FormulaFunctions.collectQuantifiersSub(univfree)
      val satform = FOTransformers.eliminatePredicates(stripped)
  
      // Checking QFree
      s.add(Z3QFree.translate(satform, ctx))
  
      // Send to z3
      val c = s.check()
      if (c == Status.UNKNOWN) {
        logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
      }
      if (c == Status.SATISFIABLE) {
//        logger.info(s"Z3 status satisfiable")
        //      logger.info(s"${s.getModel()}")
      }
      (c, s)
Christian Müller's avatar
checker    
Christian Müller committed
63
    }
Christian Müller's avatar
Christian Müller committed
64
65
    logger.info(s"Z3 call took $time ms")
    res
Christian Müller's avatar
Christian Müller committed
66
  }
Christian Müller's avatar
checker    
Christian Müller committed
67

68
69
  def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
    val precond = Preconditions.abstractPrecondition(post, b, stubborn, spec)
70

Christian Müller's avatar
Christian Müller committed
71
    // TODO: do we do this here?
72
    val firstprecond = if (isfirst) {
Christian Müller's avatar
Christian Müller committed
73
      precond.assumeEmpty(Properties.INFNAME :: spec.w.sig.preds.map(_.name).toList)
Christian Müller's avatar
Christian Müller committed
74
    } else { precond }
75
76
77
78
79
80
81
82

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

    val f = Implies(pre, firstprecond)

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

83
84
    checkOnZ3(f.simplify())
  }
85

86
87
  def checkInvariantFP(spec: Spec, inv: Formula, stubborn: Boolean) = {
    val graph = Encoding.toGraph(spec.w)
88
89
90
91
    type Node = graph.NodeT
    type Edge = graph.EdgeT

    @tailrec
92
    def checkInvariantRec(labellist: List[Map[Node, Formula]], provenlist: List[Set[Edge]]): (Boolean, List[Map[Node, Formula]], List[Set[Edge]]) = {
93

94
95
      val labels = labellist.head
      val proven = provenlist.head
96
97
98
      // 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
99
        logger.info("Everything proven. Terminating.")
100
        (true, labellist, provenlist)
101
102
103
      } else {

        // take one edge to prove
104
105
106
107
108
109
//        val next = toProve.head
        // take the edge with a minimum of following unproven edges excluding selfloops
//        val next = toProve.minBy(edge => ((edge.target.outgoing.filter(t => t.target != t.source) -- proven).size))
        // take the edge with maximum source node first
        val next = toProve.maxBy(edge => edge.source.value)
        
110
111
112
        // try to prove
        val pre = labels(next._1)
        val post = labels(next._2)
Christian Müller's avatar
Christian Müller committed
113
        val isfirst = !next._1.hasPredecessors
114
        val (status, solver) = checkBlockInvariant(spec, next, pre, post, stubborn, isfirst)
115
116
117

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
118
119
          // --> safe, continue with larger proven set.
          logger.info(s"Proven inductiveness for (${next._1} -> ${next._2}).")
120
          checkInvariantRec(labels :: labellist, (proven + next) :: provenlist)
121
122
123
124
        } 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
125
          // never relabel initial node
Christian Müller's avatar
Christian Müller committed
126
          logger.info(s"Invariant not inductive, strengthening")
Christian Müller's avatar
Christian Müller committed
127
          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
128
129
130
131
132
133
134
135
            // check if strengthened -> old_inv else use conjunction
            val strengthened = Preconditions.abstractPrecondition(post, next, stubborn, spec)
//            val newinv = if (checkOnZ3(Implies(labels(next._1), strengthened))._1 == Status.SATISFIABLE) {
//            	And(labels(next._1), strengthened).simplify()
//            } else {
//            	strengthened.simplify()
//            }
            val newinv = And(labels(next._1), strengthened).simplify()
Christian Müller's avatar
Christian Müller committed
136
            
Christian Müller's avatar
Christian Müller committed
137
            val (status2, solver2) = checkOnZ3(Implies(newinv, False))
Christian Müller's avatar
Christian Müller committed
138
            
Christian Müller's avatar
Christian Müller committed
139
140
141
142
143
            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
144
145
146
147
148
149
150
  
            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
151
              // Negation of newinv still sat, newinv does not imply false)
Christian Müller's avatar
Christian Müller committed
152
              logger.info(s"Relabeling ${next._1}. Continuing.")
153
              checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
154
155
            } else {
              logger.info(s"New invariant for ${next._1} not satisfiable. Terminating.")
156
              (false, newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
157
            }
158
          } else {
Christian Müller's avatar
Christian Müller committed
159
            logger.info("Would have to relabel initial node. Terminating.")
160
            (false, labellist, provenlist)
161
162
163
          }
        }
      }
164
165
    }

Christian Müller's avatar
Christian Müller committed
166
167
    // create labelling - FIXME: maybe use inv only for last
    val labels = (for (n <- graph.nodes) yield { n -> inv }).toMap
168
169
170
    val (result, afterlabels, proven) = checkInvariantRec(labels, List(Set()))
    
    val dot1 = afterlabels.zip(proven).reverse
171

172
173
174
    val dot2 = dot1.map((tup) => Encoding.toDot(graph)(tup._1.map(t => (t._1, t._2.pretty())), tup._2))
    
    (result, dot2)
175
  }
Christian Müller's avatar
Christian Müller committed
176
  
177
  def checkInvariantOnce(spec: Spec, inv: Formula, stubborn: Boolean) = {
Christian Müller's avatar
checker    
Christian Müller committed
178

Christian Müller's avatar
Christian Müller committed
179
    // Build graph
180
    val graph = Encoding.toGraph(spec.w)
Christian Müller's avatar
checker    
Christian Müller committed
181

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

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

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

191
192
193
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
194

195
      val (res, solver) = checkBlockInvariant(spec, b, inv, inv, stubborn, isfirst)
196

Christian Müller's avatar
Christian Müller committed
197
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
198
199
200
        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
201
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
202
203
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
204
205
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
206
207
208
209
210
211
        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
212

Christian Müller's avatar
Christian Müller committed
213
214
    val safe = list.reduceLeft(_ && _)
    if (safe) {
215
      msg ++= s"Proven safe.\n"
216
      logger.info(s"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
217
    }
Christian Müller's avatar
Christian Müller committed
218
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
219
220
  }
}