InvariantChecker.scala 8.59 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
Christian Müller's avatar
Christian Müller committed
4
import java.util.HashMap
Christian Müller's avatar
Christian Müller committed
5

Christian Müller's avatar
Christian Müller committed
6 7 8
import scala.annotation.tailrec

// labeled directed edge
Christian Müller's avatar
Christian Müller committed
9 10 11
import com.microsoft.z3.Context
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
12 13 14 15 16 17

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
18
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
19
import de.tum.workflows.ltl.FOTransformers
Christian Müller's avatar
Christian Müller committed
20
import de.tum.workflows.Utils
Christian Müller's avatar
Christian Müller committed
21
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
22

Christian Müller's avatar
Christian Müller committed
23 24
case class InvProperties(stubborn:Boolean, eliminateAux:Boolean) { }
object InvProperties {
Christian Müller's avatar
Christian Müller committed
25
  val DEFAULT = InvProperties(stubborn = true, eliminateAux = true)
Christian Müller's avatar
Christian Müller committed
26 27
}

Christian Müller's avatar
Christian Müller committed
28
object InvariantChecker extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
29

Christian Müller's avatar
Christian Müller committed
30
  val TIMEOUT = 60000 // in milliseconds
Christian Müller's avatar
Christian Müller committed
31 32

  def checkOnZ3(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
33
    
Christian Müller's avatar
Christian Müller committed
34 35
    val (time, res) = Utils.time {
      // Set up Z3
Christian Müller's avatar
Christian Müller committed
36
      val cfg = new util.HashMap[String, String]()
Christian Müller's avatar
Christian Müller committed
37 38 39 40 41 42 43 44 45 46 47 48 49
      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()
  
Christian Müller's avatar
Christian Müller committed
50
      // neg is now in E*, so can be solved as SAT Problem
Christian Müller's avatar
Christian Müller committed
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
      val stripped = FormulaFunctions.stripQuantifiers(neg)
  
      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
68
    }
Christian Müller's avatar
Christian Müller committed
69 70
    logger.info(s"Z3 call took $time ms")
    res
Christian Müller's avatar
Christian Müller committed
71
  }
Christian Müller's avatar
Christian Müller committed
72

Christian Müller's avatar
Christian Müller committed
73 74 75
  def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, isfirst: Boolean, properties:InvProperties) = {
    val precond = Preconditions.abstractPrecondition(post, b, spec, properties)
    
76
    // TODO: do we do this here?
77
    val firstprecond = if (isfirst) {
Christian Müller's avatar
Christian Müller committed
78
      precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
Christian Müller's avatar
Christian Müller committed
79
    } else { precond }
Christian Müller's avatar
Christian Müller committed
80 81 82 83 84 85 86
    val noinfprecond = if (isfirst) {
      firstprecond.assumeEmpty(List(Properties.INFNAME))
    } else { firstprecond }
    
    val z3simpednewinv = Z3QFree.simplifyUniv(noinfprecond)
    val gained = noinfprecond.toString().length() - z3simpednewinv.toString().length()
    logger.info(s"Invariant shrunken by $gained chars")
87 88 89 90

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

Christian Müller's avatar
Christian Müller committed
91
    val f = Implies(pre, z3simpednewinv)
92 93 94

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

Christian Müller's avatar
Christian Müller committed
95
    (checkOnZ3(f.simplify()), z3simpednewinv)
96
  }
97

Christian Müller's avatar
Christian Müller committed
98
  def checkInvariantFPLabelling(spec: Spec, inv: Formula, properties:InvProperties) = {
99
    val graph = Encoding.toGraph(spec.w)
100 101 102 103
    type Node = graph.NodeT
    type Edge = graph.EdgeT

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

106 107
      val labels = labellist.head
      val proven = provenlist.head
108
      // check if done, i.e. all edges proven
Christian Müller's avatar
Christian Müller committed
109
      val toProve = graph.edges -- proven
110
      if (toProve.isEmpty) {
Christian Müller's avatar
Christian Müller committed
111
        logger.info("Everything proven. Terminating.")
112
        (true, labellist, provenlist)
113 114 115
      } else {

        // take one edge to prove
116 117 118 119 120 121
//        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)
        
122 123 124
        // try to prove
        val pre = labels(next._1)
        val post = labels(next._2)
Christian Müller's avatar
Christian Müller committed
125
        val isfirst = !next._1.hasPredecessors
Christian Müller's avatar
Christian Müller committed
126
        val ((status, solver), strengthened) = checkBlockInvariant(spec, next, pre, post, isfirst, properties)
127 128 129

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
130 131
          // --> safe, continue with larger proven set.
          logger.info(s"Proven inductiveness for (${next._1} -> ${next._2}).")
132
          checkInvariantRec(labels :: labellist, (proven + next) :: provenlist)
133 134 135 136
        } 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
137
          // never relabel initial node
138
          logger.info(s"Invariant not inductive, strengthening.")
Christian Müller's avatar
Christian Müller committed
139

Christian Müller's avatar
Christian Müller committed
140 141 142 143 144 145 146 147 148 149 150
          val newinv = And(labels(next._1), strengthened).simplify()

          val nostrangebindings = FormulaFunctions.checkBindings(newinv)
          if (!nostrangebindings) {
            logger.error("New invariant binds variables more than once")
            logger.error(s"Invariant would be $newinv")
          }

          val newlabels = labels.updated(next._1, strengthened)

          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
151
            val invalidated = proven.filter(_._2 == next._1)
Christian Müller's avatar
Christian Müller committed
152

Christian Müller's avatar
Christian Müller committed
153
            val newproven = (proven -- invalidated) + next
Christian Müller's avatar
Christian Müller committed
154

Christian Müller's avatar
Christian Müller committed
155
            val (status2, solver2) = checkOnZ3(Implies(newinv, False))
Christian Müller's avatar
Christian Müller committed
156
            if (status2 == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
157
              // Negation of newinv still sat, newinv does not imply false)
158
              logger.info(s"Relabeling ${next._1}. New size: ${newinv.opsize()}. Continuing.")
159
              checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
160 161
            } else {
              logger.info(s"New invariant for ${next._1} not satisfiable. Terminating.")
162
              (false, newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
163
            }
164
          } else {
Christian Müller's avatar
Christian Müller committed
165 166 167
            logger.info("Relabelled initial node. Terminating.")
            // logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
            (false, newlabels, provenlist)
168 169 170
          }
        }
      }
171 172
    }

Christian Müller's avatar
Christian Müller committed
173 174
    // 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
175
    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(labels, List(Set())) }
176
    
Christian Müller's avatar
Christian Müller committed
177
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
178
    val dot2 = dot1.map(tup => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
Christian Müller's avatar
Christian Müller committed
179 180
      if (t._2.opsize() <= 5000) t._2.pretty() else "TOO BIG"
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
181 182 183 184

    // Find out label of initial node
    val startnode = graph.find(0).get
    val headlabel = labellings.last.get(startnode).get
185
    
Christian Müller's avatar
Christian Müller committed
186
    (result, graph, labellings.reverse, proven.reverse, dot2, time, headlabel)
Christian Müller's avatar
Christian Müller committed
187 188
  }
  
Christian Müller's avatar
Christian Müller committed
189 190 191 192 193 194 195 196
  def checkInvariantFPDot(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
    val (result, graph, afterlabels, proven, dot, time, _) = checkInvariantFPLabelling(spec, inv, properties)
    (result, dot, time)
  }

  def checkInvariantFPHeadLabel(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
    val (result, graph, afterlabels, proven, dot, time, headlabel) = checkInvariantFPLabelling(spec, inv, properties)
    (result, headlabel, time)
197
  }
Christian Müller's avatar
Christian Müller committed
198
  
Christian Müller's avatar
Christian Müller committed
199
  def checkInvariantOnce(spec: Spec, inv: Formula, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
200

Christian Müller's avatar
Christian Müller committed
201
    // Build graph
202
    val graph = Encoding.toGraph(spec.w)
Christian Müller's avatar
Christian Müller committed
203

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

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

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

213 214 215
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
216

Christian Müller's avatar
Christian Müller committed
217
      val ((res, solver), strengthened) = checkBlockInvariant(spec, b, inv, inv, isfirst, properties)
218

Christian Müller's avatar
Christian Müller committed
219
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
220 221 222
        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
223
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
224 225
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
226 227
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
228 229 230 231 232 233
        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
234

Christian Müller's avatar
Christian Müller committed
235 236
    val safe = list.reduceLeft(_ && _)
    if (safe) {
237
      msg ++= s"Proven safe.\n"
238
      logger.info(s"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
239
    }
Christian Müller's avatar
Christian Müller committed
240
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
241 242
  }
}