InvariantChecker.scala 7.82 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 java.util
Christian Müller's avatar
Christian Müller committed
4

Christian Müller's avatar
Christian Müller committed
5
import de.tum.workflows.foltl.FOTransformers
Christian Müller's avatar
Christian Müller committed
6

Christian Müller's avatar
Christian Müller committed
7 8
import scala.annotation.tailrec
import com.microsoft.z3.{Context, InterpolationContext, Status}
Christian Müller's avatar
Christian Müller committed
9
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
10 11 12 13 14
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
15
import de.tum.workflows.foltl.FormulaFunctions
Christian Müller's avatar
Christian Müller committed
16
import de.tum.workflows.Utils
Christian Müller's avatar
Christian Müller committed
17
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
18

Christian Müller's avatar
Christian Müller committed
19 20
case class InvProperties(stubborn:Boolean, eliminateAux:Boolean) { }
object InvProperties {
Christian Müller's avatar
Christian Müller committed
21
  val DEFAULT = InvProperties(stubborn = true, eliminateAux = true)
Christian Müller's avatar
Christian Müller committed
22 23
}

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


Christian Müller's avatar
Christian Müller committed
27
  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
28
    val precond = Preconditions.abstractedPrecondition(post, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
29
    
Christian Müller's avatar
Christian Müller committed
30 31 32 33 34 35 36 37 38
    // 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
Christian Müller committed
39 40 41 42
    
    val z3simpednewinv = Z3QFree.simplifyUniv(noinfprecond)
    val gained = noinfprecond.toString().length() - z3simpednewinv.toString().length()
    logger.info(s"Invariant shrunken by $gained chars")
43 44 45 46

    //      val test1 = inv.toPrenex()
    //      val test2 = stubprecond.toPrenex()

Christian Müller's avatar
Christian Müller committed
47
    val f = Implies(pre, z3simpednewinv)
48 49 50

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

Christian Müller's avatar
Christian Müller committed
51
    (Z3QFree.checkUniversal(f.simplify()), z3simpednewinv)
52
  }
53

Christian Müller's avatar
Christian Müller committed
54
  def checkInvariantFPLabelling(spec: Spec, inv: Formula, properties:InvProperties) = {
55
    val graph = Encoding.toGraph(spec.w)
56 57 58
    type Node = graph.NodeT
    type Edge = graph.EdgeT

Christian Müller's avatar
Christian Müller committed
59 60
    val untouched = Encoding.untouchedMap(graph, spec.w.sig)

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

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

        // take one edge to prove
74 75 76 77
//        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
78
        val nextEdge = toProve.maxBy(edge => edge.source.value)
79
        
80
        // try to prove
Christian Müller's avatar
Christian Müller committed
81 82 83 84
        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))
85 86 87

        if (status == Status.UNSATISFIABLE) {
          // Negation of implication unsat
Christian Müller's avatar
Christian Müller committed
88
          // --> safe, continue with larger proven set.
Christian Müller's avatar
Christian Müller committed
89 90
          logger.info(s"Proven inductiveness for (${nextEdge._1} -> ${nextEdge.to}).")
          checkInvariantRec(labels :: labellist, (proven + nextEdge) :: provenlist)
91 92 93 94
        } 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
95
          // never relabel initial node
96
          logger.info(s"Invariant not inductive, strengthening.")
Christian Müller's avatar
Christian Müller committed
97

Christian Müller's avatar
Christian Müller committed
98
          val newinv = And(labels(nextEdge._1), strengthened).simplify()
Christian Müller's avatar
Christian Müller committed
99 100 101 102 103 104 105

          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
106
          val newlabels = labels.updated(nextEdge._1, newinv)
Christian Müller's avatar
Christian Müller committed
107 108

          if (!isfirst) {
Christian Müller's avatar
Christian Müller committed
109 110
//            val invalidated = proven.filter(_.from == nextEdge.to)
            val invalidated = proven.filter(_.to == nextEdge.from)
Christian Müller's avatar
Christian Müller committed
111

Christian Müller's avatar
Christian Müller committed
112
            val newproven = (proven -- invalidated) + nextEdge
Christian Müller's avatar
Christian Müller committed
113

Christian Müller's avatar
Christian Müller committed
114
            val (status2, solver2) = Z3QFree.checkUniversal(Implies(newinv, False))
Christian Müller's avatar
Christian Müller committed
115
            if (status2 == Status.SATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
116
              // Negation of newinv still sat, newinv does not imply false)
Christian Müller's avatar
Christian Müller committed
117
              logger.info(s"Relabeling ${nextEdge._1}. New size: ${newinv.opsize()}. Continuing.")
118
              checkInvariantRec(newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
119
            } else {
Christian Müller's avatar
Christian Müller committed
120
              logger.info(s"New invariant for ${nextEdge._1} not satisfiable. Terminating.")
121
              (false, newlabels :: labellist, newproven :: provenlist)
Christian Müller's avatar
Christian Müller committed
122
            }
123
          } else {
Christian Müller's avatar
Christian Müller committed
124 125
            logger.info("Relabelled initial node. Terminating.")
            // logger.info(s"Model: ${Z3.printModel(solver.getModel())}")
126
            (false, labellist, provenlist)
127 128 129
          }
        }
      }
130 131
    }

Christian Müller's avatar
Christian Müller committed
132
    // create labelling
Christian Müller's avatar
Christian Müller committed
133
    val labels = (for (n <- graph.nodes) yield { n.value -> inv }).toMap
Christian Müller's avatar
Christian Müller committed
134 135 136 137 138 139 140

    // update labels with untouched map
    val untouchedlabels = for ((n, inv) <- labels) yield {
      n -> inv.assumeEmpty(untouched(graph.get(n)).toList)
    }

    val (time, (result, labellings, proven)) = Utils.time { checkInvariantRec(untouchedlabels, List(Set())) }
141
    
Christian Müller's avatar
Christian Müller committed
142
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
143
    val dot2 = dot1.map(tup => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
144 145
      // if (t._2.opsize() <= 5000) t._2.pretty() else "TOO BIG"
      t._2.pretty()
Christian Müller's avatar
Christian Müller committed
146
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
147

Christian Müller's avatar
Christian Müller committed
148
    (result, graph, labellings.reverse, proven.reverse, dot2, time)
Christian Müller's avatar
Christian Müller committed
149 150
  }
  
Christian Müller's avatar
Christian Müller committed
151
  def checkInvariantFPDot(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
Christian Müller's avatar
Christian Müller committed
152
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
Christian Müller's avatar
Christian Müller committed
153 154 155 156
    (result, dot, time)
  }

  def checkInvariantFPHeadLabel(spec: Spec, inv: Formula, properties:InvProperties = InvProperties.DEFAULT) = {
Christian Müller's avatar
Christian Müller committed
157 158
    val (result, graph, afterlabels, proven, dot, time) = checkInvariantFPLabelling(spec, inv, properties)
    (result, graph, afterlabels.last, time)
159
  }
Christian Müller's avatar
Christian Müller committed
160
  
Christian Müller's avatar
Christian Müller committed
161
  def checkInvariantOnce(spec: Spec, inv: Formula, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
162

Christian Müller's avatar
Christian Müller committed
163
    // Build graph
164
    val graph = Encoding.toGraph(spec.w)
Christian Müller's avatar
Christian Müller committed
165
    val untouched = Encoding.untouchedMap(graph, spec.w.sig)
Christian Müller's avatar
Christian Müller committed
166

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

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

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

176 177
      // Special handling for first block
      val isfirst = !e.from.hasPredecessors
178

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

Christian Müller's avatar
Christian Müller committed
181
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
182 183 184
        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
185
          msg ++= Z3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
186 187
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
188 189
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
190 191 192 193 194 195
        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
196

Christian Müller's avatar
Christian Müller committed
197 198
    val safe = list.reduceLeft(_ && _)
    if (safe) {
199
      msg ++= s"Proven safe.\n"
200
      logger.info(s"Workflow ${spec.w}\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
201
    }
Christian Müller's avatar
Christian Müller committed
202
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
203 204
  }
}