Enable HASH_CODE by default to avoid repeated hash computation [blocks: #3486]

[tautschnig]

On SV-COMP benchmarks, hashing accounts for >22% of CPU time (with
profiling enabled).

Do not merge: profiling data to be supplied and further improvements to SUB_IS_LIST are in the queue.

[smowton]

@tautschnig could you explain why using std::list is related to hash caching? Or is that the reduce-dt-size bit (I guess from <start, end, capacity> for vector to <start, end> for list?)

[tautschnig]

Yes, it's the reduce-dt-size bit. But it's not about going from a vector to a list (which as of C++ is three pointers as well), but instead about going from a std::map (which in GNU STL is six pointers) to a list.

[smowton]

Ah, got you, I thought SUB_IS_LIST only affected sub, not named_sub / comments. If we're looking for space saving btw, I note comments is really quite rarely distinguished from named_sub, and by convention their names cannot clash. Should we combine them and filter when we actually want the distinction (during operator== only I think?)

[smowton]

In fact it appears SUB_IS_LIST doesn't affect sub at all! Please rename it.

[allredj]

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: e42bd66).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106400003
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.

[tautschnig]

@peterschrammel @allredj Any idea why this is failing TG builds?

[tautschnig]

@peterschrammel @allredj Any idea why this is failing TG builds?

Never mind, @smowton confirmed that TG already builds with -DHASH_CODE. Will discuss on Monday whether to use #ifndef or just ask TG to remove that option from the build command line.

[smowton]

I favour #ifndef for all such options as that allows -DHASH_CODE=0 on the command-line to make a build without it

[tautschnig]

I favour #ifndef for all such options as that allows -DHASH_CODE=0 on the command-line to make a build without it

Fair point, will include this change in the next push to this branch.

[tautschnig]

Commit message updated to include data points:

On some SV-COMP benchmark categories, hashing accounts for >20% of CPU
time (with profiling enabled) - top five:

• ReachSafety-BitVectors: 29.29% (470.54 seconds, which reduces to 4.39
  seconds; for benchmarks not timing out we save 170 seconds (25%) in
  non-profiling mode)
• Systems_BusyBox_NoOverflows: 27.98% (284.15 seconds, which reduces to
  1.74 seconds; for the 1 benchmark not timing out we save 23 seconds
  (6%) in non-profiling mode)
• Systems_BusyBox_MemSafety: 24.24% (194.74 seconds, which reduces to
  0.93 seconds; no measurable difference on the 2 benchmarks not
  failing/timing out)
• NoOverflows-Other: 18.84% (1127.61 seconds, which reduces to
  23.57 seconds; for benchmarks not timing out we save 5 seconds (7%) in
  non-profiling mode)
• ReachSafety-ControlFlow: 17.75% (1194.04 seconds, which reduces to
  29.17 seconds; for benchmarks not timing out we save 200 seconds (25%)
  in non-profiling mode)

For ReachSafety-ECA it's only 4.7%, which still amounts to 3006.7
seconds. With this change this reduces to 323.07 seconds. On
ReachSafety-ECA, this enables 3055.35 symex_step calls per second over
2752.28 calls per second without this change.

[martin-cs]

HASH_CODE is one of those things we probably should have been doing for some time. If it doesn't work / has performance regressions then we should fix it and I think it should be fixable.

Semi-related : given all of the work on tidying up the constructors for exprts and the like. How far are we from making dts immutable?

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 63081a5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106523249

[smowton]

Your #ifndef actually doesn't permit manual override -- you need to do like

#ifndef HASH_CODE
 #  define HASH_CODE 1
 #endif

...

#if HASH_CODE == 1

At the moment since all the tests just use #ifdef there is in practice no way to override with -D

[tautschnig]

Your #ifndef actually doesn't permit manual override [...]

Good catch - that's now fixed!

[tautschnig]

Marking do-not-merge until we have bisected a possible performance regression and also gathered feedback on this change from customers.

[allredj]

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: abcb3c3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108705935
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.

[tautschnig]

Customer feedback indicates that the degree of performance improvement may vary, but there are no red flags. Will merge as once CI completes its work.