InvariantChecker.scala 7.66 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
src  
Christian Müller committed
15
case class InvProperties(stubborn:Boolean, eliminateAux:Boolean, eliminateB:Boolean = false) { }
Christian Müller's avatar
Christian Müller committed
16
object InvProperties {
Christian Müller's avatar
src  
Christian Müller committed
17
  val DEFAULT = InvProperties(stubborn = true, eliminateAux = true, eliminateB = false)
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
src  
Christian Müller committed
35 36

    val z3simpednewinv = Z3BSFO.simplifyBS(noinfprecond)
Christian Müller's avatar
Christian Müller committed
37 38
    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
src  
Christian Müller committed
47
    (Z3BSFO.checkAE(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
            val invalidated = proven.filter(_.to == nextEdge.from)
Christian Müller's avatar
Christian Müller committed
106
            val newproven = (proven -- invalidated) + nextEdge
Christian Müller's avatar
Christian Müller committed
107

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

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

    // 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
134
    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set())) }
135
    
Christian Müller's avatar
Christian Müller committed
136
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
137
    val dot2 = dot1.map(tup => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
Christian Müller's avatar
Christian Müller committed
138
      t._2.pretty
Christian Müller's avatar
Christian Müller committed
139
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
140

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

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

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

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

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

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

169 170
      // Special handling for first block
      val isfirst = !e.from.hasPredecessors
171

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

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

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