Merge

src/main/resources/magic_wand_snap_functions_declarations.smt2

@@ -0,0 +1 @@
+(declare-fun MWSF_apply ($MWSF $Snap) $Snap)

src/main/scala/Utils.scala

@@ -222,6 +222,7 @@ package object utils {
     case class ViperEmbedding(embeddedSort: Sort) extends silver.ast.ExtensionType {
       def substitute(typVarsMap: Predef.Map[silver.ast.TypeVar, silver.ast.Type]): silver.ast.Type = this
       def isConcrete: Boolean = true
+      override def toString: String = s"ViperEmbedding(sorts.$embeddedSort)"
     }
   }
 

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -61,6 +61,8 @@ class TermToSMTLib2Converter
 
     case sorts.FieldPermFunction() => text("$FPM")
     case sorts.PredicatePermFunction() => text("$PPM")
+
+    case sorts.MagicWandSnapFunction => text("$MWSF")
   }
 
   def convert(d: Decl): String = {
@@ -264,7 +266,7 @@ class TermToSMTLib2Converter
 
     case Lookup(field, fvf, at) => //fvf.sort match {
 //      case _: sorts.PartialFieldValueFunction =>
-        parens(text("$FVF.lookup_") <> field <+> render(fvf) <+> render(at))
+      parens(text("$FVF.lookup_") <> field <+> render(fvf) <+> render(at))
 //      case _: sorts.TotalFieldValueFunction =>
 //        render(Apply(fvf, Seq(at)))
 //        parens("$FVF.lookup_" <> field <+> render(fvf) <+> render(at))
@@ -314,6 +316,9 @@ class TermToSMTLib2Converter
       val docBindings = ssep((bindings.toSeq map (p => parens(render(p._1) <+> render(p._2)))).to(collection.immutable.Seq), space)
       parens(text("let") <+> parens(docBindings) <+> render(body))
 
+    case MagicWandSnapshot(mwsf) => render(mwsf)
+    case MWSFLookup(mwsf, snap) => renderApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
+
     case _: MagicWandChunkTerm
        | _: Quantification =>
       sys.error(s"Unexpected term $term cannot be translated to SMTLib code")

src/main/scala/decider/TermToZ3APIConverter.scala

@@ -445,6 +445,8 @@ class TermToZ3APIConverter
       case Let(bindings, body) =>
         convert(body.replace(bindings))
 
+      case MWSFLookup(mwsf, snap) => createApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
+
       case _: MagicWandChunkTerm
          | _: Quantification =>
         sys.error(s"Unexpected term $term cannot be translated to SMTLib code")

src/main/scala/extensions/ConditionalPermissionRewriter.scala

@@ -30,18 +30,20 @@ class ConditionalPermissionRewriter {
     case (i@Implies(cond, acc: AccessPredicate), cc) =>
       // Found an implication b ==> acc(...)
       // Transformation causes issues if the permission involve a wildcard, so we avoid that case.
-      val res = if (!acc.perm.contains[WildcardPerm])
+      // Also, we cannot push perm and forperm expressions further in, since their value may be different at different
+      // places in the same assertion.
+      val res = if (!acc.perm.contains[WildcardPerm] && !Expressions.containsPermissionIntrospection(cond))
         (conditionalize(acc, cc.c &*& cond), cc) // Won't recurse into acc's children (see recurseFunc below)
       else
         (Implies(And(cc.c.exp, cond)(), acc)(i.pos, i.info, i.errT), cc)
       alreadySeen.add(res._1)
       res
 
     case (i@Implies(cond, l: Let), cc) if !l.isPure =>
-      if (Expressions.proofObligations(l.exp)(p).isEmpty) {
+      if (Expressions.proofObligations(l.exp)(p).isEmpty && !Expressions.containsPermissionIntrospection(cond)) {
         (l, cc.updateContext(cc.c &*& cond))
       } else {
-        // bound expression might only be well-defined under context conditiond;
+        // bound expression might only be well-defined under context condition;
         // thus, don't push conditions further in.
         val res = (Implies(And(cc.c.exp, cond)(), l)(i.pos, i.info, i.errT), cc)
         alreadySeen.add(res._1)
@@ -50,7 +52,11 @@ class ConditionalPermissionRewriter {
 
     case (impl: Implies, cc) if !impl.right.isPure =>
       // Entering an implication b ==> A, where A is not pure, i.e. contains an accessibility accessibility
-      (impl.right, cc.updateContext(cc.c &*& impl.left))
+      if (Expressions.containsPermissionIntrospection(impl.left)) {
+        (Implies(And(cc.c.exp, impl.left)(), impl.right)(impl.pos, impl.info, impl.errT), cc)
+      } else {
+        (impl.right, cc.updateContext(cc.c &*& impl.left))
+      }
 
     case (acc: AccessPredicate, cc) if cc.c.optExp.nonEmpty =>
       // Found an accessibility predicate nested under some conditionals
@@ -86,7 +92,8 @@ class ConditionalPermissionRewriter {
   // Rewrite impure ternary expressions to a conjuction of implications in order to be able to use the implication
   // rewriter above.
   private val ternaryRewriter = ViperStrategy.Slim{
-    case ce@CondExp(cond, tExp, fExp) if !tExp.isPure || !fExp.isPure =>
+    case ce@CondExp(cond, tExp, fExp)
+        if (!tExp.isPure || !fExp.isPure) && !Expressions.containsPermissionIntrospection(cond) =>
       And(Implies(cond, tExp)(ce.pos, ce.info, ce.errT),
         Implies(Not(cond)(cond.pos, cond.info, cond.errT), fExp)(ce.pos, ce.info, ce.errT))(ce.pos, ce.info, ce.errT)
   }

src/main/scala/rules/Evaluator.scala

@@ -184,7 +184,7 @@ object evaluator extends EvaluationRules {
          *       term returned by eval, mark as constrainable on client-side (e.g. in consumer).
          */
         val s1 =
-          s.copy(functionRecorder = s.functionRecorder.recordArp(tVar, tConstraints))
+          s.copy(functionRecorder = s.functionRecorder.recordConstrainedVar(tVar, tConstraints))
            .setConstrainable(Seq(tVar), true)
         Q(s1, tVar, v)
 

src/main/scala/rules/Executor.scala

@@ -129,8 +129,12 @@ object executor extends ExecutionRules {
                      (Q: (State, Verifier) => VerificationResult)
                      : VerificationResult = {
 
-    // Find join point if it exists.
-    val jp: Option[SilverBlock] = edges.headOption.flatMap(edge => s.methodCfg.joinPoints.get(edge.source))
+    // If joining branches is enabled, find join point if it exists.
+    val jp: Option[SilverBlock] = if (s.moreJoins.id >= JoinMode.All.id) {
+      edges.headOption.flatMap(edge => s.methodCfg.joinPoints.get(edge.source))
+    } else {
+      None
+    }
 
     (edges, jp) match {
       case (Seq(), _) => Q(s, v)

src/main/scala/rules/HavocSupporter.scala

@@ -182,10 +182,17 @@ object havocSupporter extends SymbolicExecutionRules {
     val id = ChunkIdentifier(resource, s.program)
     val (relevantChunks, otherChunks) = chunkSupporter.splitHeap[NonQuantifiedChunk](s.h, id)
 
-    val newChunks = relevantChunks.map { ch =>
-      val havockedSnap = freshSnap(ch.snap.sort, v)
-      val cond = replacementCond(lhs, ch.args, condInfo)
-      ch.withSnap(Ite(cond, havockedSnap, ch.snap))
+    val newChunks = relevantChunks.map {
+      case ch: MagicWandChunk =>
+        val havockedSnap = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction)
+        val cond = replacementCond(lhs, ch.args, condInfo)
+        val magicWandSnapshot = MagicWandSnapshot(Ite(cond, havockedSnap, ch.snap.mwsf))
+        ch.withSnap(magicWandSnapshot)
+
+      case ch =>
+        val havockedSnap = freshSnap(ch.snap.sort, v)
+        val cond = replacementCond(lhs, ch.args, condInfo)
+        ch.withSnap(Ite(cond, havockedSnap, ch.snap))
     }
     otherChunks ++ newChunks
   }