From 07bb7d3bfc2554cbc2aa2168b3bcffe71f5132a7 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 5 Dec 2024 23:52:51 +0100 Subject: [PATCH] Debugger improvements (#884) * Better names for old labels that include line information, including value expression for basic field chunks, removed duplicate string representation of debug information * Adding an option to print the term representation of store, heap, assumptions and branch conditions --- src/main/scala/debugger/DebugExp.scala | 17 +++--- src/main/scala/debugger/DebugParser.scala | 2 +- src/main/scala/debugger/SiliconDebugger.scala | 40 ++++++++++--- src/main/scala/interfaces/Verification.scala | 56 +------------------ src/main/scala/interfaces/state/Chunks.scala | 2 +- .../logger/writer/SymbExLogReportWriter.scala | 4 +- src/main/scala/reporting/Converter.scala | 4 +- src/main/scala/rules/Brancher.scala | 2 - src/main/scala/rules/Evaluator.scala | 31 +++++----- src/main/scala/rules/Executor.scala | 19 ++++--- src/main/scala/rules/HavocSupporter.scala | 4 +- src/main/scala/rules/Joiner.scala | 4 +- .../rules/MoreCompleteExhaleSupporter.scala | 9 +-- src/main/scala/rules/PredicateSupporter.scala | 2 +- src/main/scala/rules/Producer.scala | 14 +++-- src/main/scala/rules/StateConsolidator.scala | 19 +++++-- .../scala/rules/SymbolicExecutionRules.scala | 2 +- src/main/scala/state/Chunks.scala | 14 +++-- src/main/scala/state/State.scala | 2 +- src/main/scala/verifier/Verifier.scala | 26 +++++++-- 20 files changed, 142 insertions(+), 131 deletions(-) diff --git a/src/main/scala/debugger/DebugExp.scala b/src/main/scala/debugger/DebugExp.scala index ab1526a6f..cbde4fb58 100644 --- a/src/main/scala/debugger/DebugExp.scala +++ b/src/main/scala/debugger/DebugExp.scala @@ -8,9 +8,8 @@ package viper.silicon.debugger import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.PathConditions -import viper.silicon.state.terms.{And, Exists, Forall, Implies, Quantification, Term, Trigger, True, Var} +import viper.silicon.state.terms.{And, Exists, Forall, Implies, Quantification, Term, Trigger, Var} import viper.silver.ast -import viper.silver.ast.TrueLit import viper.silver.ast.utility.Simplifier import scala.collection.mutable @@ -139,9 +138,10 @@ class DebugExp(val id: Int, } } - def getTopLevelString(currDepth: Int): String = { - val delimiter = if (finalExp.isDefined && description.isDefined) ": " else "" - "\n\t" + ("\t"*currDepth) + "[" + id + "] " + description.getOrElse("") + delimiter + finalExp.getOrElse("") + def getTopLevelString(currDepth: Int, config: DebugExpPrintConfiguration): String = { + val toDisplay = if (config.printInternalTermRepresentation) term else finalExp + val delimiter = if (toDisplay.isDefined && description.isDefined) ": " else "" + "\n\t" + ("\t"*currDepth) + "[" + id + "] " + description.getOrElse("") + delimiter + toDisplay.getOrElse("") } @@ -149,7 +149,7 @@ class DebugExp(val id: Int, if (isInternal_ && !config.isPrintInternalEnabled){ return "" } - getTopLevelString(currDepth) + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) + getTopLevelString(currDepth, config) + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) } def getExpWithId(id: Int, visited: mutable.HashSet[DebugExp]): Option[DebugExp] = { @@ -198,7 +198,7 @@ class ImplicationDebugExp(id: Int, } if (children.nonEmpty) { - getTopLevelString(currDepth) + " ==> " + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) + getTopLevelString(currDepth, config) + " ==> " + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) } else { "true" } @@ -231,7 +231,7 @@ class QuantifiedDebugExp(id: Int, if (qvars.nonEmpty) { "\n\t" + ("\t"*currDepth) + "[" + id + "] " + (if (quantifier == "QA") "forall" else "exists") + " " + qvars.mkString(", ") + " :: " + childrenToString(currDepth, math.max(maxDepth, config.nodeToHierarchyLevelMap.getOrElse(id, 0)), config) } else { - getTopLevelString(currDepth) + getTopLevelString(currDepth, config) } } } @@ -243,6 +243,7 @@ class DebugExpPrintConfiguration { var printHierarchyLevel: Int = 2 var nodeToHierarchyLevelMap: Map[Int, Int] = Map.empty var isPrintAxiomsEnabled: Boolean = false + var printInternalTermRepresentation: Boolean = false def setPrintHierarchyLevel(level: String): Unit ={ printHierarchyLevel = level match { diff --git a/src/main/scala/debugger/DebugParser.scala b/src/main/scala/debugger/DebugParser.scala index 7d5d9acc7..3d2a792e2 100644 --- a/src/main/scala/debugger/DebugParser.scala +++ b/src/main/scala/debugger/DebugParser.scala @@ -18,7 +18,7 @@ class DebugParser extends FastParser { ((pp: (Position, Position)) => PVersionedIdnUseExp(name = parts(0), version = parts(1))(pp)) }.pos - def debugOldLabel[$: P]: P[String] = (StringIn("debug") ~~ CharIn("@") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!.opaque("debugOldLabel") + def debugOldLabel[$: P]: P[String] = (StringIn("debug") ~~ CharIn("@") ~~ CharIn("0-9", "A-Z", "a-z", "#$_.:").repX).!.opaque("debugOldLabel") def debugOldLabelUse[$: P]: P[PVersionedIdnUseExp] = P(debugOldLabel).map { case id => val parts = id.split("@") diff --git a/src/main/scala/debugger/SiliconDebugger.scala b/src/main/scala/debugger/SiliconDebugger.scala index 38091b5b9..9151ba603 100644 --- a/src/main/scala/debugger/SiliconDebugger.scala +++ b/src/main/scala/debugger/SiliconDebugger.scala @@ -6,7 +6,7 @@ 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.terms.Term +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} @@ -26,7 +26,8 @@ case class ProofObligation(s: State, v: Verifier, proverEmits: Seq[String], preambleAssumptions: Seq[DebugAxiom], - branchConditions: Seq[(ast.Exp, ast.Exp)], + branchConditions: Seq[Term], + branchConditionExps: Seq[(ast.Exp, ast.Exp)], assumptionsExp: InsertionOrderedSet[DebugExp], assertion: Term, eAssertion: DebugExp, @@ -52,17 +53,31 @@ case class ProofObligation(s: State, }) + s"\n\t\t${originalErrorReason.readableMessage}\n\n" - private lazy val stateString: String = - s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._2.get}").mkString("\n\t\t")}\n\nHeap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n" + private lazy val stateString: 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\nHeap:\n\t\t${s.h.values.map(chunkString).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\nHeap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n" + } - private lazy val branchConditionString: String = - s"Branch Conditions:\n\t\t${branchConditions.map(bc => Simplifier.simplify(bc._2, true)).filter(bc => bc != ast.TrueLit()()).mkString("\n\t\t")}\n\n" + private lazy val 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" + } private def chunkString(c: Chunk): String = { + if (printConfig.printInternalTermRepresentation) + return c.toString val res = c match { case bc: BasicChunk => + val snapExpString = bc.snapExp match { + case Some(e) => s" -> ${Simplifier.simplify(e, true)}" + case _ => "" + } bc.resourceID match { - case FieldID => s"acc(${bc.argsExp.get.head}.${bc.id}, ${Simplifier.simplify(bc.permExp.get, true)})" + 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 mwc: MagicWandChunk => @@ -215,7 +230,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult], } val obl = Some(ProofObligation(failureContext.state.get, failureContext.verifier.get, failureContext.proverDecls, failureContext.preambleAssumptions, - failureContext.branchConditions, failureContext.assumptions, + failureContext.branchConditions, failureContext.branchConditionExps, failureContext.assumptions, failureContext.failedAssertion, failureContext.failedAssertionExp, None, new DebugExpPrintConfiguration, currResult.message.reason, new DebugResolver(this.pprogram, this.resolver.names), new DebugTranslator(this.pprogram, translator.getMembers()))) @@ -321,7 +336,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult], obl.copy(timeout = Some(timeoutInt)) } } catch { - case e: NumberFormatException => + case _: NumberFormatException => println("Invalid timeout value.") obl } @@ -533,6 +548,13 @@ class SiliconDebugger(verificationResults: List[VerificationResult], case _ => } + println(s"Enter the new value for printInternalTermRepresentation:") + readLine().toLowerCase match { + case "true" | "1" | "t" => obl.printConfig.printInternalTermRepresentation = true + case "false" | "0" | "f" => obl.printConfig.printInternalTermRepresentation = false + case _ => + } + //println(s"Enter the new value for nodeToHierarchyLevelMap:") //obl.printConfig.addHierarchyLevelForId(readLine()) } diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala index 691f35297..ad52d3bf2 100644 --- a/src/main/scala/interfaces/Verification.scala +++ b/src/main/scala/interfaces/Verification.scala @@ -135,7 +135,8 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp], override lazy val toString: String = branchConditionString + counterExampleString + reasonUnknownString } -case class SiliconDebuggingFailureContext(branchConditions: Seq[(ast.Exp, ast.Exp)], +case class SiliconDebuggingFailureContext(branchConditions: Seq[Term], + branchConditionExps: Seq[(ast.Exp, ast.Exp)], counterExample: Option[Counterexample], reasonUnknown: Option[String], state: Option[State], @@ -147,59 +148,8 @@ case class SiliconDebuggingFailureContext(branchConditions: Seq[(ast.Exp, ast.Ex assumptions: InsertionOrderedSet[DebugExp], failedAssertion: Term, failedAssertionExp: DebugExp) extends FailureContext { - lazy val branchConditionString: String = { - if (branchConditions.nonEmpty) { - val branchConditionsString = - branchConditions - .map(_._2) - .map(bc => s"$bc [ ${bc.pos} ] ") - .mkString("\t\t", " ~~> ", "") - - s"\n\t\tunder branch conditions:\n$branchConditionsString" - } else { - "" - } - } - - lazy val counterExampleString: String = { - counterExample.fold("")(ce => s"\n\t\tcounterexample:\n$ce") - } - - lazy val reasonUnknownString: String = { - if (reasonUnknown.isDefined) { - s"\nPotential prover incompleteness: ${reasonUnknown.get}" - } else { - "" - } - } - - lazy val stateString: String = { - if (state.isDefined){ - s"\n\nStore:\n\t\t${state.get.g.values.mkString("\n\t\t")}\n\nHeap:\n\t\t${state.get.h.values.mkString("\n\t\t")}" - } else { - "" - } - } - - lazy val allAssumptionsString: String = { - if (assumptions.nonEmpty) { - val config = new DebugExpPrintConfiguration - config.isPrintInternalEnabled = true - s"\n\nassumptions:\n\t${assumptions.tail.foldLeft[String](assumptions.head.toString(config))((s, de) => de.toString(config) + s)}" - } else { - "" - } - } - - lazy val failedAssertionString: String ={ - if (failedAssertionExp.finalExp.isDefined){ - s"\n\nFailed Assertion:\n\t\t${failedAssertionExp.finalExp.get.toString}" - } else { - failedAssertionExp.description.get - } - } - override lazy val toString: String = branchConditionString + counterExampleString + reasonUnknownString + stateString + allAssumptionsString + failedAssertionString + override lazy val toString: String = "" } trait SiliconCounterexample extends Counterexample { diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala index 329750248..bb1a2b9e2 100644 --- a/src/main/scala/interfaces/state/Chunks.scala +++ b/src/main/scala/interfaces/state/Chunks.scala @@ -33,7 +33,7 @@ trait NonQuantifiedChunk extends GeneralChunk { override def permMinus(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk override def permPlus(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk def withPerm(perm: Term, permExp: Option[ast.Exp]): NonQuantifiedChunk - def withSnap(snap: Term): NonQuantifiedChunk + def withSnap(snap: Term, snapExp: Option[ast.Exp]): NonQuantifiedChunk } trait QuantifiedChunk extends GeneralChunk { diff --git a/src/main/scala/logger/writer/SymbExLogReportWriter.scala b/src/main/scala/logger/writer/SymbExLogReportWriter.scala index 4cae25a80..3e00e4bd4 100644 --- a/src/main/scala/logger/writer/SymbExLogReportWriter.scala +++ b/src/main/scala/logger/writer/SymbExLogReportWriter.scala @@ -31,7 +31,7 @@ object SymbExLogReportWriter { } private def heapChunkToJSON(chunk: Chunk) = chunk match { - case BasicChunk(PredicateID, id, args, _, snap, perm, _) => + case BasicChunk(PredicateID, id, args, _, snap, _, perm, _) => JsObject( "type" -> JsString("basic_predicate_chunk"), "predicate" -> JsString(id.toString), @@ -40,7 +40,7 @@ object SymbExLogReportWriter { "perm" -> TermWriter.toJSON(perm) ) - case BasicChunk(FieldID, id, Seq(receiver), _, snap, perm, _) => + case BasicChunk(FieldID, id, Seq(receiver), _, snap, _, perm, _) => JsObject( "type" -> JsString("basic_field_chunk"), "field" -> JsString(id.toString), diff --git a/src/main/scala/reporting/Converter.scala b/src/main/scala/reporting/Converter.scala index 3c3a34c43..1723233a0 100644 --- a/src/main/scala/reporting/Converter.scala +++ b/src/main/scala/reporting/Converter.scala @@ -345,10 +345,10 @@ object Converter { def extractHeap(h: Iterable[Chunk], model: Model): ExtractedHeap = { var entries: Vector[HeapEntry] = Vector() h foreach { - case c @ BasicChunk(FieldID, _, _, _, _, _, _) => + case c @ BasicChunk(FieldID, _, _, _, _, _, _, _) => val entry = extractField(c, model) entries = entries :+ entry - case c @ BasicChunk(PredicateID, _, _, _, _, _, _) => + case c @ BasicChunk(PredicateID, _, _, _, _, _, _, _) => val entry = extractPredicate(c, model) entries = entries :+ entry case c: BasicChunk => diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 444c61181..fc2422b49 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -6,8 +6,6 @@ package viper.silicon.rules -import viper.silicon.common.collections.immutable.InsertionOrderedSet - import java.util.concurrent._ import viper.silicon.common.concurrency._ import viper.silicon.decider.PathConditionStack diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 09c0e0120..b2d90e42d 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -203,10 +203,10 @@ object evaluator extends EvaluationRules { case fa: ast.FieldAccess if s.qpFields.contains(fa.field) => eval(s, fa.rcv, pve, v)((s1, tRcvr, eRcvr, v1) => { - val debugOldLabel = v1.getDebugOldLabel(s1) + val (debugHeapName, debugLabel) = v1.getDebugOldLabel(s1, fa.pos) val newFa = Option.when(withExp)({ if (s1.isEvalInOld) ast.FieldAccess(eRcvr.get, fa.field)(fa.pos, fa.info, fa.errT) - else ast.DebugLabelledOld(ast.FieldAccess(eRcvr.get, fa.field)(), debugOldLabel)(fa.pos, fa.info, fa.errT) + else ast.DebugLabelledOld(ast.FieldAccess(eRcvr.get, fa.field)(), debugLabel)(fa.pos, fa.info, fa.errT) }) val (relevantChunks, _) = quantifiedChunkSupporter.splitHeap[QuantifiedFieldChunk](s1.h, BasicChunkIdentifier(fa.field.name)) @@ -230,7 +230,7 @@ object evaluator extends EvaluationRules { val fvfLookup = Lookup(fa.field.name, fvfDef.sm, tRcvr) val fr1 = s1.functionRecorder.recordSnapshot(fa, v1.decider.pcs.branchConditions, fvfLookup) val s2 = s1.copy(functionRecorder = fr1) - val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s2))) else s2 + val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s2))) else s2 Q(s3, fvfLookup, newFa, v1) } else { val toAssert = IsPositive(totalPermissions.replace(`?r`, tRcvr)) @@ -245,7 +245,7 @@ object evaluator extends EvaluationRules { else s1.possibleTriggers val s2 = s1.copy(functionRecorder = fr1, possibleTriggers = possTriggers) - val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s2))) else s2 + val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s2))) else s2 Q(s3, fvfLookup, newFa, v1)} } case _ => @@ -317,12 +317,12 @@ object evaluator extends EvaluationRules { chunkSupporter.lookup(s1, s1.h, resource, tArgs, eArgs, ve, v1)((s2, h2, tSnap, v2) => { val fr = s2.functionRecorder.recordSnapshot(fa, v2.decider.pcs.branchConditions, tSnap) val s3 = s2.copy(h = h2, functionRecorder = fr) - val debugOldLabel = v2.getDebugOldLabel(s3) + val (debugHeapName, debugLabel) = v2.getDebugOldLabel(s3, fa.pos) val newFa = Option.when(withExp)({ if (s3.isEvalInOld) ast.FieldAccess(eArgs.get.head, fa.field)(e.pos, e.info, e.errT) - else ast.DebugLabelledOld(ast.FieldAccess(eArgs.get.head, fa.field)(), debugOldLabel)(e.pos, e.info, e.errT) + else ast.DebugLabelledOld(ast.FieldAccess(eArgs.get.head, fa.field)(), debugLabel)(e.pos, e.info, e.errT) }) - val s4 = if (Verifier.config.enableDebugging() && !s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s3))) else s3 + val s4 = if (Verifier.config.enableDebugging() && !s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s3))) else s3 Q(s4, tSnap, newFa, v1) }) }) @@ -340,11 +340,15 @@ object evaluator extends EvaluationRules { Q(s1, t0, e0New.map(ast.Old(_)(e.pos, e.info, e.errT)), v1)) case old@ast.DebugLabelledOld(e0, lbl) => - s.oldHeaps.get(lbl) match { + val heapName = if (lbl.contains("#")) + lbl.substring(0, lbl.indexOf("#")) + else + lbl + s.oldHeaps.get(heapName) match { case None => - createFailure(pve dueTo LabelledStateNotReached(ast.LabelledOld(e0, lbl)(old.pos, old.info, old.errT)), v, s, "labelled state reached") + createFailure(pve dueTo LabelledStateNotReached(ast.LabelledOld(e0, heapName)(old.pos, old.info, old.errT)), v, s, "labelled state reached") case _ => - evalInOldState(s, lbl, e0, pve, v)((s1, t0, _, v1) => + evalInOldState(s, heapName, e0, pve, v)((s1, t0, _, v1) => Q(s1, t0, Some(old), v1)) } @@ -581,9 +585,11 @@ object evaluator extends EvaluationRules { } val currentPermAmount = PermLookup(field.name, pmDef.pm, args.head) v1.decider.prover.comment(s"perm($resacc) ~~> assume upper permission bound") - val exp = Option.when(withExp)(ast.PermLeCmp(ast.DebugLabelledOld(ast.CurrentPerm(resacc)(), v1.getDebugOldLabel(s2))(), ast.FullPerm()())()) + val (debugHeapName, debugLabel) = v1.getDebugOldLabel(s2, resacc.pos, Some(h)) + val exp = Option.when(withExp)(ast.PermLeCmp(ast.DebugLabelledOld(ast.CurrentPerm(resacc)(), debugLabel)(), ast.FullPerm()())()) v1.decider.assume(PermAtMost(currentPermAmount, FullPerm), exp, exp.map(s2.substituteVarsInExp(_))) - (s2, currentPermAmount) + val s3 = if (Verifier.config.enableDebugging()) s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> h)) else s2 + (s3, currentPermAmount) case predicate: ast.Predicate => val (relevantChunks, _) = @@ -1102,7 +1108,6 @@ object evaluator extends EvaluationRules { val assertExpNew = Option.when(withExp)(ast.GeCmp(esNew.get(1), ast.IntLit(0)())(e1.pos, e1.info, e1.errT)) v1.decider.assert(AtLeast(t1, IntLiteral(0))) { case true => - val assertExp2 = Option.when(withExp)(ast.LtCmp(e1, ast.SeqLength(e0)())(e1.pos, e1.info, e1.errT)) val assertExp2New = Option.when(withExp)(ast.LtCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())(e1.pos, e1.info, e1.errT)) v1.decider.assert(Less(t1, SeqLength(t0))) { case true => diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 5840a01c3..3f68978c9 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -378,7 +378,7 @@ object executor extends ExecutionRules { assert(!s.exhaleExt) val pve = AssignmentFailed(ass) eval(s, eRcvr, pve, v)((s1, tRcvr, eRcvrNew, v1) => - eval(s1, rhs, pve, v1)((s2, tRhs, rhsNew, v2) => { + eval(s1, rhs, pve, v1)((s2, tRhs, _, v2) => { val (relevantChunks, otherChunks) = quantifiedChunkSupporter.splitHeap[QuantifiedFieldChunk](s2.h, BasicChunkIdentifier(field.name)) val hints = quantifiedChunkSupporter.extractHints(None, Seq(tRcvr)) @@ -422,7 +422,8 @@ object executor extends ExecutionRules { v1.decider.assume(FieldTrigger(field.name, sm, tRcvr), debugExp2) } val s4 = s3.copy(h = h3 + ch) - val s5 = if (withExp) s4.copy(oldHeaps = s4.oldHeaps + (v.getDebugOldLabel(s4) -> magicWandSupporter.getEvalHeap(s4))) else s4 + val (debugHeapName, _) = v.getDebugOldLabel(s4, fa.pos) + val s5 = if (withExp) s4.copy(oldHeaps = s4.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s4))) else s4 Q(s5, v2) case (Incomplete(_, _), s3, _) => createFailure(pve dueTo InsufficientPermission(fa), v2, s3, "sufficient permission")}})) @@ -438,10 +439,11 @@ object executor extends ExecutionRules { chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), eRcvrNew.map(Seq(_)), FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT)), false, ve, v2, description)((s3, h3, _, v3) => { val (tSnap, _) = ssaifyRhs(tRhs, rhs, rhsNew, field.name, field.typ, v3, s3) val id = BasicChunkIdentifier(field.name) - val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), eRcvrNew.map(Seq(_)), tSnap, FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT))) + val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), eRcvrNew.map(Seq(_)), tSnap, rhsNew, FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT))) chunkSupporter.produce(s3, h3, newChunk, v3)((s4, h4, v4) => { val s5 = s4.copy(h = h4) - val s6 = if (withExp) s5.copy(oldHeaps = s5.oldHeaps + (v4.getDebugOldLabel(s5) -> magicWandSupporter.getEvalHeap(s5))) else s5 + val (debugHeapName, _) = v4.getDebugOldLabel(s5, fa.pos) + val s6 = if (withExp) s5.copy(oldHeaps = s5.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s5))) else s5 Q(s6, v4) }) }) @@ -452,11 +454,13 @@ object executor extends ExecutionRules { val (tRcvr, eRcvrNew) = v.decider.fresh(x) val debugExp = Option.when(withExp)(ast.NeCmp(x, ast.NullLit()())()) val debugExpSubst = Option.when(withExp)(ast.NeCmp(eRcvrNew.get, ast.NullLit()())()) + val (debugHeapName, debugLabel) = v.getDebugOldLabel(s, stmt.pos) v.decider.assume(tRcvr !== Null, debugExp, debugExpSubst) val newChunks = fields map (field => { val p = FullPerm val pExp = Option.when(withExp)(ast.FullPerm()(stmt.pos, stmt.info, stmt.errT)) val snap = v.decider.fresh(field.name, v.symbolConverter.toSort(field.typ), Option.when(withExp)(extractPTypeFromExp(x))) + val snapExp = Option.when(withExp)(ast.DebugLabelledOld(ast.FieldAccess(eRcvrNew.get, field)(), debugLabel)(stmt.pos, stmt.info, stmt.errT)) if (s.qpFields.contains(field)) { val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, field, Seq(tRcvr), snap, v) v.decider.prover.comment("Definitional axioms for singleton-FVF's value") @@ -465,14 +469,15 @@ object executor extends ExecutionRules { quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), Option.when(withExp)(Seq(ast.LocalVarDecl("r", ast.Ref)(stmt.pos, stmt.info, stmt.errT))), field, Seq(tRcvr), Option.when(withExp)(Seq(eRcvrNew.get)), p, pExp, sm, s.program) } else { - BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), Option.when(withExp)(Seq(x)), snap, p, pExp) + BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), Option.when(withExp)(Seq(x)), snap, snapExp, p, pExp) } }) val ts = viper.silicon.state.utils.computeReferenceDisjointnesses(s, tRcvr) val esNew = eRcvrNew.map(rcvr => BigAnd(viper.silicon.state.utils.computeReferenceDisjointnessesExp(s, rcvr))) val s1 = s.copy(g = s.g + (x, (tRcvr, eRcvrNew)), h = s.h + Heap(newChunks)) + val s2 = if (withExp) s1.copy(oldHeaps = s1.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s1))) else s1 v.decider.assume(ts, Option.when(withExp)(DebugExp.createInstance(Some("Reference Disjointness"), esNew, esNew, InsertionOrderedSet.empty)), enforceAssumption = false) - Q(s1, v) + Q(s2, v) case inhale @ ast.Inhale(a) => a match { case _: ast.FalseLit => @@ -536,7 +541,7 @@ object executor extends ExecutionRules { }.getOrElse(sys.error(s"Found $methodName, but no matching field or predicate $resourceName")) val h1 = Heap(s.h.values.map { case bc: BasicChunk if bc.id.name == member.name => - bc.withSnap(freshSnap(bc.snap.sort, v)) + bc.withSnap(freshSnap(bc.snap.sort, v), None) case qfc: QuantifiedFieldChunk if qfc.id.name == member.name => qfc.withSnapshotMap(freshSnap(qfc.fvf.sort, v)) case qpc: QuantifiedPredicateChunk if qpc.id.name == member.name => diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala index eb537163b..b36339812 100644 --- a/src/main/scala/rules/HavocSupporter.scala +++ b/src/main/scala/rules/HavocSupporter.scala @@ -194,12 +194,12 @@ object havocSupporter extends SymbolicExecutionRules { val havockedSnap = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction, Option.when(withExp)(PUnknown())) val cond = replacementCond(lhs, ch.args, condInfo) val magicWandSnapshot = MagicWandSnapshot(Ite(cond, havockedSnap, ch.snap.mwsf)) - ch.withSnap(magicWandSnapshot) + ch.withSnap(magicWandSnapshot, None) case ch => val havockedSnap = freshSnap(ch.snap.sort, v) val cond = replacementCond(lhs, ch.args, condInfo) - ch.withSnap(Ite(cond, havockedSnap, ch.snap)) + ch.withSnap(Ite(cond, havockedSnap, ch.snap), None) } otherChunks ++ newChunks } diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala index 575c80e61..c2dbdb6a9 100644 --- a/src/main/scala/rules/Joiner.scala +++ b/src/main/scala/rules/Joiner.scala @@ -17,6 +17,8 @@ import viper.silicon.utils.ast.{BigAnd, BigOr} import viper.silicon.verifier.Verifier import viper.silver.ast +import scala.annotation.unused + case class JoinDataEntry[D](s: State, data: D, pathConditions: RecordedPathConditions) { // Instead of merging states by calling State.merge, // we can directly merge JoinDataEntries to obtain new States, @@ -26,7 +28,7 @@ case class JoinDataEntry[D](s: State, data: D, pathConditions: RecordedPathCondi v.stateConsolidator(s).consolidate(res, v) } - def pathConditionAwareMergeWithoutConsolidation(other: JoinDataEntry[D], v: Verifier): State = { + def pathConditionAwareMergeWithoutConsolidation(other: JoinDataEntry[D], @unused v: Verifier): State = { State.merge(this.s, this.pathConditions, other.s, other.pathConditions) } } diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 4472c0fb8..9f3190767 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -36,8 +36,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { relevantChunks: Seq[NonQuantifiedChunk], resource: ast.Resource, args: Seq[Term], - argsExp: Option[Seq[ast.Exp]], - v: Verifier) + argsExp: Option[Seq[ast.Exp]]) : (State, Term, Option[ast.Exp]) = { Verifier.config.mapCache(s.ssCache.get((resource, relevantChunks, args))) match { case Some((_, _ ,_permissionSum, _permissionSumExp)) => @@ -102,8 +101,6 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { relevantChunks.foreach(ch => { val argumentEqualities = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 }) - val argumentEqualitiesExp = - Option.when(withExp)(BigAnd(ch.argsExp.get.zip(argsExp.get).map { case (e1, e2) => ast.EqCmp(e1, e2)() })) summarisingSnapshotDefinitions :+= Implies(And(argumentEqualities, IsPositive(ch.perm)), `?s` === ch.snap) @@ -144,7 +141,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { summarisingSnapshotDefinitions = summarisingSnapshotDefinitions map (_.replace(`?s`, summarisingSnapshot)) - val (_, permissionSum, permissionSumExp) = permSummariseOnly(s, relevantChunks, resource, args, argsExp, v) + val (_, permissionSum, permissionSumExp) = permSummariseOnly(s, relevantChunks, resource, args, argsExp) val ssc1 = s.ssCache + ((resource, relevantChunks, args) -> (Some(taggedSummarisingSnapshot), Some(summarisingSnapshotDefinitions), permissionSum, permissionSumExp)) val s1 = s.copy(ssCache = ssc1) @@ -265,7 +262,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { createFailure(ve, v, s1, IsPositive(permSum), permSumExp.map(IsPositive(_)())) }) } else { - val (s1, permSum, permSumExp) = permSummariseOnly(s, relevantChunks, resource, args, argsExp, v) + val (s1, permSum, permSumExp) = permSummariseOnly(s, relevantChunks, resource, args, argsExp) v.decider.assert(IsPositive(permSum)) { case true => Q(s1, h, None, v) diff --git a/src/main/scala/rules/PredicateSupporter.scala b/src/main/scala/rules/PredicateSupporter.scala index 4f4cf6640..7a0f814c1 100644 --- a/src/main/scala/rules/PredicateSupporter.scala +++ b/src/main/scala/rules/PredicateSupporter.scala @@ -113,7 +113,7 @@ object predicateSupporter extends PredicateSupportRules { functionRecorder = s2.functionRecorder.recordFvfAndDomain(smDef)) Q(s3, v1) } else { - val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgs, snap.get.convert(sorts.Snap), tPerm, ePerm) + val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgs, snap.get.convert(sorts.Snap), None, tPerm, ePerm) val s3 = s2.copy(g = s.g, smDomainNeeded = s.smDomainNeeded, permissionScalingFactor = s.permissionScalingFactor, diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index a80fd7a2f..c55e9fdc3 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -332,10 +332,14 @@ object producer extends ProductionRules { quantifiedChunkSupporter.produceSingleLocation(s3, field, Seq(`?r`), Option.when(withExp)(Seq(ast.LocalVarDecl("r", ast.Ref)(accPred.pos, accPred.info, accPred.errT))), Seq(tRcvr), Option.when(withExp)(Seq(eRcvrNew.get)), snap, gain, gainExp, trigger, v3)(Q) } else { - val ch = BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), Option.when(withExp)(Seq(eRcvrNew.get)), snap, gain, gainExp) - chunkSupporter.produce(s3, s3.h, ch, v3)((s4, h4, v4) => - Q(s4.copy(h = h4), v4)) - }}))) + val (debugHeapName, debugLabel) = v3.getDebugOldLabel(s3, accPred.pos) + val snapExp = Option.when(withExp)(ast.DebugLabelledOld(ast.FieldAccess(eRcvrNew.get, field)(), debugLabel)(accPred.pos, accPred.info, accPred.errT)) + val ch = BasicChunk(FieldID, BasicChunkIdentifier(field.name), Seq(tRcvr), Option.when(withExp)(Seq(eRcvrNew.get)), snap, snapExp, gain, gainExp) + chunkSupporter.produce(s3, s3.h, ch, v3)((s4, h4, v4) => { + val s5 = s4.copy(h = h4) + val s6 = if (withExp) s5.copy(oldHeaps = s5.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s4))) else s5 + Q(s6, v4) + })}}))) case ast.PredicateAccessPredicate(ast.PredicateAccess(eArgs, predicateName), perm) => val predicate = s.program.findPredicate(predicateName) @@ -357,7 +361,7 @@ object producer extends ProductionRules { s2, predicate, formalArgs, Option.when(withExp)(predicate.formalArgs), tArgs, eArgsNew, snap, gain, gainExp, trigger, v2)(Q) } else { val snap1 = snap.convert(sorts.Snap) - val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgsNew, snap1, gain, gainExp) + val ch = BasicChunk(PredicateID, BasicChunkIdentifier(predicate.name), tArgs, eArgsNew, snap1, None, gain, gainExp) chunkSupporter.produce(s2, s2.h, ch, v2)((s3, h3, v3) => { if (Verifier.config.enablePredicateTriggersOnInhale() && s3.functionRecorder == NoopFunctionRecorder && !Verifier.config.disableFunctionUnfoldTrigger()) { diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index a8e292100..ba38a7f9f 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -197,10 +197,10 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol // Merges two chunks that are aliases (i.e. that have the same id and the args are proven to be equal) // and returns the merged chunk or None, if the chunks could not be merged private def mergeChunks(fr1: FunctionRecorder, chunk1: Chunk, chunk2: Chunk, v: Verifier): Option[(FunctionRecorder, Chunk, Term)] = (chunk1, chunk2) match { - case (BasicChunk(rid1, id1, args1, args1Exp, snap1, perm1, perm1Exp), BasicChunk(_, _, _, _, snap2, perm2, perm2Exp)) => + case (BasicChunk(rid1, id1, args1, args1Exp, snap1, snap1Exp, perm1, perm1Exp), BasicChunk(_, _, _, _, snap2, _, perm2, perm2Exp)) => val (fr2, combinedSnap, snapEq) = combineSnapshots(fr1, snap1, snap2, perm1, perm2, v) - Some(fr2, BasicChunk(rid1, id1, args1, args1Exp, combinedSnap, PermPlus(perm1, perm2), perm1Exp.map(p1 => ast.PermAdd(p1, perm2Exp.get)())), snapEq) + Some(fr2, BasicChunk(rid1, id1, args1, args1Exp, combinedSnap, snap1Exp, PermPlus(perm1, perm2), perm1Exp.map(p1 => ast.PermAdd(p1, perm2Exp.get)())), snapEq) case (l@QuantifiedFieldChunk(id1, fvf1, condition1, condition1Exp, perm1, perm1Exp, invs1, singletonRcvr1, singletonRcvr1Exp, hints1), r@QuantifiedFieldChunk(_, fvf2, _, _, perm2, perm2Exp, _, _, _, hints2)) => assert(l.quantifiedVars == Seq(`?r`)) @@ -268,6 +268,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol val field = s.program.findField(fieldName) val (sn, smDef, pmDef) = quantifiedChunkSupporter.heapSummarisingMaps(si, field, args, fieldChunks, v) + var sf = sn if (sn.heapDependentTriggers.exists(r => r.isInstanceOf[ast.Field] && r.asInstanceOf[ast.Field].name == fieldName)) { val trigger = FieldTrigger(field.name, smDef.sm, receiver) @@ -275,7 +276,9 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol v.decider.prover.comment(s"Assume upper permission bound for field ${field.name}") val debugExp = if (withExp) { - val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.FieldAccess(receiverExp.localVar, field)())(ast.NoPosition, ast.NoInfo, ast.NoTrafos), v.getDebugOldLabel(sn))() + val (debugHeapName, debugLabel) = v.getDebugOldLabel(sn, ast.NoPosition) + sf = sf.copy(oldHeaps = sf.oldHeaps + (debugHeapName -> sf.h)) + val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.FieldAccess(receiverExp.localVar, field)())(ast.NoPosition, ast.NoInfo, ast.NoTrafos), debugLabel)() val exp = ast.Forall(Seq(receiverExp), Seq(), ast.PermLeCmp(permExp, ast.FullPerm()())())() Some(DebugExp.createInstance(exp, exp)) } else { None } @@ -291,7 +294,9 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol for (chunk <- fieldChunks) { if (chunk.singletonRcvr.isDefined){ val debugExp = if (withExp) { - val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.FieldAccess(chunk.singletonRcvrExp.get, field)())(), v.getDebugOldLabel(sn))() + val (debugHeapName, debugLabel) = v.getDebugOldLabel(sn, ast.NoPosition) + val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.FieldAccess(chunk.singletonRcvrExp.get, field)())(), debugLabel)() + sf = sf.copy(oldHeaps = sf.oldHeaps + (debugHeapName -> sf.h)) val exp = ast.PermLeCmp(permExp, ast.FullPerm()())() Some(DebugExp.createInstance(exp, exp)) } else { None } @@ -304,7 +309,9 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol val debugExp = if (withExp) { val chunkReceiverExp = chunk.quantifiedVarExps.get.head.localVar var permExp: ast.Exp = ast.CurrentPerm(ast.FieldAccess(chunkReceiverExp, field)())(chunkReceiverExp.pos, chunkReceiverExp.info, chunkReceiverExp.errT) - permExp = ast.DebugLabelledOld(permExp, v.getDebugOldLabel(sn))() + val (debugHeapName, debugLabel) = v.getDebugOldLabel(sn, ast.NoPosition) + sf = sf.copy(oldHeaps = sf.oldHeaps + (debugHeapName -> sf.h)) + permExp = ast.DebugLabelledOld(permExp, debugLabel)() val exp = ast.Forall(chunk.quantifiedVarExps.get, Seq(), ast.PermLeCmp(permExp, ast.FullPerm()())())() Some(DebugExp.createInstance(exp, exp)) } else { None } @@ -315,7 +322,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol } } - sn + sf } } } diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index 888028133..6f18728d5 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/src/main/scala/rules/SymbolicExecutionRules.scala @@ -96,7 +96,7 @@ trait SymbolicExecutionRules { if (Verifier.config.enableDebugging()){ val assumptions = v.decider.pcs.assumptionExps - res.failureContexts = Seq(SiliconDebuggingFailureContext(v.decider.pcs.branchConditionExps.map(bce => bce._1 -> bce._2.get), + res.failureContexts = Seq(SiliconDebuggingFailureContext(v.decider.pcs.branchConditions, v.decider.pcs.branchConditionExps.map(bce => bce._1 -> bce._2.get), counterexample, reasonUnknown, Some(s), Some(v), v.decider.prover.getAllEmits(), v.decider.prover.preambleAssumptions, v.decider.macroDecls, v.decider.functionDecls, assumptions, failedAssert, failedAssertExp.get)) } else { diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala index e986faded..638be4288 100644 --- a/src/main/scala/state/Chunks.scala +++ b/src/main/scala/state/Chunks.scala @@ -33,6 +33,7 @@ case class BasicChunk(resourceID: BaseID, args: Seq[Term], argsExp: Option[Seq[ast.Exp]], snap: Term, + snapExp: Option[ast.Exp], perm: Term, permExp: Option[ast.Exp]) extends NonQuantifiedChunk { @@ -49,8 +50,8 @@ case class BasicChunk(resourceID: BaseID, withPerm(PermMinus(perm, newPerm), newPermExp.map(npe => ast.PermSub(permExp.get, npe)())) override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) = withPerm(PermPlus(perm, newPerm), newPermExp.map(npe => ast.PermAdd(permExp.get, npe)())) - override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = BasicChunk(resourceID, id, args, argsExp, snap, newPerm, newPermExp) - override def withSnap(newSnap: Term) = BasicChunk(resourceID, id, args, argsExp, newSnap, perm, permExp) + override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = BasicChunk(resourceID, id, args, argsExp, snap, snapExp, newPerm, newPermExp) + override def withSnap(newSnap: Term, newSnapExp: Option[ast.Exp]) = BasicChunk(resourceID, id, args, argsExp, newSnap, newSnapExp, perm, permExp) override lazy val toString = resourceID match { case FieldID => s"${args.head}.$id -> $snap # $perm" @@ -239,9 +240,12 @@ case class MagicWandChunk(id: MagicWandIdentifier, withPerm(PermPlus(perm, newPerm), newPermExp.map(npe => ast.PermAdd(permExp.get, npe)())) override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = MagicWandChunk(id, bindings, args, argsExp, snap, newPerm, newPermExp) - override def withSnap(newSnap: Term) = newSnap match { - case s: MagicWandSnapshot => MagicWandChunk(id, bindings, args, argsExp, s, perm, permExp) - case _ => sys.error(s"MagicWand snapshot has to be of type MagicWandSnapshot but found ${newSnap.getClass}") + override def withSnap(newSnap: Term, newSnapExp: Option[ast.Exp]) = { + assert(newSnapExp.isEmpty) + newSnap match { + case s: MagicWandSnapshot => MagicWandChunk(id, bindings, args, argsExp, s, perm, permExp) + case _ => sys.error(s"MagicWand snapshot has to be of type MagicWandSnapshot but found ${newSnap.getClass}") + } } override lazy val toString = { diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index 141adc9ce..f1b190e59 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -17,7 +17,7 @@ import viper.silicon.interfaces.state.GeneralChunk import viper.silicon.state.State.OldHeaps import viper.silicon.state.terms.{Term, Var} import viper.silicon.interfaces.state.Chunk -import viper.silicon.state.terms.{And, Ite, NoPerm} +import viper.silicon.state.terms.{And, Ite} import viper.silicon.supporters.PredicateData import viper.silicon.supporters.functions.{FunctionData, FunctionRecorder, NoopFunctionRecorder} import viper.silicon.utils.ast.BigAnd diff --git a/src/main/scala/verifier/Verifier.scala b/src/main/scala/verifier/Verifier.scala index 55235dec3..7990619fa 100644 --- a/src/main/scala/verifier/Verifier.scala +++ b/src/main/scala/verifier/Verifier.scala @@ -11,7 +11,7 @@ import viper.silicon.decider.Decider import viper.silicon.reporting.StateFormatter import viper.silicon.state.terms.{AxiomRewriter, TriggerGenerator} import viper.silicon.rules.StateConsolidationRules -import viper.silicon.state.{IdentifierFactory, State, SymbolConverter} +import viper.silicon.state.{Heap, IdentifierFactory, State, SymbolConverter} import viper.silicon.supporters.{QuantifierSupporter, SnapshotSupporter} import viper.silicon.utils.Counter import viper.silicon.Config @@ -49,13 +49,29 @@ trait Verifier { def reportFurtherErrors(): Boolean = (Verifier.config.numberOfErrorsToReport() > errorsReportedSoFar.get() || Verifier.config.numberOfErrorsToReport() == 0); - def getDebugOldLabel(s: State): String = { - val equalHeaps = s.oldHeaps.filter(h => h._1.startsWith("debug@") && h._2.equals(s.h)).keys + /** + * Returns debug labels for 1) the given heap (will reuse an existing one if one already exists), independently of + * the position of the current expression, and 2) the current expression in the given heap. + * @param s the current state + * @param pos the position of the current expression + * @param h the heap to consider, if not the heap from state s + * @return a pair containing the label of the given heap, and the label of the current expression in the given heap + */ + def getDebugOldLabel(s: State, pos: ast.Position, h: Option[Heap] = None): (String, String) = { + val posString = pos match { + case column: ast.HasLineColumn => s"l:${column.line + 1}.${column.column + 1}" + case _ => s"l:unknown" + } + val heap = h match { + case Some(heap) => heap + case None => s.h + } + val equalHeaps = s.oldHeaps.filter(h => h._1.startsWith("debug@") && h._2.equals(heap)).keys if (equalHeaps.nonEmpty){ - equalHeaps.head + (equalHeaps.head, s"${equalHeaps.head}#$posString") } else { val counter = debugHeapCounter.getAndIncrement() - s"debug@$counter" + (s"debug@$counter", s"debug@$counter#$posString") } } }