InvariantChecker.scala 8.44 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 25 26 27
case class InvProperties(stubborn:Boolean, eliminateAux:Boolean) { }
object InvProperties {
  val DEFAULT = InvProperties(true, true)
}

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 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
      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
69
    }
Christian Müller's avatar
Christian Müller committed
70 71
    logger.info(s"Z3 call took $time ms")
    res
Christian Müller's avatar
Christian Müller committed
72
  }
Christian Müller's avatar
Christian Müller committed
73

Christian Müller's avatar
Christian Müller committed
74 75 76
  def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, isfirst: Boolean, properties:InvProperties) = {
    val precond = Preconditions.abstractPrecondition(post, b, spec, properties)
    
77
    // TODO: do we do this here?
78
    val firstprecond = if (isfirst) {
Christian Müller's avatar
Christian Müller committed
79
      precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
Christian Müller's avatar
Christian Müller committed
80
    } else { precond }
Christian Müller's avatar
Christian Müller committed
81 82 83 84 85 86 87
    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")
88 89 90 91

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

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

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

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

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

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

107 108
      val labels = labellist.head
      val proven = provenlist.head
109 110 111
      // 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
112
        logger.info("Everything proven. Terminating.")
113
        (true, labellist, provenlist)
114 115 116
      } else {

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

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
131 132
          // --> safe, continue with larger proven set.
          logger.info(s"Proven inductiveness for (${next._1} -> ${next._2}).")
133
          checkInvariantRec(labels :: labellist, (proven + next) :: provenlist)
134 135 136 137
        } 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
138
          // never relabel initial node
139
          logger.info(s"Invariant not inductive, strengthening.")
Christian Müller's avatar
Christian Müller committed
140
          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
141
            // check if strengthened -> old_inv else use conjunction
Christian Müller's avatar
Christian Müller committed
142
//            val strengthened = Preconditions.abstractPrecondition(post, next, spec, properties)
Christian Müller's avatar
Christian Müller committed
143
            val newinv = And(labels(next._1), strengthened).simplify()
Christian Müller's avatar
Christian Müller committed
144
            
Christian Müller's avatar
Christian Müller committed
145 146 147 148 149
            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
150 151

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

Christian Müller's avatar
Christian Müller committed
174 175
    // 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
176
    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(labels, List(Set())) }
177
    
Christian Müller's avatar
Christian Müller committed
178 179 180 181
    val dot1 = labellings.zip(proven).reverse
    val dot2 = dot1.map((tup) => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
      if (t._2.opsize() <= 5000) t._2.pretty() else "TOO BIG"
    })), tup._2))
182
    
Christian Müller's avatar
Christian Müller committed
183 184 185 186 187 188
    (result, graph, labellings.reverse, proven.reverse, dot2, time)
  }
  
  def checkInvariantFP(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
    (result, dot)
189
  }
Christian Müller's avatar
Christian Müller committed
190
  
Christian Müller's avatar
Christian Müller committed
191
  def checkInvariantOnce(spec: Spec, inv: Formula, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
192

Christian Müller's avatar
Christian Müller committed
193
    // Build graph
194
    val graph = Encoding.toGraph(spec.w)
Christian Müller's avatar
Christian Müller committed
195

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

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

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

205 206 207
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
208

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

Christian Müller's avatar
Christian Müller committed
211
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
212 213 214
        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
215
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
216 217
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
218 219
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
220 221 222 223 224 225
        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
226

Christian Müller's avatar
Christian Müller committed
227 228
    val safe = list.reduceLeft(_ && _)
    if (safe) {
229
      msg ++= s"Proven safe.\n"
230
      logger.info(s"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
231
    }
Christian Müller's avatar
Christian Müller committed
232
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
233 234
  }
}