From 8c2ddc83f2af20cacb94866b77b9d44ba2f5cf95 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 23 Oct 2024 16:53:19 +0200 Subject: [PATCH] Fixed chunk with wrong receiver being returned --- src/main/scala/interfaces/state/Chunks.scala | 1 + src/main/scala/rules/Executor.scala | 1 - src/main/scala/rules/MagicWandSupporter.scala | 2 +- .../chunks/MoreCompleteExhaleSupporter.scala | 17 +++--- src/main/scala/state/Chunks.scala | 4 ++ src/test/resources/kinduct/actualQP/basic.vpr | 22 +++++++ src/test/resources/kinduct/basic.vpr | 23 ++++++++ src/test/resources/kinduct/forceQP/basic.vpr | 23 ++++++++ src/test/scala/SiliconTestsKInduction2.scala | 58 +++++++++++++++++++ 9 files changed, 142 insertions(+), 9 deletions(-) create mode 100644 src/test/scala/SiliconTestsKInduction2.scala diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala index 641188f15..58d1ba0cc 100644 --- a/src/main/scala/interfaces/state/Chunks.scala +++ b/src/main/scala/interfaces/state/Chunks.scala @@ -30,6 +30,7 @@ trait NonQuantifiedChunk extends GeneralChunk { override def permMinus(perm: Term): NonQuantifiedChunk override def permPlus(perm: Term): NonQuantifiedChunk def withPerm(perm: Term): NonQuantifiedChunk + def withArgs(args: Seq[Term]): NonQuantifiedChunk def withSnap(snap: Term): NonQuantifiedChunk } diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 92be2f1c1..3d36acfe9 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -334,7 +334,6 @@ object executor extends ExecutionRules { val (phase, kRemaining, loopHeap) = s.loopPhaseStack.head val edges = s.methodCfg.outEdges(block) consumes(s, invs, e => LoopInvariantNotPreserved(e), v, true)((sp, _, v) => { - val shuh = s phase match { case LoopPhases.Transferring => if (kRemaining > 1) { diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 6ef56fcc7..4c07ac3bb 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -166,7 +166,7 @@ object magicWandSupporter extends SymbolicExecutionRules { case (r: Complete, sIn, hps, ch, cchs) => (r, sIn, heap +: hps, ch, None +: cchs) case (Incomplete(permsNeeded), sIn, hps, ch, cchs) => - val sInP = sIn // if (hps.nonEmpty) sIn else sIn.copy(loopReadVarStack = sIn.loopReadVarStack.tail.prepended((sIn.loopReadVarStack.head._1, false))) + val sInP = if (hps.nonEmpty) sIn else sIn.copy(loopReadVarStack = sIn.loopReadVarStack.tail.prepended((sIn.loopReadVarStack.head._1, false))) val (success, sOutP, h, cHeap, cch) = consumeFunction(sInP, heap, permsNeeded, v) val sOut = sOutP.copy(loopReadVarStack = sIn.loopReadVarStack) val tEq = (cchs.flatten.lastOption, cch) match { diff --git a/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala index 8d59a38f1..268abe8cb 100644 --- a/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala @@ -266,7 +266,10 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2, functionRecorder = fr1) if (nonEmptyChunks.isEmpty){ assert(v1.decider.check(perms === NoPerm, 0)) - Q(s1p, hs1.head, cHeap2, None, v1) + if (v1.decider.checkSmoke(false)) + Success() + else + Q(s1p, hs1.head, cHeap2, None, v1) } else { Q(s1p, hs1.head, cHeap2, nonEmptyChunks.head.map(_.asInstanceOf[NonQuantifiedChunk].snap), v1) } @@ -333,7 +336,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { var res: (ConsumptionResult, State, Heap, Heap, Option[Chunk]) = (Incomplete(perms), s, h, Heap(), None) actualConsumeCompleteConstrainable(s, relevantChunks, resource, args, perms, ve, v)((s1, updatedChunks, consumedChunks, optSnap, v2) => { //Q(s1, Heap(updatedChunks ++ otherChunks), Heap(consumedChunks), optSnap, v2) - val consumedChunk = Some(consumedChunks.head.withSnap(optSnap.get).withPerm(perms)) + val consumedChunk = Some(consumedChunks.head.withSnap(optSnap.get).withPerm(perms).withArgs(args)) res = (Complete(), s1, Heap(updatedChunks ++ otherChunks), Heap(consumedChunks), consumedChunk) Success() }) @@ -360,7 +363,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (moreNeeded) { val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 }) - val pTaken = if (true || s.functionRecorder != NoopFunctionRecorder || 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. @@ -423,18 +426,18 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { Ite(IsPositive(perms), snap.convert(sorts.Snap), Unit).convert(snap.sort) } if (!moreNeeded) { - val consumedChunk = Some(consumedChunks.head.withSnap(condSnap).withPerm(perms)) + val consumedChunk = Some(consumedChunks.head.withSnap(condSnap).withPerm(perms).withArgs(args)) result = (Complete(), s1, newHeap, consumedHeap, consumedChunk)//Q(s1, newHeap, consumedHeap, Some(condSnap), v1) Success() } else { v1.decider.assert(pNeeded === NoPerm, s1) { case true => - val consumedChunk = Some(consumedChunks.head.withSnap(condSnap).withPerm(perms)) + val consumedChunk = Some(consumedChunks.head.withSnap(condSnap).withPerm(perms).withArgs(args)) result = (Complete(), s1, newHeap, consumedHeap, consumedChunk) //Q(s1, newHeap, consumedHeap, Some(condSnap), v1) Success() case false => - val consumedChunk = if (consumedChunks.isEmpty) None else Some(consumedChunks.head.withSnap(condSnap).withPerm(PermMinus(perms, pNeeded))) + val consumedChunk = if (consumedChunks.isEmpty) None else Some(consumedChunks.head.withSnap(condSnap).withPerm(PermMinus(perms, pNeeded)).withArgs(args)) result = (Incomplete(pNeeded), s1, newHeap, consumedHeap, consumedChunk) //Q(s1, newHeap, consumedHeap, Some(condSnap), v1) Success() @@ -499,7 +502,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (moreNeeded) { val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 }) - val pTaken = if (s.functionRecorder != NoopFunctionRecorder || Verifier.config.useFlyweight) { + val pTaken = if (true) { //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. diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala index 6a3acce73..ce6f27f36 100644 --- a/src/main/scala/state/Chunks.scala +++ b/src/main/scala/state/Chunks.scala @@ -44,6 +44,8 @@ case class BasicChunk(resourceID: BaseID, override def permMinus(newPerm: Term) = withPerm(PermMinus(perm, newPerm)) override def permPlus(newPerm: Term) = withPerm(PermPlus(perm, newPerm)) override def withPerm(newPerm: Term) = BasicChunk(resourceID, id, args, snap, newPerm) + + override def withArgs(args: Seq[Term]) = BasicChunk(resourceID, id, args, snap, perm) override def withSnap(newSnap: Term) = BasicChunk(resourceID, id, args, newSnap, perm) override lazy val toString = resourceID match { @@ -210,6 +212,8 @@ case class MagicWandChunk(id: MagicWandIdentifier, case _ => sys.error(s"MagicWand snapshot has to be of type MagicWandSnapshot but found ${newSnap.getClass}") } + override def withArgs(args: Seq[Term]) = MagicWandChunk(id, bindings, args, snap, perm) + override lazy val toString = { val pos = id.ghostFreeWand.pos match { case rp: viper.silver.ast.HasLineColumn => s"${rp.line}:${rp.column}" diff --git a/src/test/resources/kinduct/actualQP/basic.vpr b/src/test/resources/kinduct/actualQP/basic.vpr index 849bb8e42..6801ce7d3 100644 --- a/src/test/resources/kinduct/actualQP/basic.vpr +++ b/src/test/resources/kinduct/actualQP/basic.vpr @@ -74,6 +74,28 @@ method ms(r1: Ref, r2: Ref, r3: Ref, b: Bool) assert accc(r2, f, 1/2) && accc(r3, f, 1/2) } +method mshuh(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires accc(r1, f, write) && accc(r2, f, 1/2) && accc(r3, f, 1/2) + requires accc(r2, g, write) +{ + var bp: Bool := b + + while (bp) + { + var tmp: Int + tmp := r1.f + tmp := r1.f + if (r2 == r3) + { + r2.f := tmp + 1 + } + //assert tmp == r1.f // should actually pass :/ does not because we dont take all the perm into the loop. + bp := havocBool() + } + r1.f := 0 + assert accc(r2, f, 1/2) && accc(r3, f, 1/2) +} + method msf(r1: Ref, r2: Ref, r3: Ref, b: Bool) requires accc(r1, f, write) && accc(r2, f, 1/2) && accc(r3, f, 1/2) requires accc(r2, g, write) diff --git a/src/test/resources/kinduct/basic.vpr b/src/test/resources/kinduct/basic.vpr index 9f15a982f..19fbf83f7 100644 --- a/src/test/resources/kinduct/basic.vpr +++ b/src/test/resources/kinduct/basic.vpr @@ -72,6 +72,29 @@ method ms(r1: Ref, r2: Ref, r3: Ref, b: Bool) assert acc(r2.f, 1/2) && acc(r3.f, 1/2) } + +method mshuh(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + var bp: Bool := b + + while (bp) + { + var tmp: Int + tmp := r1.f + tmp := r1.f + if (r2 == r3) + { + r2.f := tmp + 1 + } + //assert tmp == r1.f // should actually pass :/ does not because we dont take all the perm into the loop. + bp := havocBool() + } + r1.f := 0 + assert acc(r2.f, 1/2) && acc(r3.f, 1/2) +} + method msf(r1: Ref, r2: Ref, r3: Ref, b: Bool) requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) requires acc(r2.g) diff --git a/src/test/resources/kinduct/forceQP/basic.vpr b/src/test/resources/kinduct/forceQP/basic.vpr index 8f188653f..ae0d8a005 100644 --- a/src/test/resources/kinduct/forceQP/basic.vpr +++ b/src/test/resources/kinduct/forceQP/basic.vpr @@ -84,6 +84,29 @@ method ms(r1: Ref, r2: Ref, r3: Ref, b: Bool) assert acc(r2.f, 1/2) && acc(r3.f, 1/2) } +method mshuh(r1: Ref, r2: Ref, r3: Ref, b: Bool) + requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) + requires acc(r2.g) +{ + forceQPs() + var bp: Bool := b + + while (bp) + { + var tmp: Int + tmp := r1.f + tmp := r1.f + if (r2 == r3) + { + r2.f := tmp + 1 + } + //assert tmp == r1.f // should actually pass :/ does not because we dont take all the perm into the loop. + bp := havocBool() + } + r1.f := 0 + assert acc(r2.f, 1/2) && acc(r3.f, 1/2) +} + method msf(r1: Ref, r2: Ref, r3: Ref, b: Bool) requires acc(r1.f) && acc(r2.f, 1/2) && acc(r3.f, 1/2) requires acc(r2.g) diff --git a/src/test/scala/SiliconTestsKInduction2.scala b/src/test/scala/SiliconTestsKInduction2.scala new file mode 100644 index 000000000..615efadae --- /dev/null +++ b/src/test/scala/SiliconTestsKInduction2.scala @@ -0,0 +1,58 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2022 ETH Zurich. + +import viper.silicon.{Silicon, SiliconFrontend} +import viper.silver.reporter.NoopReporter +import viper.silver.testing.{LocatedAnnotation, MissingOutput, SilSuite, UnexpectedOutput} +import viper.silver.verifier.Verifier + +import java.nio.file.Path + +class SiliconTestsKInduction2 extends SilSuite { + private val siliconTestDirectories = + Seq("kinduct") + + private val silTestDirectories = Seq() + //Seq("all", + // "quantifiedpermissions", "quantifiedpredicates", "quantifiedcombinations", + // "wands", "termination", "refute", + // "examples") + + val testDirectories: Seq[String] = siliconTestDirectories ++ silTestDirectories + + override def frontend(verifier: Verifier, files: Seq[Path]): SiliconFrontend = { + require(files.length == 1, "tests should consist of exactly one file") + + val fe = new SiliconFrontend(NoopReporter) + fe.init(verifier) + fe.reset(files.head) + fe + } + + override def annotationShouldLeadToTestCancel(ann: LocatedAnnotation): Boolean = { + ann match { + case UnexpectedOutput(_, _, _, _, _, _) => true + case MissingOutput(_, _, _, _, _, issue) => issue != 34 + case _ => false + } + } + + val silicon: Silicon = { + val reporter = NoopReporter + val debugInfo = ("startedBy" -> "viper.silicon.SiliconTests") :: Nil + new Silicon(reporter, debugInfo) + } + + def verifiers: Seq[Silicon] = Seq(silicon) + + override def configureVerifiersFromConfigMap(configMap: Map[String, Any]): Unit = { + val args = Silicon.optionsFromScalaTestConfigMap(prefixSpecificConfigMap(configMap).getOrElse("silicon", Map())) + silicon.parseCommandLine(commandLineArguments ++ args :+ Silicon.dummyInputFilename) + } + + val commandLineArguments: Seq[String] = + Seq("--timeout", "600" /* seconds */, "--enableMoreCompleteExhale", "--enableKInduction=2") +}