Heapster memblock prover improvements#1406

Merged

eddywestbrook merged 11 commits intomasterfrom heapster-memblock-prover-improvements

Aug 6, 2021

+875-577

Commits on Aug 3, 2021

bugfix: there was an infinite loop that kept copying a block permission before eliminating it and would then go right back to trying to eliminate that same permission again...
Eddy Westbrook
committed
added debug output for return statements, which is long overdue
Eddy Westbrook
committed
changed implElimLLVMBlock to always only eliminate one step of a memblock permission; changed proveVarLLVMBlocks to focus first on eliminating memblock permissions on the left that overlap with but…
Eddy Westbrook
committed
unfold defined shapes on the left when their ranges match a shape we are trying to prove on the right
Eddy Westbrook
committed
whoops, do not try to eliminate LHS block perms when we are proving an empty block perm on the right
Eddy Westbrook
committed

Commits on Aug 4, 2021

Commits on Aug 5, 2021

Merge remote-tracking branch 'origin/master' into heapster-memblock-prover-improvements
Eddy Westbrook
committed

Commits on Aug 6, 2021

reorganized proveVarLLVMBlocks into two separate stages represented by two separate functions, all of which now take lists of multi-bindings instead of multi-bindings of lists
Eddy Westbrook
committed
whoops, forgot to change a shadowed variable...
Eddy Westbrook
committed
implemented a few more suggestions from Eric Mertens
Eddy Westbrook
committed