From bbd22aea6d6eddf180b2e83e7698f5a3a79ebe94 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 24 Apr 2023 12:34:52 +0200 Subject: [PATCH] Not generating macros in functions (since they could refer to result, which crashes other Z3 instances). Also fixing remembering non heap-dependent triggers evaluated inside old. --- src/main/scala/rules/Evaluator.scala | 4 ++- .../rules/MoreCompleteExhaleSupporter.scala | 4 ++- .../scala/rules/QuantifiedChunkSupport.scala | 28 +++++++++++++------ 3 files changed, 26 insertions(+), 10 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 264c88085..fe8dfe0b5 100644 --- 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 index 1a9f18b51..6abf20ff3 100644 --- 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 index 6d3c5fc4a..857bacb02 100644 --- 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)