Fixed chunk with wrong receiver being returned

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
 }
 

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) {

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 {

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.

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}"

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)

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)

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)

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")
+}