Use std::forward_list instead of std::map in irept by default [blocks: #3486]#4458
Use std::forward_list instead of std::map in irept by default [blocks: #3486]#4458tautschnig merged 2 commits intodiffblue:developfrom
Conversation
6a00fc5 to
c8f04da
Compare
|
Can you split? The constructor seems obvious and trivial, whereas the change to list will require us to do a lot of consulting & benchmarking. |
|
Just for the record: on ReachSafety-ECA with this change we can perform 3819.81 |
|
It seems that just about any |
Ensure typet constructor is always compatible with GCC 5's STL [blocks: #4458]
c8f04da to
ff3ab02
Compare
512e9c9 to
d0f270e
Compare
d0f270e to
8abf058
Compare
|
On a set of methods from Apache Tika, symex was overall 21% faster with the changes in this PR (20.8s vs 26.4s). |
|
On my large Webgoat run I find running time is practically identical, but the memory usage is down around 30%. |
|
Although I responded with a 👍 I didn't actually provide meaningfu
l comments to what @martin-cs said:
No worries -- I ignored your responses for a month! :-\
> I think we're going to need some large scale benchmarking before we
> can make this change.
Yes, all proposals or efforts most welcome.
Am a bit short on time but will try when I have some.
> My guess is that there is a clear bias on which of the entries of
> the map are most used. Does it make sense to sort them / use a list
> that pivots them to the front?
We might as well want to measure the median size of the map: I'd
suspect it would be 1 or 2 (expressions carry a type and maybe a
source location).
Yes; that would be the thing to do before thinking of any
optimisations.
|
|
Here are the results on my benchmark: |
|
That's starting to look quite convincing isn't it? |
|
No known regressions (including external feedback), just needs final approval from at least one of @chrisr-diffblue @forejtv @peterschrammel @thk123. |
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 754dbfc).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112051965
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: cfcc7e8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112097093
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
irep.h provides std::map if, and only if, NAMED_SUB_IS_FORWARD_LIST is not set. Also cleanup include guards (pushing them to be the outermost preprocessor directives) and indentation of includes.
This reduces the size of an irept by 5 pointers (i.e., 40 bytes on 64-bit systems). On SV-COMP's ReachSafety-ECA with this change we can perform 3819.81 symex_step calls per second, compared to 2752.28 calls per second with the std::map configuration. The performance improvements are spread across various `irept`-related operations.
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 2b9849a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112365181
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
This reduces the size of an irept by 5 pointers (i.e., 40 bytes on
64-bit systems).
Also make typet constructor compatible with the STL shipped with GCC 5.