Merge pull request #712 from viperproject/meilers_fix_711

Not generating QP/MCE macros in functions
viperproject · Apr 24, 2023 · 0ca4350 · 0ca4350
2 parents 99e9c57 + 6de233a
commit 0ca4350
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 10 deletions.
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
@@ -1099,6 +1099,7 @@ object evaluator extends EvaluationRules {
       val newPossibleTriggers = if (s.recordPossibleTriggers) {
         // For all new possible trigger expressions e and translated term t,
         // make sure we remember t as the term for old[label](e) instead.
+        // If e is not heap-dependent, we also remember t as the term for e.
         val addedOrChangedPairs = s3.possibleTriggers.filter(t =>
           !possibleTriggersBefore.contains(t._1) || possibleTriggersBefore(t._1) != t._2)
 
@@ -1110,7 +1111,8 @@ object evaluator extends EvaluationRules {
           }
         }
 
-        val oldPairs = addedOrChangedPairs.map(t => wrapInOld(t._1) -> t._2)
+        val oldPairs = addedOrChangedPairs.map(t => wrapInOld(t._1) -> t._2) ++
+          addedOrChangedPairs.filter(t => !t._1.isHeapDependent(s.program))
         s.possibleTriggers ++ oldPairs
       } else {
         s.possibleTriggers

diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -246,10 +246,12 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
           if (moreNeeded) {
             val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 })
 
-            val pTaken = if (Verifier.config.useFlyweight) {
+            val pTaken = if (s.functionRecorder != NoopFunctionRecorder || Verifier.config.useFlyweight) {
               // ME: When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different
               // (leading to new terms that have to be translated), whereas without macros, we can usually use a term
               // that already exists.
+              // During function verification, we should not define macros, since they could contain resullt, which is not
+              // defined elsewhere.
               Ite(eq, PermMin(ch.perm, pNeeded), NoPerm)
             } else {
               val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm)

diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -22,6 +22,7 @@ import viper.silicon.state.terms.perms.IsPositive
 import viper.silicon.state.terms.perms.BigPermSum
 import viper.silicon.state.terms.predef.`?r`
 import viper.silicon.state.terms.utils.consumeExactRead
+import viper.silicon.supporters.functions.NoopFunctionRecorder
 import viper.silicon.utils.notNothing.NotNothing
 import viper.silicon.verifier.Verifier
 import viper.silver.reporter.InternalWarningMessage
@@ -1358,15 +1359,26 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     var currentFunctionRecorder = s.functionRecorder
 
     val precomputedData = candidates map { ch =>
+      // ME: When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different
+      // (leading to new terms that have to be translated), whereas without macros, we can usually use a term
+      // that already exists.
+      // During function verification, we should not define macros, since they could contain resullt, which is not
+      // defined elsewhere.
+      val declareMacro = s.functionRecorder == NoopFunctionRecorder && !Verifier.config.useFlyweight
+
       val permsProvided = ch.perm
-      val permsTakenBody = Ite(condition, PermMin(permsProvided, permsNeeded), NoPerm)
-      val permsTakenArgs = codomainQVars ++ additionalArgs
-      val permsTakenDecl = v.decider.freshMacro("pTaken", permsTakenArgs, permsTakenBody)
-      val permsTakenMacro = Macro(permsTakenDecl.id, permsTakenDecl.args.map(_.sort), permsTakenDecl.body.sort)
-      val permsTaken = App(permsTakenMacro, permsTakenArgs)
-
-      currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(permsTakenDecl)
-      v.symbExLog.addMacro(permsTaken, permsTakenBody)
+      val permsTaken = if (declareMacro) {
+        val permsTakenBody = Ite(condition, PermMin(permsProvided, permsNeeded), NoPerm)
+        val permsTakenArgs = codomainQVars ++ additionalArgs
+        val permsTakenDecl = v.decider.freshMacro("pTaken", permsTakenArgs, permsTakenBody)
+        val permsTakenMacro = Macro(permsTakenDecl.id, permsTakenDecl.args.map(_.sort), permsTakenDecl.body.sort)
+        currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(permsTakenDecl)
+        val permsTakenApp = App(permsTakenMacro, permsTakenArgs)
+        v.symbExLog.addMacro(permsTakenApp, permsTakenBody)
+        permsTakenApp
+      } else {
+        Ite(condition, PermMin(permsProvided, permsNeeded), NoPerm)
+      }
 
       permsNeeded = PermMinus(permsNeeded, permsTaken)