From ee92fc62fe4ec225e306c35ffb6f76758e7367d3 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Wed, 21 Jun 2023 12:58:22 +0200
Subject: [PATCH] Add flag to turn off smart heap inference

---
 src/main/vct/main/stages/Transformation.scala    | 4 +++-
 src/main/vct/options/Options.scala               | 6 ++++++
 src/rewrite/vct/rewrite/EncodeProofHelpers.scala | 7 ++++---
 3 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala
index 410a01865c..0561ff4ea1 100644
--- a/src/main/vct/main/stages/Transformation.scala
+++ b/src/main/vct/main/stages/Transformation.scala
@@ -59,6 +59,7 @@ object Transformation {
           simplifyBeforeRelations = options.simplifyPaths.map(simplifierFor(_, options)),
           simplifyAfterRelations = options.simplifyPathsAfterRelations.map(simplifierFor(_, options)),
           checkSat = options.devCheckSat,
+          inferHeapContextIntoFrame = options.inferHeapContextIntoFrame,
           bipResults = bipResults,
           splitVerificationByProcedure = options.devSplitVerificationByProcedure,
         )
@@ -162,6 +163,7 @@ case class SilverTransformation
   override val onAfterPassKey: Seq[(String, Verification[_ <: Generation] => Unit)] = Nil,
   simplifyBeforeRelations: Seq[RewriterBuilder] = Options().simplifyPaths.map(Transformation.simplifierFor(_, Options())),
   simplifyAfterRelations: Seq[RewriterBuilder] = Options().simplifyPathsAfterRelations.map(Transformation.simplifierFor(_, Options())),
+  inferHeapContextIntoFrame: Boolean = true,
   bipResults: BIP.VerificationResults,
   checkSat: Boolean = true,
   splitVerificationByProcedure: Boolean = false,
@@ -225,7 +227,7 @@ case class SilverTransformation
     UntupledQuantifiers,
 
     // Encode proof helpers
-    EncodeProofHelpers,
+    EncodeProofHelpers.withArg(inferHeapContextIntoFrame),
 
     // Make final fields constant functions. Explicitly before ResolveExpressionSideEffects, because that pass will
     // flatten out functions in the rhs of assignments, making it harder to detect final field assignments where the
diff --git a/src/main/vct/options/Options.scala b/src/main/vct/options/Options.scala
index c196af97bb..5f512df5ec 100644
--- a/src/main/vct/options/Options.scala
+++ b/src/main/vct/options/Options.scala
@@ -134,6 +134,10 @@ case object Options {
         .action((p, c) => c.copy(bipReportFile = Some(p)))
         .text("Write JavaBIP verification report to file, or standard out if \"-\" is used"),
 
+      opt[Unit]("no-infer-heap-context-into-frame")
+        .action((_, c) => c.copy(inferHeapContextIntoFrame = false))
+        .text("Disables smart inference of contextual heap into frame statements using `forperm`"),
+
       opt[Unit]("dev-abrupt-exc").maybeHidden()
         .action((_, c) => c.copy(devAbruptExc = true))
         .text("Encode all abrupt control flow using exception, even when not necessary"),
@@ -354,6 +358,8 @@ case class Options
 
   bipReportFile: Option[PathOrStd] = None,
 
+  inferHeapContextIntoFrame: Boolean = true,
+
   // Verify options - hidden
   devAbruptExc: Boolean = false,
   devCheckSat: Boolean = true,
diff --git a/src/rewrite/vct/rewrite/EncodeProofHelpers.scala b/src/rewrite/vct/rewrite/EncodeProofHelpers.scala
index 90b7409b6f..5ff2991999 100644
--- a/src/rewrite/vct/rewrite/EncodeProofHelpers.scala
+++ b/src/rewrite/vct/rewrite/EncodeProofHelpers.scala
@@ -5,7 +5,7 @@ import vct.col.origin._
 import vct.col.ref.Ref
 import vct.col.util.AstBuildHelpers._
 
-case object EncodeProofHelpers extends RewriterBuilder {
+case object EncodeProofHelpers extends RewriterBuilderArg[Boolean] {
   override def key: String = "proofHelpers"
   override def desc: String = "Encode statements framed with FramedProof, and indeterminate integers."
 
@@ -46,7 +46,7 @@ case object EncodeProofHelpers extends RewriterBuilder {
   }
 }
 
-case class EncodeProofHelpers[Pre <: Generation]() extends Rewriter[Pre] {
+case class EncodeProofHelpers[Pre <: Generation](inferHeapContextIntoFrame: Boolean = true) extends Rewriter[Pre] {
   import vct.col.rewrite.EncodeProofHelpers._
 
   override def dispatch(stat: Statement[Pre]): Statement[Post] = stat match {
@@ -57,7 +57,8 @@ case class EncodeProofHelpers[Pre <: Generation]() extends Rewriter[Pre] {
       val locValue = new Variable[Post](TAny())(BeforeVar("x"))
       val allLocationsSame =
         ForPermWithValue(locValue, locValue.get === Old(locValue.get, Some(beforeLabel.ref))(PanicBlame("loop body reached after label before it")))
-      val allLocationsSameOnInhale = PolarityDependent(allLocationsSame, tt)
+      val allLocationsSameOnInhale =
+        if(inferHeapContextIntoFrame) PolarityDependent(allLocationsSame, tt) else tt[Post]
 
       val once = new Variable[Post](TBool())(Once)
       val loop = Loop(