InvariantChecker.scala 7.02 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 62
  def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
    val precond = Preconditions.abstractPrecondition(post, b, stubborn, spec)
63

64
    // TODO: do we do this here?
65
    val firstprecond = if (isfirst) {
66
      precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
Christian Müller's avatar
Christian Müller committed
67
    } 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
  def checkInvariantFP(spec: Spec, inv: Formula, stubborn: Boolean) = {
    val graph = Encoding.toGraph(spec.w)
81 82 83 84
    type Node = graph.NodeT
    type Edge = graph.EdgeT

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

87 88
      val labels = labellist.head
      val proven = provenlist.head
89 90 91
      // 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
92
        logger.info("Everything proven. Terminating.")
93
        (true, labellist, provenlist)
94 95 96
      } else {

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

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

Christian Müller's avatar
Christian Müller committed
151 152
    // create labelling - FIXME: maybe use inv only for last
    val labels = (for (n <- graph.nodes) yield { n -> inv }).toMap
153 154 155
    val (result, afterlabels, proven) = checkInvariantRec(labels, List(Set()))
    
    val dot1 = afterlabels.zip(proven).reverse
156

157 158 159
    val dot2 = dot1.map((tup) => Encoding.toDot(graph)(tup._1.map(t => (t._1, t._2.pretty())), tup._2))
    
    (result, dot2)
160
  }
Christian Müller's avatar
Christian Müller committed
161
  
162
  def checkInvariantOnce(spec: Spec, inv: Formula, stubborn: Boolean) = {
Christian Müller's avatar
Christian Müller committed
163

Christian Müller's avatar
Christian Müller committed
164
    // Build graph
165
    val graph = Encoding.toGraph(spec.w)
Christian Müller's avatar
Christian Müller committed
166

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

170
    // Check all edges
Christian Müller's avatar
Christian Müller committed
171
    val list = for (e <- graph.edges) yield {
Christian Müller's avatar
Christian Müller committed
172

Christian Müller's avatar
Christian Müller committed
173
      // Check I -> WP[w](inv)
Christian Müller's avatar
Christian Müller committed
174
      val b: SimpleBlock = e
175

176 177 178
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
179

180
      val (res, solver) = checkBlockInvariant(spec, b, inv, inv, stubborn, isfirst)
181

Christian Müller's avatar
Christian Müller committed
182
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
183 184 185
        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
186
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
187 188
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
189 190
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
191 192 193 194 195 196
        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
197

Christian Müller's avatar
Christian Müller committed
198 199
    val safe = list.reduceLeft(_ && _)
    if (safe) {
200
      msg ++= s"Proven safe.\n"
201
      logger.info(s"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
202
    }
Christian Müller's avatar
Christian Müller committed
203
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
204 205
  }
}