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.
This commit is contained in:
parent
3b384edeab
commit
8affad0554
|
@ -33,7 +33,7 @@ protected:
|
|||
symbol_exprt let_symbol;
|
||||
};
|
||||
|
||||
#ifdef HASH_CODE
|
||||
#if HASH_CODE
|
||||
using seen_expressionst = std::unordered_map<exprt, let_count_idt, irep_hash>;
|
||||
#else
|
||||
using seen_expressionst = irep_hash_mapt<exprt, let_count_idt>;
|
||||
|
|
|
@ -16,8 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/std_expr.h>
|
||||
#include <util/byte_operators.h>
|
||||
|
||||
#ifndef HASH_CODE
|
||||
#include <util/irep_hash_container.h>
|
||||
#if !HASH_CODE
|
||||
# include <util/irep_hash_container.h>
|
||||
#endif
|
||||
|
||||
#include <solvers/prop/prop_conv.h>
|
||||
|
|
|
@ -519,7 +519,7 @@ std::size_t irept::number_of_non_comments(const named_subt &named_sub)
|
|||
|
||||
std::size_t irept::hash() const
|
||||
{
|
||||
#ifdef HASH_CODE
|
||||
#if HASH_CODE
|
||||
if(read().hash_code!=0)
|
||||
return read().hash_code;
|
||||
#endif
|
||||
|
@ -543,7 +543,7 @@ std::size_t irept::hash() const
|
|||
|
||||
result = hash_finalize(result, sub.size() + number_of_named_ireps);
|
||||
|
||||
#ifdef HASH_CODE
|
||||
#if HASH_CODE
|
||||
read().hash_code=result;
|
||||
#endif
|
||||
#ifdef IREP_HASH_STATS
|
||||
|
|
|
@ -17,7 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include "irep_ids.h"
|
||||
|
||||
#define SHARING
|
||||
// #define HASH_CODE
|
||||
#ifndef HASH_CODE
|
||||
# define HASH_CODE 1
|
||||
#endif
|
||||
// #define NAMED_SUB_IS_FORWARD_LIST
|
||||
|
||||
#ifdef NAMED_SUB_IS_FORWARD_LIST
|
||||
|
@ -138,7 +140,7 @@ public:
|
|||
named_subt named_sub;
|
||||
subt sub;
|
||||
|
||||
#ifdef HASH_CODE
|
||||
#if HASH_CODE
|
||||
mutable std::size_t hash_code = 0;
|
||||
#endif
|
||||
|
||||
|
@ -147,7 +149,7 @@ public:
|
|||
data.clear();
|
||||
sub.clear();
|
||||
named_sub.clear();
|
||||
#ifdef HASH_CODE
|
||||
#if HASH_CODE
|
||||
hash_code = 0;
|
||||
#endif
|
||||
}
|
||||
|
@ -157,7 +159,7 @@ public:
|
|||
d.data.swap(data);
|
||||
d.sub.swap(sub);
|
||||
d.named_sub.swap(named_sub);
|
||||
#ifdef HASH_CODE
|
||||
#if HASH_CODE
|
||||
std::swap(d.hash_code, hash_code);
|
||||
#endif
|
||||
}
|
||||
|
@ -278,7 +280,7 @@ public:
|
|||
dt &write()
|
||||
{
|
||||
detach();
|
||||
#ifdef HASH_CODE
|
||||
#if HASH_CODE
|
||||
data->hash_code = 0;
|
||||
#endif
|
||||
return *data;
|
||||
|
@ -319,7 +321,7 @@ public:
|
|||
|
||||
dt &write()
|
||||
{
|
||||
#ifdef HASH_CODE
|
||||
#if HASH_CODE
|
||||
data.hash_code = 0;
|
||||
#endif
|
||||
return data;
|
||||
|
|
|
@ -53,7 +53,7 @@ SCENARIO("irept_memory", "[core][utils][irept]")
|
|||
# endif
|
||||
#endif
|
||||
|
||||
#ifdef HASH_CODE
|
||||
#if HASH_CODE
|
||||
const std::size_t hash_code_size = sizeof(std::size_t);
|
||||
#else
|
||||
const std::size_t hash_code_size = 0;
|
||||
|
|
Loading…
Reference in New Issue