Merge pull request #473 from viperproject/meilers_general_perm_forperm

Add missing features

src/main/scala/viper/carbon/modules/HeapModule.scala

@@ -92,23 +92,15 @@ trait HeapModule extends Module with CarbonStateComponent {
   def predicateGhostFieldDecl(f: sil.Predicate): Seq[Decl]
 
   /**
-   * Translation of a resource access (field read/write, predicate or wand instance)
+   * Translation of a field read, predicate instance, or wand instance.
    */
-  def translateResourceAccess(r: sil.ResourceAccess): Exp = r match {
-    case la: LocationAccess => translateLocationAccess(la)
-    case mw: MagicWand => sys.error(s"Unexpectedly found magic wand $mw")
-  }
-
-  /**
-   * Translation of a field read or predicate instance
-   */
-  def translateLocationAccess(f: sil.LocationAccess): Exp
+  def translateResourceAccess(f: sil.ResourceAccess): Exp
   /**
     * Translation of a field read.
     */
   def translateLocationAccess(rcv: Exp, loc:Exp):Exp
 
-  def translateLocation(f: sil.LocationAccess): Exp
+  def translateResource(f: sil.ResourceAccess): Exp
   def translateLocation(pred: sil.Predicate, args: Seq[Exp]): Exp
 
   /**
@@ -147,15 +139,14 @@ trait HeapModule extends Module with CarbonStateComponent {
   def isPredicateField(f: Exp): Exp
 
   /**
-    * get Predicate Id (unique for each Predicate)
+    * get Predicate or wand Id (unique for each Predicate or wand)
     */
-  def getPredicateId(f:Exp): Exp
+  def getPredicateOrWandId(f:Exp): Exp
 
   /**
-    * Predicate name mapping to Id
+    * Predicate or (internal) wand name mapping to Id
     */
-
-  def getPredicateId(s:String):BigInt
+  def getPredicateOrWandId(s:String):BigInt
   /**
    * Is the given field a wand field?
    */

src/main/scala/viper/carbon/modules/PermModule.scala

@@ -99,15 +99,12 @@ trait PermModule extends Module with CarbonStateComponent {
 
   def zeroPMask: Exp
 
-  def hasDirectPerm(la: sil.LocationAccess): Exp
-
-  def permissionLookup(la: sil.LocationAccess) : Exp
-/** FIXME: duplicate method, here */
+  def hasDirectPerm(ra: sil.ResourceAccess): Exp
 
   /**
    * The expression for the current permission at a location.
    */
-  def currentPermission(loc: sil.LocationAccess): Exp
+  def currentPermission(loc: sil.ResourceAccess): Exp
 
   def currentPermission(rcv:Exp, loc:Exp):Exp
 

src/main/scala/viper/carbon/modules/WandModule.scala

@@ -61,6 +61,10 @@ trait WandModule extends Module with ComponentRegistry[TransferComponent] {
 
   def getWandRepresentation(w: sil.MagicWand):Exp
 
+  def getWandRepresentationWithArgs(w: sil.MagicWand, args: Seq[sil.Exp]):Exp
+
+  def getWandName(w: sil.MagicWand): String
+
   /**
     * Translates the 'apply' statements to the corresponding Boogie statements
     * the 'statesStackForPackageStmt', 'allStateAssms' and 'insidePackageStmt' parameters are used when being called inside a package statement

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

@@ -69,11 +69,13 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
       case r@sil.Result(_) =>
         translateResult(r)
       case f@sil.FieldAccess(_, _) =>
-        translateLocationAccess(f)
+        translateResourceAccess(f)
       case sil.InhaleExhaleExp(_, _) =>
         sys.error("should not occur here (either, we inhale or exhale this expression, in which case whenInhaling/whenExhaling should be used, or the expression is not allowed to occur.")
       case p@sil.PredicateAccess(_, _) =>
-        translateLocationAccess(p)
+        translateResourceAccess(p)
+      case w: sil.MagicWand =>
+        translateResourceAccess(w)
       case sil.Unfolding(_, exp) =>
         translateExp(exp)
       case sil.Applying(_, exp) => translateExp(exp)
@@ -144,41 +146,32 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
       }
       case sil.ForPerm(variables, accessRes, body) => {
 
-        val variable = variables.head
-
-        if (variables.length != 1) sys.error("Carbon only supports a single quantified variable in forperm, see Carbon issue #243")
-        if (variable.typ != Ref) sys.error("Carbon only supports Ref type in forperm, see Carbon issue #243")
-        accessRes match {
-          case _: MagicWand => sys.error("Carbon does not support magic wands in forperm, see Carbon issue #243")
-          case p: PredicateAccess => if (p.loc(program).formalArgs.length != 1) sys.error("Carbon only supports predicates with a single argument in forperm, see Carbon issue #243")
-          case _ =>
-        }
-
-        val locations = Seq(accessRes.asInstanceOf[LocationAccess].loc(program))
+        val locations = Seq(accessRes)
 
         // alpha renaming, to avoid clashes in context
-        val renamedVar: sil.LocalVarDecl = {
+        val renamedVars: Seq[sil.LocalVarDecl] = variables.map(variable => {
           val v1 = env.makeUniquelyNamed(variable); env.define(v1.localVar); v1
-        }
-        val renaming = (e: sil.Exp) => Expressions.instantiateVariables(e, Seq(variable.localVar), Seq(renamedVar.localVar))
-        // val ts = triggers map (t => Trigger(t.exps map {e => verifier.funcPredModule.toTriggers(translateExp(renaming(e)))} // no triggers yet?
-        val perLocFilter: sil.Location => (Exp, Trigger) = loc => {
-          val locAccess: LocationAccess = loc match {
-            case f: sil.Field => sil.FieldAccess(renamedVar.localVar, f)(loc.pos, loc.info)
-            case p: sil.Predicate => sil.PredicateAccess(Seq(renamedVar.localVar), p)(loc.pos, loc.info, loc.errT)
-          }
-          (hasDirectPerm(locAccess), Trigger(permissionLookup(locAccess)))
+        })
+        val renaming = (e: sil.Exp) => Expressions.instantiateVariables(e, variables.map(_.localVar), renamedVars.map(_.localVar))
+        val perResFilter: sil.ResourceAccess => (Exp, Seq[Trigger]) = resAcc => {
+          val zipped = variables.map(_.localVar) zip renamedVars.map(_.localVar)
+          val replacements = zipped.toMap
+
+          val substitutedResAccess: sil.ResourceAccess = resAcc.replace(replacements)
+          val maskRead = currentPermission(substitutedResAccess)
+          val heapRead = translateResourceAccess(substitutedResAccess)
+          (hasDirectPerm(substitutedResAccess), Seq(Trigger(maskRead), Trigger(heapRead)))
         }
         val filter = locations.foldLeft[(Exp, Seq[Trigger])](BoolLit(false), Seq())((soFar, loc) => soFar match {
           case (exp, triggers) =>
-            perLocFilter(loc) match {
-              case (newExp, newTrigger) => (BinExp(exp, Or, newExp), triggers ++ Seq(newTrigger))
+            perResFilter(loc) match {
+              case (newExp, newTriggers) => (BinExp(exp, Or, newExp), triggers ++ newTriggers)
             }
         })
 
-        val res = Forall(translateLocalVarDecl(renamedVar), filter._2, // no triggers yet :(
+        val res = Forall(renamedVars.map(renamedVar => translateLocalVarDecl(renamedVar)), filter._2, // no triggers yet :(
           BinExp(filter._1, Implies, translateExp(renaming(body))))
-        env.undefine(renamedVar.localVar)
+        renamedVars.foreach(renamedVar => env.undefine(renamedVar.localVar))
         res
       }
       case sil.WildcardPerm() =>
@@ -430,15 +423,7 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
           val res = if (e.isInstanceOf[sil.ForPerm]) {
             val eAsForallRef = Expressions.renameVariables(e, orig_vars.map(_.localVar), bound_vars.map(_.localVar)).asInstanceOf[sil.ForPerm]
 
-            if (eAsForallRef.variables.length != 1) sys.error("Carbon only supports a single quantified variable in forperm, see Carbon issue #243")
-            if (eAsForallRef.variables.head.typ != Ref) sys.error("Carbon only supports Ref type in forperm, see Carbon issue #243")
-            eAsForallRef.resource match {
-              case _: MagicWand => sys.error("Carbon does not support magic wands in forperm, see Carbon issue #243")
-              case p: PredicateAccess => if (p.loc(program).formalArgs.length != 1) sys.error("Carbon only supports predicates with a single argument in forperm, see Carbon issue #243")
-              case _ =>
-            }
-
-            val filter: Exp = hasDirectPerm(eAsForallRef.resource.asInstanceOf[LocationAccess])
+            val filter: Exp = hasDirectPerm(eAsForallRef.resource)
 
             handleQuantifiedLocals(bound_vars, If(filter, translate(eAsForallRef, definednessStateOpt), Nil))
           } else {

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

@@ -532,7 +532,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     }
     assertion match {
       case s@sil.AccessPredicate(la, perm) =>
-        val fragmentBody = translateLocationAccess(renaming(la).asInstanceOf[sil.LocationAccess])
+        val fragmentBody = translateResourceAccess(renaming(la).asInstanceOf[sil.LocationAccess])
         val fragment = if (s.isInstanceOf[PredicateAccessPredicate]) fragmentBody else frameFragment(fragmentBody)
         if (permModule.conservativeIsPositivePerm(perm)) fragment else
         FuncApp(condFrameName, Seq(translatePerm(renaming(perm)),fragment),frameType)
@@ -962,7 +962,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
       val location = acc.loc
       val predicate = verifier.program.findPredicate(location.predicateName)
       val translatedArgs = location.args map (x => translateExpInWand(x))
-      Assume(translateLocationAccess(location) === getPredicateFrame(predicate,translatedArgs)._1)
+      Assume(translateResourceAccess(location) === getPredicateFrame(predicate,translatedArgs)._1)
     }
 
     foldInfo = null
@@ -999,7 +999,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
         val location = acc.loc
         val predicate = verifier.program.findPredicate(location.predicateName)
         val translatedArgs = location.args map translateExp
-        Assume(translateLocationAccess(location) === getPredicateFrame(predicate,translatedArgs)._1)
+        Assume(translateResourceAccess(location) === getPredicateFrame(predicate,translatedArgs)._1)
       } ++
       (if(exhaleUnfoldedPredicate)
           exhaleSingleWithoutDefinedness(acc, error, havocHeap = false, statesStackForPackageStmt = statesStackForPackageStmt, insidePackageStmt = insidePackageStmt)

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

@@ -96,7 +96,7 @@ class DefaultHeapModule(val verifier: Verifier)
   private var PredIdMap:Map[String, BigInt] = Map()
   private var NextPredicateId:BigInt = 0
   private val isWandFieldName = Identifier("IsWandField")
-  private val getPredicateIdName = Identifier("getPredicateId")
+  private val getPredicateOrWandIdName = Identifier("getPredWandId")
   private val sumHeapName = Identifier("SumHeap")
   private val readHeapName = Identifier("readHeap")
   private val updateHeapName = Identifier("updHeap")
@@ -167,7 +167,7 @@ class DefaultHeapModule(val verifier: Verifier)
       Func(isWandFieldName,
         Seq(LocalVarDecl(Identifier("f"), fieldType)),
         Bool) ++
-      Func(getPredicateIdName,
+      Func(getPredicateOrWandIdName,
         Seq(LocalVarDecl(Identifier("f"), fieldType)),
         Int) ++
       {
@@ -413,11 +413,11 @@ class DefaultHeapModule(val verifier: Verifier)
   }
 
   // returns predicate Id
-  override def getPredicateId(f:Exp): Exp = {
-    FuncApp(getPredicateIdName,Seq(f), Int)
+  override def getPredicateOrWandId(f:Exp): Exp = {
+    FuncApp(getPredicateOrWandIdName,Seq(f), Int)
   }
 
-  override def getPredicateId(s:String): BigInt = {
+  override def getPredicateOrWandId(s:String): BigInt = {
     if (!PredIdMap.contains(s)) {
       val predId:BigInt = getNewPredId;
       PredIdMap += (s -> predId)
@@ -447,7 +447,7 @@ class DefaultHeapModule(val verifier: Verifier)
     val pmT = predicateMaskFieldTypeOf(p)
     val varDecls = p.formalArgs map mainModule.translateLocalVarDecl
     val vars = varDecls map (_.l)
-    val predId:BigInt = getPredicateId(p.name)
+    val predId:BigInt = getPredicateOrWandId(p.name)
     val f0 = FuncApp(predicate, vars, t)
     val f1 = predicateMaskField(f0)
     val f2 = FuncApp(pmField, vars, pmT)
@@ -456,7 +456,7 @@ class DefaultHeapModule(val verifier: Verifier)
       Func(pmField, varDecls, pmT) ++
       Axiom(MaybeForall(varDecls, Trigger(f1), f1 === f2)) ++
       Axiom(MaybeForall(varDecls, Trigger(f0), isPredicateField(f0))) ++
-      Axiom(MaybeForall(varDecls, Trigger(f0), getPredicateId(f0) === IntLit(predId))) ++
+      Axiom(MaybeForall(varDecls, Trigger(f0), getPredicateOrWandId(f0) === IntLit(predId))) ++
       Func(predicateTriggerIdentifier(p), Seq(LocalVarDecl(heapName, heapTyp), LocalVarDecl(Identifier("pred"), predicateVersionFieldType())), Bool) ++
       Func(predicateTriggerAnyStateIdentifier(p), Seq(LocalVarDecl(Identifier("pred"), predicateVersionFieldType())), Bool) ++
       {
@@ -537,7 +537,7 @@ class DefaultHeapModule(val verifier: Verifier)
   }
   override def predicateTrigger(extras : Seq[Exp], pred: sil.PredicateAccess, anyState : Boolean = false): Exp = {
     val predicate = verifier.program.findPredicate(pred.predicateName)
-    val location = translateLocation(pred)
+    val location = translateResource(pred)
     if (anyState) predicateTriggerAnyState(predicate, location) else predicateTrigger(extras, predicate, location)
   }
 
@@ -562,10 +562,11 @@ class DefaultHeapModule(val verifier: Verifier)
     }
   }
 
-  def rcvAndFieldExp(f: sil.LocationAccess) : (Exp, Exp) =
+  def rcvAndFieldExp(f: sil.ResourceAccess) : (Exp, Exp) =
     f match {
-      case sil.FieldAccess(rcv, _) => (translateExp(rcv), translateLocation(f))
-      case sil.PredicateAccess(_, _) => (nullLit, translateLocation(f))
+      case sil.FieldAccess(rcv, _) => (translateExp(rcv), translateResource(f))
+      case sil.PredicateAccess(_, _) => (nullLit, translateResource(f))
+      case w: sil.MagicWand => (nullLit, translateResource(f))
     }
 
   override def currentHeapAssignUpdate(f: sil.LocationAccess, newVal: Exp): Stmt = {
@@ -589,10 +590,10 @@ class DefaultHeapModule(val verifier: Verifier)
       FuncApp(if(isPMask) { permModule.pmaskTypeDesugared.storeId } else { updateHeapName }, Seq(heap, rcv, field, newVal), Bool)
   }
 
-  override def translateLocationAccess(f: sil.LocationAccess): Exp = {
-    translateLocationAccess(f, heapExp)
+  override def translateResourceAccess(f: sil.ResourceAccess): Exp = {
+    translateResourceAccess(f, heapExp)
   }
-  private def translateLocationAccess(f: sil.LocationAccess, heap: Exp, isPMask: Boolean = false): Exp = {
+  private def translateResourceAccess(f: sil.ResourceAccess, heap: Exp, isPMask: Boolean = false): Exp = {
     val (rcvExp, fieldExp) = rcvAndFieldExp(f)
     lookup(heap, rcvExp, fieldExp, isPMask)
   }
@@ -602,14 +603,16 @@ class DefaultHeapModule(val verifier: Verifier)
     lookup(heap, rcv, loc)
   }
 
-  override def translateLocation(l: sil.LocationAccess): Exp = {
+  override def translateResource(l: sil.ResourceAccess): Exp = {
     l match {
       case sil.PredicateAccess(args, predName) =>
         val pred = verifier.program.findPredicate(predName)
         val t = predicateMetaTypeOf(pred)
         FuncApp(locationIdentifier(pred), args map translateExp, t)
       case sil.FieldAccess(rcv, field) =>
         Const(locationIdentifier(field))
+      case w: sil.MagicWand =>
+        wandModule.getWandRepresentation(w)
     }
   }
 
@@ -726,7 +729,7 @@ class DefaultHeapModule(val verifier: Verifier)
           MaybeComment("register all known folded permissions guarded by predicate " + loc.predicateName,
             Havoc(newPMask) ++
               Assume(Forall(Seq(obj, field), Seq(Trigger(pm2)), (pm1 ==> pm2))) ++
-                Assume(Forall(vsFresh.map(vFresh => translateLocalVarDecl(vFresh)),Seq(),translatedCond ==> (translateLocationAccess(renamingFieldAccess, newPMask, true) === TrueLit()) ))) ++
+                Assume(Forall(vsFresh.map(vFresh => translateLocalVarDecl(vFresh)),Seq(),translatedCond ==> (translateResourceAccess(renamingFieldAccess, newPMask, true) === TrueLit()) ))) ++
             curHeapAssignUpdatePredWandMask(pmask.maskField, newPMask)
         vsFresh.foreach(vFresh => env.undefine(vFresh.localVar))
         res

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

@@ -111,10 +111,18 @@ DefaultWandModule(val verifier: Verifier) extends WandModule with StmtComponent
   override def preamble = wandToShapes.values.collect({
     case fun@Func(name,args,typ,_) =>
       val vars = args.map(decl => decl.l)
-      val f0 = FuncApp(name,vars,typ)
+      val args2 = args map (
+        v => LocalVarDecl(Identifier(v.name.name + "_2")(v.name.namespace), v.typ))
+      val vars2 = args2 map (_.l)
+      val varsEqual = All((vars zip vars2) map {
+        case (v1, v2) => v1 === v2
+      })
+      val f0 = FuncApp(name, vars, typ)
+      val f0_2 = FuncApp(name, vars2, typ)
       val f1 = FuncApp(heapModule.wandMaskIdentifier(name), vars, heapModule.predicateMaskFieldTypeOfWand(name.name)) // w#sm (wands secondary mask)
       val f2 = FuncApp(heapModule.wandFtIdentifier(name), vars, heapModule.predicateVersionFieldTypeOfWand(name.name)) // w#ft (permission to w#fm is added when at the begining of a package statement)
       val f3 = wandMaskField(f2) // wandMaskField (wandMaskField(w) == w#sm)
+      val wandId = heapModule.getPredicateOrWandId(name.name)
       val typeDecl: Seq[TypeDecl] = heapModule.wandBasicType(name.preferredName) match {
         case named: NamedType => TypeDecl(named)
         case _ => Nil
@@ -127,25 +135,40 @@ DefaultWandModule(val verifier: Verifier) extends WandModule with StmtComponent
         Axiom(MaybeForall(args, Trigger(f2),heapModule.isWandField(f2))) ++
         Axiom(MaybeForall(args, Trigger(f0),heapModule.isPredicateField(f0).not)) ++
         Axiom(MaybeForall(args, Trigger(f2),heapModule.isPredicateField(f2).not)) ++
-        Axiom(MaybeForall(args, Trigger(f3), f1 === f3))
+        Axiom(MaybeForall(args, Trigger(f3), f1 === f3)) ++
+        Axiom(MaybeForall(args, Trigger(f0), heapModule.getPredicateOrWandId(f0) === IntLit(wandId))) ++
+        Axiom(Forall(args ++ args2, Trigger(Seq(f0, f0_2)),
+          (f0 === f0_2) ==> varsEqual))
     }).flatten[Decl].toSeq
 
   /*
    * method returns the boogie predicate which corresponds to the magic wand shape of the given wand
    * if the shape hasn't yet been recorded yet then it will be stored
    */
   def getWandRepresentation(wand: sil.MagicWand):Exp = {
+    //get all the expressions which form the "holes" of the shape,
+    val arguments = wand.subexpressionsToEvaluate(mainModule.verifier.program)
+    val translatedArgs = arguments.map(arg => expModule.translateExp(arg))
 
-    //need to compute shape of wand
-    val ghostFreeWand = wand
+    getWandExpression(wand, translatedArgs)
+  }
 
-    //get all the expressions which form the "holes" of the shape,
-    val arguments = ghostFreeWand.subexpressionsToEvaluate(mainModule.verifier.program)
+  def getWandRepresentationWithArgs(wand: sil.MagicWand, args: Seq[sil.Exp]): Exp = {
+    getWandExpression(wand, args.map(arg => expModule.translateExp(arg)))
+  }
 
-    val shape:WandShape = wandToShapes(wand.structure(mainModule.verifier.program))
+  private def getWandExpression(wand: sil.MagicWand, arguments: Seq[Exp]): Exp = {
+    val shape: WandShape = wandToShapes(wand.structure(mainModule.verifier.program))
+
+    shape match {
+      case Func(name, _, typ, _) => FuncApp(name, arguments, typ)
+    }
+  }
 
+  override def getWandName(w: MagicWand): String = {
+    val shape = wandToShapes(w.structure(mainModule.verifier.program))
     shape match {
-      case Func(name, _, typ,_) => FuncApp(name, arguments.map(arg => expModule.translateExp(arg)), typ)
+      case Func(name, _, _, _) => name.name
     }
   }
 
@@ -559,7 +582,7 @@ private def setupTransferableEntity(e: sil.Exp, permTransfer: Exp):(Transferable
   e match {
     case fa@sil.FieldAccessPredicate(loc, _) =>
       val assignStmt = rcvLocal := expModule.translateExpInWand(loc.rcv)
-      val evalLoc = heapModule.translateLocation(loc)
+      val evalLoc = heapModule.translateResource(loc)
       (TransferableFieldAccessPred(rcvLocal, evalLoc, permTransfer,fa), assignStmt)
 
     case p@sil.PredicateAccessPredicate(loc, _) =>