consume

viperproject · Aug 2, 2023 · abfbf48 · abfbf48
1 parent b1b847d
commit abfbf48
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 3 deletions.
diff --git a/silver b/silver
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
@@ -23,6 +23,8 @@ import viper.silicon.state.terms.predef.`?r`
 import viper.silicon.utils.freshSnap
 import viper.silicon.verifier.Verifier
 import viper.silver.cfg.ConditionalEdge
+import viper.silver.reporter.BenchmarkingAccumulator
+import viper.silver.reporter.ProverActionIDs
 
 trait ExecutionRules extends SymbolicExecutionRules {
   def exec(s: State,
@@ -143,7 +145,13 @@ object executor extends ExecutionRules {
           (Q: (State, Verifier) => VerificationResult)
           : VerificationResult = {
 
-    exec(s, graph.entry, cfg.Kind.Normal, v)(Q)
+    val execID = ProverActionIDs.getID
+    println(s"OIJOIEWJFOIJW $execID")
+    v.reporter report BenchmarkingAccumulator("exec", execID, true)
+    exec(s, graph.entry, cfg.Kind.Normal, v)((s, v) => {
+      v.reporter report BenchmarkingAccumulator("exec", execID)
+      Q(s, v)
+    })
   }
 
   def exec(s: State, block: SilverBlock, incomingEdgeKind: cfg.Kind.Value, v: Verifier)

diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala
@@ -19,6 +19,8 @@ import viper.silicon.state._
 import viper.silicon.supporters.functions.NoopFunctionRecorder
 import viper.silicon.verifier.Verifier
 import viper.silver.verifier.reasons.{NegativePermission, QPAssertionNotInjective}
+import viper.silver.reporter.ProverActionIDs
+import viper.silver.reporter.BenchmarkingAccumulator
 
 trait ProductionRules extends SymbolicExecutionRules {
 
@@ -125,7 +127,13 @@ object producer extends ProductionRules {
       allPves ++= pves
     })
 
-    produceTlcs(s, sf, allTlcs.result(), allPves.result(), v)(Q)
+    val produceID = ProverActionIDs.getID
+    v.reporter report BenchmarkingAccumulator("produce", produceID)
+
+    produceTlcs(s, sf, allTlcs.result(), allPves.result(), v)((s, v) => {
+      v.reporter report BenchmarkingAccumulator("produce", produceID)
+      Q(s, v)
+    })
   }
 
   private def produceTlcs(s: State,

diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala
@@ -322,6 +322,8 @@ class DefaultMainVerifier(config: Config,
     reporter report BenchmarkingReport("method well definedness", "meth_well_def")
     reporter report BenchmarkingReport("prover", "prover")
     reporter report BenchmarkingReport("consume", "consume")
+    reporter report BenchmarkingReport("produce", "produce")
+    reporter report BenchmarkingReport("eval", "eval")
     reporter report BenchmarkingReport("branch", "branching")
 
     (   functionVerificationResults