Skip to content

Debugger records all old heaps and their parent heaps #973

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jackstodart wants to merge 22 commits into
base: master
Choose a base branch
from
Open

Debugger records all old heaps and their parent heaps #973

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
93d0c2f
improve debugger display and fix evalInOld bug
jackstodart Mar 5, 2026
f0bf99c
starting to add heap parents
jackstodart May 5, 2026
28049b4
Merge remote-tracking branch 'origin/reworking_debugger' into reworki…
jackstodart May 5, 2026
9a46009
added recordOldHeap function to Verifier and finished reworking old h…
jackstodart May 7, 2026
5566c8e
removing warnings, etc
jackstodart May 7, 2026
d2ff327
added missing recordOldHeap for method calls
jackstodart May 7, 2026
9c89c1e
fixed recordOldHeap in Applying case and changed how we record branch…
jackstodart May 7, 2026
9a71d36
fixed recording wrong old branch conditions
jackstodart May 7, 2026
09a32c7
Merge branch 'master' into reworking_debugger
jackstodart May 7, 2026
ee9a05c
separated old heaps from debug heaps, now records partial produce/con…
jackstodart May 10, 2026
cc256f8
Merge remote-tracking branch 'origin/reworking_debugger' into reworki…
jackstodart May 10, 2026
3b5115a
corrected recording heaps in consumeTlc
jackstodart May 12, 2026
2245b0e
re-re-reworked to only record intermediate heaps as required during i…
jackstodart May 14, 2026
4382632
Merge branch 'master' into reworking_debugger
jackstodart May 14, 2026
b7be739
fixed wrong recording of final heaps after unfold inhale etc
jackstodart May 14, 2026
7d8ddbf
Merge branch 'master' into reworking_debugger
jackstodart May 21, 2026
5098e76
fixed bug in merge for intermediateHeapCause
jackstodart May 21, 2026
f3fad40
fixed some heaps not recorded before unfolding etc, replaced old reco…
jackstodart May 27, 2026
48253a4
fixed heap equality by values, don't replace heaps for new labels
jackstodart May 28, 2026
359c8f6
fixed all sorts of nonsense
jackstodart May 28, 2026
cb912d8
record heaps in loops, but heaps after loops not recorded yet
jackstodart May 29, 2026
03ff629
corrected loop recording, please be finished now
jackstodart May 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 1 addition & 4 deletions src/main/scala/debugger/DebugExp.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,7 @@ object DebugExp {
debugExp
}
}

class DebugExp(val id: Int,
val description : Option[String],
val originalExp : Option[ast.Exp],
Expand Down Expand Up @@ -173,7 +174,6 @@ class DebugExp(val id: Int,

}


class ImplicationDebugExp(id: Int,
description : Option[String],
originalExp : Option[ast.Exp],
Expand Down Expand Up @@ -203,7 +203,6 @@ class ImplicationDebugExp(id: Int,
}
}


class QuantifiedDebugExp(id: Int,
description : Option[String],
isInternal_ : Boolean,
Expand Down Expand Up @@ -234,7 +233,6 @@ class QuantifiedDebugExp(id: Int,
}
}


class DebugExpPrintConfiguration {
var isPrintInternalEnabled: Boolean = false
var nChildrenToShow: Int = 5
Expand Down Expand Up @@ -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"
}
Expand Down
83 changes: 49 additions & 34 deletions src/main/scala/debugger/SiliconDebugger.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,26 +54,43 @@ 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"
}

private def heapString: String = {
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"

storeString + heapString
if (!printConfig.printOldHeaps)
s"Heap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n"
else {
def oldHeapDescriptor(label: String): String = {
if (!s.oldHeapParents.contains(label))
s"Heap $label:\n"
else {
val (parentLabel, cause, branch) = s.oldHeapParents(label).asStrings
val condString = branch.map(" under condition: " + _).getOrElse("")
s"Heap $label:\n\tParent: $parentLabel\n" +
s"\tCause: $cause$condString\n"
}
}
s"Current Heap:\n\t\t${heapToString(s.h)}\n\n" + s.oldHeaps.map {
case (k, v) => s"${oldHeapDescriptor(k)}\t\t${heapToString(v)}\n\n"
}.mkString("")
}
}

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 = {
Expand All @@ -82,51 +99,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
Expand Down Expand Up @@ -166,7 +183,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
}
}

Expand Down Expand Up @@ -306,10 +324,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)
Expand Down Expand Up @@ -367,7 +385,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
Expand Down Expand Up @@ -570,12 +588,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 {
Expand Down
36 changes: 19 additions & 17 deletions src/main/scala/rules/Evaluator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,6 +146,8 @@ object evaluator extends EvaluationRules {
(Q: (State, Term, Option[ast.Exp], Verifier) => VerificationResult)
: VerificationResult = {
val eOpt = Option.when(withExp)(e)
val oldPCS = v.decider.pcs.duplicate()

val resultTerm = e match {
case _: ast.TrueLit => Q(s, True, eOpt, v)
case _: ast.FalseLit => Q(s, False, eOpt, v)
Expand Down Expand Up @@ -204,15 +206,12 @@ object evaluator extends EvaluationRules {

val ve = pve dueTo InsufficientPermission(fa)
v.heapSupporter.evalFieldAccess(s1, fa, tRcvr, eRcvr, ve, v1)((s2, snap, v2) => {
val (debugHeapName, debugLabel) = v1.getDebugOldLabel(s2, fa.pos, Some(magicWandSupporter.getEvalHeap(s2)))
val (_, debugLabel) = v1.getDebugOldLabel(s2, fa.pos, Some(magicWandSupporter.getEvalHeap(s2)))
Copy link
Copy Markdown
Contributor

@marcoeilers marcoeilers May 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So this now assumes that the heap in which we're evaluating the field access has already been recorded, right? But I don't think that's necessarily the case, because of the scenario we I think briefly talked about but then got interrupted (or if there was some conclusion I don't remember it):

// heap h1
inhale acc(x.f) && x.f > 8 && acc(x.g)
// heap h2

x.f is evaluated in a heap that is neither h1 nor h2, but an intermediate one that is h1 + the x.f permission. So I think here you'd get a new debug label that doesn't correspond to an existing heap, but the new heap is also not recorded.

Copy link
Copy Markdown
Author

@jackstodart jackstodart May 14, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK I think this is finally fixed and now we record intermediate heaps when they are used (with either funcapp or field access).

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)(), debugLabel)(fa.pos, fa.info, fa.errT)
})
val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld)
s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s2)))
else s2
Q(s3, snap, newFa, v2)
Q(s2, snap, newFa, v2)
})
})

Expand Down Expand Up @@ -581,7 +580,6 @@ object evaluator extends EvaluationRules {
else ast.DebugLabelledOld(funcAppNew.get, debugLabel)(fapp.pos, fapp.info, fapp.errT)
})

val s1a = if (Verifier.config.enableDebugging()) s1.copy(oldHeaps = s1.oldHeaps + (debugHeapName -> s1.h)) else s1
/* TODO: Does it matter that the above filterNot does not filter out quantified
* variables that are not "raw" function arguments, but instead are used
* in an expression that is used as a function argument?
Expand All @@ -592,7 +590,7 @@ object evaluator extends EvaluationRules {
* Hence, the joinedFApp will take two arguments, namely, i*i and i,
* although the latter is not necessary.
*/
joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](s1a, v1)((s2, v2, QB) => {
joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](s1, v1)((s2, v2, QB) => {
val pres = func.pres.map(_.transform {
/* [Malte 2018-08-20] Two examples of the test suite, one of which is the regression
* for Carbon issue #210, fail if the subsequent code that strips out triggers from
Expand Down Expand Up @@ -706,10 +704,9 @@ object evaluator extends EvaluationRules {
if (s1.isEvalInOld) unfoldingNew.get
else ast.DebugLabelledOld(unfoldingNew.get, debugLabel)(uf.pos, uf.info, uf.errT)
})
val s2a = if (Verifier.config.enableDebugging()) s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> s2.h)) else s2
v2.decider.assert(IsPositive(tPerm)) { // TODO: Replace with permissionSupporter.assertNotNegative
case true =>
joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](s2a, v2)((s3, v3, QB) => {
joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](s2, v2)((s3, v3, QB) => {
val s4 = s3.incCycleCounter(predicate)
.copy(recordVisited = true)
/* [2014-12-10 Malte] The commented code should replace the code following
Expand Down Expand Up @@ -755,7 +752,8 @@ object evaluator extends EvaluationRules {
constrainableARPs = s1.constrainableARPs)
.decCycleCounter(predicate)
val s10 = v5.stateConsolidator(s9).consolidateOptionally(s9, v5)
eval(s10, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))
val s11 = if (withExp) v5.recordOldHeap(s10, s1.h, uf, oldPCS) else s10
eval(s11, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))
})
} else {
produce(s7a, toSf(snap.get), body, pve, v4)((s8, v5) => {
Expand All @@ -767,33 +765,36 @@ object evaluator extends EvaluationRules {
constrainableARPs = s1.constrainableARPs)
.decCycleCounter(predicate)
val s10 = v5.stateConsolidator(s9).consolidateOptionally(s9, v5)
eval(s10, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))})
val s11 = if (withExp) v5.recordOldHeap(s10, s1.h, uf, oldPCS) else s10
eval(s11, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))})
}
})
})(join(eIn.typ, "joined_unfolding", s2a.relevantQuantifiedVariables.map(_._1),
})(join(eIn.typ, "joined_unfolding", s2.relevantQuantifiedVariables.map(_._1),
joinExp, v2))((s12, r12, v7)
=> {
v7.decider.finishDebugSubExp(s"unfolded(${predicate.name})")
Q(s12, r12._1, r12._2, v7)})
case false =>
v2.decider.finishDebugSubExp(s"unfolded(${predicate.name})")
createFailure(pve dueTo NonPositivePermission(ePerm.get), v2, s2a, IsPositive(tPerm), ePermNew.map(p => ast.PermGtCmp(p, ast.NoPerm()())(p.pos, p.info, p.errT)))}}))
createFailure(pve dueTo NonPositivePermission(ePerm.get), v2, s2, IsPositive(tPerm), ePermNew.map(p => ast.PermGtCmp(p, ast.NoPerm()())(p.pos, p.info, p.errT)))}}))
} else {
val unknownValue = v.decider.appliedFresh("recunf", v.symbolConverter.toSort(eIn.typ), s.relevantQuantifiedVariables.map(_._1))
val newFuncRec = s.functionRecorder.recordFreshSnapshot(unknownValue.applicable.asInstanceOf[Function])
Q(s.copy(functionRecorder = newFuncRec), unknownValue, Option.when(withExp)(ast.LocalVarWithVersion("unknownValue", eIn.typ)(eIn.pos, eIn.info, eIn.errT)), v)
}

case apl@ast.Applying(wand, eIn) =>
val (debugHeapName, debugLabel) = v.getDebugOldLabel(s, apl.pos)
val (_, debugLabel) = v.getDebugOldLabel(s, apl.pos)
val joinExp = Option.when(withExp)({
if (s.isEvalInOld) apl
else ast.DebugLabelledOld(apl, debugLabel)(apl.pos, apl.info, apl.errT)
})
val sa = if (Verifier.config.enableDebugging()) s.copy(oldHeaps = s.oldHeaps + (debugHeapName -> s.h)) else s
joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](sa, v)((s1, v1, QB) =>
joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](s, v)((s1, v1, QB) =>
magicWandSupporter.applyWand(s1, wand, pve, v1)((s2, v2) => {
eval(s2, eIn, pve, v2)((s3, t, eInNew, v3) => QB(s3, (t, eInNew), v3))
eval(s2, eIn, pve, v2)((s3, t, eInNew, v3) => {
val s4 = if (withExp) v1.recordOldHeap(s3, s.h, apl, oldPCS) else s3
QB(s4, (t, eInNew), v3)
})
}))(join(eIn.typ, "joined_applying", s.relevantQuantifiedVariables.map(_._1),
joinExp, v))((s4, r4, v4)
=> Q(s4, r4._1, r4._2, v4))
Expand Down Expand Up @@ -1185,6 +1186,7 @@ object evaluator extends EvaluationRules {
}
val s4 = s3.copy(h = s.h,
oldHeaps = s3.oldHeaps + (label -> s3.h),
oldHeapParents = s3.oldHeapParents + (label -> HeapParent(label, Right(e))),
partiallyConsumedHeap = s.partiallyConsumedHeap,
possibleTriggers = newPossibleTriggers,
isEvalInOld = s.isEvalInOld)
Expand Down
Loading
Loading