@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?)

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.

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?)

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

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

@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.

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

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.

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.

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

Good catch - that's now fixed!

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

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.