From 0659fcaa41ae03302fee2e94a453f029ae85e75e Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 15 Feb 2024 23:09:22 +0100 Subject: [PATCH 1/3] Avoiding folds in the encoding of unfolding expressions --- .../termination/transformation/ExpTransformer.scala | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala index c771f084f..ce7621c4b 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala @@ -58,10 +58,12 @@ trait ExpTransformer extends ProgramManager with ErrorReporter { val permCheck = transformExp(acc.perm, c, false) val unfoldBody = transformExp(unfBody, c, inhaleExp) // only unfold and fold if body contains something - val (unfold, fold) = (Unfold(acc)(), Fold(acc)()) - - val stmts = Seq(permCheck, unfold, unfoldBody, fold) - Seqn(stmts, Nil)() + val unfold = Unfold(acc)() + val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT) + val assumeFalse = Inhale(FalseLit()())() + val thenBranch = Seqn(Seq(permCheck, unfold, unfoldBody, assumeFalse), Nil)() + val elseBranch = if (inhaleExp) Seqn(Seq(Inhale(e)(e.pos, e.info)), Nil)() else EmptyStmt + If(nonDetVarDecl.localVar, thenBranch, elseBranch)() case Applying(wand, body) => // note that this case is untested -- it's not possible to write a function with an `applying` expression val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT) From b6a43e2a8ff5c319fc06c7e29c1b589d8900911c Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 15 Feb 2024 23:17:05 +0100 Subject: [PATCH 2/3] Removed outdated comment --- .../standard/termination/transformation/ExpTransformer.scala | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala index ce7621c4b..a5580641f 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala @@ -57,7 +57,6 @@ trait ExpTransformer extends ProgramManager with ErrorReporter { case Unfolding(acc, unfBody) => val permCheck = transformExp(acc.perm, c, false) val unfoldBody = transformExp(unfBody, c, inhaleExp) - // only unfold and fold if body contains something val unfold = Unfold(acc)() val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT) val assumeFalse = Inhale(FalseLit()())() From d3d1efa62b156f06e1e088f8eb0b0adc977382b4 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 16 Feb 2024 00:41:57 +0100 Subject: [PATCH 3/3] Fixed missing variable declaration --- .../standard/termination/transformation/ExpTransformer.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala index a5580641f..c9a486303 100644 --- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala +++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala @@ -62,7 +62,7 @@ trait ExpTransformer extends ProgramManager with ErrorReporter { val assumeFalse = Inhale(FalseLit()())() val thenBranch = Seqn(Seq(permCheck, unfold, unfoldBody, assumeFalse), Nil)() val elseBranch = if (inhaleExp) Seqn(Seq(Inhale(e)(e.pos, e.info)), Nil)() else EmptyStmt - If(nonDetVarDecl.localVar, thenBranch, elseBranch)() + Seqn(Seq(If(nonDetVarDecl.localVar, thenBranch, elseBranch)()), Seq(nonDetVarDecl))() case Applying(wand, body) => // note that this case is untested -- it's not possible to write a function with an `applying` expression val nonDetVarDecl = LocalVarDecl(uniqueName("b"), Bool)(e.pos, e.info, e.errT)