Skip to content

Commit 223e3a6

Browse files
tautschnigtautschnig
authored
Merge pull request #2035 from tautschnig/forward-list
irept: Use singly-linked lists with SUB_IS_LIST [depends on: #3606]
2 parents f214211 + a4828df commit 223e3a6

6 files changed

Lines changed: 137 additions & 50 deletions

File tree

‎src/util/irep.cpp‎

Lines changed: 48 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
1717
#include "string_hash.h"
1818
#include "irep_hash.h"
1919

20-
#ifdef SUB_IS_LIST
20+
#ifdef NAMED_SUB_IS_FORWARD_LIST
2121
#include <algorithm>
2222
#endif
2323

@@ -31,7 +31,7 @@ irept nil_rep_storage;
3131
irept::dt irept::empty_d;
3232
#endif
3333

34-
#ifdef SUB_IS_LIST
34+
#ifdef NAMED_SUB_IS_FORWARD_LIST
3535
static inline bool named_subt_order(
3636
const std::pair<irep_namet, irept> &a,
3737
const irep_namet &b)
@@ -152,9 +152,9 @@ void irept::nonrecursive_destructor(dt *old_data)
152152

153153
if(d->ref_count==0)
154154
{
155-
stack.reserve(stack.size()+
156-
d->named_sub.size()+
157-
d->sub.size());
155+
stack.reserve(
156+
stack.size() + std::distance(d->named_sub.begin(), d->named_sub.end()) +
157+
d->sub.size());
158158

159159
for(named_subt::iterator
160160
it=d->named_sub.begin();
@@ -203,7 +203,7 @@ const irep_idt &irept::get(const irep_namet &name) const
203203
{
204204
const named_subt &s = get_named_sub();
205205

206-
#ifdef SUB_IS_LIST
206+
#ifdef NAMED_SUB_IS_FORWARD_LIST
207207
named_subt::const_iterator it=named_subt_lower_bound(s, name);
208208

209209
if(it==s.end() ||
@@ -259,11 +259,16 @@ void irept::remove(const irep_namet &name)
259259
{
260260
named_subt &s = get_named_sub();
261261

262-
#ifdef SUB_IS_LIST
262+
#ifdef NAMED_SUB_IS_FORWARD_LIST
263263
named_subt::iterator it=named_subt_lower_bound(s, name);
264264

265265
if(it!=s.end() && it->first==name)
266-
s.erase(it);
266+
{
267+
named_subt::iterator before = s.before_begin();
268+
while(std::next(before) != it)
269+
++before;
270+
s.erase_after(before);
271+
}
267272
#else
268273
s.erase(name);
269274
#endif
@@ -273,7 +278,7 @@ const irept &irept::find(const irep_namet &name) const
273278
{
274279
const named_subt &s = get_named_sub();
275280

276-
#ifdef SUB_IS_LIST
281+
#ifdef NAMED_SUB_IS_FORWARD_LIST
277282
named_subt::const_iterator it=named_subt_lower_bound(s, name);
278283

279284
if(it==s.end() ||
@@ -293,12 +298,17 @@ irept &irept::add(const irep_namet &name)
293298
{
294299
named_subt &s = get_named_sub();
295300

296-
#ifdef SUB_IS_LIST
301+
#ifdef NAMED_SUB_IS_FORWARD_LIST
297302
named_subt::iterator it=named_subt_lower_bound(s, name);
298303

299304
if(it==s.end() ||
300305
it->first!=name)
301-
it=s.insert(it, std::make_pair(name, irept()));
306+
{
307+
named_subt::iterator before = s.before_begin();
308+
while(std::next(before) != it)
309+
++before;
310+
it = s.emplace_after(before, name, irept());
311+
}
302312

303313
return it->second;
304314
#else
@@ -310,12 +320,17 @@ irept &irept::add(const irep_namet &name, const irept &irep)
310320
{
311321
named_subt &s = get_named_sub();
312322

313-
#ifdef SUB_IS_LIST
323+
#ifdef NAMED_SUB_IS_FORWARD_LIST
314324
named_subt::iterator it=named_subt_lower_bound(s, name);
315325

316326
if(it==s.end() ||
317327
it->first!=name)
318-
it=s.insert(it, std::make_pair(name, irep));
328+
{
329+
named_subt::iterator before = s.before_begin();
330+
while(std::next(before) != it)
331+
++before;
332+
it = s.emplace_after(before, name, irep);
333+
}
319334
else
320335
it->second=irep;
321336

@@ -407,13 +422,24 @@ bool irept::full_eq(const irept &other) const
407422

408423
const irept::subt &i1_sub=get_sub();
409424
const irept::subt &i2_sub=other.get_sub();
425+
426+
if(i1_sub.size() != i2_sub.size())
427+
return false;
428+
410429
const irept::named_subt &i1_named_sub=get_named_sub();
411430
const irept::named_subt &i2_named_sub=other.get_named_sub();
412431

432+
#ifdef NAMED_SUB_IS_FORWARD_LIST
413433
if(
414-
i1_sub.size() != i2_sub.size() ||
415-
i1_named_sub.size() != i2_named_sub.size())
434+
std::distance(i1_named_sub.begin(), i1_named_sub.end()) !=
435+
std::distance(i2_named_sub.begin(), i2_named_sub.end()))
436+
{
437+
return false;
438+
}
439+
#else
440+
if(i1_named_sub.size() != i2_named_sub.size())
416441
return false;
442+
#endif
417443

418444
for(std::size_t i=0; i<i1_sub.size(); i++)
419445
if(!i1_sub[i].full_eq(i2_sub[i]))
@@ -667,7 +693,13 @@ std::size_t irept::full_hash() const
667693
result=hash_combine(result, it->second.full_hash());
668694
}
669695

670-
result = hash_finalize(result, named_sub.size() + sub.size());
696+
#ifdef NAMED_SUB_IS_FORWARD_LIST
697+
const std::size_t named_sub_size =
698+
std::distance(named_sub.begin(), named_sub.end());
699+
#else
700+
const std::size_t named_sub_size = named_sub.size();
701+
#endif
702+
result = hash_finalize(result, named_sub_size + sub.size());
671703

672704
return result;
673705
}

‎src/util/irep.h‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,10 @@ Author: Daniel Kroening, kroening@kroening.com
2020
#define SHARING
2121
// #define HASH_CODE
2222
#define USE_MOVE
23-
// #define SUB_IS_LIST
23+
// #define NAMED_SUB_IS_FORWARD_LIST
2424

25-
#ifdef SUB_IS_LIST
26-
#include <list>
25+
#ifdef NAMED_SUB_IS_FORWARD_LIST
26+
#include <forward_list>
2727
#else
2828
#include <map>
2929
#endif
@@ -160,11 +160,11 @@ class irept
160160
// use std::forward_list or std::vector< unique_ptr<T> > to save
161161
// memory and increase efficiency.
162162

163-
#ifdef SUB_IS_LIST
164-
typedef std::list<std::pair<irep_namet, irept> > named_subt;
165-
#else
163+
#ifdef NAMED_SUB_IS_FORWARD_LIST
164+
typedef std::forward_list<std::pair<irep_namet, irept>> named_subt;
165+
#else
166166
typedef std::map<irep_namet, irept> named_subt;
167-
#endif
167+
#endif
168168

169169
bool is_nil() const { return id()==ID_nil; }
170170
bool is_not_nil() const { return id()!=ID_nil; }

‎src/util/irep_hash_container.cpp‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,15 +54,21 @@ void irep_hash_container_baset::pack(
5454
{
5555
// we pack: the irep id, the sub size, the subs, the named-sub size, and
5656
// each of the named subs with their ids
57-
packed.reserve(1 + 1 + sub.size() + 1 + named_sub.size() * 2);
57+
#ifdef NAMED_SUB_IS_FORWARD_LIST
58+
const std::size_t named_sub_size =
59+
std::distance(named_sub.begin(), named_sub.end());
60+
#else
61+
const std::size_t named_sub_size = named_sub.size();
62+
#endif
63+
packed.reserve(1 + 1 + sub.size() + 1 + named_sub_size * 2);
5864

5965
packed.push_back(irep_id_hash()(irep.id()));
6066

6167
packed.push_back(sub.size());
6268
forall_irep(it, sub)
6369
packed.push_back(number(*it));
6470

65-
packed.push_back(named_sub.size());
71+
packed.push_back(named_sub_size);
6672
for(const auto &sub_irep : named_sub)
6773
{
6874
packed.push_back(irep_id_hash()(sub_irep.first)); // id

‎src/util/lispirep.cpp‎

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

49-
dest.reserve(2 + 2 * src.get_sub().size() + 2 * src.get_named_sub().size());
49+
#ifdef NAMED_SUB_IS_FORWARD_LIST
50+
const std::size_t named_sub_size =
51+
std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
52+
#else
53+
const std::size_t named_sub_size = src.get_named_sub().size();
54+
#endif
55+
dest.reserve(2 + 2 * src.get_sub().size() + 2 * named_sub_size);
5056

5157
lispexprt id;
5258
id.type=lispexprt::String;

‎src/util/merge_irep.cpp‎

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

31-
result=hash_finalize(result, named_sub.size()+sub.size());
31+
#ifdef NAMED_SUB_IS_FORWARD_LIST
32+
const std::size_t named_sub_size =
33+
std::distance(named_sub.begin(), named_sub.end());
34+
#else
35+
const std::size_t named_sub_size = named_sub.size();
36+
#endif
37+
result = hash_finalize(result, named_sub_size + sub.size());
3238

3339
return result;
3440
}
@@ -45,8 +51,17 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const
4551

4652
if(sub.size()!=o_sub.size())
4753
return false;
54+
#ifdef NAMED_SUB_IS_FORWARD_LIST
55+
if(
56+
std::distance(named_sub.begin(), named_sub.end()) !=
57+
std::distance(o_named_sub.begin(), o_named_sub.end()))
58+
{
59+
return false;
60+
}
61+
#else
4862
if(named_sub.size()!=o_named_sub.size())
4963
return false;
64+
#endif
5065

5166
{
5267
irept::subt::const_iterator s_it=sub.begin();
@@ -95,13 +110,19 @@ const merged_irept &merged_irepst::merged(const irept &irep)
95110
const irept::named_subt &src_named_sub=irep.get_named_sub();
96111
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
97112

113+
#ifdef NAMED_SUB_IS_FORWARD_LIST
114+
irept::named_subt::iterator before = dest_named_sub.before_begin();
115+
#endif
98116
forall_named_irep(it, src_named_sub)
99-
#ifdef SUB_IS_LIST
100-
dest_named_sub.push_back(
101-
std::make_pair(it->first, merged(it->second))); // recursive call
102-
#else
117+
{
118+
#ifdef NAMED_SUB_IS_FORWARD_LIST
119+
dest_named_sub.emplace_after(
120+
before, it->first, merged(it->second)); // recursive call
121+
++before;
122+
#else
103123
dest_named_sub[it->first]=merged(it->second); // recursive call
104-
#endif
124+
#endif
125+
}
105126

106127
std::pair<to_be_merged_irep_storet::const_iterator, bool> result=
107128
to_be_merged_irep_store.insert(to_be_merged_irept(new_irep));
@@ -140,13 +161,19 @@ const irept &merge_irept::merged(const irept &irep)
140161
const irept::named_subt &src_named_sub=irep.get_named_sub();
141162
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
142163

164+
#ifdef NAMED_SUB_IS_FORWARD_LIST
165+
irept::named_subt::iterator before = dest_named_sub.before_begin();
166+
#endif
143167
forall_named_irep(it, src_named_sub)
144-
#ifdef SUB_IS_LIST
145-
dest_named_sub.push_back(
146-
std::make_pair(it->first, merged(it->second))); // recursive call
147-
#else
168+
{
169+
#ifdef NAMED_SUB_IS_FORWARD_LIST
170+
dest_named_sub.emplace_after(
171+
before, it->first, merged(it->second)); // recursive call
172+
++before;
173+
#else
148174
dest_named_sub[it->first]=merged(it->second); // recursive call
149-
#endif
175+
#endif
176+
}
150177

151178
return *irep_store.insert(std::move(new_irep)).first;
152179
}
@@ -177,13 +204,19 @@ const irept &merge_full_irept::merged(const irept &irep)
177204
const irept::named_subt &src_named_sub=irep.get_named_sub();
178205
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
179206

207+
#ifdef NAMED_SUB_IS_FORWARD_LIST
208+
irept::named_subt::iterator before = dest_named_sub.before_begin();
209+
#endif
180210
forall_named_irep(it, src_named_sub)
181-
#ifdef SUB_IS_LIST
182-
dest_named_sub.push_back(
183-
std::make_pair(it->first, merged(it->second))); // recursive call
184-
#else
211+
{
212+
#ifdef NAMED_SUB_IS_FORWARD_LIST
213+
dest_named_sub.emplace_after(
214+
before, it->first, merged(it->second)); // recursive call
215+
++before;
216+
#else
185217
dest_named_sub[it->first]=merged(it->second); // recursive call
186-
#endif
218+
#endif
219+
}
187220

188221
return *irep_store.insert(std::move(new_irep)).first;
189222
}

‎unit/util/irep.cpp‎

Lines changed: 18 additions & 8 deletions
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 SUB_IS_LIST
38+
#ifndef NAMED_SUB_IS_FORWARD_LIST
3939
const std::size_t named_size = sizeof(std::map<int, int>);
4040
# ifndef _GLIBCXX_DEBUG
4141
# ifdef __APPLE__
@@ -47,9 +47,9 @@ SCENARIO("irept_memory", "[core][utils][irept]")
4747
# endif
4848
# endif
4949
#else
50-
const std::size_t named_size = sizeof(std::list<int>);
50+
const std::size_t named_size = sizeof(std::forward_list<int>);
5151
# ifndef _GLIBCXX_DEBUG
52-
REQUIRE(sizeof(std::list<int>) == 3 * sizeof(void *));
52+
REQUIRE(sizeof(std::forward_list<int>) == sizeof(void *));
5353
# endif
5454
#endif
5555

@@ -140,12 +140,16 @@ SCENARIO("irept_memory", "[core][utils][irept]")
140140
irep.add("a_new_element", irep2);
141141
REQUIRE(!irept::is_comment("a_new_element"));
142142
REQUIRE(irep.find("a_new_element").id() == "second_irep");
143-
REQUIRE(irep.get_named_sub().size() == 1);
143+
std::size_t named_sub_size =
144+
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
145+
REQUIRE(named_sub_size == 1);
144146

145147
irep.add("#a_comment", irep2);
146148
REQUIRE(irept::is_comment("#a_comment"));
147149
REQUIRE(irep.find("#a_comment").id() == "second_irep");
148-
REQUIRE(irep.get_named_sub().size() == 2);
150+
named_sub_size =
151+
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
152+
REQUIRE(named_sub_size == 2);
149153
REQUIRE(irept::number_of_non_comments(irep.get_named_sub()) == 1);
150154

151155
irept bak(irep);
@@ -160,17 +164,23 @@ SCENARIO("irept_memory", "[core][utils][irept]")
160164

161165
irep.move_to_named_sub("another_entry", irep2);
162166
REQUIRE(irep.get_sub().size() == 1);
163-
REQUIRE(irep.get_named_sub().size() == 2);
167+
named_sub_size =
168+
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
169+
REQUIRE(named_sub_size == 2);
164170

165171
irept irep3;
166172
irep.move_to_named_sub("#a_comment", irep3);
167173
REQUIRE(irep.find("#a_comment").id().empty());
168174
REQUIRE(irep.get_sub().size() == 1);
169-
REQUIRE(irep.get_named_sub().size() == 2);
175+
named_sub_size =
176+
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
177+
REQUIRE(named_sub_size == 2);
170178

171179
irept irep4;
172180
irep.move_to_named_sub("#another_comment", irep4);
173-
REQUIRE(irep.get_named_sub().size() == 3);
181+
named_sub_size =
182+
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
183+
REQUIRE(named_sub_size == 3);
174184
}
175185

176186
THEN("Setting and getting works")

0 commit comments

Comments
 (0)