Skip to content

Commit dbaeda0

Browse files
tautschnigtautschnig
committed
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.
1 parent 64af489 commit dbaeda0

File tree

9 files changed

+32
-29
lines changed

9 files changed

+32
-29
lines changed

‎.travis.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -177,7 +177,7 @@ jobs:
177177
- CCACHE_CPP2=yes
178178
script: echo "Not running any tests for a debug build."
179179

180-
# cmake build using g++-7, enable NAMED_SUB_IS_FORWARD_LIST
180+
# cmake build using g++-7, disable NAMED_SUB_IS_FORWARD_LIST
181181
- stage: Test different OS/CXX/Flags
182182
os: linux
183183
sudo: false
@@ -200,7 +200,7 @@ jobs:
200200
install:
201201
- ccache -z
202202
- ccache --max-size=1G
203-
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST'
203+
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST=0'
204204
- git submodule update --init --recursive
205205
- cmake --build build -- -j4
206206
script: (cd build; bin/unit "[core][irept]")

‎src/util/irep.cpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ Author: Daniel Kroening, [email protected]
1717
#include "string_hash.h"
1818
#include "irep_hash.h"
1919

20-
#ifdef NAMED_SUB_IS_FORWARD_LIST
21-
#include <algorithm>
20+
#if NAMED_SUB_IS_FORWARD_LIST
21+
# include <algorithm>
2222
#endif
2323

2424
#ifdef IREP_DEBUG
@@ -27,7 +27,7 @@ Author: Daniel Kroening, [email protected]
2727

2828
irept nil_rep_storage;
2929

30-
#ifdef NAMED_SUB_IS_FORWARD_LIST
30+
#if NAMED_SUB_IS_FORWARD_LIST
3131
static inline bool named_subt_order(
3232
const std::pair<irep_namet, irept> &a,
3333
const irep_namet &b)
@@ -77,7 +77,7 @@ const irep_idt &irept::get(const irep_namet &name) const
7777
{
7878
const named_subt &s = get_named_sub();
7979

80-
#ifdef NAMED_SUB_IS_FORWARD_LIST
80+
#if NAMED_SUB_IS_FORWARD_LIST
8181
named_subt::const_iterator it=named_subt_lower_bound(s, name);
8282

8383
if(it==s.end() ||
@@ -132,7 +132,7 @@ void irept::remove(const irep_namet &name)
132132
{
133133
named_subt &s = get_named_sub();
134134

135-
#ifdef NAMED_SUB_IS_FORWARD_LIST
135+
#if NAMED_SUB_IS_FORWARD_LIST
136136
named_subt::iterator it=named_subt_lower_bound(s, name);
137137

138138
if(it!=s.end() && it->first==name)
@@ -151,7 +151,7 @@ const irept &irept::find(const irep_namet &name) const
151151
{
152152
const named_subt &s = get_named_sub();
153153

154-
#ifdef NAMED_SUB_IS_FORWARD_LIST
154+
#if NAMED_SUB_IS_FORWARD_LIST
155155
named_subt::const_iterator it=named_subt_lower_bound(s, name);
156156

157157
if(it==s.end() ||
@@ -171,7 +171,7 @@ irept &irept::add(const irep_namet &name)
171171
{
172172
named_subt &s = get_named_sub();
173173

174-
#ifdef NAMED_SUB_IS_FORWARD_LIST
174+
#if NAMED_SUB_IS_FORWARD_LIST
175175
named_subt::iterator it=named_subt_lower_bound(s, name);
176176

177177
if(it==s.end() ||
@@ -193,7 +193,7 @@ irept &irept::add(const irep_namet &name, irept irep)
193193
{
194194
named_subt &s = get_named_sub();
195195

196-
#ifdef NAMED_SUB_IS_FORWARD_LIST
196+
#if NAMED_SUB_IS_FORWARD_LIST
197197
named_subt::iterator it=named_subt_lower_bound(s, name);
198198

199199
if(it==s.end() ||
@@ -304,7 +304,7 @@ bool irept::full_eq(const irept &other) const
304304
const irept::named_subt &i1_named_sub=get_named_sub();
305305
const irept::named_subt &i2_named_sub=other.get_named_sub();
306306

307-
#ifdef NAMED_SUB_IS_FORWARD_LIST
307+
#if NAMED_SUB_IS_FORWARD_LIST
308308
if(
309309
std::distance(i1_named_sub.begin(), i1_named_sub.end()) !=
310310
std::distance(i2_named_sub.begin(), i2_named_sub.end()))
@@ -568,7 +568,7 @@ std::size_t irept::full_hash() const
568568
result=hash_combine(result, it->second.full_hash());
569569
}
570570

571-
#ifdef NAMED_SUB_IS_FORWARD_LIST
571+
#if NAMED_SUB_IS_FORWARD_LIST
572572
const std::size_t named_sub_size =
573573
std::distance(named_sub.begin(), named_sub.end());
574574
#else

‎src/util/irep.h

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,12 @@ Author: Daniel Kroening, [email protected]
2020
#ifndef HASH_CODE
2121
# define HASH_CODE 1
2222
#endif
23-
// #define NAMED_SUB_IS_FORWARD_LIST
23+
#ifndef NAMED_SUB_IS_FORWARD_LIST
24+
# define NAMED_SUB_IS_FORWARD_LIST 1
25+
#endif
2426

25-
#ifdef NAMED_SUB_IS_FORWARD_LIST
26-
#include <forward_list>
27+
#if NAMED_SUB_IS_FORWARD_LIST
28+
# include <forward_list>
2729
#else
2830
#include <map>
2931
#endif
@@ -126,7 +128,7 @@ class tree_nodet : public ref_count_ift<sharing>
126128
// use std::forward_list or std::vector< unique_ptr<T> > to save
127129
// memory and increase efficiency.
128130

129-
#ifdef NAMED_SUB_IS_FORWARD_LIST
131+
#if NAMED_SUB_IS_FORWARD_LIST
130132
typedef std::forward_list<std::pair<irep_namet, treet>> named_subt;
131133
#else
132134
typedef std::map<irep_namet, treet> named_subt;

‎src/util/irep_hash_container.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ void irep_hash_container_baset::pack(
5555
{
5656
// we pack: the irep id, the sub size, the subs, the named-sub size, and
5757
// each of the named subs with their ids
58-
#ifdef NAMED_SUB_IS_FORWARD_LIST
58+
#if NAMED_SUB_IS_FORWARD_LIST
5959
const std::size_t named_sub_size =
6060
std::distance(named_sub.begin(), named_sub.end());
6161
#else

‎src/util/irep_serialization.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -76,14 +76,14 @@ irept irep_serializationt::read_irep(std::istream &in)
7676
sub.push_back(reference_convert(in));
7777
}
7878

79-
#ifdef NAMED_SUB_IS_FORWARD_LIST
79+
#if NAMED_SUB_IS_FORWARD_LIST
8080
irept::named_subt::iterator before = named_sub.before_begin();
8181
#endif
8282
while(in.peek()=='N')
8383
{
8484
in.get();
8585
irep_idt id = read_string_ref(in);
86-
#ifdef NAMED_SUB_IS_FORWARD_LIST
86+
#if NAMED_SUB_IS_FORWARD_LIST
8787
named_sub.emplace_after(before, id, reference_convert(in));
8888
++before;
8989
#else
@@ -95,7 +95,7 @@ irept irep_serializationt::read_irep(std::istream &in)
9595
{
9696
in.get();
9797
irep_idt id = read_string_ref(in);
98-
#ifdef NAMED_SUB_IS_FORWARD_LIST
98+
#if NAMED_SUB_IS_FORWARD_LIST
9999
named_sub.emplace_after(before, id, reference_convert(in));
100100
++before;
101101
#else

‎src/util/lispirep.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ void irep2lisp(const irept &src, lispexprt &dest)
4646
dest.value.clear();
4747
dest.type=lispexprt::List;
4848

49-
#ifdef NAMED_SUB_IS_FORWARD_LIST
49+
#if NAMED_SUB_IS_FORWARD_LIST
5050
const std::size_t named_sub_size =
5151
std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
5252
#else

‎src/util/merge_irep.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ std::size_t to_be_merged_irept::hash() const
2828
result, static_cast<const merged_irept &>(it->second).hash());
2929
}
3030

31-
#ifdef NAMED_SUB_IS_FORWARD_LIST
31+
#if NAMED_SUB_IS_FORWARD_LIST
3232
const std::size_t named_sub_size =
3333
std::distance(named_sub.begin(), named_sub.end());
3434
#else
@@ -51,7 +51,7 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const
5151

5252
if(sub.size()!=o_sub.size())
5353
return false;
54-
#ifdef NAMED_SUB_IS_FORWARD_LIST
54+
#if NAMED_SUB_IS_FORWARD_LIST
5555
if(
5656
std::distance(named_sub.begin(), named_sub.end()) !=
5757
std::distance(o_named_sub.begin(), o_named_sub.end()))
@@ -110,12 +110,12 @@ const merged_irept &merged_irepst::merged(const irept &irep)
110110
const irept::named_subt &src_named_sub=irep.get_named_sub();
111111
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
112112

113-
#ifdef NAMED_SUB_IS_FORWARD_LIST
113+
#if NAMED_SUB_IS_FORWARD_LIST
114114
irept::named_subt::iterator before = dest_named_sub.before_begin();
115115
#endif
116116
forall_named_irep(it, src_named_sub)
117117
{
118-
#ifdef NAMED_SUB_IS_FORWARD_LIST
118+
#if NAMED_SUB_IS_FORWARD_LIST
119119
dest_named_sub.emplace_after(
120120
before, it->first, merged(it->second)); // recursive call
121121
++before;
@@ -214,12 +214,12 @@ const irept &merge_full_irept::merged(const irept &irep)
214214
const irept::named_subt &src_named_sub=irep.get_named_sub();
215215
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
216216

217-
#ifdef NAMED_SUB_IS_FORWARD_LIST
217+
#if NAMED_SUB_IS_FORWARD_LIST
218218
irept::named_subt::iterator before = dest_named_sub.before_begin();
219219
#endif
220220
forall_named_irep(it, src_named_sub)
221221
{
222-
#ifdef NAMED_SUB_IS_FORWARD_LIST
222+
#if NAMED_SUB_IS_FORWARD_LIST
223223
dest_named_sub.emplace_after(
224224
before, it->first, merged(it->second)); // recursive call
225225
++before;

‎src/util/type.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,8 @@ class typet:public irept
3232

3333
explicit typet(const irep_idt &_id):irept(_id) { }
3434

35-
#if defined(__clang__) || !defined(__GNUC__) || __GNUC__ >= 6
35+
// the STL implementation shipped with GCC 5 is broken
36+
#if !defined(__GLIBCXX__) || __GLIBCXX__ >= 20181026
3637
typet(irep_idt _id, typet _subtype)
3738
: irept(std::move(_id), {}, {std::move(_subtype)})
3839
{

‎unit/util/irep.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ SCENARIO("irept_memory", "[core][utils][irept]")
3535
REQUIRE(sizeof(std::vector<int>) == 3 * sizeof(void *));
3636
#endif
3737

38-
#ifndef NAMED_SUB_IS_FORWARD_LIST
38+
#if !NAMED_SUB_IS_FORWARD_LIST
3939
const std::size_t named_size = sizeof(std::map<int, int>);
4040
# ifndef _GLIBCXX_DEBUG
4141
# ifdef __APPLE__

0 commit comments

Comments
 (0)