Skip to content

Commit 17a4c89

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 6c8954b commit 17a4c89

File tree

1 file changed

+8
-6
lines changed

1 file changed

+8
-6
lines changed

src/util/irep.h

Lines changed: 8 additions & 6 deletions
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 1
22+
#endif
2123
// #define NAMED_SUB_IS_FORWARD_LIST
2224

2325
#ifdef NAMED_SUB_IS_FORWARD_LIST
@@ -138,7 +140,7 @@ class tree_nodet : public ref_count_ift<sharing>
138140
named_subt named_sub;
139141
subt sub;
140142

141-
#ifdef HASH_CODE
143+
#if HASH_CODE
142144
mutable std::size_t hash_code = 0;
143145
#endif
144146

@@ -147,7 +149,7 @@ class tree_nodet : public ref_count_ift<sharing>
147149
data.clear();
148150
sub.clear();
149151
named_sub.clear();
150-
#ifdef HASH_CODE
152+
#if HASH_CODE
151153
hash_code = 0;
152154
#endif
153155
}
@@ -157,7 +159,7 @@ class tree_nodet : public ref_count_ift<sharing>
157159
d.data.swap(data);
158160
d.sub.swap(sub);
159161
d.named_sub.swap(named_sub);
160-
#ifdef HASH_CODE
162+
#if HASH_CODE
161163
std::swap(d.hash_code, hash_code);
162164
#endif
163165
}
@@ -278,7 +280,7 @@ class sharing_treet
278280
dt &write()
279281
{
280282
detach();
281-
#ifdef HASH_CODE
283+
#if HASH_CODE
282284
data->hash_code = 0;
283285
#endif
284286
return *data;
@@ -319,7 +321,7 @@ class non_sharing_treet
319321

320322
dt &write()
321323
{
322-
#ifdef HASH_CODE
324+
#if HASH_CODE
323325
data.hash_code = 0;
324326
#endif
325327
return data;

0 commit comments

Comments
 (0)