InvariantChecker.scala 9.3 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 19 20 21 22 23 24 25
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
26
object InvProperties {
Christian Müller's avatar
Christian Müller committed
27 28 29
  val DEFAULT = InvProperties(
    stubborn = true,
    eliminateA = true,
30 31
    eliminateB = true,
    approxElim = true
Christian Müller's avatar
Christian Müller committed
32
  )
Christian Müller's avatar
Christian Müller committed
33 34
}

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


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

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

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

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

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

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

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

69
    @tailrec
70 71
    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]]) = {
72

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

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

        // take one edge to prove
85 86 87 88
//        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
89 90 91 92 93 94 95 96
        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)
        }

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

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

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

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

          logger.info(s"Proven inductiveness for ($from -> $to).")
120
          checkInvariantRec(labels :: labellist, (proven + nextEdge) :: provenlist, newstrats :: strategylist)
121 122 123 124
        } 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
125
          // never relabel initial node
Christian Müller's avatar
Christian Müller committed
126 127 128 129 130
          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
131

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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