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
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
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
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
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
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

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
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
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
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
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
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
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
  }
}