InvariantChecker.scala 7.75 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
            val invalidated = proven.filter(_.from == nextEdge.to)
Christian Müller's avatar
Christian Müller committed
110

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

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

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

    // 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())) }
140
    
Christian Müller's avatar
Christian Müller committed
141
    val dot1 = labellings.zip(proven).reverse
Christian Müller's avatar
Christian Müller committed
142
    val dot2 = dot1.map(tup => Encoding.toDot(graph)(tup._1.map(t => (t._1, {
143 144
      // if (t._2.opsize() <= 5000) t._2.pretty() else "TOO BIG"
      t._2.pretty()
Christian Müller's avatar
Christian Müller committed
145
    })), tup._2))
Christian Müller's avatar
Christian Müller committed
146

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

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

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

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

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

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

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

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

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

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