Add CoW base to value-set #3053
Conversation
This means when the underlying datastructure changes we don't have to update several users.
It appears to be impossible to create a free statement (as opposed to a call to stdlib's free); therefore this path can't be exercised. All the better, since updating everyone's pointers (rather than tracking allocated / deallocated status with the object itself) is surely a mistake in any case.
This is a simple copy-on-write base, intended to allow cheap local analysis on top of a potentially large, possibly mutable global state.
This ensures that in a simple case with constant and non-constant pointers to the same target, the value-set domain appears to behave the same way for both, but in fact optimises by avoiding storing the constant pointer.
smowton
requested review from
chrisr-diffblue,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
One minor note below, but the high-level feedback might be more important:
- I think this could be several PRs, some of the commits seem easy to merge without much discussion.
- Doing work to speed up value-set operations has been on my list for a long time (but surely hasn't happened...) - my thinking was to make use of sharing maps. Did you consider this and, if so, why did you rule it out?
| /// \return a constant pointer to an entry if found, or null otherwise. | ||
| /// Note the pointer may be invalidated by insert operations, including | ||
| /// get_entry. | ||
| const entryt *find_entry(const idt &id) const; |
There was a problem hiding this comment.
Would optionalt be a possibility?
There was a problem hiding this comment.
Personal preference: T * not optionalt<reference_wrapper<T>>
There was a problem hiding this comment.
What about optionalt<T *>? It would more clearly express the intent and remove the role of nullptr as a sentinel value that can accidentally be dereferenced.
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: e8015b8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86048937
|
Sharing map: haven't looked at it in great detail; my loose impression was it was to be employed when there is arbitrary sharing between lots of closely-related trees, whereas for my plan "snapshot once after global init, then normal |
|
(@tautschnig if you're not interested because it's not general enough then fair enough, I'll keep this in our fork, just putting this up to see what you think) |
|
Months later ... @smowton would you mind taking a look at tautschnig@e09a575 as that might solve the problem for you? (It'll require #4274 to compile, though.) |
|
@tautschnig that does look rather good. I haven't used this in symex our side, but I'll give this a go soon. Hadn't realised sharing-map has this delta-view concept, which sounds ideal. |
|
Also I note to really get the benefit here, once @JohnDumbell has simplified the renaming maps they should work similarly, so that |
|
Unnecessary now that we have value-sets backed by |
Add support for a simple CoW base to value-set. This is intended to permit VSA of a function where there is a large global context which we expect to sparsely modify. I don't make any decisions here about how and why to use the facility -- my first stab will be snapshotting the state of the world after __CPROVER_initialize has run -- but simply add support for the feature.
value_sett::do_freewould have been awkward to accommodate, but there didn't seem to be any way to actually use it (I can't find anything that creates acodetwithstatement == ID_free), so I removed this entirely on suspicion that it is dead code. @peterschrammel @tautschnig might disagree.