InvariantChecker.scala 9.2 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
12
import de.tum.niwo.graphs.TSGraphEncoding.TSGraph
Christian Müller's avatar
Christian Müller committed
13 14

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

Christian Müller's avatar
Christian Müller committed
16 17 18
case class InvProperties(stubborn:Boolean,
                         eliminateA:Boolean = true,
                         eliminateB:Boolean = true,
Christian Müller's avatar
Christian Müller committed
19
                         approxElim:Boolean = true) {
Christian Müller's avatar
Christian Müller committed
20 21
  override def toString: String = {
    s"InvProperties(stubborn=$stubborn, eliminateA=$eliminateA, eliminateB=$eliminateB," +
Christian Müller's avatar
Christian Müller committed
22
      s"approxElim=$approxElim)"
Christian Müller's avatar
Christian Müller committed
23 24
  }
}
Christian Müller's avatar
Christian Müller committed
25
object InvProperties {
Christian Müller's avatar
Christian Müller committed
26 27 28
  val DEFAULT = InvProperties(
    stubborn = true,
    eliminateA = true,
29 30
    eliminateB = true,
    approxElim = true
Christian Müller's avatar
Christian Müller committed
31
  )
Christian Müller's avatar
Christian Müller committed
32 33
}

Christian Müller's avatar
Christian Müller committed
34
object InvariantChecker extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
35 36


37 38 39 40 41 42
  def checkBlockInvariant(spec: InvariantSpec,
                          b: SimpleTSBlock,
                          pre: Formula,
                          post: Formula,
                          properties:InvProperties,
                          untouched:Set[String],
43 44
                          diverged:Boolean): ((Status, Solver), Formula, String) = {
    val (precond, strategy) = Preconditions.abstractedPrecondition(post, b, spec, properties, untouched, diverged)
45

Christian Müller's avatar
Christian Müller committed
46
    // pre is universal, spec.always is AE
47
    val f = Implies(And(pre, spec.axioms), precond)
48 49 50

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

51
    (Z3BSFO.checkAE(f.simplify), precond, strategy)
52
  }
53

Christian Müller's avatar
Christian Müller committed
54
  def checkInvariantFPLabelling(spec: InvariantSpec, properties:InvProperties) = {
Christian Müller's avatar
Christian Müller committed
55 56 57 58 59 60 61

    // 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)
62 63 64
    type Node = graph.NodeT
    type Edge = graph.EdgeT

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

68
    @tailrec
69 70
    def checkInvariantRec(labellist: List[Map[Int, Formula]], provenlist: List[Set[Edge]], strategylist:List[Map[Edge, String]]):
        (Boolean, List[Map[Int, Formula]], List[Set[Edge]], List[Map[Edge, String]]) = {
71

72 73
      val labels = labellist.head
      val proven = provenlist.head
74 75
      val strats = strategylist.head

76
      // check if done, i.e. all edges proven
Christian Müller's avatar
Christian Müller committed
77
      val toProve = graph.edges -- proven
78
      if (toProve.isEmpty) {
Christian Müller's avatar
Christian Müller committed
79
        logger.info("Everything proven. Terminating.")
80
        (true, labellist, provenlist, strategylist)
81 82 83
      } else {

        // take one edge to prove
84 85 86 87
//        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
88
        val nextEdge = if (spec.universe.isDefined) {
Christian Müller's avatar
Christian Müller committed
89 90 91 92 93 94 95
          // counterexample mode: try to go to source
          toProve.minBy(edge => edge.source.value)
        } else {
          // proving mode: try to iterate loops
          toProve.maxBy(edge => edge.source.value)
        }

96
        // try to prove
Christian Müller's avatar
Christian Müller committed
97 98
        val pre = labels(nextEdge.from)
        val post = labels(nextEdge.to)
99
        val ((status, solver), strengthened, strategy) =
Christian Müller's avatar
Christian Müller committed
100 101 102 103 104 105
          checkBlockInvariant(
            spec,
            TSGraphEncoding.toBlock(nextEdge),
            pre,
            post,
            properties,
106 107
            untouched(nextEdge.from),
            diverged(nextEdge.from))
108

Christian Müller's avatar
Christian Müller committed
109 110
        val from = TSGraphEncoding.toNumber(nextEdge._1)
        val to = TSGraphEncoding.toNumber(nextEdge._2)
111

112 113
        val newstrats = strats.updated(nextEdge, strategy)

114 115
        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
116
          // --> safe, continue with larger proven set.
117 118

          logger.info(s"Proven inductiveness for ($from -> $to).")
119
          checkInvariantRec(labels :: labellist, (proven + nextEdge) :: provenlist, newstrats :: strategylist)
120 121 122 123
        } 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
124
          // never relabel initial node
Christian Müller's avatar
Christian Müller committed
125 126 127 128 129
          logger.info(s"Invariant not inductive for ($from -> $to), strengthening.")
          if (Utils.DEBUG_MODE) {
            val model = solver.getModel
            logger.debug(model.toString)
          }
Christian Müller's avatar
Christian Müller committed
130

131
          val newinv = And(labels(from), strengthened).simplify
Christian Müller's avatar
Christian Müller committed
132 133 134 135 136 137 138

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

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

141
          val isfirst = !nextEdge.from.hasPredecessors
Christian Müller's avatar
Christian Müller committed
142
          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
143
            val invalidated = proven.filter(_.to == nextEdge.from)
Christian Müller's avatar
Christian Müller committed
144
            val newproven = (proven -- invalidated) + nextEdge
Christian Müller's avatar
Christian Müller committed
145

Christian Müller's avatar
src  
Christian Müller committed
146
            val (status2, solver2) = Z3BSFO.checkAE(Implies(newinv, False))
Christian Müller's avatar
Christian Müller committed
147
            if (status2 == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
148
              // Negation of newinv still sat, newinv does not imply false)
149
              logger.info(s"Relabeling $from. New size: ${newinv.opsize}. Continuing.")
150
              checkInvariantRec(newlabels :: labellist, newproven :: provenlist, newstrats :: strategylist)
Christian Müller's avatar
Christian Müller committed
151
            } else {
152
              logger.info(s"New invariant for $from not satisfiable. Terminating.")
153
              (false, newlabels :: labellist, newproven :: provenlist, newstrats :: strategylist)
Christian Müller's avatar
Christian Müller committed
154
            }
155
          } else {
Christian Müller's avatar
Christian Müller committed
156 157
            logger.info("Relabelled initial node. Terminating.")
            // logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
158
            (false, newlabels :: labellist, (proven + nextEdge) :: provenlist, newstrats :: strategylist)
159 160 161
          }
        }
      }
162 163
    }

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

167
    // update initial labels with untouched map
Christian Müller's avatar
Christian Müller committed
168 169 170 171
    val untouchedlabels = for ((n, inv) <- labels) yield {
      n -> inv.assumeEmpty(untouched(graph.get(n)).toList)
    }

Christian Müller's avatar
Christian Müller committed
172 173
    logger.info(s"Beginning inference for invariant $spec.inv")

174
    val (time, (result, labellings, proven, strategies)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set()), List(Map())) }
175
    
Christian Müller's avatar
Christian Müller committed
176
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
177
    val dot2 = dot1.map(tup => TSGraphEncoding.toDot(graph)(tup._1.map(t => (t._1, {
Christian Müller's avatar
Christian Müller committed
178
      t._2.pretty
Christian Müller's avatar
Christian Müller committed
179
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
180

181
    (result, graph, labellings.reverse, proven.reverse, strategies.reverse, dot2, time)
Christian Müller's avatar
Christian Müller committed
182 183
  }
  
Christian Müller's avatar
Christian Müller committed
184 185 186
  def checkInvariantFPDot(spec: InvariantSpec,
                          properties:InvProperties = InvProperties.DEFAULT
                         ): (Boolean, List[String], Long) = {
187
    val (result, graph, afterlabels, proven, strategies, dot, time) = checkInvariantFPLabelling(spec, properties)
Christian Müller's avatar
Christian Müller committed
188 189 190
    (result, dot, time)
  }

Christian Müller's avatar
Christian Müller committed
191 192 193
  def checkInvariantFPHeadLabel(spec: InvariantSpec,
                                properties:InvProperties = InvProperties.DEFAULT
                               ): (Boolean, WorkflowGraph, Map[Int, Formula], Long) = {
194
    val (result, graph, afterlabels, proven, strategies, dot, time) = checkInvariantFPLabelling(spec, properties)
Christian Müller's avatar
Christian Müller committed
195
    (result, graph, afterlabels.last, time)
196
  }
Christian Müller's avatar
Christian Müller committed
197
  
Christian Müller's avatar
Christian Müller committed
198
  def checkInvariantOnce(spec: InvariantSpec, properties: InvProperties): (Boolean, StringBuilder) = {
Christian Müller's avatar
Christian Müller committed
199

Christian Müller's avatar
Christian Müller committed
200
    // Build graph
Christian Müller's avatar
Christian Müller committed
201 202
    val graph = TSGraphEncoding.toGraph(spec.ts)
    val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
203
    val diverged = TSGraphEncoding.divergedMap(graph, spec.ts.sig, properties)
Christian Müller's avatar
Christian Müller committed
204

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

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

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

214
      val ((res, solver), _, strategies) = checkBlockInvariant(spec, b, spec.inv, spec.inv, properties, untouched(e.from), diverged(e.from))
215

Christian Müller's avatar
Christian Müller committed
216
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
217 218 219
        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
220
          msg ++= Z3FOEncoding.printModel(solver.getModel()).linesIterator.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
221 222
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
223 224
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
225
        logger.info(s"Could not prove invariant ${spec.inv}")
Christian Müller's avatar
Christian Müller committed
226 227 228
        logger.info(s"Z3 status $res")
        logger.info(s"Block ${e.label} may not uphold it")
      }
229 230

      msg ++= s"Strategies used:\n" + strategies
Christian Müller's avatar
Christian Müller committed
231 232
      res == Status.UNSATISFIABLE
    }
Christian Müller's avatar
Christian Müller committed
233

Christian Müller's avatar
Christian Müller committed
234 235
    val safe = list.reduceLeft(_ && _)
    if (safe) {
236
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
237
      logger.info(s"Workflow ${spec.ts}\n proven safe for invariant:\n${spec.inv.pretty}")
Christian Müller's avatar
Christian Müller committed
238
    }
Christian Müller's avatar
Christian Müller committed
239
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
240 241
  }
}