Preconditions.scala 7.32 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4
package de.tum.workflows

import com.typesafe.scalalogging._
import blocks._
5
import de.tum.workflows.foltl.{FOLTL, FOTransformers, FormulaFunctions, Properties}
Christian Müller's avatar
Christian Müller committed
6
import de.tum.workflows.foltl.FOLTL._
Christian Müller's avatar
Christian Müller committed
7
import de.tum.workflows.foltl.Properties._
8
import de.tum.workflows.toz3.{InvProperties, Z3BSFO}
Christian Müller's avatar
Christian Müller committed
9 10

object Preconditions extends LazyLogging {
Christian Müller's avatar
Christian Müller committed
11

Christian Müller's avatar
Christian Müller committed
12 13 14 15 16 17 18 19 20 21 22 23
  private def elaborateSteps(b: SimpleBlock, spec: NISpec, properties: InvProperties): List[SimpleBlock] = {

    val guardfix = if (!b.isoracly && b.pred.isDefined) {
      // is "normal" may block
      val choice = Fun(b.pred.get, b.agents)

      for (s <- b.steps) yield {
        val first = s.tuple.head
        val inner = if (first.typ == spec.target.params.head.typ) {
          if (properties.stubborn) {
            choice.in(T1)
          } else {
Christian Müller's avatar
Christian Müller committed
24
            val inf = Fun(INFNAME, List(b.agents.head))
Christian Müller's avatar
Christian Müller committed
25 26 27 28 29 30 31 32 33 34 35 36
            Or(And(Neg(inf.in(T1)), choice.in(T1)), And(inf.in(T1), choice))
          }
        } else {
          choice
        }
        val newguard = And(s.guard, inner)
        s.updateGuard(newguard)
      }
    } else {
      b.steps
    }

Christian Müller's avatar
Christian Müller committed
37 38 39 40 41 42 43
    val newb = b.updateSteps(guardfix)

    // for causality, add informedness updates
    if (properties.stubborn) {
      List(newb)
    } else {
      val newsteps = for (
44
        stmt <- b.steps
Christian Müller's avatar
Christian Müller committed
45 46
        if spec.causals.map(_.typ).contains(stmt.tuple.head.typ) ||
          stmt.tuple.head.typ == spec.target.params.head.typ) yield {
Christian Müller's avatar
Christian Müller committed
47 48 49 50 51 52
        val fun = Fun(stmt.fun, stmt.tuple)
        // TODO
        val guard = Neg(Equiv(fun.in(T1), fun.in(T2)))
        ForallBlock(stmt.tuple, List(Add(guard, INFNAME, List(stmt.tuple.head))))
      }
      newb :: newsteps
Christian Müller's avatar
Christian Müller committed
53
    }
54
  }
Christian Müller's avatar
Christian Müller committed
55

Christian Müller's avatar
Christian Müller committed
56
  // For oracly blocks, remove O from guard and add to ForallMay choice predicate
Christian Müller's avatar
Christian Müller committed
57
  private def elaborateOraclyBlock(b: SimpleBlock, spec: NISpec) = {
Christian Müller's avatar
Christian Müller committed
58
    if (b.isoracly) {
Christian Müller's avatar
Christian Müller committed
59

Christian Müller's avatar
Christian Müller committed
60
      val stmt = b.steps.head // can only be one
Christian Müller's avatar
Christian Müller committed
61 62

      def findOracle(f: Formula) = {
Christian Müller's avatar
Christian Müller committed
63
        f.collect {
Christian Müller's avatar
Christian Müller committed
64
          case f: Fun if f.isOracle => List(f.name)
Christian Müller's avatar
Christian Müller committed
65 66
        }
      }
Christian Müller's avatar
Christian Müller committed
67 68 69 70 71 72 73 74 75 76 77
      val oracles = findOracle(stmt.guard)
      val name = oracles.head

      if (oracles.size != 1) {
        logger.error(s"Found oracly block $b with more than one oracle")
      }

      val choice = Fun(name, b.agents)

      def fixguard(f: Formula, choice:Fun) = {
        val nooracles = f.everywhere {
Christian Müller's avatar
Christian Müller committed
78
          case f: Fun if f.isOracle => True
Christian Müller's avatar
Christian Müller committed
79 80
        }

Christian Müller's avatar
Christian Müller committed
81
        val decl = spec.declass.getOrElse(name, (List(), False))._2
Christian Müller's avatar
Christian Müller committed
82 83 84 85 86
        // FIXME: substitutions?
        // FIXME: decl in T2?
        And(nooracles, Or(And(decl.in(T1), choice.in(T1)), And(Neg(decl.in(T1)), choice)))
      }

Christian Müller's avatar
Christian Müller committed
87

Christian Müller's avatar
Christian Müller committed
88
      val newstmt = stmt match {
Christian Müller's avatar
Christian Müller committed
89 90
        case Add(guard, fun, tuple)    => Add(fixguard(guard, choice).simplify, fun, tuple)
        case Remove(guard, fun, tuple) => Remove(fixguard(guard, choice).simplify, fun, tuple)
Christian Müller's avatar
Christian Müller committed
91 92 93 94
      }
      ForallMayBlock(b.agents, name, List(newstmt))
    } else b
  }
Christian Müller's avatar
Christian Müller committed
95

Christian Müller's avatar
Christian Müller committed
96
  def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleBlock): Formula = {
Christian Müller's avatar
Christian Müller committed
97

98 99 100 101 102
    updates.foldRight(f)((update, f) => {
      val (repname, (vars, form)) = update
      f everywhere {
        case Fun(name, ind, params) if name == repname => {
          val renamed = form.parallelRename(vars, params)
Christian Müller's avatar
Christian Müller committed
103

104 105 106 107 108 109 110 111 112 113
          // Annotate the precondition with the index
          if (ind.isDefined) {
            FormulaFunctions.annotate(renamed, ind.get)
          } else {
            renamed
          }
        }
      }
    })
  }
114

Christian Müller's avatar
Christian Müller committed
115
  def getUpdate(s:Statement, spec:NISpec, properties:InvProperties): Formula = {
116

Christian Müller's avatar
Christian Müller committed
117
      val frees = s.guard.freeVars -- s.tuple.toSet -- spec.constants
Christian Müller's avatar
Christian Müller committed
118 119 120

      val form = s match {
        case Add(_, _, _) => {
Christian Müller's avatar
Christian Müller committed
121
          Or(Fun(s.fun, s.tuple), Exists(frees.toList, s.guard)).simplify
Christian Müller's avatar
Christian Müller committed
122
        }
Christian Müller's avatar
Christian Müller committed
123
        case Remove(_, _, _) => {
Christian Müller's avatar
Christian Müller committed
124
          And(Fun(s.fun, s.tuple), Forall(frees.toList, Neg(s.guard))).simplify
Christian Müller's avatar
Christian Müller committed
125 126 127 128 129
        }
      }
      form
  }

Christian Müller's avatar
Christian Müller committed
130 131
  def elaborate(block: SimpleBlock, spec:NISpec, properties:InvProperties): List[SimpleBlock] = {
    val stepOne = elaborateSteps(block, spec, properties)
Christian Müller's avatar
Christian Müller committed
132 133 134
    stepOne map { b =>  elaborateOraclyBlock(b, spec) }
  }

Christian Müller's avatar
Christian Müller committed
135
  def weakestPrecondition(post: Formula, outerb: SimpleBlock, spec: NISpec, properties: InvProperties): Formula = {
Christian Müller's avatar
Christian Müller committed
136

Christian Müller's avatar
Christian Müller committed
137
    // TODO: Make 2-trace elaboration optional
Christian Müller's avatar
Christian Müller committed
138

Christian Müller's avatar
Christian Müller committed
139
    val steps = elaborate(outerb, spec, properties)
Christian Müller's avatar
Christian Müller committed
140 141

    val precond = steps.foldRight(post)((b, f) => {
Christian Müller's avatar
Christian Müller committed
142
      val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
143
      innerprecond
144
    })
Christian Müller's avatar
Christian Müller committed
145 146 147
    precond
  }

Christian Müller's avatar
Christian Müller committed
148
  private def weakestPreconditionSingle(f: Formula, b:SimpleBlock, spec: NISpec, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
149 150 151

    val updates = for (s <- b.steps) yield {
      s.fun -> (s.tuple, {
Christian Müller's avatar
Christian Müller committed
152
        getUpdate(s, spec, properties)
Christian Müller's avatar
Christian Müller committed
153 154 155
      })
    }

Christian Müller's avatar
Christian Müller committed
156
    // Replace literals with their precondition
157
    val replaced = subst(f, updates, b)
Christian Müller's avatar
Christian Müller committed
158

Christian Müller's avatar
Christian Müller committed
159 160
    // TODO: have we proven this correct?
    val removed = FOTransformers.eliminateDoubleQuantifiers(replaced)
161
    if (Utils.DEBUG_MODE) {
Christian Müller's avatar
Christian Müller committed
162 163 164 165
      val neg1 = replaced.toNegNf
      val neg2 = removed.toNegNf
      if (FormulaFunctions.collectQuantifiers(neg1) != FormulaFunctions.collectQuantifiers(neg2)) {
        logger.warn(s"Would have removed a quantifier:\nBefore: ${neg1}\nAfter:  $neg2")
166 167
      }
    }
Christian Müller's avatar
Christian Müller committed
168

Christian Müller's avatar
Christian Müller committed
169
    replaced
Christian Müller's avatar
Christian Müller committed
170
  }
Christian Müller's avatar
Christian Müller committed
171

Christian Müller's avatar
Christian Müller committed
172
  def abstractedPrecondition(f: Formula, b: SimpleBlock, spec: NISpec, properties: InvProperties, untouched: Set[String]): Formula = {
173
    val precond = weakestPrecondition(f, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
174

Christian Müller's avatar
Christian Müller committed
175
    // Assume untouched predicates empty
176 177 178 179
    val untouchedprecond = precond.assumeEmpty(untouched.toList)

    val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)

180 181 182 183 184 185 186 187 188
    // if informedness untouched T1 and T2 are equal anyway, so remove annotations
    // TODO: better recognition for necessarily equal
    val removedannotations = if (untouched.contains(Properties.INFNAME)) {
      val rels = spec.w.sig.preds.map(_.name)
      rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r)))
    } else {
      z3simpednewinv
    }

189
    // Abstract away inner existentials
190
    val universalinv = if (removedannotations.toNegNf.hasSubFormula {
Christian Müller's avatar
Christian Müller committed
191
      case _:Exists => true
192
    }) {
193
      FOTransformers.abstractExistentials(removedannotations)
Christian Müller's avatar
Christian Müller committed
194
    } else {
195
      removedannotations
Christian Müller's avatar
Christian Müller committed
196
    }
Christian Müller's avatar
Christian Müller committed
197

198
    // Eliminate Choices
Christian Müller's avatar
Christian Müller committed
199
    val auxless = if (b.pred.isDefined && properties.eliminateA) {
Christian Müller's avatar
Christian Müller committed
200
      FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get)
Christian Müller's avatar
Christian Müller committed
201 202 203
    } else {
      universalinv
    }
Christian Müller's avatar
src  
Christian Müller committed
204

205
    // Eliminate Oracles
Christian Müller's avatar
Christian Müller committed
206 207
    val oless = if (properties.eliminateA) {
      val oracles = spec.w.sig.as.map(_.name)
208 209 210 211 212
      oracles.foldRight(auxless)((b, inv) => FOTransformers.eliminateAuxiliaryPredicate(inv, b))
    } else {
      auxless
    }

Christian Müller's avatar
src  
Christian Müller committed
213 214
    // Win game
    val bless = if (properties.eliminateB) {
Christian Müller's avatar
ineq  
Christian Müller committed
215 216 217 218 219 220 221 222 223
      val bs = spec.w.sig.bs

      val occuringBs = bs.filter(b =>
        oless.hasSubFormula {
          case Fun(b.name, _, _) => true
        }
      )

      if (occuringBs.nonEmpty && !untouched.contains(Properties.INFNAME)) {
224 225 226
        logger.error("Trying to compute strategies for B with B,B' not necessarily equal")
      }

Christian Müller's avatar
ineq  
Christian Müller committed
227
      occuringBs.foldRight(oless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
Christian Müller's avatar
src  
Christian Müller committed
228
    } else {
229
      oless
Christian Müller's avatar
src  
Christian Müller committed
230 231
    }

232 233 234 235 236 237

    if (Utils.DEBUG_MODE) {
      val possibleAttack = Z3BSFO.debugmodelBS(Neg(bless))
      logger.trace(s"Possible attack: $possibleAttack")
    }

238
    Z3BSFO.simplifyBS(bless.simplify)
Christian Müller's avatar
Christian Müller committed
239 240
  }
}