Array speedup #1874
Array speedup #1874
Conversation
tautschnig
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
romainbrenguier and
smowton
as code owners
| return false; | ||
| } | ||
|
|
||
| void arrayst::weg_path_condition( |
There was a problem hiding this comment.
should be documented
There was a problem hiding this comment.
using a verb in the function name is generally clearer
|
@tautschnig This PR is still waiting on some changes to address reviewer comments (and now a rebase). Is there a plan to progress on this PR since it is mentioned in others? |
Yes, this is on my pile of TODOs. In terms of performance, it's probably one of the most urgent to work on. Just trying to address the soundness-related ones first. |
|
@tautschnig : Trevor and I have been having some issues with the current array code and may need to look at it in the next few months. Reviewing this / getting it merged might well help us with that. |
tautschnig
force-pushed
the
array-speedup
branch
from
c820fbd to
211fb19
Compare
tautschnig
force-pushed
the
array-speedup
branch
from
211fb19 to
837dbac
Compare
Uses the capabilities of binding_exprt instead of relying on the unrelated replace_exprt to do the right thing.
tautschnig
force-pushed
the
array-speedup
branch
from
837dbac to
31ade23
Compare
All existing tests rely on indexed access to arrays, which is covered by the read-over-write axiom.
There is not really anything wrong in having empty bitvectors, which we otherwise already support (as of e021eef).
The test specification expects that the indices 0, 1, and one other are instantiated. The array theory is only required to do so when also reading from these elements.
This implements Christ and Hoenicke's Weakly Equivalent Arrays (https://arxiv.org/pdf/1405.6939.pdf) with in-place depth-first path enumeration. Co-authored-by: Michael Tautschnig <[email protected]>
tautschnig
force-pushed
the
array-speedup
branch
from
31ade23 to
a02b480
Compare
tautschnig
dismissed
romainbrenguier’s stale review
Code has now largely been rewritten.
|
Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work. |
No description provided.