Skip to content

Commit 3815661

Browse files
tautschnigtautschnig
committed
irept: Use singly-linked lists with SUB_IS_LIST
This reduces the memory footprint by two pointers for both named_sub and comments. The cost is that computing the size of lists and add/remove require additional iterator increments.
1 parent e6a9127 commit 3815661

File tree

6 files changed

+151
-37
lines changed

6 files changed

+151
-37
lines changed

‎src/util/irep.cpp‎

Lines changed: 49 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,11 @@ void irept::remove(const irep_namet &name)
133133
named_subt::iterator it=named_subt_lower_bound(s, name);
134134

135135
if(it!=s.end() && it->first==name)
136-
s.erase(it);
136+
{
137+
named_subt::iterator before = s.before_begin();
138+
while(std::next(before) != it) ++before;
139+
s.erase_after(before);
140+
}
137141
#else
138142
s.erase(name);
139143
#endif
@@ -170,7 +174,11 @@ irept &irept::add(const irep_namet &name)
170174

171175
if(it==s.end() ||
172176
it->first!=name)
173-
it=s.insert(it, std::make_pair(name, irept()));
177+
{
178+
named_subt::iterator before = s.before_begin();
179+
while(std::next(before) != it) ++before;
180+
it = s.emplace_after(before, name, irept());
181+
}
174182

175183
return it->second;
176184
#else
@@ -188,7 +196,11 @@ irept &irept::add(const irep_namet &name, const irept &irep)
188196

189197
if(it==s.end() ||
190198
it->first!=name)
191-
it=s.insert(it, std::make_pair(name, irep));
199+
{
200+
named_subt::iterator before = s.before_begin();
201+
while(std::next(before) != it) ++before;
202+
it = s.emplace_after(before, name, irep);
203+
}
192204
else
193205
it->second=irep;
194206

@@ -251,10 +263,20 @@ bool irept::full_eq(const irept &other) const
251263
const irept::named_subt &i1_comments=get_comments();
252264
const irept::named_subt &i2_comments=other.get_comments();
253265

266+
#ifdef SUB_IS_LIST
267+
if(
268+
i1_sub.size() != i2_sub.size() ||
269+
std::distance(i1_named_sub.begin(), i1_named_sub.end()) !=
270+
std::distance(i2_named_sub.begin(), i2_named_sub.end()) ||
271+
std::distance(i1_comments.begin(), i1_comments.end()) !=
272+
std::distance(i2_comments.begin(), i2_comments.end()))
273+
return false;
274+
#else
254275
if(i1_sub.size()!=i2_sub.size() ||
255276
i1_named_sub.size()!=i2_named_sub.size() ||
256277
i1_comments.size()!=i2_comments.size())
257278
return false;
279+
#endif
258280

259281
for(std::size_t i=0; i<i1_sub.size(); i++)
260282
if(!i1_sub[i].full_eq(i2_sub[i]))
@@ -385,8 +407,15 @@ int irept::compare(const irept &i) const
385407
"Unequal lengths will return before this");
386408
}
387409

410+
#ifdef SUB_IS_LIST
411+
const named_subt::size_type n_size =
412+
std::distance(get_named_sub().begin(), get_named_sub().end());
413+
const named_subt::size_type i_n_size =
414+
std::distance(i.get_named_sub().begin(), i.get_named_sub().end());
415+
#else
388416
const named_subt::size_type n_size=get_named_sub().size(),
389417
i_n_size=i.get_named_sub().size();
418+
#endif
390419
if(n_size<i_n_size)
391420
return -1;
392421
if(n_size>i_n_size)
@@ -449,7 +478,13 @@ std::size_t irept::hash() const
449478
result=hash_combine(result, it->second.hash());
450479
}
451480

452-
result=hash_finalize(result, named_sub.size()+sub.size());
481+
#ifdef SUB_IS_LIST
482+
const std::size_t named_sub_size =
483+
std::distance(named_sub.begin(), named_sub.end());
484+
#else
485+
const std::size_t named_sub_size = named_sub.size();
486+
#endif
487+
result = hash_finalize(result, named_sub_size + sub.size());
453488

454489
#ifdef HASH_CODE
455490
read().hash_code=result;
@@ -482,9 +517,16 @@ std::size_t irept::full_hash() const
482517
result=hash_combine(result, it->second.full_hash());
483518
}
484519

485-
result=hash_finalize(
486-
result,
487-
named_sub.size()+sub.size()+comments.size());
520+
#ifdef SUB_IS_LIST
521+
const std::size_t named_sub_size =
522+
std::distance(named_sub.begin(), named_sub.end());
523+
const std::size_t comments_size =
524+
std::distance(comments.begin(), comments.end());
525+
#else
526+
const std::size_t named_sub_size = named_sub.size();
527+
const std::size_t comments_size = comments.size();
528+
#endif
529+
result = hash_finalize(result, named_sub_size + sub.size() + comments_size);
488530

489531
return result;
490532
}

‎src/util/irep.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ Author: Daniel Kroening, [email protected]
2626
#endif
2727

2828
#ifdef SUB_IS_LIST
29-
#include <list>
29+
#include <forward_list>
3030
#else
3131
#include <map>
3232
#endif
@@ -98,7 +98,7 @@ class irept
9898
// memory and increase efficiency.
9999

100100
#ifdef SUB_IS_LIST
101-
typedef std::list<std::pair<irep_namet, irept> > named_subt;
101+
typedef std::forward_list<std::pair<irep_namet, irept> > named_subt;
102102
#else
103103
typedef std::map<irep_namet, irept> named_subt;
104104
#endif

‎src/util/irep_hash_container.cpp‎

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -49,17 +49,24 @@ void irep_hash_container_baset::pack(
4949
const irept::named_subt &named_sub=irep.get_named_sub();
5050
const irept::named_subt &comments=irep.get_comments();
5151

52-
packed.reserve(
53-
1+1+sub.size()+named_sub.size()*2+
54-
(full?comments.size()*2:0));
52+
#ifdef SUB_IS_LIST
53+
const std::size_t named_sub_size =
54+
std::distance(named_sub.begin(), named_sub.end());
55+
const std::size_t comments_size = full ?
56+
std::distance(comments.begin(), comments.end()) : 0;
57+
#else
58+
const std::size_t named_sub_size = named_sub.size();
59+
const std::size_t comments_size = full ? comments.size() : 0;
60+
#endif
61+
packed.reserve(1 + 1 + sub.size() + named_sub_size * 2 + comments_size * 2);
5562

5663
packed.push_back(irep_id_hash()(irep.id()));
5764

5865
packed.push_back(sub.size());
5966
forall_irep(it, sub)
6067
packed.push_back(number(*it));
6168

62-
packed.push_back(named_sub.size());
69+
packed.push_back(named_sub_size);
6370
forall_named_irep(it, named_sub)
6471
{
6572
packed.push_back(irep_id_hash()(it->first)); // id
@@ -68,7 +75,7 @@ void irep_hash_container_baset::pack(
6875

6976
if(full)
7077
{
71-
packed.push_back(comments.size());
78+
packed.push_back(comments_size);
7279
forall_named_irep(it, comments)
7380
{
7481
packed.push_back(irep_id_hash()(it->first)); // id

‎src/util/lispirep.cpp‎

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -46,9 +46,17 @@ 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()
50-
+2*src.get_named_sub().size()
51-
+2*src.get_comments().size());
49+
#ifdef SUB_IS_LIST
50+
const std::size_t named_sub_size =
51+
std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
52+
const std::size_t comments_size =
53+
std::distance(src.get_comments().begin(), src.get_comments().end());
54+
#else
55+
const std::size_t named_sub_size = src.get_named_sub().size();
56+
const std::size_t comments_size = src.get_comments().size();
57+
#endif
58+
dest.reserve(
59+
2 + 2 * src.get_sub().size() + 2 * named_sub_size + 2 * comments_size);
5260

5361
lispexprt id;
5462
id.type=lispexprt::String;

‎src/util/merge_irep.cpp‎

Lines changed: 56 additions & 13 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 SUB_IS_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
}
@@ -44,9 +50,16 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const
4450
const irept::named_subt &o_named_sub=other.get_named_sub();
4551

4652
if(sub.size()!=o_sub.size())
47-
return true;
53+
return false;
54+
#ifdef SUB_IS_LIST
55+
if(
56+
std::distance(named_sub.begin(), named_sub.end()) !=
57+
std::distance(o_named_sub.begin(), o_named_sub.end()))
58+
return false;
59+
#else
4860
if(named_sub.size()!=o_named_sub.size())
49-
return true;
61+
return false;
62+
#endif
5063

5164
{
5265
irept::subt::const_iterator s_it=sub.begin();
@@ -95,13 +108,19 @@ const merged_irept &merged_irepst::merged(const irept &irep)
95108
const irept::named_subt &src_named_sub=irep.get_named_sub();
96109
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
97110

111+
#ifdef SUB_IS_LIST
112+
irept::named_subt::iterator before = dest_named_sub.before_begin();
113+
#endif
98114
forall_named_irep(it, src_named_sub)
115+
{
99116
#ifdef SUB_IS_LIST
100-
dest_named_sub.push_back(
101-
std::make_pair(it->first, merged(it->second))); // recursive call
117+
dest_named_sub.emplace_after(
118+
before, it->first, merged(it->second)); // recursive call
119+
++before;
102120
#else
103121
dest_named_sub[it->first]=merged(it->second); // recursive call
104122
#endif
123+
}
105124

106125
std::pair<to_be_merged_irep_storet::const_iterator, bool> result=
107126
to_be_merged_irep_store.insert(to_be_merged_irept(new_irep));
@@ -140,24 +159,36 @@ const irept &merge_irept::merged(const irept &irep)
140159
const irept::named_subt &src_named_sub=irep.get_named_sub();
141160
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
142161

162+
#ifdef SUB_IS_LIST
163+
irept::named_subt::iterator before = dest_named_sub.before_begin();
164+
#endif
143165
forall_named_irep(it, src_named_sub)
166+
{
144167
#ifdef SUB_IS_LIST
145-
dest_named_sub.push_back(
146-
std::make_pair(it->first, merged(it->second))); // recursive call
168+
dest_named_sub.emplace_after(
169+
before, it->first, merged(it->second)); // recursive call
170+
++before;
147171
#else
148172
dest_named_sub[it->first]=merged(it->second); // recursive call
149173
#endif
174+
}
150175

151176
const irept::named_subt &src_comments=irep.get_comments();
152177
irept::named_subt &dest_comments=new_irep.get_comments();
153178

179+
#ifdef SUB_IS_LIST
180+
before = dest_comments.before_begin();
181+
#endif
154182
forall_named_irep(it, src_comments)
183+
{
155184
#ifdef SUB_IS_LIST
156-
dest_comments.push_back(
157-
std::make_pair(it->first, merged(it->second))); // recursive call
185+
dest_comments.emplace_after(
186+
before, it->first, merged(it->second)); // recursive call
187+
++before;
158188
#else
159189
dest_comments[it->first]=merged(it->second); // recursive call
160190
#endif
191+
}
161192

162193
return *irep_store.insert(new_irep).first;
163194
}
@@ -188,24 +219,36 @@ const irept &merge_full_irept::merged(const irept &irep)
188219
const irept::named_subt &src_named_sub=irep.get_named_sub();
189220
irept::named_subt &dest_named_sub=new_irep.get_named_sub();
190221

222+
#ifdef SUB_IS_LIST
223+
irept::named_subt::iterator before = dest_named_sub.before_begin();
224+
#endif
191225
forall_named_irep(it, src_named_sub)
226+
{
192227
#ifdef SUB_IS_LIST
193-
dest_named_sub.push_back(
194-
std::make_pair(it->first, merged(it->second))); // recursive call
228+
dest_named_sub.emplace_after(
229+
before, it->first, merged(it->second)); // recursive call
230+
++before;
195231
#else
196232
dest_named_sub[it->first]=merged(it->second); // recursive call
197233
#endif
234+
}
198235

199236
const irept::named_subt &src_comments=irep.get_comments();
200237
irept::named_subt &dest_comments=new_irep.get_comments();
201238

239+
#ifdef SUB_IS_LIST
240+
before = dest_comments.before_begin();
241+
#endif
202242
forall_named_irep(it, src_comments)
243+
{
203244
#ifdef SUB_IS_LIST
204-
dest_comments.push_back(
205-
std::make_pair(it->first, merged(it->second))); // recursive call
245+
dest_comments.emplace_after(
246+
before, it->first, merged(it->second)); // recursive call
247+
++before;
206248
#else
207249
dest_comments[it->first]=merged(it->second); // recursive call
208250
#endif
251+
}
209252

210253
return *irep_store.insert(new_irep).first;
211254
}

‎unit/util/irep.cpp‎

Lines changed: 21 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -90,11 +90,15 @@ SCENARIO("irept_memory", "[core][utils][irept]")
9090
irept irep2("second_irep");
9191
irep.add("a_new_element", irep2);
9292
REQUIRE(irep.find("a_new_element").id() == "second_irep");
93-
REQUIRE(irep.get_named_sub().size() == 1);
93+
std::size_t named_sub_size = std::distance(
94+
irep.get_named_sub().begin(), irep.get_named_sub().end());
95+
REQUIRE(named_sub_size == 1);
9496

9597
irep.add("#a_comment", irep2);
9698
REQUIRE(irep.find("#a_comment").id() == "second_irep");
97-
REQUIRE(irep.get_comments().size() == 1);
99+
std::size_t comments_size =
100+
std::distance(irep.get_comments().begin(), irep.get_comments().end());
101+
REQUIRE(comments_size == 1);
98102

99103
irept bak(irep);
100104
irep.remove("no_such_id");
@@ -108,19 +112,29 @@ SCENARIO("irept_memory", "[core][utils][irept]")
108112

109113
irep.move_to_named_sub("another_entry", irep2);
110114
REQUIRE(irep.get_sub().size() == 1);
111-
REQUIRE(irep.get_named_sub().size() == 1);
112-
REQUIRE(irep.get_comments().size() == 1);
115+
named_sub_size = std::distance(
116+
irep.get_named_sub().begin(), irep.get_named_sub().end());
117+
REQUIRE(named_sub_size == 1);
118+
comments_size =
119+
std::distance(irep.get_comments().begin(), irep.get_comments().end());
120+
REQUIRE(comments_size == 1);
113121

114122
irept irep3;
115123
irep.move_to_named_sub("#a_comment", irep3);
116124
REQUIRE(irep.find("#a_comment").id().empty());
117125
REQUIRE(irep.get_sub().size() == 1);
118-
REQUIRE(irep.get_named_sub().size() == 1);
119-
REQUIRE(irep.get_comments().size() == 1);
126+
named_sub_size = std::distance(
127+
irep.get_named_sub().begin(), irep.get_named_sub().end());
128+
REQUIRE(named_sub_size == 1);
129+
comments_size =
130+
std::distance(irep.get_comments().begin(), irep.get_comments().end());
131+
REQUIRE(comments_size == 1);
120132

121133
irept irep4;
122134
irep.move_to_named_sub("#another_comment", irep4);
123-
REQUIRE(irep.get_comments().size() == 2);
135+
comments_size =
136+
std::distance(irep.get_comments().begin(), irep.get_comments().end());
137+
REQUIRE(comments_size == 2);
124138
}
125139

126140
THEN("Setting and getting works")

0 commit comments

Comments
 (0)