InvariantChecker.scala 7.76 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 scala.annotation.tailrec
Christian Müller's avatar
Christian Müller committed
4
import com.microsoft.z3.Status
Christian Müller's avatar
Christian Müller committed
5
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
6 7 8 9 10
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
11
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
12
import de.tum.workflows.Utils
Christian Müller's avatar
Christian Müller committed
13
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
14

Christian Müller's avatar
Christian Müller committed
15 16
case class InvProperties(stubborn:Boolean, eliminateAux:Boolean) { }
object InvProperties {
Christian Müller's avatar
Christian Müller committed
17
  val DEFAULT = InvProperties(stubborn = true, eliminateAux = true)
Christian Müller's avatar
Christian Müller committed
18 19
}

Christian Müller's avatar
Christian Müller committed
20
object InvariantChecker extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
21 22


Christian Müller's avatar
Christian Müller committed
23
  def checkBlockInvariant(spec:Spec, b: SimpleBlock, pre: Formula, post: Formula, isfirst: Boolean, properties:InvProperties, untouched:Set[String]) = {
Christian Müller's avatar
Christian Müller committed
24
    val precond = Preconditions.abstractedPrecondition(post, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
25
    
Christian Müller's avatar
Christian Müller committed
26 27 28 29 30 31 32 33 34
    // Assume untoucheds empty
    val untouchedprecond = precond.assumeEmpty(untouched.toList)

//    val firstprecond = if (isfirst) {
//      precond.assumeEmpty(spec.w.sig.preds.map(_.name).toList)
//    } else { precond }
    val noinfprecond = if (isfirst && !properties.stubborn) {
        untouchedprecond.assumeEmpty(List(Properties.INFNAME))
    } else { untouchedprecond }
Christian Müller's avatar
Christian Müller committed
35 36 37 38
    
    val z3simpednewinv = Z3QFree.simplifyUniv(noinfprecond)
    val gained = noinfprecond.toString().length() - z3simpednewinv.toString().length()
    logger.info(s"Invariant shrunken by $gained chars")
39 40 41 42

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

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

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

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

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

Christian Müller's avatar
Christian Müller committed
55 56
    val untouched = Encoding.untouchedMap(graph, spec.w.sig)

57
    @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
//        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
Christian Müller's avatar
Christian Müller committed
74
        val nextEdge = toProve.maxBy(edge => edge.source.value)
75
        
76
        // try to prove
Christian Müller's avatar
Christian Müller committed
77 78 79 80
        val pre = labels(nextEdge.from)
        val post = labels(nextEdge.to)
        val isfirst = !nextEdge.from.hasPredecessors
        val ((status, solver), strengthened) = checkBlockInvariant(spec, nextEdge, pre, post, isfirst, properties, untouched(nextEdge.from))
81 82 83

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
84
          // --> safe, continue with larger proven set.
Christian Müller's avatar
Christian Müller committed
85 86
          logger.info(s"Proven inductiveness for (${nextEdge._1} -> ${nextEdge.to}).")
          checkInvariantRec(labels :: labellist, (proven + nextEdge) :: 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
          val newinv = And(labels(nextEdge._1), strengthened).simplify()
Christian Müller's avatar
Christian Müller committed
95 96 97 98 99 100 101

          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
102
          val newlabels = labels.updated(nextEdge._1, newinv)
Christian Müller's avatar
Christian Müller committed
103 104

          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
105 106
//            val invalidated = proven.filter(_.from == nextEdge.to)
            val invalidated = proven.filter(_.to == nextEdge.from)
Christian Müller's avatar
Christian Müller committed
107

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

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

Christian Müller's avatar
Christian Müller committed
128
    // create labelling
Christian Müller's avatar
Christian Müller committed
129
    val labels = (for (n <- graph.nodes) yield { n.value -> inv }).toMap
Christian Müller's avatar
Christian Müller committed
130 131 132 133 134 135

    // update labels with untouched map
    val untouchedlabels = for ((n, inv) <- labels) yield {
      n -> inv.assumeEmpty(untouched(graph.get(n)).toList)
    }

Christian Müller's avatar
Christian Müller committed
136
    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set())) }
137
    
Christian Müller's avatar
Christian Müller committed
138
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
139
    val dot2 = dot1.map(tup => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
140
      // if (t._2.opsize() <= 5000) t._2.pretty() else "TOO BIG"
Christian Müller's avatar
Christian Müller committed
141
      t._2.pretty
Christian Müller's avatar
Christian Müller committed
142
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
143

Christian Müller's avatar
Christian Müller committed
144
    (result, graph, labellings.reverse, proven.reverse, dot2, time)
Christian Müller's avatar
Christian Müller committed
145 146
  }
  
Christian Müller's avatar
Christian Müller committed
147
  def checkInvariantFPDot(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
Christian Müller's avatar
Christian Müller committed
148
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
Christian Müller's avatar
Christian Müller committed
149 150 151 152
    (result, dot, time)
  }

  def checkInvariantFPHeadLabel(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
Christian Müller's avatar
Christian Müller committed
153 154
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
    (result, graph, afterlabels.last, time)
155
  }
Christian Müller's avatar
Christian Müller committed
156
  
Christian Müller's avatar
Christian Müller committed
157
  def checkInvariantOnce(spec: Spec, inv: Formula, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
158

Christian Müller's avatar
Christian Müller committed
159
    // Build graph
160
    val graph = Encoding.toGraph(spec.w)
Christian Müller's avatar
Christian Müller committed
161
    val untouched = Encoding.untouchedMap(graph, spec.w.sig)
Christian Müller's avatar
Christian Müller committed
162

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

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

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

172 173
      // Special handling for first block
      val isfirst = !e.from.hasPredecessors
174

Christian Müller's avatar
Christian Müller committed
175
      val ((res, solver), strengthened) = checkBlockInvariant(spec, b, inv, inv, isfirst, properties, untouched(e.from))
176

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

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