Merge pull request #1041 from utwente-fmt/issue1040

Add flag to turn off smart heap inference

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

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,

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(