InvariantChecker.scala 5.45 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
5
6
7
8
9
package de.tum.workflows.toz3

import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Implicits._
import de.tum.workflows.WorkflowParser
import de.tum.workflows.Encoding
import de.tum.workflows.Preconditions
Christian Müller's avatar
Christian Müller committed
10
11
import de.tum.workflows.foltl.Properties.T1
import de.tum.workflows.foltl.Properties.T2
Christian Müller's avatar
Christian Müller committed
12
13
14
15
16
17
18

import scalax.collection.edge.LDiEdge // labeled directed edge
import com.microsoft.z3.Context
import java.util.HashMap
import org.omg.CORBA.TIMEOUT
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
Christian Müller's avatar
Christian Müller committed
19
import de.tum.workflows.foltl.Properties
Christian Müller's avatar
Christian Müller committed
20
21

object InvariantChecker extends LazyLogging {
Christian Müller's avatar
checker    
Christian Müller committed
22

Christian Müller's avatar
Christian Müller committed
23
  val TIMEOUT = 60000 // in milliseconds
Christian Müller's avatar
checker    
Christian Müller committed
24
25
26
27
28
29

  def checkOnZ3(f: Formula) = {
    // Set up Z3
    val cfg = new HashMap[String, String]()
    cfg.put("timeout", TIMEOUT.toString())
    val ctx = new Context(cfg)
30
31
32
33
34
35

    val qe = ctx.mkTactic("qe")
    val default = ctx.mkTactic("smt")
    val t = ctx.andThen(qe, default)

    val s = ctx.mkSolver(t)
Christian Müller's avatar
checker    
Christian Müller committed
36
37
38
39
40
41
42
43
44

    s.add(toZ3.translate(f, ctx))

    // Send to z3
    val c = s.check()
    if (c == Status.UNKNOWN) {
      logger.info(s"Z3 status unknown: ${s.getReasonUnknown()}")
    }
    if (c == Status.SATISFIABLE) {
45
46
      logger.info(s"Z3 status satisfiable")
//      logger.info(s"${s.getModel()}")
Christian Müller's avatar
checker    
Christian Müller committed
47
48
    }
    (c, s)
Christian Müller's avatar
Christian Müller committed
49
  }
Christian Müller's avatar
checker    
Christian Müller committed
50

51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
  def checkBlockInvariant(sig:Signature, b: SimpleBlock, pre: Formula, post: Formula, stubborn: Boolean, isfirst: Boolean) = {
    val precond = Preconditions.weakestPrecondition(post, b)

    // Stubborn agents -> remove trace variable from choice predicate
    val stubprecond = if (stubborn) {
      precond.everywhere {
        case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
      }
    } else precond
    
    // TODO: do not do this here
    val firstprecond = if (isfirst) {
      stubprecond.assumeEmpty(sig.preds.map(_.name).toList)
    } else { stubprecond }

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

    val f = Implies(pre, firstprecond)

    logger.info(s"Checking invariant implication for $b")
    val tocheck = Neg(f).simplify()

    //      val test3 = tocheck.toPrenex()

    // Transform to existential
    if (!tocheck.isBS()) {
      logger.error(s"Not in BS: Invariant implication ${tocheck.pretty}")
    }

    val negnf = tocheck.toNegNf()

    val (agents, inner) = LTL.eliminateExistentials(negnf)
    val existbound = Exists(agents, inner)
    val univfree = LTL.eliminateUniversals(existbound, agents)

    //      val test3 = univfree.pretty()
    //      println(test3)

    checkOnZ3(univfree.simplify())
  }

Christian Müller's avatar
checker    
Christian Müller committed
93
94
  def checkInvariant(w: Workflow, inv: Formula, stubborn: Boolean) = {

Christian Müller's avatar
Christian Müller committed
95
96
    // Build graph
    val graph = Encoding.toGraph(w)
Christian Müller's avatar
checker    
Christian Müller committed
97

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

Christian Müller's avatar
Christian Müller committed
101
102
    // Check all edges 
    val list = for (e <- graph.edges) yield {
Christian Müller's avatar
checker    
Christian Müller committed
103

Christian Müller's avatar
Christian Müller committed
104
      // Check I -> WP[w](inv)
Christian Müller's avatar
checker    
Christian Müller committed
105
      val b: SimpleBlock = e
106
      
107
108
109
      // Special handling for first block
      // TODO: Replace by iteration
      val isfirst = !e.from.hasPredecessors
110
      
111
      val (res, solver) = checkBlockInvariant(w.sig, b, inv, inv, stubborn, isfirst)
112

Christian Müller's avatar
Christian Müller committed
113
      if (res != Status.UNSATISFIABLE) {
Christian Müller's avatar
Christian Müller committed
114
115
116
        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
117
          msg ++= toZ3.printModel(solver.getModel()).lines.map("  " + _).mkString("\n")
Christian Müller's avatar
Christian Müller committed
118
119
        } else if (res == Status.UNKNOWN) {
          msg ++= s"Z3 result: $res (${solver.getReasonUnknown()})\n"
Christian Müller's avatar
Christian Müller committed
120
121
        }
        msg ++= "\n"
Christian Müller's avatar
Christian Müller committed
122
123
124
125
126
127
        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
checker    
Christian Müller committed
128

Christian Müller's avatar
Christian Müller committed
129
130
    val safe = list.reduceLeft(_ && _)
    if (safe) {
131
      msg ++= s"Proven safe.\n"
Christian Müller's avatar
Christian Müller committed
132
      logger.info(s"Workflow $w\n proven safe for invariant:\n${inv.pretty()}")
Christian Müller's avatar
Christian Müller committed
133
    }
Christian Müller's avatar
Christian Müller committed
134
    (safe, msg)
Christian Müller's avatar
Christian Müller committed
135
  }
Christian Müller's avatar
checker    
Christian Müller committed
136
137

  def genEq(f: Fun, p: List[Var]) = {
Christian Müller's avatar
Christian Müller committed
138
139
140
    val newf = f.parallelRename(f.params, p)
    Eq(newf.in(T1), newf.in(T2))
  }
Christian Müller's avatar
checker    
Christian Müller committed
141
142

  def invariantNoninterStubborn(spec: Spec) = {
Christian Müller's avatar
Christian Müller committed
143
    val agent = spec.target.params(0)
Christian Müller's avatar
checker    
Christian Müller committed
144
145

    val premise = And.make(for ((o, t) <- spec.declass) yield {
Christian Müller's avatar
Christian Müller committed
146
147
      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2) 
      Forall(o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
Christian Müller's avatar
Christian Müller committed
148
    })
Christian Müller's avatar
checker    
Christian Müller committed
149

Christian Müller's avatar
Christian Müller committed
150
151
    val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
      val quant = r.params.drop(1)
Christian Müller's avatar
checker    
Christian Müller committed
152
      Forall(quant, genEq(r, agent :: quant))
Christian Müller's avatar
Christian Müller committed
153
    })
Christian Müller's avatar
checker    
Christian Müller committed
154

Christian Müller's avatar
Christian Müller committed
155
    Forall(agent, premise  conclusion).simplify()
Christian Müller's avatar
Christian Müller committed
156
  }
Christian Müller's avatar
checker    
Christian Müller committed
157

158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
  def invariantNoninterStubbornBS(spec: Spec) = {
    val agent = spec.target.params(0)

    val premise = for ((o, t) <- spec.declass) yield {
      // Forall fv(o). (t_T1 or t_t2) -> G (o_T1 <-> o_T2) 
      (o.freeVars().toList, Implies(Or(t.in(T1), t.in(T2)), Eq(o.in(T1), o.in(T2))))
    }
    val quants = premise.flatMap(_._1).toSet.toList // eliminate doubles

    val conclusion = And.make(for (r <- spec.w.sig.preds.toList if r.params.head.typ == agent.typ) yield {
      val quant = r.params.drop(1)
      Forall(quant, genEq(r, agent :: quant))
    })

    Forall(agent, Forall(quants, Implies(And.make(premise.map(_._2)), conclusion))).simplify()
  }

Christian Müller's avatar
Christian Müller committed
175
176
177
178
179
180
  def invariantAllEqual(spec: Spec) = {
    And.make(for (r <- spec.w.sig.preds.toList) yield {
      Forall(r.params, genEq(r, r.params))
    })
  }

Christian Müller's avatar
Christian Müller committed
181
}