From 21f7eb492cc2c323740dad1ba86dd446820b65d0 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 23 Apr 2024 17:12:05 +0200 Subject: [PATCH 1/9] Adding missing condition --- src/main/scala/rules/QuantifiedChunkSupport.scala | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 166a33a87..d2fb8fc8d 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -271,9 +271,15 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val qvarsToInversesOfCodomain = inverseFunctions.qvarsToInversesOf(codomainQVars) + val receiverMatches = + And( + codomainQVars + .zip(arguments) + .map { case (x, a) => x === a }).replace(qvarsToInversesOfCodomain) + val conditionalizedPermissions = Ite( - And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)), + And(And(imagesOfCodomain), receiverMatches, condition.replace(qvarsToInversesOfCodomain)), permissions.replace(qvarsToInversesOfCodomain), NoPerm) From 79a485edf63da9e6c291783fc709ef2f89fdafe6 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 23 Apr 2024 22:10:30 +0200 Subject: [PATCH 2/9] Emitting missing definitions for new quantified chunk inverse functions --- src/main/scala/rules/QuantifiedChunkSupport.scala | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index d2fb8fc8d..162f88b79 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1167,7 +1167,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { case Complete() => rPerm case Incomplete(remaining) => PermMinus(rPerm, remaining) } - val (consumedChunk, _) = quantifiedChunkSupporter.createQuantifiedChunk( + val (consumedChunk, inverseFunctions) = quantifiedChunkSupporter.createQuantifiedChunk( qvars, condOfInvOfLoc, resource, @@ -1181,6 +1181,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v2, s.program ) + v.decider.assume(FunctionPreconditionTransformer.transform(inverseFunctions.axiomInvertiblesOfInverses, s3.program)) + v.decider.assume(inverseFunctions.axiomInvertiblesOfInverses) val h2 = Heap(remainingChunks ++ otherChunks) val s4 = s3.copy(smCache = smCache2, constrainableARPs = s.constrainableARPs) @@ -1390,7 +1392,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { // converting to a Z3 term. // 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 declareMacro = false && s.functionRecorder == NoopFunctionRecorder // && !Verifier.config.useFlyweight val permsProvided = ch.perm val permsTaken = if (declareMacro) { From 00bd0d6e8eb903cce8036cb9be65e25c1f67d6df Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 24 Apr 2024 15:39:29 +0200 Subject: [PATCH 3/9] Added test in silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 0e9b9615f..761be4673 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 0e9b9615f82e5cb9e50f87acfc2aae25fd478f56 +Subproject commit 761be4673f68b43b761e67126b6955fbfb90bfb7 From 8be227b5563fc70015a5714aa091dd68c4dd2812 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 24 Apr 2024 15:42:37 +0200 Subject: [PATCH 4/9] Undid accidental change --- src/main/scala/rules/QuantifiedChunkSupport.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 162f88b79..10826b8eb 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1392,7 +1392,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { // converting to a Z3 term. // During function verification, we should not define macros, since they could contain resullt, which is not // defined elsewhere. - val declareMacro = false && s.functionRecorder == NoopFunctionRecorder // && !Verifier.config.useFlyweight + val declareMacro = s.functionRecorder == NoopFunctionRecorder // && !Verifier.config.useFlyweight val permsProvided = ch.perm val permsTaken = if (declareMacro) { From 8d1ad0f9e417ded8e8224d7c3abeaa08c67550a6 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 26 Apr 2024 22:01:16 +0200 Subject: [PATCH 5/9] Trying to get rid of unsound assumption that all references map to some receiver --- silver | 2 +- src/main/scala/rules/QuantifiedChunkSupport.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/silver b/silver index 761be4673..068f121f6 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 761be4673f68b43b761e67126b6955fbfb90bfb7 +Subproject commit 068f121f63a651723c6e3de6ce3c9b62812ad188 diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 10826b8eb..25c543476 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1666,7 +1666,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { inversesOfFcts(idx) = inv(invertibles) inversesOfCodomains(idx) = inv(codomainQVars) - if (qvar.sort != sorts.Int && qvar.sort != sorts.Ref) { + if (true) { // Types known to be infinite, thus there is no need to constrain the domain using image functions. val imgFun = v.decider.fresh("img", (additionalInvArgs map (_.sort)) ++ invertibles.map(_.sort), sorts.Bool) val img = (ts: Seq[Term]) => App(imgFun, additionalInvArgs ++ ts) From 320842bdcebc4d29a204852ee248ffef6ef34a50 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 4 May 2024 18:31:03 +0200 Subject: [PATCH 6/9] Undoing unnecessary change --- .../scala/rules/QuantifiedChunkSupport.scala | 26 +++++-------------- 1 file changed, 7 insertions(+), 19 deletions(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 25c543476..d361336d3 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -271,15 +271,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val qvarsToInversesOfCodomain = inverseFunctions.qvarsToInversesOf(codomainQVars) - val receiverMatches = - And( - codomainQVars - .zip(arguments) - .map { case (x, a) => x === a }).replace(qvarsToInversesOfCodomain) - val conditionalizedPermissions = Ite( - And(And(imagesOfCodomain), receiverMatches, condition.replace(qvarsToInversesOfCodomain)), + And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)), permissions.replace(qvarsToInversesOfCodomain), NoPerm) @@ -1666,19 +1660,13 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { inversesOfFcts(idx) = inv(invertibles) inversesOfCodomains(idx) = inv(codomainQVars) - if (true) { - // Types known to be infinite, thus there is no need to constrain the domain using image functions. - val imgFun = v.decider.fresh("img", (additionalInvArgs map (_.sort)) ++ invertibles.map(_.sort), sorts.Bool) - val img = (ts: Seq[Term]) => App(imgFun, additionalInvArgs ++ ts) + // Types known to be infinite, thus there is no need to constrain the domain using image functions. + val imgFun = v.decider.fresh("img", (additionalInvArgs map (_.sort)) ++ invertibles.map(_.sort), sorts.Bool) + val img = (ts: Seq[Term]) => App(imgFun, additionalInvArgs ++ ts) - imageFunctions(idx) = imgFun - imagesOfFcts(idx) = img(invertibles) - imagesOfCodomains(idx) = img(codomainQVars) - } else { - // imageFunctions(idx) remains null, will be filtered out later. - imagesOfFcts(idx) = True - imagesOfCodomains(idx) = True - } + imageFunctions(idx) = imgFun + imagesOfFcts(idx) = img(invertibles) + imagesOfCodomains(idx) = img(codomainQVars) } /* f_1(inv_1(rs), ..., inv_n(rs)), ..., f_m(inv_1(rs), ..., inv_n(rs)) */ From 7d9bccf3396590545b96f750386b3d22484a9ace Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sat, 4 May 2024 22:25:47 +0200 Subject: [PATCH 7/9] Adding missing assumptions about inverse functions for transferred chunks --- silver | 2 +- src/main/scala/rules/QuantifiedChunkSupport.scala | 11 +++++++++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/silver b/silver index 068f121f6..e15d3566b 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 068f121f63a651723c6e3de6ce3c9b62812ad188 +Subproject commit e15d3566b602b0bc0a497fd38cc856ab35852365 diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index d361336d3..7bb9ddc80 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1114,6 +1114,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val qvarsToInvOfLoc = inverseFunctions.qvarsToInversesOf(formalQVars) val condOfInvOfLoc = tCond.replace(qvarsToInvOfLoc) val lossOfInvOfLoc = loss.replace(qvarsToInvOfLoc) + val argsOfInvOfLoc = tArgs.map(a => a.replace(qvarsToInvOfLoc)) + // ME: We include the following condition to make sure the arguments are contained in the condition (and + // can trigger other quantifiers) even if neither tCond not loss term mention the arguments. + val argumentsMatch = And(formalQVars.zip(argsOfInvOfLoc).map(va => va._1 === va._2)) v.decider.prover.comment("Definitional axioms for inverse functions") v.decider.assume(inverseFunctions.definitionalAxioms.map(a => FunctionPreconditionTransformer.transform(a, s.program))) @@ -1145,7 +1149,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { s2, relevantChunks, formalQVars, - And(condOfInvOfLoc, And(imagesOfFormalQVars)), + And(condOfInvOfLoc, And(imagesOfFormalQVars), argumentsMatch), None, resource, rPerm, @@ -1177,6 +1181,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { ) v.decider.assume(FunctionPreconditionTransformer.transform(inverseFunctions.axiomInvertiblesOfInverses, s3.program)) v.decider.assume(inverseFunctions.axiomInvertiblesOfInverses) + val substitutedAxiomInversesOfInvertibles = inverseFunctions.axiomInversesOfInvertibles.replace(formalQVars, tArgs) + v.decider.assume(FunctionPreconditionTransformer.transform(substitutedAxiomInversesOfInvertibles, s3.program)) + v.decider.assume(substitutedAxiomInversesOfInvertibles) val h2 = Heap(remainingChunks ++ otherChunks) val s4 = s3.copy(smCache = smCache2, constrainableARPs = s.constrainableARPs) @@ -1194,7 +1201,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { s.copy(smCache = smCache1), relevantChunks, formalQVars, - And(condOfInvOfLoc, And(imagesOfFormalQVars)), + And(condOfInvOfLoc, And(imagesOfFormalQVars), argumentsMatch), None, resource, lossOfInvOfLoc, From 429ddbd72fcb82347b211726f300e516e68b859c Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 5 May 2024 00:04:17 +0200 Subject: [PATCH 8/9] Including image functions in quasihavoc encoding --- src/main/scala/rules/HavocSupporter.scala | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala index b0422750e..51096a3b4 100644 --- a/src/main/scala/rules/HavocSupporter.scala +++ b/src/main/scala/rules/HavocSupporter.scala @@ -26,7 +26,7 @@ object havocSupporter extends SymbolicExecutionRules { // should replace the snapshot. Different data is needed for `havoc` and `havocall`. // For more information, see `replacementCond`. sealed trait HavocHelperData - case class HavocallData(inverseFunctions: InverseFunctions) extends HavocHelperData + case class HavocallData(inverseFunctions: InverseFunctions, codomainQVars: Seq[Var], imagesOfCodomain: Seq[Term]) extends HavocHelperData case class HavocOneData(args: Seq[Term]) extends HavocHelperData /** Execute the statement `havoc c ==> R`, where c is a conditional expression and @@ -130,8 +130,7 @@ object havocSupporter extends SymbolicExecutionRules { case false => createFailure(pve dueTo notInjectiveReason, v, s1) case true => // Generate the inverse axioms - // TODO: Second return value (imagesOfCodomain) currently not used — OK? - val (inverseFunctions, _) = quantifiedChunkSupporter.getFreshInverseFunctions( + val (inverseFunctions, imagesOfCodomain) = quantifiedChunkSupporter.getFreshInverseFunctions( qvars = tVars, condition = tCond, invertibles = tArgs, @@ -149,9 +148,9 @@ object havocSupporter extends SymbolicExecutionRules { // the HavocHelperData inside of a HavocAllData case. val newChunks = if (usesQPChunks(s1, resource)) - havocQuantifiedResource(s1, tCond, resource, HavocallData(inverseFunctions), v1) + havocQuantifiedResource(s1, tCond, resource, HavocallData(inverseFunctions, codomainQVars, imagesOfCodomain), v1) else - havocNonQuantifiedResource(s1, tCond, resource, HavocallData(inverseFunctions), v1) + havocNonQuantifiedResource(s1, tCond, resource, HavocallData(inverseFunctions, codomainQVars, imagesOfCodomain), v1) Q(s1.copy(h = Heap(newChunks)), v1) } @@ -291,9 +290,9 @@ object havocSupporter extends SymbolicExecutionRules { case HavocOneData(args) => val eqs = And(chunkArgs.zip(args).map{ case (t1, t2) => t1 === t2 }) And(lhs, eqs) - case HavocallData(inverseFunctions) => + case HavocallData(inverseFunctions, codomainQVars, imagesOfCodomain) => val replaceMap = inverseFunctions.qvarsToInversesOf(chunkArgs) - lhs.replace(replaceMap) + And(lhs.replace(replaceMap), And(imagesOfCodomain.map(_.replace(codomainQVars, chunkArgs)))) } } From 67763663d588e3e8b3d876f7b72844c93ac96027 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Sun, 5 May 2024 00:42:16 +0200 Subject: [PATCH 9/9] Removed outdated comment --- src/main/scala/rules/QuantifiedChunkSupport.scala | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 7bb9ddc80..2cf59b7aa 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1667,7 +1667,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { inversesOfFcts(idx) = inv(invertibles) inversesOfCodomains(idx) = inv(codomainQVars) - // Types known to be infinite, thus there is no need to constrain the domain using image functions. val imgFun = v.decider.fresh("img", (additionalInvArgs map (_.sort)) ++ invertibles.map(_.sort), sorts.Bool) val img = (ts: Seq[Term]) => App(imgFun, additionalInvArgs ++ ts)