From f199b1a8e52cc2aa78d9cf3162aeb31bdf0e7d6a Mon Sep 17 00:00:00 2001 From: Manuel Dublanc <19774382+manud99@users.noreply.github.com> Date: Mon, 20 May 2024 10:05:47 +0200 Subject: [PATCH 1/5] Implement first draft of an inhaling expression. --- src/main/scala/rules/Evaluator.scala | 8 +++++++- src/main/scala/supporters/ExpressionTranslator.scala | 1 + src/main/scala/verifier/DefaultMainVerifier.scala | 3 ++- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 0b999061a..d68a4275d 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -18,7 +18,7 @@ import viper.silicon.state.terms._ import viper.silicon.state.terms.implicits._ import viper.silicon.state.terms.perms.{IsNonNegative, IsPositive} import viper.silicon.state.terms.predef.`?r` -import viper.silicon.utils.toSf +import viper.silicon.utils.{freshSnap, toSf} import viper.silicon.utils.ast.flattenOperator import viper.silicon.verifier.Verifier import viper.silicon.{Map, TriggerSets} @@ -912,6 +912,12 @@ object evaluator extends EvaluationRules { eval(s2, eIn, pve, v2)(QB) }))(join(v.symbolConverter.toSort(eIn.typ), "joined_applying", s.relevantQuantifiedVariables, v))(Q) + case ast.Inhaling(exp, body) => + produce(s, freshSnap, exp, pve, v)((s2, v2) => { + eval(s2, body, pve, v2)((_, tBody, _) => { + Q(s, tBody, v) + })}) + /* Sequences */ case ast.SeqContains(e0, e1) => evalBinOp(s, e1, e0, SeqIn, pve, v)(Q) diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index 914e2911f..ce6dd4470 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -259,6 +259,7 @@ trait ExpressionTranslator { | _: ast.Result | _: ast.Unfolding | _: ast.Applying + | _: ast.Inhaling | _: ast.InhaleExhaleExp | _: ast.PredicateAccess | _: ast.FuncApp diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 61c4e31f5..b48c631d2 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -189,7 +189,8 @@ class DefaultMainVerifier(config: Config, } if (config.printTranslatedProgram()) { - println(program) + val str = program.toString() + println(str) } predSnapGenerator.setup(program) // TODO: Why did Nadja put this here? From afee4a1042127d25181610506c975e895939fa96 Mon Sep 17 00:00:00 2001 From: Manuel Dublanc <19774382+manud99@users.noreply.github.com> Date: Mon, 20 May 2024 10:11:00 +0200 Subject: [PATCH 2/5] Update reference to silver. --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 1b588f0db..d125182ee 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 1b588f0db96acd641a35c9eb1424acda80084561 +Subproject commit d125182ee2ebe23193c3cea319214ef291563325 From ca63db54710d3e69558070ea03bebbf309d1beee Mon Sep 17 00:00:00 2001 From: Manuel Dublanc <19774382+manud99@users.noreply.github.com> Date: Mon, 20 May 2024 10:31:14 +0200 Subject: [PATCH 3/5] Move tests. --- silver | 2 +- src/test/scala/SiliconTests.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/silver b/silver index d125182ee..eb72cbaa1 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit d125182ee2ebe23193c3cea319214ef291563325 +Subproject commit eb72cbaa1ca393762bc43b91f528e497f51caf9c diff --git a/src/test/scala/SiliconTests.scala b/src/test/scala/SiliconTests.scala index 1a8669c43..a25f92697 100644 --- a/src/test/scala/SiliconTests.scala +++ b/src/test/scala/SiliconTests.scala @@ -20,7 +20,7 @@ class SiliconTests extends SilSuite { private val silTestDirectories = Seq("all", "quantifiedpermissions", "quantifiedpredicates", "quantifiedcombinations", - "wands", "termination", "refute", + "wands", "termination", "refute", "inhaling", "examples") val testDirectories: Seq[String] = siliconTestDirectories ++ silTestDirectories From d01deb62561a1fddffae6636b3acb3b0264c1587 Mon Sep 17 00:00:00 2001 From: Manuel Dublanc <19774382+manud99@users.noreply.github.com> Date: Mon, 20 May 2024 14:31:23 +0200 Subject: [PATCH 4/5] Add more tests, execute inhaling body in its own scope, and write documentation for executionFlowController. --- silver | 2 +- src/main/scala/rules/Evaluator.scala | 14 ++++++--- .../scala/rules/ExecutionFlowController.scala | 31 +++++++++++++++++++ .../scala/verifier/DefaultMainVerifier.scala | 3 +- 4 files changed, 42 insertions(+), 8 deletions(-) diff --git a/silver b/silver index eb72cbaa1..8ccaedef4 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit eb72cbaa1ca393762bc43b91f528e497f51caf9c +Subproject commit 8ccaedef4b662001b4295e87b55dbd774a1f5f7a diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index d68a4275d..27094b546 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -912,11 +912,15 @@ object evaluator extends EvaluationRules { eval(s2, eIn, pve, v2)(QB) }))(join(v.symbolConverter.toSort(eIn.typ), "joined_applying", s.relevantQuantifiedVariables, v))(Q) - case ast.Inhaling(exp, body) => - produce(s, freshSnap, exp, pve, v)((s2, v2) => { - eval(s2, body, pve, v2)((_, tBody, _) => { - Q(s, tBody, v) - })}) + case ast.Inhaling(a, body) => + executionFlowController.locallyWithResult[Term](s, v)((s1, v1, QL) => { + produce(s1, freshSnap, a, pve, v1)((s2, v2) => { + v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterInhale) + eval(s2, body, pve, v2)((_, tBody, _) => { + QL(tBody) + }) + }) + })(t => Q(s, t, v)) /* Sequences */ diff --git a/src/main/scala/rules/ExecutionFlowController.scala b/src/main/scala/rules/ExecutionFlowController.scala index 8cc287d0f..2de809511 100644 --- a/src/main/scala/rules/ExecutionFlowController.scala +++ b/src/main/scala/rules/ExecutionFlowController.scala @@ -49,6 +49,29 @@ trait ExecutionFlowRules extends SymbolicExecutionRules { } object executionFlowController extends ExecutionFlowRules { + /** + * Execute a local block within its own scope. The continuation Q is invoked + * with the result of the local block if the local block succeeded. Changes + * to the state and verifier are not propagated outside of the local block. + * + * Usage example: + * {{{ + * locallyWithResult[Term](s, v)((s1, v1, QL) => { + * eval(s2, exp, pve, v2)((_, tExp, _) => { + * QL(tExp) + * }) + * })(t => Q(s, t, v)) + * }}} + * + * @param s State to be used for the local block. + * @param v Verifier to be used for the local block. + * @param block Local block to be executed. It accepts the current state, verifier, and a + * continuation QL that is invoked with the result of the block. + * @param Q Continuation that is invoked with the result of the local block if the local block + * succeeded. + * @tparam R Type of the result of the local block. + * @return Verification result after executing the local block and the continuation Q. + */ def locallyWithResult[R](s: State, v: Verifier) (block: (State, Verifier, R => VerificationResult) => VerificationResult) (Q: R => VerificationResult) @@ -92,6 +115,14 @@ object executionFlowController extends ExecutionFlowRules { } } + /** + * Execute a local block that is executed within its own scope. + * + * @param s State to be used for the local block. + * @param v Verifier to be used for the local block. + * @param block Local block to be executed. It accepts a state and a verifier and returns a verification result. + * @return Verification result of executing the local block. + */ def locally(s: State, v: Verifier) (block: (State, Verifier) => VerificationResult) : VerificationResult = diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index b48c631d2..61c4e31f5 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -189,8 +189,7 @@ class DefaultMainVerifier(config: Config, } if (config.printTranslatedProgram()) { - val str = program.toString() - println(str) + println(program) } predSnapGenerator.setup(program) // TODO: Why did Nadja put this here? From 5fa82f9663a36210ef722bd462b9f21ab7c404ee Mon Sep 17 00:00:00 2001 From: Manuel Dublanc <19774382+manud99@users.noreply.github.com> Date: Thu, 30 May 2024 10:52:31 +0200 Subject: [PATCH 5/5] Fix joining of execution paths after inhaling. --- silver | 2 +- src/main/scala/rules/Evaluator.scala | 22 ++++++++++++++++------ src/main/scala/rules/Joiner.scala | 19 +++++++++++++++++++ 3 files changed, 36 insertions(+), 7 deletions(-) diff --git a/silver b/silver index 8ccaedef4..b564483e6 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 8ccaedef4b662001b4295e87b55dbd774a1f5f7a +Subproject commit b564483e653528d4554e4e82bef9deae3032f4cd diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 27094b546..02928b923 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -910,17 +910,16 @@ object evaluator extends EvaluationRules { joiner.join[Term, Term](s, v)((s1, v1, QB) => magicWandSupporter.applyWand(s1, wand, pve, v1)((s2, v2) => { eval(s2, eIn, pve, v2)(QB) - }))(join(v.symbolConverter.toSort(eIn.typ), "joined_applying", s.relevantQuantifiedVariables, v))(Q) + }) + )(join(v.symbolConverter.toSort(eIn.typ), "joined_applying", s.relevantQuantifiedVariables, v))(Q) case ast.Inhaling(a, body) => - executionFlowController.locallyWithResult[Term](s, v)((s1, v1, QL) => { + joiner.join[Term, Term](s, v)((s1, v1, QB) => produce(s1, freshSnap, a, pve, v1)((s2, v2) => { v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterInhale) - eval(s2, body, pve, v2)((_, tBody, _) => { - QL(tBody) - }) + eval(s2, body, pve, v2)(QB) }) - })(t => Q(s, t, v)) + )(join(v.symbolConverter.toSort(body.typ), "joined_inhaling", s.relevantQuantifiedVariables, v))(Q) /* Sequences */ @@ -1475,6 +1474,17 @@ object evaluator extends EvaluationRules { } } + /** + * Method that takes a list of [[viper.silicon.rules.JoinDataEntry]] from [[viper.silicon.rules.joiner.join]] + * and joins them using a symbolic join function with the given name and arguments. + * + * @param joinSort The sort of the result of the join function. + * @param joinFunctionName The name of the join function. + * @param joinFunctionArgs The arguments of the join function. + * @param v The current verifier. + * @param entries The list of JoinDataEntry to join. + * @return A tuple containing the new state and the term resulting from the join. + */ private def join(joinSort: Sort, joinFunctionName: String, joinFunctionArgs: Seq[Term], diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala index 9c25fc108..5ccf8afc8 100644 --- a/src/main/scala/rules/Joiner.scala +++ b/src/main/scala/rules/Joiner.scala @@ -36,6 +36,25 @@ trait JoiningRules extends SymbolicExecutionRules { } object joiner extends JoiningRules { + + /** + * This method is a higher-order function that handles the joining of different execution + * paths in a symbolic execution engine. It records the data collected from each execution path + * and merges it into a single data structure. The final data structure is then passed to a + * function that performs some final verification step. + * + * @param s The current state of the symbolic execution. + * @param v The current verifier. + * @param resetState A flag indicating whether the state should be reset after each execution path. + * @param block A function that executes a block of code symbolically and collects data + * from each feasible execution path. + * @param merge A function that merges the data collected from each feasible execution path. + * @param Q A function that is called after all execution paths have been joined and the data has been merged. + * It is expected to perform some final verification step. + * @tparam D The generic type parameter for the data collected from each execution path. + * @tparam JD The generic type parameter for the merged data. + * @return The final result of the join method, which is the result of the Q function. + */ def join[D, JD](s: State, v: Verifier, resetState: Boolean = true) (block: (State, Verifier, (State, D, Verifier) => VerificationResult) => VerificationResult) (merge: Seq[JoinDataEntry[D]] => (State, JD))