From e73492542404046ab89fb6be00a25a893cf5515a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 10 Nov 2023 16:04:57 +0100 Subject: [PATCH] Moving check of out-edge condition well-definedness for loop head blocks until after statements are executed --- src/main/scala/rules/Executor.scala | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 6090c1e1a..0f6904763 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -253,13 +253,8 @@ object executor extends ExecutionRules { phase1data = phase1data :+ (s1, v1.decider.pcs.after(mark), v1.decider.freshFunctions /* [BRANCH-PARALLELISATION] */) - v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions") - edgeConditions.foldLeft(Success(): VerificationResult) { - case (result, _) if !result.continueVerification => result - case (intermediateResult, eCond) => - intermediateResult combine executionFlowController.locally(s1, v1)((s2, v2) => { - eval(s2, eCond, WhileFailed(eCond), v2)((_, _, _) => - Success())})}})}) + Success() + })}) combine executionFlowController.locally(s, v)((s0, v0) => { v0.decider.prover.comment("Loop head block: Establish invariant") consumes(s0, invs, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => { @@ -276,8 +271,19 @@ object executor extends ExecutionRules { Success() else { execs(s3, stmts, v2)((s4, v3) => { + val edgeCondWelldefinedness = { + v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions") + edgeConditions.foldLeft(Success(): VerificationResult) { + case (result, _) if !result.continueVerification => result + case (intermediateResult, eCond) => + intermediateResult combine executionFlowController.locally(s4, v3)((s5, v4) => { + eval(s5, eCond, WhileFailed(eCond), v4)((_, _, _) => + Success()) + }) + } + } v3.decider.prover.comment("Loop head block: Follow loop-internal edges") - follows(s4, sortedEdges, WhileFailed, v3, joinPoint)(Q)})}})}})})) + edgeCondWelldefinedness combine follows(s4, sortedEdges, WhileFailed, v3, joinPoint)(Q)})}})}})})) case _ => /* We've reached a loop head block via an edge other than an in-edge: a normal edge or