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

Christian Müller's avatar
Christian Müller committed
15 16 17 18 19 20 21 22 23 24
case class InvProperties(stubborn:Boolean,
                         eliminateA:Boolean = true,
                         eliminateB:Boolean = true,
                         approxElim:Boolean = true,
                         universe:Option[Map[String, List[Var]]] = None) {
  override def toString: String = {
    s"InvProperties(stubborn=$stubborn, eliminateA=$eliminateA, eliminateB=$eliminateB," +
      s"approxElim=$approxElim,universe:$universe)"
  }
}
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 43 44
  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)
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)
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
Christian Müller's avatar
Christian Müller committed
69
    def checkInvariantRec(labellist: List[Map[Int, Formula]], provenlist: List[Set[Edge]]): (Boolean, List[Map[Int, Formula]], List[Set[Edge]]) = {
70

71 72
      val labels = labellist.head
      val proven = provenlist.head
73
      // check if done, i.e. all edges proven
Christian Müller's avatar
Christian Müller committed
74
      val toProve = graph.edges -- proven
75
      if (toProve.isEmpty) {
Christian Müller's avatar
Christian Müller committed
76
        logger.info("Everything proven. Terminating.")
77
        (true, labellist, provenlist)
78 79 80
      } else {

        // take one edge to prove
81 82 83 84
//        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
85 86 87 88 89 90 91 92
        val nextEdge = if (properties.universe.isDefined) {
          // 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)
        }

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

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

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

          logger.info(s"Proven inductiveness for ($from -> $to).")
Christian Müller's avatar
Christian Müller committed
114
          checkInvariantRec(labels :: labellist, (proven + nextEdge) :: provenlist)
115 116 117 118
        } 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
119
          // never relabel initial node
Christian Müller's avatar
Christian Müller committed
120 121 122 123 124
          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
125

126
          val newinv = And(labels(from), strengthened).simplify
Christian Müller's avatar
Christian Müller committed
127 128 129 130 131 132 133

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

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

136
          val isfirst = !nextEdge.from.hasPredecessors
Christian Müller's avatar
Christian Müller committed
137
          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
138
            val invalidated = proven.filter(_.to == nextEdge.from)
Christian Müller's avatar
Christian Müller committed
139
            val newproven = (proven -- invalidated) + nextEdge
Christian Müller's avatar
Christian Müller committed
140

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

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

162
    // update initial labels with untouched map
Christian Müller's avatar
Christian Müller committed
163 164 165 166
    val untouchedlabels = for ((n, inv) <- labels) yield {
      n -> inv.assumeEmpty(untouched(graph.get(n)).toList)
    }

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

Christian Müller's avatar
Christian Müller committed
169
    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(List(untouchedlabels), List(Set())) }
170
    
Christian Müller's avatar
Christian Müller committed
171
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
172
    val dot2 = dot1.map(tup => TSGraphEncoding.toDot(graph)(tup._1.map(t => (t._1, {
Christian Müller's avatar
Christian Müller committed
173
      t._2.pretty
Christian Müller's avatar
Christian Müller committed
174
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
175

Christian Müller's avatar
Christian Müller committed
176
    (result, graph, labellings.reverse, proven.reverse, dot2, time)
Christian Müller's avatar
Christian Müller committed
177 178
  }
  
Christian Müller's avatar
Christian Müller committed
179 180 181 182
  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
183 184 185
    (result, dot, time)
  }

Christian Müller's avatar
Christian Müller committed
186 187 188 189
  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
190
    (result, graph, afterlabels.last, time)
191
  }
Christian Müller's avatar
Christian Müller committed
192
  
Christian Müller's avatar
Christian Müller committed
193
  def checkInvariantOnce(spec: InvariantSpec, properties: InvProperties): (Boolean, StringBuilder) = {
Christian Müller's avatar
Christian Müller committed
194

Christian Müller's avatar
Christian Müller committed
195
    // Build graph
Christian Müller's avatar
Christian Müller committed
196 197
    val graph = TSGraphEncoding.toGraph(spec.ts)
    val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
198
    val diverged = TSGraphEncoding.divergedMap(graph, spec.ts.sig, properties)
Christian Müller's avatar
Christian Müller committed
199

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

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

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

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

Christian Müller's avatar
Christian Müller committed
211
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
212 213 214
        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
215
          msg ++= Z3FOEncoding.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
216 217
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
218 219
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
220
        logger.info(s"Could not prove invariant ${spec.inv}")
Christian Müller's avatar
Christian Müller committed
221 222 223 224 225
        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
226

Christian Müller's avatar
Christian Müller committed
227 228
    val safe = list.reduceLeft(_ && _)
    if (safe) {
229
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
230
      logger.info(s"Workflow ${spec.ts}\n proven safe for invariant:\n${spec.inv.pretty}")
Christian Müller's avatar
Christian Müller committed
231
    }
Christian Müller's avatar
Christian Müller committed
232
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
233 234
  }
}