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
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
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
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
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
Christian Müller committed
46
    // Checking QFree
47
    s.add(Z3QFree.translate(satform, ctx))
Christian Müller's avatar
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
Christian Müller committed
57 58
    }
    (c, s)
Christian Müller's avatar
Christian Müller committed
59
  }
Christian Müller's avatar
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

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