Debugger records all old heaps and their parent heaps

src/main/scala/debugger/DebugExp.scala

@@ -85,6 +85,7 @@ object DebugExp {
     debugExp
   }
 }
+
 class DebugExp(val id: Int,
                val description : Option[String],
                val originalExp : Option[ast.Exp],
@@ -173,7 +174,6 @@ class DebugExp(val id: Int,
 
 }
 
-
 class ImplicationDebugExp(id: Int,
                           description : Option[String],
                           originalExp : Option[ast.Exp],
@@ -203,7 +203,6 @@ class ImplicationDebugExp(id: Int,
   }
 }
 
-
 class QuantifiedDebugExp(id: Int,
                          description : Option[String],
                          isInternal_ : Boolean,
@@ -234,7 +233,6 @@ class QuantifiedDebugExp(id: Int,
   }
 }
 
-
 class DebugExpPrintConfiguration {
   var isPrintInternalEnabled: Boolean = false
   var nChildrenToShow: Int = 5
@@ -284,7 +282,6 @@ class DebugExpPrintConfiguration {
 }
 
 class DebugAxiom(val description: String, val terms: InsertionOrderedSet[Term]){
-
   override def toString: String = {
     s"$description:\n\t\t${terms.mkString("\n\t\t")}\n"
   }

src/main/scala/debugger/SiliconDebugger.scala

@@ -6,9 +6,9 @@ import viper.silicon.interfaces.state.Chunk
 import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, Success, VerificationResult}
 import viper.silicon.resources.{FieldID, PredicateID}
 import viper.silicon.rules.evaluator
-import viper.silicon.state.Heap
+import viper.silicon.state.State.TemporaryRecord
+import viper.silicon.state._
 import viper.silicon.state.terms.{Term, True}
-import viper.silicon.state.{BasicChunk, IdentifierFactory, MagicWandChunk, QuantifiedFieldChunk, QuantifiedMagicWandChunk, QuantifiedPredicateChunk, State}
 import viper.silicon.utils.ast.simplifyVariableName
 import viper.silicon.verifier.{MainVerifier, Verifier, WorkerVerifier}
 import viper.silver.ast
@@ -54,26 +54,87 @@ case class ProofObligation(s: State,
       }) +
       s"\n\t\t${originalErrorReason.readableMessage}\n\n"
 
-  private def stateString: String = {
-    val storeString = if (printConfig.printInternalTermRepresentation)
+  private def storeString: String = {
+    if (printConfig.printInternalTermRepresentation)
       s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._1}").mkString("\n\t\t")}\n\n"
     else
       s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._2.get}").mkString("\n\t\t")}\n\n"
+  }
 
-    def heapToString(h: Heap): String = h.values.map(chunkString).mkString("\n\t\t")
-    val heapString = if (printConfig.printOldHeaps)
-      s"Current Heap:\n\t\t${heapToString(s.h)}\n\n" + s.oldHeaps.map {case (k, v) => s"Heap $k:\n\t\t${heapToString(v)}\n\n"}.mkString("")
-    else
-      s"Heap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n"
+  private def causeToString(cause: HeapCause): String = {
+    cause match {
+      case InhalePre => "inhale precondition"
+      case ExhalePost => "exhale postcondition"
+      case InhaleInv => "inhale loop invariants"
+      case ExhaleInv => "exhale loop invariants"
+      case MergeContext => "merge framed heap"
+      case CreateLabel => "heap label"
+      case StateConsolidation => "state consolidation"
+      case ExecStmt(stmt) => s"\"$stmt\""
+      case EvalExp(exp) => s"\"$exp\""
+    }
+  }
+
+  private def heapChunksString(h: Heap, isIntermediateHeap: Boolean = false): String = {
+    val tabs = if (isIntermediateHeap) "\t\t\t" else "\t\t"
+    if (h.values.isEmpty) s"$tabs(Empty heap)\n"
+    else h.values.map(c => s"$tabs${chunkString(c)}\n").mkString("")
+  }
+
+  private def debugHeapString(label: String, heapRecord: HeapRecord): String = {
+    val condString = if (heapRecord.branchConds.nonEmpty)
+      "\tNew branch conditions: " + heapRecord.branchConds.map(bc => bc._1.toString).mkString(", ") + "\n"
+    else ""
+    s"Heap $label:\n" +
+      s"\tParent: ${heapRecord.parentLabel}\n" +
+      s"\tCause: ${causeToString(heapRecord.cause)}\n" +
+      condString +
+      heapChunksString(heapRecord.heap) + "\n" +
+      heapRecord.intermediateHeaps.map { case (l, r) => intermediateHeapString(l, r) + "\n" }.mkString("")
+  }
 
-    storeString + heapString
+  private def intermediateHeapString(label: String, heapRecord: IntermediateHeapRecord): String = {
+    val condString = if (heapRecord.newBranchConds.nonEmpty)
+      "\t\tNew branch conditions: " + heapRecord.newBranchConds.map(bc => bc._1.toString).mkString(", ") + "\n"
+    else ""
+    val causeString = heapRecord.intermediateCause match {
+      case Some(cause) => s"\t\tCause: ${causeToString(cause)}\n"
+      case None => ""
+    }
+    s"\tIntermediate heap $label:\n" +
+      causeString +
+      condString +
+      heapChunksString(heapRecord.heap, isIntermediateHeap = true)
   }
 
+  private def tempHeapString(tempRecord: Option[TemporaryRecord]): String = {
+    tempRecord match {
+      case None => ""
+      case Some((label, cause, pcs, heaps)) =>
+        s"Current intermediate heaps:\n" +
+          s"\tCause: ${causeToString(cause)}\n" +
+          heaps.map { case (l, r) => intermediateHeapString(l, r) + "\n" }.mkString("")
+    }
+  }
+
+  private def heapString: String = {
+    if (!printConfig.printOldHeaps)
+      s"Heap:\n${heapChunksString(s.h)}\n"
+    else {
+      s"Current Heap:\n${heapChunksString(s.h)}\n" +
+        s.debugOldHeaps.map { case (label, dh) => debugHeapString(label, dh) }.mkString("") +
+        tempHeapString(s.temporaryHeapRecord)
+    }
+  }
+
+  private def simplify[N <: Node](n: N): N = Simplifier.simplify(n, assumeWelldefinedness = true)
+
   private def branchConditionString: String = {
     if (printConfig.printInternalTermRepresentation)
       s"Branch Conditions:\n\t\t${branchConditions.filter(bc => bc != True).mkString("\n\t\t")}\n\n"
     else
-      s"Branch Conditions:\n\t\t${branchConditionExps.map(bc => Simplifier.simplify(bc._2, true)).filter(bc => bc != ast.TrueLit()()).mkString("\n\t\t")}\n\n"
+      s"Branch Conditions:\n\t\t${branchConditionExps.map(bc => simplify(bc._2))
+        .filter(bc => bc != ast.TrueLit()()).mkString("\n\t\t")}\n\n"
   }
 
   private def chunkString(c: Chunk): String = {
@@ -82,51 +143,51 @@ case class ProofObligation(s: State,
     val res = c match {
       case bc: BasicChunk =>
         val snapExpString = bc.snapExp match {
-          case Some(e) => s" -> ${Simplifier.simplify(e, true)}"
+          case Some(e) => s" -> ${simplify(e)}"
           case _ => ""
         }
         bc.resourceID match {
-          case FieldID => s"acc(${bc.argsExp.get.head}.${bc.id}, ${Simplifier.simplify(bc.permExp.get, true)})$snapExpString"
-          case PredicateID => s"acc(${bc.id}(${bc.argsExp.mkString(", ")}), ${Simplifier.simplify(bc.permExp.get, true)})"
+          case FieldID => s"acc(${bc.argsExp.get.head}.${bc.id}, ${simplify(bc.permExp.get)})$snapExpString"
+          case PredicateID => s"acc(${bc.id}(${bc.argsExp.mkString(", ")}), ${simplify(bc.permExp.get)})"
         }
       case mwc: MagicWandChunk =>
         val shape = mwc.id.ghostFreeWand
         val expBindings = mwc.bindings.map(b => b._1 -> b._2._2.get)
         val instantiated = shape.replace(expBindings)
-        s"acc(${instantiated.toString}, ${Simplifier.simplify(mwc.permExp.get, true)})"
+        s"acc(${instantiated.toString}, ${simplify(mwc.permExp.get)})"
       case qfc: QuantifiedFieldChunk =>
         if (qfc.singletonRcvrExp.isDefined) {
-          val receiver = Simplifier.simplify(qfc.singletonRcvrExp.get, true)
-          val perm = Simplifier.simplify(qfc.permExp.get.replace(qfc.quantifiedVarExps.get.head.localVar, receiver), true)
-          s"acc(${receiver}.${qfc.id}, ${perm})"
+          val receiver = simplify(qfc.singletonRcvrExp.get)
+          val perm = simplify(qfc.permExp.get.replace(qfc.quantifiedVarExps.get.head.localVar, receiver))
+          s"acc($receiver.${qfc.id}, $perm)"
         } else {
           val varsString = qfc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
           val qvarsString = "forall " + qfc.invs.get.qvarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
-          val varsEqualString = qfc.quantifiedVarExps.get.zip(qfc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
-          s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${qfc.quantifiedVarExps.get.head.name}.${qfc.id}, ${Simplifier.simplify(qfc.permExp.get, true)})"
+          val varsEqualString = qfc.quantifiedVarExps.get.zip(qfc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${simplify(v._2)}").mkString(" && ")
+          s"forall $varsString :: $qvarsString :: $varsEqualString ==> acc(${qfc.quantifiedVarExps.get.head.name}.${qfc.id}, ${simplify(qfc.permExp.get)})"
         }
       case qpc: QuantifiedPredicateChunk =>
         if (qpc.singletonArgExps.isDefined) {
-          s"acc(${qpc.id}(${qpc.singletonArgExps.get.map(e => Simplifier.simplify(e, true)).mkString(", ")}), ${Simplifier.simplify(qpc.permExp.get, true)})"
+          s"acc(${qpc.id}(${qpc.singletonArgExps.get.map(e => simplify(e)).mkString(", ")}), ${simplify(qpc.permExp.get)})"
         } else {
           val varsString = qpc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
           val qvarsString = "forall " + qpc.invs.get.qvarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
-          val varsEqualString = qpc.quantifiedVarExps.get.zip(qpc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
-          s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${qpc.id}(${qpc.quantifiedVarExps.get.map(_.name).mkString(", ")}), ${Simplifier.simplify(qpc.permExp.get, true)})"
+          val varsEqualString = qpc.quantifiedVarExps.get.zip(qpc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${simplify(v._2)}").mkString(" && ")
+          s"forall $varsString :: $qvarsString :: $varsEqualString ==> acc(${qpc.id}(${qpc.quantifiedVarExps.get.map(_.name).mkString(", ")}), ${simplify(qpc.permExp.get)})"
         }
       case qwc: QuantifiedMagicWandChunk =>
         val shape = qwc.id.ghostFreeWand
         if (qwc.singletonArgExps.isDefined) {
-          val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.singletonArgExps.get).map(e => e._1 -> Simplifier.simplify(e._2, true)).toMap)
-          val permReplaced = Simplifier.simplify(qwc.permExp.get.replace(qwc.quantifiedVarExps.get.zip(qwc.singletonArgExps.get).map(e => e._1.localVar -> e._2).toMap), true)
+          val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.singletonArgExps.get).map(e => e._1 -> simplify(e._2)).toMap)
+          val permReplaced = simplify(qwc.permExp.get.replace(qwc.quantifiedVarExps.get.zip(qwc.singletonArgExps.get).map(e => e._1.localVar -> e._2).toMap))
 
-          s"acc(${instantiated.toString}, ${permReplaced})"
+          s"acc(${instantiated.toString}, $permReplaced)"
         } else{
           val varsString = qwc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
           val qvarsString = "forall " + qwc.invs.get.qvarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
-          val varsEqualString = qwc.quantifiedVarExps.get.zip(qwc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
-          val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.invs.get.invertibleExps.get).map(e => e._1 -> Simplifier.simplify(e._2, true)).toMap)
-          s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${instantiated}, ${Simplifier.simplify(qwc.permExp.get, true)})"
+          val varsEqualString = qwc.quantifiedVarExps.get.zip(qwc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${simplify(v._2)}").mkString(" && ")
+          val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.invs.get.invertibleExps.get).map(e => e._1 -> simplify(e._2)).toMap)
+          s"forall $varsString :: $qvarsString :: $varsEqualString ==> acc($instantiated, ${simplify(qwc.permExp.get)})"
         }
     }
     res
@@ -166,7 +227,8 @@ case class ProofObligation(s: State,
   }
 
   override def toString: String = {
-    "\n" + originalErrorInfo + branchConditionString + stateString + axiomsString + declarationsString + assumptionString + assertionString
+    "\n" + originalErrorInfo + branchConditionString + storeString + heapString +
+      axiomsString + declarationsString + assumptionString + assertionString
   }
 }
 
@@ -306,10 +368,10 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
             obl = removeAssumptions(obl)
             println(s"Current obligation:\n$obl")
           case "af" | "assume" | "add free assumption" =>
-            obl = addAssumptions(obl, true)
+            obl = addAssumptions(obl, free = true)
             println(s"Current obligation:\n$obl")
           case "ap" | "assert" | "add and prove assumption" =>
-            obl = addAssumptions(obl, false)
+            obl = addAssumptions(obl, free = false)
             println(s"Current obligation:\n$obl")
           //case "ass" | "assertion" | "set assertion" =>
           //  obl = chooseAssertion(obl)
@@ -367,7 +429,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     }
   }
 
-  private def showAssumptions(obl: ProofObligation) = {
+  private def showAssumptions(obl: ProofObligation): Unit = {
     println(s"Enter the assumption you want to zoom in on:")
     val userInput = readLine()
     val indexOpt = userInput.trim.toIntOption
@@ -570,12 +632,9 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
       case "false" | "0" | "f" => obl.printConfig.printOldHeaps = false
       case _ =>
     }
-
-    //println(s"Enter the new value for nodeToHierarchyLevelMap:")
-    //obl.printConfig.addHierarchyLevelForId(readLine())
   }
 
-  private def printSingleAssumption(obl: ProofObligation): Unit={
+  private def printSingleAssumption(obl: ProofObligation): Unit = {
     println(s"Enter the id of the assumption that should be printed:")
     val userInput = readLine()
     userInput.toIntOption match {

src/main/scala/rules/ChunkSupporter.scala

@@ -91,7 +91,7 @@ object chunkSupporter extends ChunkSupportRules {
            * registered with the function recorder. However, since nothing was consumed,
            * returning the unit snapshot seems more appropriate.
            */
-          val fresh = v2.decider.fresh(sorts.Snap, Option.when(withExp)(PUnknown()))
+          val fresh = v2.decider.fresh(sorts.Snap, Option.when(debugOn)(PUnknown()))
           val s3 = s2.copy(functionRecorder = s2.functionRecorder.recordFreshSnapshot(fresh.applicable))
           Q(s3, h2, Some(fresh), v2)
         case None => Q(s2, h2, None, v2)
@@ -164,7 +164,7 @@ object chunkSupporter extends ChunkSupportRules {
       val interpreter = new NonQuantifiedPropertyInterpreter(heap.values, v)
       val resource = Resources.resourceDescriptions(chunk.resourceID)
       val pathCond = interpreter.buildPathConditionsForChunk(chunk, resource.instanceProperties(s.mayAssumeUpperBounds))
-      pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
+      pathCond.foreach(p => v.decider.assume(p._1, Option.when(debugOn)(DebugExp.createInstance(p._2, p._2))))
     }
 
     findChunk[NonQuantifiedChunk](h.values, id, args, v) match {
@@ -191,7 +191,7 @@ object chunkSupporter extends ChunkSupportRules {
         } else {
           if (v.decider.check(ch.perm !== NoPerm, Verifier.config.checkTimeout())) {
             val constraintExp = permsExp.map(pe => ast.PermLtCmp(pe, ch.permExp.get)(pe.pos, pe.info, pe.errT))
-            v.decider.assume(PermLess(perms, ch.perm), Option.when(withExp)(DebugExp.createInstance(constraintExp, constraintExp)))
+            v.decider.assume(PermLess(perms, ch.perm), Option.when(debugOn)(DebugExp.createInstance(constraintExp, constraintExp)))
             val newPermExp = permsExp.map(pe => ast.PermSub(ch.permExp.get, pe)(pe.pos, pe.info, pe.errT))
             val newChunk = ch.withPerm(PermMinus(ch.perm, perms), newPermExp)
             val takenChunk = ch.withPerm(perms, permsExp)
@@ -257,7 +257,7 @@ object chunkSupporter extends ChunkSupportRules {
         Q(s, ch.snap, v)
       case _ if v.decider.checkSmoke(true) =>
         if (s.isInPackage) {
-          val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(withExp)(PUnknown()))
+          val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(debugOn)(PUnknown()))
           Q(s, snap, v)
         } else {
           Success() // TODO: Mark branch as dead?