Preconditions.scala 4.54 KB
Newer Older
1
package de.tum.niwo.invariants
Christian Müller's avatar
Christian Müller committed
2

3 4 5 6
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.Utils
import de.tum.niwo.blocks.{InvariantSpec, SetStmt, SimpleTSBlock}
import de.tum.niwo.foltl.FOLTL.{Exists, Formula, Fun, Neg}
7
import de.tum.niwo.foltl.{FOLTL, FOTransformers, FormulaFunctions, Properties}
Christian Müller's avatar
Christian Müller committed
8
import de.tum.niwo.toz3.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
  def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleTSBlock): Formula = {
Christian Müller's avatar
Christian Müller committed
13 14
    // TODO: should this contain f.freeVars?
    val boundvars = f.boundVars
15 16
    updates.foldRight(f)((update, f) => {
      val (repname, (vars, form)) = update
Christian Müller's avatar
Christian Müller committed
17 18
      val fixupdate = FormulaFunctions.fixBinding(form, boundvars -- vars)

Christian Müller's avatar
Christian Müller committed
19
      val res = f everywhere {
20
        case Fun(name, ind, params) if name == repname => {
Christian Müller's avatar
Christian Müller committed
21
          val renamed = fixupdate.parallelRename(vars, params)
Christian Müller's avatar
Christian Müller committed
22

23 24 25 26 27 28 29 30
          // 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
31
      res
32 33
    })
  }
34

Christian Müller's avatar
Christian Müller committed
35 36 37
  def getUpdate(s:SetStmt, spec:InvariantSpec, properties:InvProperties): Formula = {
    val frees = s.guard.freeVars -- s.tuple.toSet -- spec.ts.sig.constants
    Exists(frees.toList, s.guard).simplify
Christian Müller's avatar
Christian Müller committed
38 39
  }

Christian Müller's avatar
Christian Müller committed
40 41 42 43 44 45 46 47
  // FIXME: is this still needed?
//  def weakestPrecondition(post: Formula, outerb: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties): Formula = {
//    val precond = outerb.steps.foldRight(post)((b, f) => {
//      val innerprecond = weakestPreconditionSingle(f, b, spec, properties)
//      innerprecond
//    })
//    precond
//  }
Christian Müller's avatar
Christian Müller committed
48

Christian Müller's avatar
Christian Müller committed
49
  def weakestPrecondition(f: Formula, b:SimpleTSBlock, spec: InvariantSpec, properties: InvProperties) = {
Christian Müller's avatar
Christian Müller committed
50 51 52

    val updates = for (s <- b.steps) yield {
      s.fun -> (s.tuple, {
Christian Müller's avatar
Christian Müller committed
53
        getUpdate(s, spec, properties)
Christian Müller's avatar
Christian Müller committed
54 55 56
      })
    }

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

Christian Müller's avatar
Christian Müller committed
60 61
    // TODO: have we proven this correct?
    val removed = FOTransformers.eliminateDoubleQuantifiers(replaced)
62
    if (Utils.DEBUG_MODE) {
Christian Müller's avatar
Christian Müller committed
63 64 65
      val neg1 = replaced.toNegNf
      val neg2 = removed.toNegNf
      if (FormulaFunctions.collectQuantifiers(neg1) != FormulaFunctions.collectQuantifiers(neg2)) {
Christian Müller's avatar
Christian Müller committed
66
        logger.error(s"Would have removed a quantifier:\nBefore: ${neg1}\nAfter:  $neg2")
67 68
      }
    }
Christian Müller's avatar
Christian Müller committed
69

Christian Müller's avatar
Christian Müller committed
70 71
    replaced
//    removed
Christian Müller's avatar
Christian Müller committed
72
  }
Christian Müller's avatar
Christian Müller committed
73

74 75 76
  def abstractedPrecondition(f: Formula, b: SimpleTSBlock, spec: InvariantSpec,
                             properties: InvProperties, untouched: Set[String], diverged:Boolean): Formula = {

77
    val precond = weakestPrecondition(f, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
78

Christian Müller's avatar
Christian Müller committed
79
    // Assume untouched predicates empty
80 81 82 83
    val untouchedprecond = precond.assumeEmpty(untouched.toList)

    val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)

84
    // If not diverged yet, remove annotations from all predicates since all copies are equal
85 86 87 88 89 90 91
    // TODO: this is hyperproperty-specific
    val removedannotations = if (!diverged) {
            val rels = spec.ts.sig.preds.map(_.name)
            rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r)))
          } else {
            z3simpednewinv
          }
92

93
    // Abstract away inner existentials
94
    val universalinv = if (removedannotations.toNegNf.hasSubFormula {
Christian Müller's avatar
Christian Müller committed
95
      case _:Exists => true
96
    }) {
97
      FOTransformers.abstractExistentials(removedannotations)
Christian Müller's avatar
Christian Müller committed
98
    } else {
99
      removedannotations
Christian Müller's avatar
Christian Müller committed
100
    }
Christian Müller's avatar
Christian Müller committed
101

Christian Müller's avatar
Christian Müller committed
102
    // Eliminate As (choices/oracles)
Christian Müller's avatar
Christian Müller committed
103
    val oless = if (properties.eliminateA) {
Christian Müller's avatar
Christian Müller committed
104 105 106 107 108 109 110
      val oracles = spec.ts.sig.as.map(_.name)

      val occuringAs = oracles.filter(AUX =>
        universalinv.hasSubFormula { case Fun(AUX, _, _) => true }
      )

      occuringAs.foldRight(universalinv)((AUX, inv) =>
111
        FOTransformers.eliminateAuxiliaryPredicate(inv, AUX, properties)
Christian Müller's avatar
Christian Müller committed
112
      )
113
    } else {
Christian Müller's avatar
Christian Müller committed
114
      universalinv
115 116
    }

Christian Müller's avatar
Christian Müller committed
117
    // Eliminate Bs (Win game)
Christian Müller's avatar
src  
Christian Müller committed
118
    val bless = if (properties.eliminateB) {
Christian Müller's avatar
Christian Müller committed
119
      val bs = spec.ts.sig.bs
Christian Müller's avatar
ineq  
Christian Müller committed
120 121

      val occuringBs = bs.filter(b =>
Christian Müller's avatar
Christian Müller committed
122
        oless.hasSubFormula { case Fun(b.name, _, _) => true }
Christian Müller's avatar
ineq  
Christian Müller committed
123 124
      )

Christian Müller's avatar
Christian Müller committed
125
      if (occuringBs.nonEmpty && diverged) {
126 127 128
        logger.error("Trying to compute strategies for B with B,B' not necessarily equal")
      }

Christian Müller's avatar
ineq  
Christian Müller committed
129
      occuringBs.foldRight(oless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
Christian Müller's avatar
src  
Christian Müller committed
130
    } else {
131
      oless
Christian Müller's avatar
src  
Christian Müller committed
132 133
    }

134 135 136 137 138 139

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

140
    Z3BSFO.simplifyBS(bless.simplify)
Christian Müller's avatar
Christian Müller committed
141
  }
142
}