Use std::forward_list instead of std::map in irept by default [blocks: #3486]

[tautschnig]

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.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[kroening]

Can you split? The constructor seems obvious and trivial, whereas the change to list will require us to do a lot of consulting & benchmarking.

[tautschnig]

@kroening The constructor change is now in #4460.

[tautschnig]

Just for the record: on ReachSafety-ECA with this change we can perform 3819.81 symex_step calls per second, compared to 2752.28 calls per second with develop. I'll now try to figure out what exactly makes so much of a difference.

[tautschnig]

It seems that just about any irept-related operation is cheaper (creating fresh irepts of course, but also irept::operator==).

[danpoe]

On a set of methods from Apache Tika, symex was overall 21% faster with the changes in this PR (20.8s vs 26.4s).

[smowton]

On my large Webgoat run I find running time is practically identical, but the memory usage is down around 30%.

[martin-cs]

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.

[romainbrenguier]

Here are the results on my benchmark:

overall forward lists were about 10% faster

[martin-cs]

That's starting to look quite convincing isn't it?

[tautschnig]

No known regressions (including external feedback), just needs final approval from at least one of @chrisr-diffblue @forejtv @peterschrammel @thk123.

[allredj]

⚠️
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]

⚠️
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.

[allredj]

⚠️
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.