From 71eaad6b435730b359276104c3ee81e1dbddd164 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 30 Mar 2019 14:53:43 +0000 Subject: [PATCH 1/2] Add missing std::map include irep.h provides std::map if, and only if, NAMED_SUB_IS_FORWARD_LIST is not set. Also cleanup include guards (pushing them to be the outermost preprocessor directives) and indentation of includes. --- src/memory-analyzer/gdb_api.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index 1312bebe6fb..f9874b09033 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -22,6 +22,7 @@ Author: Malte Mues #include #include #include +#include #include From 2b9849af73f150bab0ffd592b807aef7eea1feea Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 29 Mar 2019 22:11:30 +0000 Subject: [PATCH 2/2] Use std::forward_list instead of std::map in irept by default This reduces the size of an irept by 5 pointers (i.e., 40 bytes on 64-bit systems). On SV-COMP's ReachSafety-ECA with this change we can perform 3819.81 symex_step calls per second, compared to 2752.28 calls per second with the std::map configuration. The performance improvements are spread across various `irept`-related operations. --- .travis.yml | 4 ++-- src/util/irep.cpp | 4 ++-- src/util/irep.h | 8 +++++--- src/util/irep_hash_container.cpp | 2 +- src/util/irep_serialization.cpp | 6 +++--- src/util/lispirep.cpp | 2 +- src/util/merge_irep.cpp | 10 +++++----- src/util/type.h | 3 ++- unit/util/irep.cpp | 2 +- 9 files changed, 22 insertions(+), 19 deletions(-) diff --git a/.travis.yml b/.travis.yml index da479b9317b..5dff223acd1 100644 --- a/.travis.yml +++ b/.travis.yml @@ -182,7 +182,7 @@ jobs: - WITH_MEMORY_ANALYZER=1 script: echo "Not running any tests for a debug build." - # cmake build using g++-7, enable NAMED_SUB_IS_FORWARD_LIST + # cmake build using g++-7, disable NAMED_SUB_IS_FORWARD_LIST - stage: Test different OS/CXX/Flags os: linux sudo: false @@ -205,7 +205,7 @@ jobs: install: - ccache -z - ccache --max-size=1G - - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST' '-DWITH_MEMORY_ANALYZER=On' + - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST=0' '-DWITH_MEMORY_ANALYZER=On' - git submodule update --init --recursive - cmake --build build -- -j4 script: (cd build; bin/unit "[core][irept]") diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 0099c3cc157..302a1a4a4ff 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -92,7 +92,7 @@ void irept::set(const irep_namet &name, const long long value) void irept::remove(const irep_namet &name) { -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST return get_named_sub().remove(name); #else named_subt &s = get_named_sub(); @@ -120,7 +120,7 @@ irept &irept::add(const irep_namet &name, irept irep) { named_subt &s = get_named_sub(); -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST return s.add(name, std::move(irep)); #else std::pair entry = s.emplace( diff --git a/src/util/irep.h b/src/util/irep.h index 2e2dacf91c0..c57a715cb42 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -20,9 +20,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef HASH_CODE # define HASH_CODE 1 #endif -// #define NAMED_SUB_IS_FORWARD_LIST +#ifndef NAMED_SUB_IS_FORWARD_LIST +# define NAMED_SUB_IS_FORWARD_LIST 1 +#endif -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST # include "forward_list_as_map.h" #else #include @@ -386,7 +388,7 @@ class irept : public non_sharing_treet< irept, #endif -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST forward_list_as_mapt> #else std::map> diff --git a/src/util/irep_hash_container.cpp b/src/util/irep_hash_container.cpp index a4563af27cf..631ebbdd062 100644 --- a/src/util/irep_hash_container.cpp +++ b/src/util/irep_hash_container.cpp @@ -55,7 +55,7 @@ void irep_hash_container_baset::pack( { // we pack: the irep id, the sub size, the subs, the named-sub size, and // each of the named subs with their ids -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST const std::size_t named_sub_size = std::distance(named_sub.begin(), named_sub.end()); #else diff --git a/src/util/irep_serialization.cpp b/src/util/irep_serialization.cpp index 635eb4a2ca8..e8405c4aa13 100644 --- a/src/util/irep_serialization.cpp +++ b/src/util/irep_serialization.cpp @@ -76,14 +76,14 @@ irept irep_serializationt::read_irep(std::istream &in) sub.push_back(reference_convert(in)); } -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST irept::named_subt::iterator before = named_sub.before_begin(); #endif while(in.peek()=='N') { in.get(); irep_idt id = read_string_ref(in); -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST named_sub.emplace_after(before, id, reference_convert(in)); ++before; #else @@ -95,7 +95,7 @@ irept irep_serializationt::read_irep(std::istream &in) { in.get(); irep_idt id = read_string_ref(in); -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST named_sub.emplace_after(before, id, reference_convert(in)); ++before; #else diff --git a/src/util/lispirep.cpp b/src/util/lispirep.cpp index 63b3cca5baa..3a2f2b762ff 100644 --- a/src/util/lispirep.cpp +++ b/src/util/lispirep.cpp @@ -46,7 +46,7 @@ void irep2lisp(const irept &src, lispexprt &dest) dest.value.clear(); dest.type=lispexprt::List; -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST const std::size_t named_sub_size = std::distance(src.get_named_sub().begin(), src.get_named_sub().end()); #else diff --git a/src/util/merge_irep.cpp b/src/util/merge_irep.cpp index 45436b63fff..69977d4b0a1 100644 --- a/src/util/merge_irep.cpp +++ b/src/util/merge_irep.cpp @@ -46,7 +46,7 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const if(sub.size()!=o_sub.size()) return false; -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST if( std::distance(named_sub.begin(), named_sub.end()) != std::distance(o_named_sub.begin(), o_named_sub.end())) @@ -105,12 +105,12 @@ const merged_irept &merged_irepst::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST irept::named_subt::iterator before = dest_named_sub.before_begin(); #endif forall_named_irep(it, src_named_sub) { -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST dest_named_sub.emplace_after( before, it->first, merged(it->second)); // recursive call ++before; @@ -209,12 +209,12 @@ const irept &merge_full_irept::merged(const irept &irep) const irept::named_subt &src_named_sub=irep.get_named_sub(); irept::named_subt &dest_named_sub=new_irep.get_named_sub(); -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST irept::named_subt::iterator before = dest_named_sub.before_begin(); #endif forall_named_irep(it, src_named_sub) { -#ifdef NAMED_SUB_IS_FORWARD_LIST +#if NAMED_SUB_IS_FORWARD_LIST dest_named_sub.emplace_after( before, it->first, merged(it->second)); // recursive call ++before; diff --git a/src/util/type.h b/src/util/type.h index 7f38fc5a335..e8152909706 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -32,7 +32,8 @@ class typet:public irept explicit typet(const irep_idt &_id):irept(_id) { } -#if defined(__clang__) || !defined(__GNUC__) || __GNUC__ >= 6 + // the STL implementation shipped with GCC 5 is broken +#if !defined(__GLIBCXX__) || __GLIBCXX__ >= 20181026 typet(irep_idt _id, typet _subtype) : irept(std::move(_id), {}, {std::move(_subtype)}) { diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp index d9da47bb18b..f80b04a8aa7 100644 --- a/unit/util/irep.cpp +++ b/unit/util/irep.cpp @@ -35,7 +35,7 @@ SCENARIO("irept_memory", "[core][utils][irept]") REQUIRE(sizeof(std::vector) == 3 * sizeof(void *)); #endif -#ifndef NAMED_SUB_IS_FORWARD_LIST +#if !NAMED_SUB_IS_FORWARD_LIST const std::size_t named_size = sizeof(std::map); # ifndef _GLIBCXX_DEBUG # ifdef __APPLE__