InvariantChecker.scala 7.28 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

Christian Müller's avatar
Christian Müller committed
5
import de.tum.workflows.foltl.FOTransformers
Christian Müller's avatar
Christian Müller committed
6

Christian Müller's avatar
Christian Müller committed
7 8
import scala.annotation.tailrec
import com.microsoft.z3.{Context, InterpolationContext, Status}
Christian Müller's avatar
Christian Müller committed
9
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
10 11 12 13 14
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
15
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
16
import de.tum.workflows.Utils
Christian Müller's avatar
Christian Müller committed
17
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
18

Christian Müller's avatar
Christian Müller committed
19 20
case class InvProperties(stubborn:Boolean, eliminateAux:Boolean) { }
object InvProperties {
Christian Müller's avatar
Christian Müller committed
21
  val DEFAULT = InvProperties(stubborn = true, eliminateAux = true)
Christian Müller's avatar
Christian Müller committed
22 23
}

Christian Müller's avatar
Christian Müller committed
24
object InvariantChecker extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
25 26


Christian Müller's avatar
Christian Müller committed
27
  def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, isfirst: Boolean, properties:InvProperties) = {
Christian Müller's avatar
Christian Müller committed
28
    val precond = Preconditions.abstractedPrecondition(post, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
29
    
30
    // TODO: do we do this here?
31
    val firstprecond = if (isfirst) {
Christian Müller's avatar
Christian Müller committed
32
      precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
Christian Müller's avatar
Christian Müller committed
33
    } else { precond }
Christian Müller's avatar
Christian Müller committed
34 35 36 37 38 39 40
    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")
41 42 43 44

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

Christian Müller's avatar
Christian Müller committed
45
    val f = Implies(pre, z3simpednewinv)
46 47 48

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

Christian Müller's avatar
Christian Müller committed
49
    (Z3QFree.checkUniversal(f.simplify()), z3simpednewinv)
50
  }
51

Christian Müller's avatar
Christian Müller committed
52
  def checkInvariantFPLabelling(spec: Spec, inv: Formula, properties:InvProperties) = {
53
    val graph = Encoding.toGraph(spec.w)
54 55 56 57
    type Node = graph.NodeT
    type Edge = graph.EdgeT

    @tailrec
Christian Müller's avatar
Christian Müller committed
58
    def checkInvariantRec(labellist: List[Map[Int, Formula]], provenlist: List[Set[Edge]]): (Boolean, List[Map[Int, Formula]], List[Set[Edge]]) = {
59

60 61
      val labels = labellist.head
      val proven = provenlist.head
62
      // check if done, i.e. all edges proven
Christian Müller's avatar
Christian Müller committed
63
      val toProve = graph.edges -- proven
64
      if (toProve.isEmpty) {
Christian Müller's avatar
Christian Müller committed
65
        logger.info("Everything proven. Terminating.")
66
        (true, labellist, provenlist)
67 68 69
      } else {

        // take one edge to prove
70 71 72 73 74 75
//        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)
        
76 77 78
        // try to prove
        val pre = labels(next._1)
        val post = labels(next._2)
Christian Müller's avatar
Christian Müller committed
79
        val isfirst = !next._1.hasPredecessors
Christian Müller's avatar
Christian Müller committed
80
        val ((status, solver), strengthened) = checkBlockInvariant(spec, next, pre, post, isfirst, properties)
81 82 83

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
84 85
          // --> safe, continue with larger proven set.
          logger.info(s"Proven inductiveness for (${next._1} -> ${next._2}).")
86
          checkInvariantRec(labels :: labellist, (proven + next) :: provenlist)
87 88 89 90
        } 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
91
          // never relabel initial node
92
          logger.info(s"Invariant not inductive, strengthening.")
Christian Müller's avatar
Christian Müller committed
93

Christian Müller's avatar
Christian Müller committed
94 95 96 97 98 99 100 101 102 103 104
          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
105
            val invalidated = proven.filter(_._2 == next._1)
Christian Müller's avatar
Christian Müller committed
106

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

Christian Müller's avatar
Christian Müller committed
109
            val (status2, solver2) = Z3QFree.checkUniversal(Implies(newinv, False))
Christian Müller's avatar
Christian Müller committed
110
            if (status2 == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
111
              // Negation of newinv still sat, newinv does not imply false)
112
              logger.info(s"Relabeling ${next._1}. New size: ${newinv.opsize()}. Continuing.")
113
              checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
114 115
            } else {
              logger.info(s"New invariant for ${next._1} not satisfiable. Terminating.")
116
              (false, newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
117
            }
118
          } else {
Christian Müller's avatar
Christian Müller committed
119 120 121
            logger.info("Relabelled initial node. Terminating.")
            // logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
            (false, newlabels, provenlist)
122 123 124
          }
        }
      }
125 126
    }

Christian Müller's avatar
Christian Müller committed
127
    // create labelling - FIXME: maybe use inv only for last
Christian Müller's avatar
Christian Müller committed
128
    val labels = (for (n <- graph.nodes) yield { n.value -> inv }).toMap
Christian Müller's avatar
Christian Müller committed
129
    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(labels, List(Set())) }
130
    
Christian Müller's avatar
Christian Müller committed
131
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
132
    val dot2 = dot1.map(tup => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
Christian Müller's avatar
Christian Müller committed
133 134
      if (t._2.opsize() <= 5000) t._2.pretty() else "TOO BIG"
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
135

Christian Müller's avatar
Christian Müller committed
136
    (result, graph, labellings.reverse, proven.reverse, dot2, time)
Christian Müller's avatar
Christian Müller committed
137 138
  }
  
Christian Müller's avatar
Christian Müller committed
139
  def checkInvariantFPDot(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
Christian Müller's avatar
Christian Müller committed
140
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
Christian Müller's avatar
Christian Müller committed
141 142 143 144
    (result, dot, time)
  }

  def checkInvariantFPHeadLabel(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
Christian Müller's avatar
Christian Müller committed
145 146
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
    (result, graph, afterlabels.last, time)
147
  }
Christian Müller's avatar
Christian Müller committed
148
  
Christian Müller's avatar
Christian Müller committed
149
  def checkInvariantOnce(spec: Spec, inv: Formula, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
150

Christian Müller's avatar
Christian Müller committed
151
    // Build graph
152
    val graph = Encoding.toGraph(spec.w)
Christian Müller's avatar
Christian Müller committed
153

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

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

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

163 164 165
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
166

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

Christian Müller's avatar
Christian Müller committed
169
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
170 171 172
        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
173
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
174 175
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
176 177
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
178 179 180 181 182 183
        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
184

Christian Müller's avatar
Christian Müller committed
185 186
    val safe = list.reduceLeft(_ && _)
    if (safe) {
187
      msg ++= s"Proven safe.\n"
188
      logger.info(s"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
189
    }
Christian Müller's avatar
Christian Müller committed
190
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
191 192
  }
}