InvariantChecker.scala 8.04 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
package de.tum.niwo.invariants
Christian Müller's avatar
Christian Müller committed
2

Christian Müller's avatar
Christian Müller committed
3
import com.microsoft.z3.{Solver, Status}
Christian Müller's avatar
Christian Müller committed
4
import com.typesafe.scalalogging.LazyLogging
5 6 7
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
8
import de.tum.niwo.graphs.WFGraphEncoding.WorkflowGraph
Christian Müller's avatar
Christian Müller committed
9 10
import de.tum.niwo.graphs.{TSGraphEncoding, WFGraphEncoding}
import de.tum.niwo.toz3.{Z3BSFO, Z3FOEncoding}
11
import de.tum.niwo.Utils
Christian Müller's avatar
Christian Müller committed
12 13

import scala.annotation.tailrec
Christian Müller's avatar
Christian Müller committed
14

15
case class InvProperties(stubborn:Boolean, eliminateA:Boolean = true, eliminateB:Boolean = true, approxElim:Boolean = true) { }
Christian Müller's avatar
Christian Müller committed
16
object InvProperties {
Christian Müller's avatar
Christian Müller committed
17 18 19
  val DEFAULT = InvProperties(
    stubborn = true,
    eliminateA = true,
20 21
    eliminateB = true,
    approxElim = true
Christian Müller's avatar
Christian Müller committed
22
  )
Christian Müller's avatar
Christian Müller committed
23 24
}

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


28 29 30 31 32 33 34 35
  def checkBlockInvariant(spec: InvariantSpec,
                          b: SimpleTSBlock,
                          pre: Formula,
                          post: Formula,
                          properties:InvProperties,
                          untouched:Set[String],
                          diverged:Boolean): ((Status, Solver), Formula) = {
    val precond = Preconditions.abstractedPrecondition(post, b, spec, properties, untouched, diverged)
36

Christian Müller's avatar
Christian Müller committed
37
    // pre is universal, spec.always is AE
38
    val f = Implies(And(pre, spec.axioms), precond)
39 40 41

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

42
    (Z3BSFO.checkAE(f.simplify), precond)
43
  }
44

Christian Müller's avatar
Christian Müller committed
45
  def checkInvariantFPLabelling(spec: InvariantSpec, properties:InvProperties) = {
Christian Müller's avatar
Christian Müller committed
46 47 48 49 50 51 52

    // if approximating A-elim, saturate theta with equalities
    val ts = if (properties.approxElim) {
      Saturator.saturate(spec.ts)
    } else { spec.ts }

    val graph = TSGraphEncoding.toGraph(ts)
53 54 55
    type Node = graph.NodeT
    type Edge = graph.EdgeT

Christian Müller's avatar
fix  
Christian Müller committed
56
    val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
57
    val diverged  = TSGraphEncoding.divergedMap(graph, spec.ts.sig, properties)
Christian Müller's avatar
Christian Müller committed
58

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

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

        // take one edge to prove
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
Christian Müller's avatar
Christian Müller committed
76
        val nextEdge = toProve.maxBy(edge => edge.source.value)
77
        
78
        // try to prove
Christian Müller's avatar
Christian Müller committed
79 80
        val pre = labels(nextEdge.from)
        val post = labels(nextEdge.to)
Christian Müller's avatar
Christian Müller committed
81 82 83 84 85 86 87
        val ((status, solver), strengthened) =
          checkBlockInvariant(
            spec,
            TSGraphEncoding.toBlock(nextEdge),
            pre,
            post,
            properties,
88 89
            untouched(nextEdge.from),
            diverged(nextEdge.from))
90

Christian Müller's avatar
Christian Müller committed
91 92
        val from = TSGraphEncoding.toNumber(nextEdge._1)
        val to = TSGraphEncoding.toNumber(nextEdge._2)
93 94 95

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
96
          // --> safe, continue with larger proven set.
97 98

          logger.info(s"Proven inductiveness for ($from -> $to).")
Christian Müller's avatar
Christian Müller committed
99
          checkInvariantRec(labels :: labellist, (proven + nextEdge) :: provenlist)
100 101 102 103
        } 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
104
          // never relabel initial node
105
          logger.info(s"Invariant not inductive, strengthening.")
Christian Müller's avatar
Christian Müller committed
106

107
          val newinv = And(labels(from), strengthened).simplify
Christian Müller's avatar
Christian Müller committed
108 109 110 111 112 113 114

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

115
          val newlabels = labels.updated(from, newinv)
Christian Müller's avatar
Christian Müller committed
116

117
          val isfirst = !nextEdge.from.hasPredecessors
Christian Müller's avatar
Christian Müller committed
118
          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
119
            val invalidated = proven.filter(_.to == nextEdge.from)
Christian Müller's avatar
Christian Müller committed
120
            val newproven = (proven -- invalidated) + nextEdge
Christian Müller's avatar
Christian Müller committed
121

Christian Müller's avatar
src  
Christian Müller committed
122
            val (status2, solver2) = Z3BSFO.checkAE(Implies(newinv, False))
Christian Müller's avatar
Christian Müller committed
123
            if (status2 == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
124
              // Negation of newinv still sat, newinv does not imply false)
125
              logger.info(s"Relabeling $from. New size: ${newinv.opsize}. Continuing.")
126
              checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
127
            } else {
128
              logger.info(s"New invariant for $from not satisfiable. Terminating.")
129
              (false, newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
130
            }
131
          } else {
Christian Müller's avatar
Christian Müller committed
132 133
            logger.info("Relabelled initial node. Terminating.")
            // logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
Christian Müller's avatar
Christian Müller committed
134
            (false, newlabels :: labellist, (proven + nextEdge) :: provenlist)
135 136 137
          }
        }
      }
138 139
    }

Christian Müller's avatar
Christian Müller committed
140
    // create labelling
Christian Müller's avatar
Christian Müller committed
141
    val labels = (for (n <- graph.nodes) yield { n.value -> spec.inv }).toMap
Christian Müller's avatar
Christian Müller committed
142

143
    // update initial labels with untouched map
Christian Müller's avatar
Christian Müller committed
144 145 146 147
    val untouchedlabels = for ((n, inv) <- labels) yield {
      n -> inv.assumeEmpty(untouched(graph.get(n)).toList)
    }

Christian Müller's avatar
Christian Müller committed
148
    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set())) }
149
    
Christian Müller's avatar
Christian Müller committed
150
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
151
    val dot2 = dot1.map(tup => TSGraphEncoding.toDot(graph)(tup._1.map(t => (t._1, {
Christian Müller's avatar
Christian Müller committed
152
      t._2.pretty
Christian Müller's avatar
Christian Müller committed
153
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
154

Christian Müller's avatar
Christian Müller committed
155
    (result, graph, labellings.reverse, proven.reverse, dot2, time)
Christian Müller's avatar
Christian Müller committed
156 157
  }
  
Christian Müller's avatar
Christian Müller committed
158 159 160 161
  def checkInvariantFPDot(spec: InvariantSpec,
                          properties:InvProperties = InvProperties.DEFAULT
                         ): (Boolean, List[String], Long) = {
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, properties)
Christian Müller's avatar
Christian Müller committed
162 163 164
    (result, dot, time)
  }

Christian Müller's avatar
Christian Müller committed
165 166 167 168
  def checkInvariantFPHeadLabel(spec: InvariantSpec,
                                properties:InvProperties = InvProperties.DEFAULT
                               ): (Boolean, WorkflowGraph, Map[Int, Formula], Long) = {
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, properties)
Christian Müller's avatar
Christian Müller committed
169
    (result, graph, afterlabels.last, time)
170
  }
Christian Müller's avatar
Christian Müller committed
171
  
Christian Müller's avatar
Christian Müller committed
172
  def checkInvariantOnce(spec: InvariantSpec, properties: InvProperties): (Boolean, StringBuilder) = {
Christian Müller's avatar
Christian Müller committed
173

Christian Müller's avatar
Christian Müller committed
174
    // Build graph
Christian Müller's avatar
Christian Müller committed
175 176
    val graph = TSGraphEncoding.toGraph(spec.ts)
    val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
177
    val diverged = TSGraphEncoding.divergedMap(graph, spec.ts.sig, properties)
Christian Müller's avatar
Christian Müller committed
178

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

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

Christian Müller's avatar
Christian Müller committed
185
      // Check I -> WP[w](inv)
Christian Müller's avatar
Christian Müller committed
186
      val b = TSGraphEncoding.toBlock(e)
187

188
      val ((res, solver), _) = checkBlockInvariant(spec, b, spec.inv, spec.inv, properties, untouched(e.from), diverged(e.from))
189

Christian Müller's avatar
Christian Müller committed
190
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
191 192 193
        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
194
          msg ++= Z3FOEncoding.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
195 196
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
197 198
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
199
        logger.info(s"Could not prove invariant ${spec.inv}")
Christian Müller's avatar
Christian Müller committed
200 201 202 203 204
        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
205

Christian Müller's avatar
Christian Müller committed
206 207
    val safe = list.reduceLeft(_ && _)
    if (safe) {
208
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
209
      logger.info(s"Workflow ${spec.ts}\n proven safe for invariant:\n${spec.inv.pretty}")
Christian Müller's avatar
Christian Müller committed
210
    }
Christian Müller's avatar
Christian Müller committed
211
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
212 213
  }
}