Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add flag to turn off smart heap inference #1041

Merged
merged 1 commit into from
Jun 21, 2023
Merged

Add flag to turn off smart heap inference #1041

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion src/main/vct/main/stages/Transformation.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
)
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down
6 changes: 6 additions & 0 deletions src/main/vct/options/Options.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
Expand Down Expand Up @@ -354,6 +358,8 @@ case class Options

bipReportFile: Option[PathOrStd] = None,

inferHeapContextIntoFrame: Boolean = true,

// Verify options - hidden
devAbruptExc: Boolean = false,
devCheckSat: Boolean = true,
Expand Down
7 changes: 4 additions & 3 deletions src/rewrite/vct/rewrite/EncodeProofHelpers.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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."

Expand Down Expand Up @@ -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 {
Expand All @@ -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(
Expand Down