From 175e0c38899911798415c7f7e8b0bcf2407e30d1 Mon Sep 17 00:00:00 2001 From: trk Date: Mon, 4 Mar 2024 15:06:21 +0100 Subject: [PATCH 01/10] use forked silver --- .gitmodules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitmodules b/.gitmodules index 57fc76362..f68200d4c 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,3 @@ [submodule "silver"] path = silver - url = https://github.com/viperproject/silver.git + url = https://github.com/trktby/silver.git From ecbcb0148f2e9edaf14ef9cbc5cc064d5acdbbf3 Mon Sep 17 00:00:00 2001 From: trk Date: Fri, 15 Mar 2024 18:39:38 +0100 Subject: [PATCH 02/10] Send BlockReached/ProcessedMessage Only labeled blocks are reported. BlockProcessedMessages are currently sent when the entire subtree rooted in the respective block has finished executing. --- src/main/scala/rules/Executor.scala | 31 ++++++++++++++++++++++++++--- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index d07c1e5fd..5e085c729 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -15,6 +15,7 @@ import viper.silver.cfg.silver.SilverCfg import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge} import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError} import viper.silver.verifier.errors._ +import viper.silver.reporter.{BlockProcessedMessage, BlockReachedMessage} import viper.silver.verifier.reasons._ import viper.silver.{ast, cfg} import viper.silicon.decider.RecordedPathConditions @@ -211,7 +212,22 @@ object executor extends ExecutionRules { (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - block match { + var blockLabel = "None" + block.elements + .iterator + .takeWhile(_ => blockLabel == "None") + .foreach( element => + element match { + case Left(stmt) => stmt match { + case ast.Label(name, _) => + blockLabel = name + case _ => + } + case Right(_) => + } + ) + + val executed = block match { case cfg.StatementBlock(stmt) => execs(s, stmt, v)((s1, v1) => follows(s1, magicWandSupporter.getOutEdges(s1, block), IfFailed, v1, joinPoint)(Q)) @@ -306,16 +322,24 @@ object executor extends ExecutionRules { Success()) } } + /* TODO: coarse. might want more intermedeate results. this waits until all + * following blocks have resolved. + * maybe move to `exec(State, ast.Stmt, Verifier)` or `execs` function + * in the else. + */ + if(blockLabel != "None") + v.reporter.report(BlockProcessedMessage(blockLabel, executed.toString())) + executed } - def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier) + def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier) (Q: (State, Verifier) => VerificationResult) : VerificationResult = if (stmts.nonEmpty) exec(s, stmts.head, v)((s1, v1) => execs(s1, stmts.tail, v1)(Q)) - else + else Q(s, v) def exec(s: State, stmt: ast.Stmt, v: Verifier) @@ -353,6 +377,7 @@ object executor extends ExecutionRules { case ast.Label(name, _) => val s1 = s.copy(oldHeaps = s.oldHeaps + (name -> magicWandSupporter.getEvalHeap(s))) + v.reporter.report(BlockReachedMessage(name)) Q(s1, v) case ast.LocalVarDeclStmt(decl) => From 33e41a693f9b86af94f3e1d69c9e1fd5c8af21dd Mon Sep 17 00:00:00 2001 From: trk Date: Tue, 19 Mar 2024 14:27:59 +0100 Subject: [PATCH 03/10] Add parallel branch execution handling Use a path id and method names to communicate messages with execution paths. --- silver | 2 +- src/main/scala/rules/Executor.scala | 75 ++++++++++++++++++----------- 2 files changed, 49 insertions(+), 28 deletions(-) diff --git a/silver b/silver index 0410211aa..af9b2f799 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 0410211aa49e7ab338d008e7308e7bb872a23260 +Subproject commit af9b2f79980131cd353d166f388c635a7da707b7 diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 5e085c729..5cdf76203 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -29,6 +29,7 @@ import viper.silicon.utils.ast.{BigAnd, extractPTypeFromExp, simplifyVariableNam import viper.silicon.utils.freshSnap import viper.silicon.verifier.Verifier import viper.silver.cfg.{ConditionalEdge, StatementBlock} +import java.util.concurrent.atomic.AtomicInteger trait ExecutionRules extends SymbolicExecutionRules { def exec(s: State, @@ -50,8 +51,13 @@ object executor extends ExecutionRules { import consumer._ import evaluator._ import producer._ + private val pathIdGenerator = new AtomicInteger(0) - private def follow(s: State, edge: SilverEdge, v: Verifier, joinPoint: Option[SilverBlock]) + def nextPathId(): Int = { + pathIdGenerator.incrementAndGet() + } + + private def follow(s: State, edge: SilverEdge, v: Verifier, joinPoint: Option[SilverBlock], pathId: Int) (Q: (State, Verifier) => VerificationResult) : VerificationResult = { @@ -73,7 +79,7 @@ object executor extends ExecutionRules { */ brancher.branch(s2.copy(parallelizeBranches = false), tCond, (ce.condition, condNew), v1)( (s3, v3) => - exec(s3.copy(parallelizeBranches = s2.parallelizeBranches), ce.target, ce.kind, v3, joinPoint)((s4, v4) => { + exec(s3.copy(parallelizeBranches = s2.parallelizeBranches), ce.target, ce.kind, v3, joinPoint, pathId)((s4, v4) => { v4.symbExLog.closeScope(sepIdentifier) Q(s4, v4) }), @@ -84,7 +90,7 @@ object executor extends ExecutionRules { case ue: cfg.UnconditionalEdge[ast.Stmt, ast.Exp] => val s1 = handleOutEdge(s, edge, v) - exec(s1, ue.target, ue.kind, v, joinPoint)(Q) + exec(s1, ue.target, ue.kind, v, joinPoint, pathId)(Q) } } } @@ -106,7 +112,8 @@ object executor extends ExecutionRules { edges: Seq[SilverEdge], @unused pvef: ast.Exp => PartialVerificationError, v: Verifier, - joinPoint: Option[SilverBlock]) + joinPoint: Option[SilverBlock], + pathId: Int) (Q: (State, Verifier) => VerificationResult) : VerificationResult = { @@ -119,7 +126,7 @@ object executor extends ExecutionRules { (edges, jp) match { case (Seq(), _) => Q(s, v) - case (Seq(edge), _) => follow(s, edge, v, joinPoint)(Q) + case (Seq(edge), _) => follow(s, edge, v, joinPoint, pathId)(Q) case (Seq(edge1, edge2), Some(newJoinPoint)) if s.moreJoins.id >= JoinMode.All.id && // Can't directly match type because of type erasure ... @@ -148,8 +155,8 @@ object executor extends ExecutionRules { joiner.join[scala.Null, scala.Null](s1, v1, resetState = false)((s2, v2, QB) => { brancher.branch(s2, t0, (cedge1.condition, condNew), v2)( // Follow only until join point. - (s3, v3) => follow(s3, edge1, v3, Some(newJoinPoint))((s, v) => QB(s, null, v)), - (s3, v3) => follow(s3, edge2, v3, Some(newJoinPoint))((s, v) => QB(s, null, v)) + (s3, v3) => follow(s3, edge1, v3, Some(newJoinPoint), pathId)((s, v) => QB(s, null, v)), + (s3, v3) => follow(s3, edge2, v3, Some(newJoinPoint), nextPathId())((s, v) => QB(s, null, v)) ) })(entries => { val s2 = entries match { @@ -166,7 +173,9 @@ object executor extends ExecutionRules { Q(s4, v4) } else { // Continue after merging at join point. - exec(s4, newJoinPoint, s4.methodCfg.inEdges(newJoinPoint).head.kind, v4, joinPoint)(Q) + // Guessing this means that everything after a merge will have the path id of + // the first branch (don't know yet if that's ok) + exec(s4, newJoinPoint, s4.methodCfg.inEdges(newJoinPoint).head.kind, v4, joinPoint, pathId)(Q) } }) ) @@ -178,10 +187,10 @@ object executor extends ExecutionRules { val res = eval(s, thenEdge.condition, IfFailed(thenEdge.condition), v)((s2, tCond, eCondNew, v1) => brancher.branch(s2, tCond, (thenEdge.condition, eCondNew), v1)( (s3, v3) => { - follow(s3, thenEdge, v3, joinPoint)(Q) + follow(s3, thenEdge, v3, joinPoint, pathId)(Q) }, (s3, v3) => { - follow(s3, elseEdge, v3, joinPoint)(Q) + follow(s3, elseEdge, v3, joinPoint, nextPathId())(Q) })) res @@ -193,7 +202,7 @@ object executor extends ExecutionRules { v.symbExLog.switchToNextBranch(uidBranchPoint) } v.symbExLog.markReachable(uidBranchPoint) - result combine follow(s, edge, v, joinPoint)(Q) + result combine follow(s, edge, v, joinPoint, pathId)(Q) } } v.symbExLog.endBranchPoint(uidBranchPoint) @@ -205,32 +214,45 @@ object executor extends ExecutionRules { (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - exec(s, graph.entry, cfg.Kind.Normal, v, None)(Q) + exec(s, graph.entry, cfg.Kind.Normal, v, None, nextPathId())(Q) } - def exec(s: State, block: SilverBlock, incomingEdgeKind: cfg.Kind.Value, v: Verifier, joinPoint: Option[SilverBlock]) + def exec(s: State, block: SilverBlock, incomingEdgeKind: cfg.Kind.Value, v: Verifier, joinPoint: Option[SilverBlock], pathId: Int) (Q: (State, Verifier) => VerificationResult) : VerificationResult = { + // Get the label of the block for messages used by Prusti Assistant + // Can simplify this if labels are always the first statement in the block var blockLabel = "None" block.elements - .iterator - .takeWhile(_ => blockLabel == "None") - .foreach( element => - element match { - case Left(stmt) => stmt match { - case ast.Label(name, _) => - blockLabel = name + .iterator + .takeWhile(_ => blockLabel == "None") + .foreach( element => + element match { + case Left(stmt) => stmt match { + case ast.Label(name, _) => + blockLabel = name case _ => } - case Right(_) => - } - ) + case Right(_) => + } + ) + var methodName = "None" + if(s.isMethodVerification){ + methodName = s.currentMember.get.asInstanceOf[ast.Method].name + // if(methodName.startsWith("builtin")){ + // methodName = "None" + // } + } + if(blockLabel != "None"){ + + v.reporter.report(BlockReachedMessage(methodName, blockLabel, pathId)) + } val executed = block match { case cfg.StatementBlock(stmt) => execs(s, stmt, v)((s1, v1) => - follows(s1, magicWandSupporter.getOutEdges(s1, block), IfFailed, v1, joinPoint)(Q)) + follows(s1, magicWandSupporter.getOutEdges(s1, block), IfFailed, v1, joinPoint, pathId)(Q)) case _: cfg.PreconditionBlock[ast.Stmt, ast.Exp] | _: cfg.PostconditionBlock[ast.Stmt, ast.Exp] => @@ -310,7 +332,7 @@ object executor extends ExecutionRules { } } v3.decider.prover.comment("Loop head block: Follow loop-internal edges") - edgeCondWelldefinedness combine follows(s4, sortedEdges, WhileFailed, v3, joinPoint)(Q)})}})}})})) + edgeCondWelldefinedness combine follows(s4, sortedEdges, WhileFailed, v3, joinPoint, pathId)(Q)})}})}})})) case _ => /* We've reached a loop head block via an edge other than an in-edge: a normal edge or @@ -328,7 +350,7 @@ object executor extends ExecutionRules { * in the else. */ if(blockLabel != "None") - v.reporter.report(BlockProcessedMessage(blockLabel, executed.toString())) + v.reporter.report(BlockProcessedMessage(methodName, blockLabel, pathId, executed.toString())) executed } @@ -377,7 +399,6 @@ object executor extends ExecutionRules { case ast.Label(name, _) => val s1 = s.copy(oldHeaps = s.oldHeaps + (name -> magicWandSupporter.getEvalHeap(s))) - v.reporter.report(BlockReachedMessage(name)) Q(s1, v) case ast.LocalVarDeclStmt(decl) => From aca1a0d222dfae41bd8d7f253efb7433bb22197c Mon Sep 17 00:00:00 2001 From: trk Date: Mon, 25 Mar 2024 10:36:00 +0100 Subject: [PATCH 04/10] Update silver submodule --- .gitignore | 2 ++ src/main/scala/rules/Executor.scala | 47 +++++++++++++++-------------- 2 files changed, 26 insertions(+), 23 deletions(-) diff --git a/.gitignore b/.gitignore index 62b7de5ec..bfffe5b01 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,7 @@ common/target project/project project/target +project/metals.sbt target .settings/ .cache @@ -24,3 +25,4 @@ viper_tutorial_examples .bsp/ .bloop/ .metals/ +.vscode diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 5cdf76203..57cd8deb1 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -15,7 +15,7 @@ import viper.silver.cfg.silver.SilverCfg import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge} import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError} import viper.silver.verifier.errors._ -import viper.silver.reporter.{BlockProcessedMessage, BlockReachedMessage} +import viper.silver.reporter.{PathProcessedMessage, BlockReachedMessage} import viper.silver.verifier.reasons._ import viper.silver.{ast, cfg} import viper.silicon.decider.RecordedPathConditions @@ -52,6 +52,7 @@ object executor extends ExecutionRules { import evaluator._ import producer._ private val pathIdGenerator = new AtomicInteger(0) + private val pathComplete = collection.mutable.HashMap[Int, Boolean](); def nextPathId(): Int = { pathIdGenerator.incrementAndGet() @@ -222,21 +223,22 @@ object executor extends ExecutionRules { : VerificationResult = { // Get the label of the block for messages used by Prusti Assistant - // Can simplify this if labels are always the first statement in the block var blockLabel = "None" - block.elements - .iterator - .takeWhile(_ => blockLabel == "None") - .foreach( element => - element match { - case Left(stmt) => stmt match { - case ast.Label(name, _) => - blockLabel = name - case _ => - } - case Right(_) => - } - ) + + // block.elements + // .iterator + // .takeWhile(_ => blockLabel == "None") + // .foreach( element => + // element match { + // case Left(ast.Label(name, _)) => blockLabel = name + // case _ => + // } + // ) + // Can simplify the above if labels are _always_ the first statement in the block + block.elements.head match { + case Left(ast.Label(name, _)) => blockLabel = name + case _ => + } var methodName = "None" if(s.isMethodVerification){ methodName = s.currentMember.get.asInstanceOf[ast.Method].name @@ -245,8 +247,8 @@ object executor extends ExecutionRules { // } } if(blockLabel != "None"){ - v.reporter.report(BlockReachedMessage(methodName, blockLabel, pathId)) + pathComplete.addOne((pathId, false)) } val executed = block match { @@ -344,13 +346,12 @@ object executor extends ExecutionRules { Success()) } } - /* TODO: coarse. might want more intermedeate results. this waits until all - * following blocks have resolved. - * maybe move to `exec(State, ast.Stmt, Verifier)` or `execs` function - * in the else. - */ - if(blockLabel != "None") - v.reporter.report(BlockProcessedMessage(methodName, blockLabel, pathId, executed.toString())) + + if(blockLabel != "None" && !pathComplete.get(pathId).get){ + v.reporter.report(PathProcessedMessage(methodName, blockLabel, pathId, executed.getClass().getSimpleName())) + pathComplete.update(pathId, true) + } + executed } From 2ae38b910d87902cdebf8860e567cb005d2ee4d3 Mon Sep 17 00:00:00 2001 From: trk Date: Fri, 14 Jun 2024 13:23:27 +0200 Subject: [PATCH 05/10] Add flag "--generateBlockMessages" to enable block level reporting Also fix minor bug causing crashes for empty blocks. --- src/main/scala/Config.scala | 7 +++ src/main/scala/rules/Executor.scala | 71 +++++++++++++++++------------ 2 files changed, 50 insertions(+), 28 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index b0fd1cfb6..ad667ffb5 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -723,6 +723,13 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { noshort = true ) + val generateBlockMessages: ScallopOption[Boolean] = opt[Boolean]("generateBlockMessages", + descr = ( "Generate a message whenever a label is first reached and when a path of the symbloic execution run " + + "has finished."), + default = Some(false), + noshort = true + ) + val printTranslatedProgram: ScallopOption[Boolean] = opt[Boolean]("printTranslatedProgram", descr ="Print the final program that is going to be verified to stdout.", default = Some(false), diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 57cd8deb1..f8167ae01 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -222,33 +222,39 @@ object executor extends ExecutionRules { (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - // Get the label of the block for messages used by Prusti Assistant var blockLabel = "None" - - // block.elements - // .iterator - // .takeWhile(_ => blockLabel == "None") - // .foreach( element => - // element match { - // case Left(ast.Label(name, _)) => blockLabel = name - // case _ => - // } - // ) - // Can simplify the above if labels are _always_ the first statement in the block - block.elements.head match { - case Left(ast.Label(name, _)) => blockLabel = name - case _ => - } var methodName = "None" - if(s.isMethodVerification){ - methodName = s.currentMember.get.asInstanceOf[ast.Method].name - // if(methodName.startsWith("builtin")){ - // methodName = "None" - // } - } - if(blockLabel != "None"){ - v.reporter.report(BlockReachedMessage(methodName, blockLabel, pathId)) - pathComplete.addOne((pathId, false)) + if(Verifier.config.generateBlockMessages()){ + // // Get the label of the block for messages used by Prusti Assistant + // block.elements + // .iterator + // .takeWhile(_ => blockLabel == "None") + // .foreach( element => + // element match { + // case Left(ast.Label(name, _)) => blockLabel = name + // case _ => + // } + // ) + // Can simplify the above if labels are _always_ the first statement in the block + if (block.elements.length > 0){ + block.elements.head match { + case Left(ast.Label(name, _)) => blockLabel = name + case _ => + } + } + if(s.isMethodVerification){ + methodName = s.currentMember.get.asInstanceOf[ast.Method].name + // if(methodName.startsWith("builtin")){ + // methodName = "None" + // } + } + if(blockLabel != "None"){ + v.reporter.report(BlockReachedMessage(methodName, blockLabel, pathId)) + pathComplete.synchronized{ + if(!pathComplete.contains(pathId)) + pathComplete.addOne((pathId, false)) + } + } } val executed = block match { @@ -347,9 +353,18 @@ object executor extends ExecutionRules { } } - if(blockLabel != "None" && !pathComplete.get(pathId).get){ - v.reporter.report(PathProcessedMessage(methodName, blockLabel, pathId, executed.getClass().getSimpleName())) - pathComplete.update(pathId, true) + if(Verifier.config.generateBlockMessages()){ + if(blockLabel != "None"){ + // Only send the message from the offending node + var incomplete = false + pathComplete.synchronized{ + incomplete = !pathComplete.get(pathId).get + if (incomplete) + pathComplete.update(pathId, true) + } + if (incomplete) + v.reporter.report(PathProcessedMessage(methodName, blockLabel, pathId, executed.getClass().getSimpleName())) + } } executed From 6b993acdd702cb792f1a75e15f88e3dde23d792d Mon Sep 17 00:00:00 2001 From: trk Date: Sat, 3 Aug 2024 12:43:24 +0200 Subject: [PATCH 06/10] Fix path ids not being incremented in non-parallelized branches --- src/main/scala/rules/Executor.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index f8167ae01..1a1d2f2f3 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -174,8 +174,6 @@ object executor extends ExecutionRules { Q(s4, v4) } else { // Continue after merging at join point. - // Guessing this means that everything after a merge will have the path id of - // the first branch (don't know yet if that's ok) exec(s4, newJoinPoint, s4.methodCfg.inEdges(newJoinPoint).head.kind, v4, joinPoint, pathId)(Q) } }) @@ -199,11 +197,13 @@ object executor extends ExecutionRules { val uidBranchPoint = v.symbExLog.insertBranchPoint(edges.length) val res = edges.zipWithIndex.foldLeft(Success(): VerificationResult) { case (result: VerificationResult, (edge, edgeIndex)) => { + var branchPathId = pathId if (edgeIndex != 0) { v.symbExLog.switchToNextBranch(uidBranchPoint) + branchPathId = nextPathId() } v.symbExLog.markReachable(uidBranchPoint) - result combine follow(s, edge, v, joinPoint, pathId)(Q) + result combine follow(s, edge, v, joinPoint, branchPathId)(Q) } } v.symbExLog.endBranchPoint(uidBranchPoint) From 51820579980db8237dd8b3a98ba22b6e7fc25c66 Mon Sep 17 00:00:00 2001 From: trk Date: Thu, 29 Aug 2024 11:19:33 +0200 Subject: [PATCH 07/10] Add emission of BlockFailureMessages, clean up a bit There were issues with the --numErrorsToReport option. PathProcessedMessages may have emitted false results since the result of the last explored block did not match the expected path result. It was success if the last explored block succeeded, while it was expected to be Failure if any block on the path failed. Now the message should merely signify that the path has finished. --- src/main/scala/Config.scala | 4 +- src/main/scala/rules/Executor.scala | 75 +++++++------------ .../scala/rules/SymbolicExecutionRules.scala | 15 +++- src/main/scala/state/State.scala | 7 ++ .../scala/verifier/DefaultMainVerifier.scala | 2 + 5 files changed, 54 insertions(+), 49 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index ad667ffb5..c72931f6d 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -724,8 +724,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { ) val generateBlockMessages: ScallopOption[Boolean] = opt[Boolean]("generateBlockMessages", - descr = ( "Generate a message whenever a label is first reached and when a path of the symbloic execution run " + - "has finished."), + descr = ( "Generate a message whenever an execution path reaches a new block, a block fails" + + " , or a path has finished"), default = Some(false), noshort = true ) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 1a1d2f2f3..7915f8e5d 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -222,44 +222,28 @@ object executor extends ExecutionRules { (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - var blockLabel = "None" - var methodName = "None" - if(Verifier.config.generateBlockMessages()){ - // // Get the label of the block for messages used by Prusti Assistant - // block.elements - // .iterator - // .takeWhile(_ => blockLabel == "None") - // .foreach( element => - // element match { - // case Left(ast.Label(name, _)) => blockLabel = name - // case _ => - // } - // ) - // Can simplify the above if labels are _always_ the first statement in the block - if (block.elements.length > 0){ - block.elements.head match { - case Left(ast.Label(name, _)) => blockLabel = name - case _ => - } - } - if(s.isMethodVerification){ - methodName = s.currentMember.get.asInstanceOf[ast.Method].name - // if(methodName.startsWith("builtin")){ - // methodName = "None" - // } - } - if(blockLabel != "None"){ - v.reporter.report(BlockReachedMessage(methodName, blockLabel, pathId)) - pathComplete.synchronized{ + var blockLabel: Option[String] = None + var methodName: Option[String] = None + var sLocal = s + if(Verifier.config.generateBlockMessages() && s.isMethodVerification && block.elements.length > 0){ + block.elements.head match { + case Left(ast.Label(name, _)) => { + blockLabel = Some(name) + methodName = Some(s.currentMember.get.asInstanceOf[ast.Method].name) + sLocal = s.setCurrentBlock(blockLabel.get, pathId) + v.reporter.report(BlockReachedMessage(methodName.get, blockLabel.get, pathId)) + pathComplete.synchronized{ if(!pathComplete.contains(pathId)) pathComplete.addOne((pathId, false)) + } } + case _ => } } val executed = block match { case cfg.StatementBlock(stmt) => - execs(s, stmt, v)((s1, v1) => + execs(sLocal, stmt, v)((s1, v1) => follows(s1, magicWandSupporter.getOutEdges(s1, block), IfFailed, v1, joinPoint, pathId)(Q)) case _: cfg.PreconditionBlock[ast.Stmt, ast.Exp] @@ -286,15 +270,15 @@ object executor extends ExecutionRules { */ /* Havoc local variables that are assigned to in the loop body */ - val wvs = s.methodCfg.writtenVars(block) + val wvs = sLocal.methodCfg.writtenVars(block) /* TODO: BUG: Variables declared by LetWand show up in this list, but shouldn't! */ - val gBody = Store(wvs.foldLeft(s.g.values)((map, x) => { + val gBody = Store(wvs.foldLeft(sLocal.g.values)((map, x) => { val xNew = v.decider.fresh(x) map.updated(x, xNew)})) - val sBody = s.copy(g = gBody, h = Heap()) + val sBody = sLocal.copy(g = gBody, h = Heap()) - val edges = s.methodCfg.outEdges(block) + val edges = sLocal.methodCfg.outEdges(block) val (outEdges, otherEdges) = edges partition(_.kind == cfg.Kind.Out) val sortedEdges = otherEdges ++ outEdges val edgeConditions = sortedEdges.collect{case ce: cfg.ConditionalEdge[ast.Stmt, ast.Exp] => ce.condition} @@ -312,7 +296,7 @@ object executor extends ExecutionRules { v1.decider.freshFunctions /* [BRANCH-PARALLELISATION] */) Success() })}) - combine executionFlowController.locally(s, v)((s0, v0) => { + combine executionFlowController.locally(sLocal, 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)") @@ -348,23 +332,22 @@ object executor extends ExecutionRules { * attempting to re-establish the invariant. */ v.decider.prover.comment("Loop head block: Re-establish invariant") - consumes(s, invs, e => LoopInvariantNotPreserved(e), v)((_, _, _) => + consumes(sLocal, invs, e => LoopInvariantNotPreserved(e), v)((_, _, _) => Success()) } } - if(Verifier.config.generateBlockMessages()){ - if(blockLabel != "None"){ - // Only send the message from the offending node - var incomplete = false - pathComplete.synchronized{ - incomplete = !pathComplete.get(pathId).get - if (incomplete) - pathComplete.update(pathId, true) - } + // Only send a path processed message from the last explored node of a path + if(Verifier.config.generateBlockMessages() && blockLabel.isDefined){ + var incomplete = false + pathComplete.synchronized{ + incomplete = !pathComplete.get(pathId).get if (incomplete) - v.reporter.report(PathProcessedMessage(methodName, blockLabel, pathId, executed.getClass().getSimpleName())) + pathComplete.update(pathId, true) } + + if (incomplete) + v.reporter.report(PathProcessedMessage(methodName.get, pathId, executed.getClass().getSimpleName())) } executed diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index 888028133..e3552e8a2 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -15,6 +15,7 @@ import viper.silver.ast import viper.silver.frontend.{MappedModel, NativeModel, VariablesModel} import viper.silver.verifier.errors.ErrorWrapperWithExampleTransformer import viper.silver.verifier.{Counterexample, CounterexampleTransformer, VerificationError} +import viper.silver.reporter.BlockFailureMessage trait SymbolicExecutionRules { lazy val withExp = Verifier.config.enableDebugging() @@ -44,7 +45,19 @@ trait SymbolicExecutionRules { } protected def createFailure(ve: VerificationError, v: Verifier, s: State, failedAssert: Term, failedAssertExp: Option[DebugExp], generateNewModel: Boolean): Failure = { - if (s.retryLevel == 0 && !ve.isExpected) v.errorsReportedSoFar.incrementAndGet() + if (s.retryLevel == 0 && !ve.isExpected) { + if (Verifier.config.generateBlockMessages()) { + s.currentMember.foreach((member) => { + val memberName = member.name + s.currentBlock.foreach((block) => + v.reporter.report(BlockFailureMessage(memberName, block._1, block._2)) + ) + }) + } + + v.errorsReportedSoFar.incrementAndGet() + } + var ceTrafo: Option[CounterexampleTransformer] = None val res = ve match { case ErrorWrapperWithExampleTransformer(wrapped, trafo) => diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 314edc6fa..77ee99baf 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -29,6 +29,7 @@ final case class State(g: Store = Store(), h: Heap = Heap(), program: ast.Program, currentMember: Option[ast.Member], + currentBlock: Option[(String, Integer)], // (block label, path id) predicateData: Map[ast.Predicate, PredicateData], functionData: Map[ast.Function, FunctionData], oldHeaps: OldHeaps = Map.empty, @@ -88,6 +89,8 @@ final case class State(g: Store = Store(), currentMember.isEmpty || currentMember.get.isInstanceOf[ast.Method] } + def setCurrentBlock(b: (String, Integer)) = copy(currentBlock = Some(b)) + val isLastRetry: Boolean = retryLevel == 0 def incCycleCounter(m: ast.Predicate) = @@ -155,6 +158,7 @@ object State { s1 match { /* Decompose state s1 */ case State(g1, h1, program, member, + block, predicateData, functionData, oldHeaps1, @@ -181,6 +185,7 @@ object State { s2 match { case State(`g1`, `h1`, `program`, `member`, + `block`, `predicateData`, `functionData`, `oldHeaps1`, `parallelizeBranches1`, @@ -306,6 +311,7 @@ object State { s1 match { /* Decompose state s1 */ case State(g1, h1, program, member, + block, predicateData, functionData, oldHeaps1, parallelizeBranches1, @@ -330,6 +336,7 @@ object State { /* Decompose state s2: most values must match those of s1 */ s2 match { case State(g2, h2, `program`, `member`, + `block`, `predicateData`, `functionData`, oldHeaps2, `parallelizeBranches1`, diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index b395ed213..0a0bb87e7 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -393,6 +393,7 @@ class DefaultMainVerifier(config: Config, } else InsertionOrderedSet.empty State(program = program, + currentBlock = None, functionData = functionData, predicateData = predicateData, qpFields = quantifiedFields, @@ -418,6 +419,7 @@ class DefaultMainVerifier(config: Config, State( program = program, currentMember = None, + currentBlock = None, functionData = functionData, predicateData = predicateData, qpFields = quantifiedFields, From fafb2470206219863c22a7d6075f6f16c1fad6a2 Mon Sep 17 00:00:00 2001 From: trk Date: Mon, 2 Sep 2024 10:33:05 +0200 Subject: [PATCH 08/10] Redirect submodule to viperproject --- .gitmodules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitmodules b/.gitmodules index f68200d4c..723bf0d3e 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,3 @@ [submodule "silver"] path = silver - url = https://github.com/trktby/silver.git + url = https://github.com/viperproject/silver.git \ No newline at end of file From a35d3eebd4d967938e2f2c0cdba9a05761c96238 Mon Sep 17 00:00:00 2001 From: trk Date: Mon, 2 Sep 2024 16:34:53 +0200 Subject: [PATCH 09/10] Simplify path completion tracking --- src/main/scala/rules/Executor.scala | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 7915f8e5d..caedb0a3e 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -52,7 +52,7 @@ object executor extends ExecutionRules { import evaluator._ import producer._ private val pathIdGenerator = new AtomicInteger(0) - private val pathComplete = collection.mutable.HashMap[Int, Boolean](); + private val pathComplete = collection.mutable.HashSet[Int](); def nextPathId(): Int = { pathIdGenerator.incrementAndGet() @@ -233,9 +233,9 @@ object executor extends ExecutionRules { sLocal = s.setCurrentBlock(blockLabel.get, pathId) v.reporter.report(BlockReachedMessage(methodName.get, blockLabel.get, pathId)) pathComplete.synchronized{ - if(!pathComplete.contains(pathId)) - pathComplete.addOne((pathId, false)) - } + if(!pathComplete.contains(pathId)) + pathComplete.addOne(pathId) + } } case _ => } @@ -339,15 +339,12 @@ object executor extends ExecutionRules { // Only send a path processed message from the last explored node of a path if(Verifier.config.generateBlockMessages() && blockLabel.isDefined){ - var incomplete = false pathComplete.synchronized{ - incomplete = !pathComplete.get(pathId).get - if (incomplete) - pathComplete.update(pathId, true) + if (pathComplete.contains(pathId)) { + pathComplete.remove(pathId) + v.reporter.report(PathProcessedMessage(methodName.get, pathId, executed.getClass().getSimpleName())) + } } - - if (incomplete) - v.reporter.report(PathProcessedMessage(methodName.get, pathId, executed.getClass().getSimpleName())) } executed From b4b3ddcd5c76d61929e890cc1686fea974ac322a Mon Sep 17 00:00:00 2001 From: trk Date: Wed, 4 Sep 2024 19:00:36 +0200 Subject: [PATCH 10/10] Whitespace fix --- .gitmodules | 2 +- src/main/scala/rules/Executor.scala | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.gitmodules b/.gitmodules index 723bf0d3e..57fc76362 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,3 @@ [submodule "silver"] path = silver - url = https://github.com/viperproject/silver.git \ No newline at end of file + url = https://github.com/viperproject/silver.git diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index caedb0a3e..c92ca19f4 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -350,14 +350,14 @@ object executor extends ExecutionRules { executed } - def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier) + def execs(s: State, stmts: Seq[ast.Stmt], v: Verifier) (Q: (State, Verifier) => VerificationResult) : VerificationResult = if (stmts.nonEmpty) exec(s, stmts.head, v)((s1, v1) => execs(s1, stmts.tail, v1)(Q)) - else + else Q(s, v) def exec(s: State, stmt: ast.Stmt, v: Verifier)