Debugger records all old heaps and their parent heaps#973
Conversation
…eaps in Executor, Evaluator
| 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))) |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
OK I think this is finally fixed and now we record intermediate heaps when they are used (with either funcapp or field access).
| def recordOldHeap(s: State, heap: Heap, parent: Heap, | ||
| cause: Either[ast.Stmt, ast.Exp], | ||
| oldPCS: Option[PathConditionStack]): State = { | ||
| val childLabel = getDebugHeapLabel(s, Some(heap)) |
There was a problem hiding this comment.
Somehow this feels like we're mixing debug and old heaps in a way we maybe shouldn't. This will generate a debug heap labeleven when debugging is not enabled, e.g. when this is called for an ast.Label statement, right?
Maybe we could use this as an opportunity to separate actual old heaps and debug heaps, and record the parents only for the debug heaps?
There was a problem hiding this comment.
Yeah probably a good idea, I will re-rework this to separate the heaps then.
| Some(mergeHeap(heap1, cond1._1, cond1._2, heap2, cond2._1, cond2._2)) | ||
| })) | ||
|
|
||
| val oldHeapParents3 = Map.from(mergeMaps(oldHeapParents1, (), oldHeapParents2, ()) |
There was a problem hiding this comment.
My understanding is that since the heap parents already contain branch condition information, you can probably just take oldHeapParents1 ++ oldHeapParents2?
…sume heaps, not all checked yet
…nhale, unfolding etc
2 participants
Changing the debugger from recording only heaps referenced in assumptions, to recording all heaps when they are created. Also records the statement or expression that caused the heap to be created, and any possible branch conditions.
Debugger now prints the parents and causes when printOldHeaps is on; it's a little verbose maybe, but it's off by default anyway.