K-induction without heaps might work

src/main/scala/Config.scala

@@ -647,6 +647,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     case _ => opt
   }
 
+  val kinduction: ScallopOption[Int] = opt[Int]("enableKInduction",
+    descr = "Enable k-induction with the given k (default: 0, i.e., disabled).",
+    default = None,
+    noshort = true
+  )
+
   // DEPRECATED and replaced by exhaleMode.
   val moreCompleteExhale: ScallopOption[Boolean] = opt[Boolean]("enableMoreCompleteExhale",
     descr =  "Warning: This option is deprecated. "

src/main/scala/decider/Decider.scala

@@ -49,7 +49,7 @@ trait Decider {
    *         1. It passes State and Operations to the continuation
    *         2. The implementation reacts to a failing assertion by e.g. a state consolidation
    */
-  def assert(t: Term, timeout: Option[Int] = None)(Q:  Boolean => VerificationResult): VerificationResult
+  def assert(t: Term, s: State, timeout: Option[Int] = None)(Q:  Boolean => VerificationResult): VerificationResult
 
   def fresh(id: String, sort: Sort): Var
   def fresh(id: String, argSorts: Seq[Sort], resultSort: Sort): Function
@@ -238,14 +238,19 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def checkSmoke(isAssert: Boolean = false): Boolean = {
       val timeout = if (isAssert) Verifier.config.assertTimeout.toOption else Verifier.config.checkTimeout.toOption
+
       prover.check(timeout) == Unsat
     }
 
     def check(t: Term, timeout: Int): Boolean = deciderAssert(t, Some(timeout))
 
-    def assert(t: Term, timeout: Option[Int] = Verifier.config.assertTimeout.toOption)
+    def assert(t: Term, s: State, timeout: Option[Int] = Verifier.config.assertTimeout.toOption)
               (Q: Boolean => VerificationResult)
               : VerificationResult = {
+      if (s.loopPhaseStack.nonEmpty && s.loopPhaseStack.head._1 == LoopPhases.Assuming) {
+        assume(t)
+        return Q(true)
+      }
 
       val success = deciderAssert(t, timeout)
 

src/main/scala/rules/Consumer.scala

@@ -6,6 +6,8 @@
 
 package viper.silicon.rules
 
+import viper.silicon.rules.chunks.chunkSupporter
+
 import scala.collection.mutable
 import viper.silver.ast
 import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion
@@ -480,7 +482,7 @@ object consumer extends ConsumptionRules {
             Quantification(q, vars, Implies(transformed, body), trgs, name, isGlob, weight)
           case _ => t
         }
-        v2.decider.assert(termToAssert) {
+        v2.decider.assert(termToAssert, s3) {
           case true =>
             v2.decider.assume(t)
             QS(s3, v2)

src/main/scala/rules/Evaluator.scala

@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silicon.rules.chunks.chunkSupporter
 import viper.silver.ast
 import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, VerifierWarning}
 import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, PreconditionInAppFalse}
@@ -213,7 +214,7 @@ object evaluator extends EvaluationRules {
                 val s2 = s1.copy(functionRecorder = fr1)
                 Q(s2, fvfLookup, v1)
               } else {
-                v1.decider.assert(IsPositive(totalPermissions.replace(`?r`, tRcvr))) {
+                v1.decider.assert(IsPositive(totalPermissions.replace(`?r`, tRcvr)), s1) {
                   case false =>
                     createFailure(pve dueTo InsufficientPermission(fa), v1, s1)
                   case true =>
@@ -247,7 +248,7 @@ object evaluator extends EvaluationRules {
                   val totalPermissions = PermLookup(fa.field.name, pmDef1.pm, tRcvr)
                   IsPositive(totalPermissions)
                 }
-              v1.decider.assert(permCheck) {
+              v1.decider.assert(permCheck, s1) {
                 case false =>
                   createFailure(pve dueTo InsufficientPermission(fa), v1, s1)
                 case true =>
@@ -791,7 +792,7 @@ object evaluator extends EvaluationRules {
         if (s.cycles(predicate) < Verifier.config.recursivePredicateUnfoldings()) {
           evals(s, eArgs, _ => pve, v)((s1, tArgs, v1) =>
             eval(s1, ePerm, pve, v1)((s2, tPerm, v2) =>
-              v2.decider.assert(IsNonNegative(tPerm)) { // TODO: Replace with permissionSupporter.assertNotNegative
+              v2.decider.assert(IsNonNegative(tPerm), s2) { // TODO: Replace with permissionSupporter.assertNotNegative
                 case true =>
                   joiner.join[Term, Term](s2, v2)((s3, v3, QB) => {
                     val s4 = s3.incCycleCounter(predicate)
@@ -854,9 +855,9 @@ object evaluator extends EvaluationRules {
           if (s1.triggerExp) {
             Q(s1, SeqAt(t0, t1), v1)
           } else {
-            v1.decider.assert(AtLeast(t1, IntLiteral(0))) {
+            v1.decider.assert(AtLeast(t1, IntLiteral(0)), s1) {
               case true =>
-                v1.decider.assert(Less(t1, SeqLength(t0))) {
+                v1.decider.assert(Less(t1, SeqLength(t0)), s1) {
                   case true =>
                     Q(s1, SeqAt(t0, t1), v1)
                   case false =>
@@ -869,7 +870,7 @@ object evaluator extends EvaluationRules {
                 val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1)
                 if (s1.retryLevel == 0) {
                   v1.decider.assume(AtLeast(t1, IntLiteral(0)))
-                  v1.decider.assert(Less(t1, SeqLength(t0))) {
+                  v1.decider.assert(Less(t1, SeqLength(t0)), s1) {
                     case true =>
                       failure1 combine Q(s1, SeqAt(t0, t1), v1)
                     case false =>
@@ -892,9 +893,9 @@ object evaluator extends EvaluationRules {
           if (s1.triggerExp) {
             Q(s1, SeqUpdate(t0, t1, t2), v1)
           } else {
-            v1.decider.assert(AtLeast(t1, IntLiteral(0))) {
+            v1.decider.assert(AtLeast(t1, IntLiteral(0)), s1) {
               case true =>
-                v1.decider.assert(Less(t1, SeqLength(t0))) {
+                v1.decider.assert(Less(t1, SeqLength(t0)), s1) {
                   case true =>
                     Q(s1, SeqUpdate(t0, t1, t2), v1)
                   case false =>
@@ -907,7 +908,7 @@ object evaluator extends EvaluationRules {
                 val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1)
                 if (s1.retryLevel == 0) {
                   v1.decider.assume(AtLeast(t1, IntLiteral(0)))
-                  v1.decider.assert(Less(t1, SeqLength(t0))) {
+                  v1.decider.assert(Less(t1, SeqLength(t0)), s1) {
                     case true =>
                       failure1 combine Q(s1, SeqUpdate(t0, t1, t2), v1)
                     case false =>
@@ -1003,7 +1004,7 @@ object evaluator extends EvaluationRules {
       case ast.MapLookup(base, key) =>
         evals2(s, Seq(base, key), Nil, _ => pve, v)({
           case (s1, Seq(baseT, keyT), v1) if s1.triggerExp => Q(s1, MapLookup(baseT, keyT), v1)
-          case (s1, Seq(baseT, keyT), v1) => v1.decider.assert(SetIn(keyT, MapDomain(baseT))) {
+          case (s1, Seq(baseT, keyT), v1) => v1.decider.assert(SetIn(keyT, MapDomain(baseT)), s1) {
             case true => Q(s1, MapLookup(baseT, keyT), v1)
             case false =>
               v1.decider.assume(SetIn(keyT, MapDomain(baseT)))
@@ -1214,7 +1215,7 @@ object evaluator extends EvaluationRules {
                              (Q: (State, Term, Verifier) => VerificationResult)
                              : VerificationResult = {
 
-    v.decider.assert(tDivisor !== tZero){
+    v.decider.assert(tDivisor !== tZero, s){
       case true => Q(s, t, v)
       case false =>
         val failure = createFailure(pve dueTo DivisionByZero(eDivisor), v, s)

src/main/scala/rules/Executor.scala

@@ -6,6 +6,8 @@
 
 package viper.silicon.rules
 
+import viper.silicon.rules.chunks.chunkSupporter
+
 import scala.annotation.unused
 import viper.silver.cfg.silver.SilverCfg
 import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge}
@@ -77,6 +79,29 @@ object executor extends ExecutionRules {
 
   def handleOutEdge(s: State, edge: SilverEdge, v: Verifier): State = {
     edge.kind match {
+      case cfg.Kind.Out if Verifier.config.kinduction.isSupplied =>
+        val (phase, kRemaining, loopHeap) = s.loopPhaseStack.head
+        val sPop = s.copy(loopPhaseStack = s.loopPhaseStack.tail)
+        val sNew = phase match {
+          case LoopPhases.Transferring =>
+            // just merge back
+            val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s.h, s.loopHeapStack.head, v)
+            val s1 = s.copy(functionRecorder = fr1, h = h1,
+              loopHeapStack = s.loopHeapStack.tail, loopReadVarStack = s.loopReadVarStack.tail)
+            s1
+          case LoopPhases.Assuming =>
+            v.decider.assume(False)
+            // assume false
+            val s1 = s.copy(loopHeapStack = s.loopHeapStack.tail, loopReadVarStack = s.loopReadVarStack.tail)
+            s1
+          case LoopPhases.Checking =>
+            // just merge back
+            val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s.h, s.loopHeapStack.head, v)
+            val s1 = s.copy(functionRecorder = fr1, h = h1,
+              loopHeapStack = s.loopHeapStack.tail, loopReadVarStack = s.loopReadVarStack.tail)
+            s1
+        }
+        sNew
       case cfg.Kind.Out =>
         val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s.h, s.invariantContexts.head, v)
         val s1 = s.copy(functionRecorder = fr1, h = h1,
@@ -166,6 +191,19 @@ object executor extends ExecutionRules {
 
       case block @ cfg.LoopHeadBlock(invs, stmts, _) =>
         incomingEdgeKind match {
+          case cfg.Kind.In if Verifier.config.kinduction.isSupplied =>
+            val readPerm = v.decider.fresh(sorts.Perm)
+            v.decider.assume(PermLess(NoPerm, readPerm))
+            val sFirstPhase = s.copy(loopPhaseStack = s.loopPhaseStack.prepended((LoopPhases.Transferring, Verifier.config.kinduction(), block)),
+              loopHeapStack = s.loopHeapStack.prepended(s.h),
+              h = Heap(),
+              loopReadVarStack = s.loopReadVarStack.prepended(readPerm))
+            val edges = s.methodCfg.outEdges(block)
+
+            execs(sFirstPhase, stmts, v)((s4, v3) => {
+              v3.decider.prover.comment("Loop head block: Follow loop-internal edges")
+              follows(s4, edges, WhileFailed, v3)(Q)
+            })
           case cfg.Kind.In =>
             /* We've reached a loop head block via an in-edge. Steps to perform:
              *   - Check loop invariant for self-framingness
@@ -223,10 +261,55 @@ object executor extends ExecutionRules {
                         if (v2.decider.checkSmoke())
                           Success()
                         else {
+                          //if (stmts.nonEmpty)
+                          //  throw new Exception()
                           execs(s3, stmts, v2)((s4, v3) => {
                             v3.decider.prover.comment("Loop head block: Follow loop-internal edges")
                             follows(s4, sortedEdges, WhileFailed, v3)(Q)})}})}})}))
 
+          case _ if Verifier.config.kinduction.isSupplied =>
+            val (phase, kRemaining, loopHeap) = s.loopPhaseStack.head
+            val edges = s.methodCfg.outEdges(block)
+            consumes(s, invs, e => LoopInvariantNotPreserved(e), v)((_, _, v) =>
+              phase match {
+                case LoopPhases.Transferring =>
+                  if (kRemaining > 1) {
+                    val sNew = s.copy(loopPhaseStack = (LoopPhases.Transferring, kRemaining - 1, loopHeap) +: s.loopPhaseStack.tail)
+                    execs(sNew, stmts, v)((s4, v3) => {
+                      follows(s4, edges, WhileFailed, v3)(Q)
+                    })
+                  } else {
+                    /* Havoc local variables that are assigned to in the loop body */
+                    val wvs = s.methodCfg.writtenVars(block)
+                    /* TODO: BUG: Variables declared by LetWand show up in this list, but shouldn't! */
+
+                    val gBody = Store(wvs.foldLeft(s.g.values)((map, x) => map.updated(x, v.decider.fresh(x))))
+                    val sNew = s.copy(g = gBody, h = Heap(),
+                      loopPhaseStack = (LoopPhases.Assuming, Verifier.config.kinduction(), loopHeap) +: s.loopPhaseStack.tail)
+                    execs(sNew, stmts, v)((s4, v3) => {
+                      follows(s4, edges, WhileFailed, v3)(Q)
+                    })
+                  }
+                case LoopPhases.Assuming =>
+                  if (kRemaining > 1) {
+                    val sNew = s.copy(loopPhaseStack = (LoopPhases.Assuming, kRemaining - 1, loopHeap) +: s.loopPhaseStack.tail)
+                    execs(sNew, stmts, v)((s4, v3) => {
+                      follows(s4, edges, WhileFailed, v3)(Q)
+                    })
+                  } else {
+                    val sNew = s.copy(loopPhaseStack = (LoopPhases.Checking, 1, loopHeap) +: s.loopPhaseStack.tail)
+                    execs(sNew, stmts, v)((s4, v3) => {
+                      follows(s4, edges, WhileFailed, v3)(Q)
+                    })
+                  }
+                case LoopPhases.Checking =>
+                  val outEdges = edges filter(_.kind == cfg.Kind.Out)
+                  execs(s, stmts, v)((s4, v3) => {
+                    follows(s4, outEdges, WhileFailed, v3)(Q)
+                  })
+              }
+            )
+
           case _ =>
             /* We've reached a loop head block via an edge other than an in-edge: a normal edge or
              * and out-edge. We consider this edge to be a back-edge and we break the cycle by

src/main/scala/rules/HavocSupporter.scala

@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silicon.rules.chunks.chunkSupporter
 import viper.silicon.interfaces.VerificationResult
 import viper.silicon.interfaces.state.{Chunk, NonQuantifiedChunk}
 import viper.silicon.Map
@@ -17,7 +18,7 @@ import viper.silicon.state.terms.predef.{`?r`, `?s`}
 import viper.silicon.utils.freshSnap
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
-import viper.silver.verifier.errors.{QuasihavocFailed, HavocallFailed}
+import viper.silver.verifier.errors.{HavocallFailed, QuasihavocFailed}
 import viper.silver.verifier.reasons.QuasihavocallNotInjective
 
 object havocSupporter extends SymbolicExecutionRules {
@@ -125,7 +126,7 @@ object havocSupporter extends SymbolicExecutionRules {
         v.decider.prover.comment("Check havocall receiver injectivity")
         val notInjectiveReason = QuasihavocallNotInjective(havocall)
 
-        v.decider.assert(receiverInjectivityCheck) {
+        v.decider.assert(receiverInjectivityCheck, s1) {
           case false => createFailure(pve dueTo notInjectiveReason, v, s1)
           case true =>
             // Generate the inverse axioms

src/main/scala/rules/PermissionSupporter.scala

@@ -23,7 +23,7 @@ object permissionSupporter extends SymbolicExecutionRules {
       case k: Var if s.constrainableARPs.contains(k) =>
         Q(s, v)
       case _ =>
-        v.decider.assert(perms.IsNonNegative(tPerm)) {
+        v.decider.assert(perms.IsNonNegative(tPerm), s) {
           case true => Q(s, v)
           case false => createFailure(pve dueTo NegativePermission(ePerm), v, s)
         }

src/main/scala/rules/PredicateSupporter.scala

@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silicon.rules.chunks.chunkSupporter
 import viper.silver.ast
 import viper.silver.verifier.PartialVerificationError
 import viper.silver.verifier.reasons.InsufficientPermission

src/main/scala/rules/Producer.scala

@@ -6,6 +6,8 @@
 
 package viper.silicon.rules
 
+import viper.silicon.rules.chunks.chunkSupporter
+
 import scala.collection.mutable
 import viper.silver.ast
 import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -862,7 +862,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm))
     val nonNegTerm = Forall(qvars, Implies(FunctionPreconditionTransformer.transform(nonNegImplication, s.program), nonNegImplication), Nil)
     // TODO: Replace by QP-analogue of permissionSupporter.assertNotNegative
-    v.decider.assert(nonNegTerm) {
+    v.decider.assert(nonNegTerm, s) {
       case true =>
 
         /* TODO: Can we omit/simplify the injectivity check in certain situations? */
@@ -882,7 +882,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           }
         v.decider.prover.comment("Check receiver injectivity")
         v.decider.assume(FunctionPreconditionTransformer.transform(receiverInjectivityCheck, s.program))
-        v.decider.assert(receiverInjectivityCheck) {
+        v.decider.assert(receiverInjectivityCheck, s) {
           case true =>
             val ax = inverseFunctions.axiomInversesOfInvertibles
             val inv = inverseFunctions.copy(axiomInversesOfInvertibles = Forall(ax.vars, ax.body, effectiveTriggers))
@@ -1067,7 +1067,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm))
     val nonNegTerm = Forall(qvars, Implies(FunctionPreconditionTransformer.transform(nonNegImplication, s.program), nonNegImplication), Nil)
     // TODO: Replace by QP-analogue of permissionSupporter.assertNotNegative
-    v.decider.assert(nonNegTerm) {
+    v.decider.assert(nonNegTerm, s) {
       case true =>
         val hints = quantifiedChunkSupporter.extractHints(Some(tCond), tArgs)
         val chunkOrderHeuristics =
@@ -1100,7 +1100,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             qidPrefix = qid,
             program = s.program)
         v.decider.prover.comment("Check receiver injectivity")
-        v.decider.assert(receiverInjectivityCheck) {
+        v.decider.assert(receiverInjectivityCheck, s) {
           case true =>
             val qvarsToInvOfLoc = inverseFunctions.qvarsToInversesOf(formalQVars)
             val condOfInvOfLoc = tCond.replace(qvarsToInvOfLoc)

src/main/scala/rules/StateConsolidator.scala

@@ -6,6 +6,8 @@
 
 package viper.silicon.rules
 
+import viper.silicon.rules.chunks.{chunkSupporter, moreCompleteExhaleSupporter}
+
 import scala.annotation.unused
 import viper.silicon.Config
 import viper.silicon.common.collections.immutable.InsertionOrderedSet