From abfbf4864058650fcf6a4abd500d4a98dfae2275 Mon Sep 17 00:00:00 2001
From: Dspil <dennisspiliopoylos@gmail.com>
Date: Wed, 2 Aug 2023 19:52:33 +0200
Subject: [PATCH] consume

---
 silver                                            |  2 +-
 src/main/scala/rules/Executor.scala               | 10 +++++++++-
 src/main/scala/rules/Producer.scala               | 10 +++++++++-
 src/main/scala/verifier/DefaultMainVerifier.scala |  2 ++
 4 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/silver b/silver
index c2c1b1183..a97622701 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit c2c1b1183e19a71a5793a7503aae452c77512b2d
+Subproject commit a9762270181ddfd05d6997de5858fb8b6f82498e
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 24d2c602d..c123a428d 100644
--- 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
index a29672f59..99ea9b186 100644
--- 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
index bbc71ce6d..39da31975 100644
--- 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