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

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

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

Christian Müller's avatar
Christian Müller committed
13
  def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleTSBlock): Formula = {
Christian Müller's avatar
Christian Müller committed
14 15
    // TODO: should this contain f.freeVars?
    val boundvars = f.boundVars
16 17
    updates.foldRight(f)((update, f) => {
      val (repname, (vars, form)) = update
Christian Müller's avatar
Christian Müller committed
18 19
      val fixupdate = FormulaFunctions.fixBinding(form, boundvars -- vars)

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

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

Christian Müller's avatar
Christian Müller committed
36 37 38
  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
39 40
  }

Christian Müller's avatar
Christian Müller committed
41 42 43 44 45 46 47 48
  // 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
49

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

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

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

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

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

Christian Müller's avatar
Christian Müller committed
75
  def abstractedPrecondition(f: Formula, b: SimpleTSBlock, spec: InvariantSpec, properties: InvProperties, untouched: Set[String]): Formula = {
76
    val precond = weakestPrecondition(f, b, spec, properties)
Christian Müller's avatar
Christian Müller committed
77

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

    val z3simpednewinv = Z3BSFO.simplifyBS(untouchedprecond)

Christian Müller's avatar
Christian Müller committed
83 84
    // if informedness untouched then T1 and T2 are equal anyway, so remove annotations
    // TODO: better recognition for necessarily equal, this does not work for general cases (also, this is hyperprop-specific)
85
    val removedannotations = if (untouched.contains(Properties.INFNAME)) {
Christian Müller's avatar
Christian Müller committed
86
      val rels = spec.ts.sig.preds.map(_.name)
87 88 89 90 91
      rels.foldRight(z3simpednewinv)((r, f) => Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, r)))
    } else {
      z3simpednewinv
    }

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

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

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

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

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

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

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

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

133 134 135 136 137 138

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

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