Preconditions.scala 7.5 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
    // TODO: should this contain f.freeVars?
    val boundvars = f.boundVars
99 100
    updates.foldRight(f)((update, f) => {
      val (repname, (vars, form)) = update
Christian Müller's avatar
Christian Müller committed
101 102
      val fixupdate = FormulaFunctions.fixBinding(form, boundvars -- vars)

Christian Müller's avatar
Christian Müller committed
103
      val res = f everywhere {
104
        case Fun(name, ind, params) if name == repname => {
Christian Müller's avatar
Christian Müller committed
105
          val renamed = fixupdate.parallelRename(vars, params)
Christian Müller's avatar
Christian Müller committed
106

107 108 109 110 111 112 113 114
          // Annotate the precondition with the index
          if (ind.isDefined) {
            FormulaFunctions.annotate(renamed, ind.get)
          } else {
            renamed
          }
        }
      }
Christian Müller's avatar
Christian Müller committed
115
      res
116 117
    })
  }
118

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

Christian Müller's avatar
Christian Müller committed
121
      val frees = s.guard.freeVars -- s.tuple.toSet -- spec.constants
Christian Müller's avatar
Christian Müller committed
122 123 124

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

Christian Müller's avatar
Christian Müller committed
134 135
  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
136 137 138
    stepOne map { b =>  elaborateOraclyBlock(b, spec) }
  }

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

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

Christian Müller's avatar
Christian Müller committed
143
    val steps = elaborate(outerb, spec, properties)
Christian Müller's avatar
Christian Müller committed
144 145

    val precond = steps.foldRight(post)((b, f) => {
Christian Müller's avatar
Christian Müller committed
146
      val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
147
      innerprecond
148
    })
Christian Müller's avatar
Christian Müller committed
149 150 151
    precond
  }

Christian Müller's avatar
Christian Müller committed
152
  private def weakestPreconditionSingle(f: Formula, b:SimpleBlock, spec: NISpec, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
153 154 155

    val updates = for (s <- b.steps) yield {
      s.fun -> (s.tuple, {
Christian Müller's avatar
Christian Müller committed
156
        getUpdate(s, spec, properties)
Christian Müller's avatar
Christian Müller committed
157 158 159
      })
    }

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

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

Christian Müller's avatar
Christian Müller committed
173 174
//    replaced
    removed
Christian Müller's avatar
Christian Müller committed
175
  }
Christian Müller's avatar
Christian Müller committed
176

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

Christian Müller's avatar
Christian Müller committed
180
    // Assume untouched predicates empty
181 182 183 184
    val untouchedprecond = precond.assumeEmpty(untouched.toList)

    val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)

185 186 187 188 189 190 191 192 193
    // 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
    }

194
    // Abstract away inner existentials
195
    val universalinv = if (removedannotations.toNegNf.hasSubFormula {
Christian Müller's avatar
Christian Müller committed
196
      case _:Exists => true
197
    }) {
198
      FOTransformers.abstractExistentials(removedannotations)
Christian Müller's avatar
Christian Müller committed
199
    } else {
200
      removedannotations
Christian Müller's avatar
Christian Müller committed
201
    }
Christian Müller's avatar
Christian Müller committed
202

203
    // Eliminate Choices
Christian Müller's avatar
Christian Müller committed
204
    val auxless = if (b.pred.isDefined && properties.eliminateA) {
Christian Müller's avatar
Christian Müller committed
205
      FOTransformers.eliminateAuxiliaryPredicate(universalinv, b.pred.get)
Christian Müller's avatar
Christian Müller committed
206 207 208
    } else {
      universalinv
    }
Christian Müller's avatar
src  
Christian Müller committed
209

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

Christian Müller's avatar
src  
Christian Müller committed
218 219
    // Win game
    val bless = if (properties.eliminateB) {
Christian Müller's avatar
ineq  
Christian Müller committed
220 221 222 223 224 225 226 227 228
      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)) {
229 230 231
        logger.error("Trying to compute strategies for B with B,B' not necessarily equal")
      }

Christian Müller's avatar
ineq  
Christian Müller committed
232
      occuringBs.foldRight(oless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
Christian Müller's avatar
src  
Christian Müller committed
233
    } else {
234
      oless
Christian Müller's avatar
src  
Christian Müller committed
235 236
    }

237 238 239 240 241 242

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

243
    Z3BSFO.simplifyBS(bless.simplify)
Christian Müller's avatar
Christian Müller committed
244 245
  }
}