InvariantChecker.scala 7.63 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
21

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

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

  def checkOnZ3(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
26
    
Christian Müller's avatar
Christian Müller committed
27
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
    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
62
    }
Christian Müller's avatar
Christian Müller committed
63
64
    logger.info(s"Z3 call took $time ms")
    res
Christian Müller's avatar
Christian Müller committed
65
  }
Christian Müller's avatar
checker    
Christian Müller committed
66

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

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

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

    val f = Implies(pre, firstprecond)

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

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

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

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

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

        // take one edge to prove
103
104
105
106
107
108
//        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)
        
109
110
111
        // try to prove
        val pre = labels(next._1)
        val post = labels(next._2)
Christian Müller's avatar
Christian Müller committed
112
        val isfirst = !next._1.hasPredecessors
113
        val (status, solver) = checkBlockInvariant(spec, next, pre, post, stubborn, isfirst)
114
115
116

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

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

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

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

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

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

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

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

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

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

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