Skip to content

Commit 63081a5

Browse files
committed
Enable HASH_CODE by default to avoid repeated hash computation
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.
1 parent 9876561 commit 63081a5

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/util/irep.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,9 @@ Author: Daniel Kroening, [email protected]
1717
#include "irep_ids.h"
1818

1919
#define SHARING
20-
// #define HASH_CODE
20+
#ifndef HASH_CODE
21+
# define HASH_CODE
22+
#endif
2123
// #define NAMED_SUB_IS_FORWARD_LIST
2224

2325
#ifdef NAMED_SUB_IS_FORWARD_LIST

0 commit comments

Comments
 (0)