Merge pull request #482 from viperproject/old_state_refactoring

Use local variables for the old state

Author: gauravpartha

src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala

@@ -623,7 +623,6 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     val res = sil.Result(f.typ)()
     val init : Stmt = MaybeCommentBlock("Initializing the state",
       stateModule.initBoogieState ++ (f.formalArgs map (a => allAssumptionsAboutValue(a.typ,mainModule.translateLocalVarDecl(a),true))) ++ assumeFunctionsAt(heights(f.name)))
-    val initOld : Stmt = MaybeCommentBlock("Initializing the old state", stateModule.initOldState)
     val checkPre : Stmt = checkFunctionPreconditionDefinedness(f)
     val checkExp : Stmt = if (f.isAbstract) MaybeCommentBlock("(no definition for abstract function)",Nil) else
       MaybeCommentBlock("Check definedness of function body",
@@ -632,7 +631,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
       MaybeCommentBlock("Translate function body",
       translateResult(res) := translateExp(f.body.get))
     val checkPost = checkFunctionPostconditionDefinedness(f)
-    val body : Stmt = Seq(init, initOld, checkPre, checkExp, exp, checkPost)
+    val body : Stmt = Seq(init, checkPre, checkExp, exp, checkPost)
     val definednessChecks = Procedure(Identifier(f.name + "#definedness"), args, translateResultDecl(res), body)
     checkingDefinednessOfFunction = None
     definednessChecks

src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala

@@ -82,7 +82,7 @@ class DefaultHeapModule(val verifier: Verifier)
   private val qpHeap = LocalVar(qpHeapName, heapTyp)
   private var heap: Var = originalHeap
   private def heapVar: Var = {assert (!usingOldState); heap}
-  private def heapExp: Exp = if (usingPureState) dummyHeap else (if (usingOldState) Old(heap) else heap)
+  private def heapExp: Exp = if (usingPureState) dummyHeap else heap
   private val nullName = Identifier("null")
   private val nullLit = Const(nullName)
   private val freshObjectName = Identifier("freshObj")
@@ -774,10 +774,6 @@ class DefaultHeapModule(val verifier: Verifier)
   def resetBoogieState: Stmt = {
     Havoc(heapVar)
   }
-  def initOldState: Stmt = {
-    val hVar = heapVar
-    Assume(Old(hVar) === hVar)
-  }
 
   def staticStateContributions(withHeap: Boolean, withPermissions: Boolean): Seq[LocalVarDecl] = if(withHeap) Seq(LocalVarDecl(heapName, heapTyp)) else Seq()
   def currentStateContributions: Seq[LocalVarDecl] = Seq(LocalVarDecl(heap.name, heapTyp))

src/main/scala/viper/carbon/modules/impls/DefaultStateModule.scala

@@ -63,7 +63,7 @@ class DefaultStateModule(val verifier: Verifier) extends StateModule {
 
     // initialize the state of all components and assume that afterwards the
     // whole state is good
-  val firstStmt =  components map (_.initBoogieState)
+    val firstStmt =  components map (_.initBoogieState)
     // note: this code should come afterwards, to allow the components to reset their state variables
     for (c <- components) {
       curState.put(c, c.currentStateVars)
@@ -85,12 +85,9 @@ class DefaultStateModule(val verifier: Verifier) extends StateModule {
   }
 
   def initOldState: Stmt = {
-    curOldState = new StateComponentMapping()
-    for (c <- components) yield {
-      val exps = curState.get(c)
-      curOldState.put(c, exps) // Logic: whenever we *get* on the old state, we should wrap in "Old"
-      exps map (e => Assume(e === Old(e))): Stmt
-    }
+    val freshSnapshot = freshTempStateKeepCurrentAux("old", true)
+    curOldState = freshSnapshot._1
+    initToCurrentStmt(freshSnapshot)
   }
 
 
@@ -104,7 +101,7 @@ class DefaultStateModule(val verifier: Verifier) extends StateModule {
         res ++= hashMap.get(c)
       }
     }
-    if(usingOldState) (res map (v => Old(v))) else res // ALEX: I think this conditional should be on the element of the StateSnapshot
+    res
   }
 
 
@@ -130,6 +127,8 @@ class DefaultStateModule(val verifier: Verifier) extends StateModule {
   override def stateRepositoryGet(name:String) : Option[StateSnapshot] = stateRepository.get(name)
 
   override def freshTempState(name: String, discardCurrent: Boolean = false, initialise: Boolean = false): (Stmt, StateSnapshot) = {
+    assert(name != "old")
+
     val previousState = new StateSnapshot(new StateComponentMapping(), usingOldState, usingPureState)
 
     curState = new StateComponentMapping() // essentially, the code below "clones" what curState should represent anyway. But, if we omit this line, we inadvertently alias the previous hash map.
@@ -149,6 +148,12 @@ class DefaultStateModule(val verifier: Verifier) extends StateModule {
   }
 
   override def freshTempStateKeepCurrent(name: String) : StateSnapshot = {
+    freshTempStateKeepCurrentAux(name, false)
+  }
+
+  private def freshTempStateKeepCurrentAux(name: String, usedForOldState: Boolean) : StateSnapshot = {
+    assert(usedForOldState || name != "old")
+
     val freshState = new StateComponentMapping()
 
     for (c <- components) yield {

src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala

@@ -85,7 +85,7 @@ class QuantifiedPermModule(val verifier: Verifier)
   private val originalMask = GlobalVar(maskName, maskType)
   private var mask: Var = originalMask // When reading, don't use this directly: use either maskVar or maskExp as needed
   private def maskVar : Var = {assert (!usingOldState); mask}
-  private def maskExp : Exp = if (usingPureState) zeroMask else (if (usingOldState) Old(mask) else mask)
+  private def maskExp : Exp = if (usingPureState) zeroMask else mask
   private val zeroMaskName = Identifier("ZeroMask")
   private val zeroMask = Const(zeroMaskName)
   private val zeroPMaskName = Identifier("ZeroPMask")
@@ -252,10 +252,6 @@ class QuantifiedPermModule(val verifier: Verifier)
   def resetBoogieState = {
     (maskVar := zeroMask)
   }
-  def initOldState: Stmt = {
-    val mVar = maskVar
-    Assume(Old(mVar) === mVar)
-  }
 
   override def reset = {
     mask = originalMask