Adjusting no of errors reported in branch parallelization code, sligh…

…tly better parameter naming
viperproject · Aug 24, 2023 · ea2173c · ea2173c
1 parent d794d4a
commit ea2173c
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 3 deletions.
diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
@@ -379,8 +379,8 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     def freshFunctions: Set[FunctionDecl] = _declaredFreshFunctions
     def freshMacros: Vector[MacroDecl] = _declaredFreshMacros
 
-    def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toStack: Boolean): Unit = {
-      if (!toStack) {
+    def declareAndRecordAsFreshFunctions(functions: Set[FunctionDecl], toSymbolStack: Boolean): Unit = {
+      if (!toSymbolStack) {
         functions foreach prover.declare
 
         _declaredFreshFunctions = _declaredFreshFunctions ++ functions

diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala
@@ -91,6 +91,7 @@ object brancher extends BranchingRules {
     var functionsOfElseBranchDecider: Set[FunctionDecl] = null
     var macrosOfElseBranchDecider: Seq[MacroDecl] = null
     var pcsForElseBranch: PathConditionStack = null
+    var noOfErrors = 0
 
     val elseBranchVerificationTask: Verifier => VerificationResult =
       if (executeElseBranch) {
@@ -106,6 +107,7 @@ object brancher extends BranchingRules {
           functionsOfCurrentDecider = v.decider.freshFunctions
           macrosOfCurrentDecider = v.decider.freshMacros
           pcsForElseBranch = v.decider.pcs.duplicate()
+          noOfErrors = v.errorsReportedSoFar.get()
         }
 
         (v0: Verifier) => {
@@ -129,6 +131,7 @@ object brancher extends BranchingRules {
 
             v0.decider.prover.comment(s"Taking path conditions from source verifier ${v.uniqueId}")
             v0.decider.setPcs(pcsForElseBranch)
+            v0.errorsReportedSoFar.set(noOfErrors)
           }
           elseBranchVerifier = v0.uniqueId
 
@@ -193,6 +196,7 @@ object brancher extends BranchingRules {
       try {
         if (parallelizeElseBranch) {
           val pcsAfterThenBranch = v.decider.pcs.duplicate()
+          val noOfErrorsAfterThenBranch = v.errorsReportedSoFar.get()
 
           val pcsBefore = v.decider.pcs
 
@@ -202,6 +206,7 @@ object brancher extends BranchingRules {
             // we have done other work during the join, need to reset
             v.decider.prover.comment(s"Resetting path conditions after interruption")
             v.decider.setPcs(pcsAfterThenBranch)
+            v.errorsReportedSoFar.set(noOfErrorsAfterThenBranch)
             v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
           }
         }else{

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
@@ -260,7 +260,7 @@ object executor extends ExecutionRules {
                       intermediateResult combine executionFlowController.locally(s1, v1)((s2, v2) => {
                         eval(s2, eCond, WhileFailed(eCond), v2)((_, _, _) =>
                           Success())})}})})
-            && executionFlowController.locally(s, v)((s0, v0) => {
+            combine executionFlowController.locally(s, v)((s0, v0) => {
                 v0.decider.prover.comment("Loop head block: Establish invariant")
                 consumes(s0, invs, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => {
                   v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)")