Skip to content

Commit be7b9da

Browse files
committed
cfgt: use dense_integer_mapt to provide instruction -> cfg node mapping
This saves a lot of allocations, memory, and time when the cfg is frequently queried.
1 parent 5eb010f commit be7b9da

File tree

8 files changed

+109
-45
lines changed

8 files changed

+109
-45
lines changed

Diff for: src/analyses/cfg_dominators.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -248,17 +248,17 @@ inline void dominators_pretty_print_node(
248248
template <class P, class T, bool post_dom>
249249
void cfg_dominators_templatet<P, T, post_dom>::output(std::ostream &out) const
250250
{
251-
for(const auto &node : cfg.entries())
251+
for(const auto &n : cfg.keys())
252252
{
253-
auto n=node.first;
253+
const auto &node = cfg.get_node(n);
254254

255255
dominators_pretty_print_node(n, out);
256256
if(post_dom)
257257
out << " post-dominated by ";
258258
else
259259
out << " dominated by ";
260260
bool first=true;
261-
for(const auto &d : cfg[node.second].dominators)
261+
for(const auto &d : cfg[node].dominators)
262262
{
263263
if(!first)
264264
out << ", ";

Diff for: src/goto-analyzer/unreachable_instructions.cpp

+3-7
Original file line numberDiff line numberDiff line change
@@ -32,15 +32,11 @@ static void unreachable_instructions(
3232
cfg_dominatorst dominators;
3333
dominators(goto_program);
3434

35-
for(cfg_dominatorst::cfgt::entry_mapt::const_iterator
36-
it=dominators.cfg.entry_map.begin();
37-
it!=dominators.cfg.entry_map.end();
38-
++it)
35+
for(const auto instruction : dominators.cfg.keys())
3936
{
40-
const cfg_dominatorst::cfgt::nodet &n=dominators.cfg[it->second];
37+
const cfg_dominatorst::cfgt::nodet &n = dominators.get_node(instruction);
4138
if(n.dominators.empty())
42-
dest.insert(std::make_pair(it->first->location_number,
43-
it->first));
39+
dest.insert(std::make_pair(instruction->location_number, instruction));
4440
}
4541
}
4642

Diff for: src/goto-instrument/dump_c.cpp

+3
Original file line numberDiff line numberDiff line change
@@ -663,6 +663,9 @@ void dump_ct::cleanup_decl(
663663

664664
tmp.add(goto_programt::make_end_function());
665665

666+
// goto_program2codet requires valid location numbers:
667+
tmp.update();
668+
666669
std::unordered_set<irep_idt> typedef_names;
667670
for(const auto &td : typedef_map)
668671
typedef_names.insert(td.first);

Diff for: src/goto-instrument/full_slicer.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -271,10 +271,9 @@ void full_slicert::operator()(
271271
// declarations or dead instructions may be necessary as well
272272
decl_deadt decl_dead;
273273

274-
for(const auto &instruction_and_index : cfg.entries())
274+
for(const auto &instruction : cfg.keys())
275275
{
276-
const auto &instruction = instruction_and_index.first;
277-
const auto instruction_node_index = instruction_and_index.second;
276+
const auto instruction_node_index = cfg.get_node_index(instruction);
278277
if(criterion(cfg[instruction_node_index].function_id, instruction))
279278
add_to_queue(queue, instruction_node_index, instruction);
280279
else if(implicit(instruction))

Diff for: src/goto-instrument/goto_instrument_parse_options.cpp

+17
Original file line numberDiff line numberDiff line change
@@ -669,6 +669,10 @@ int goto_instrument_parse_optionst::doit()
669669
// applied
670670
restore_returns(goto_model);
671671

672+
// dump_c (actually goto_program2code) requires valid instruction
673+
// location numbers:
674+
goto_model.goto_functions.update();
675+
672676
if(cmdline.args.size()==2)
673677
{
674678
#ifdef _MSC_VER
@@ -1497,6 +1501,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
14971501
do_indirect_call_and_rtti_removal();
14981502

14991503
log.status() << "Performing a reachability slice" << messaget::eom;
1504+
1505+
// reachability_slicer requires that the model has unique location numbers:
1506+
goto_model.goto_functions.update();
1507+
15001508
if(cmdline.isset("property"))
15011509
reachability_slicer(goto_model, cmdline.get_values("property"));
15021510
else
@@ -1523,7 +1531,11 @@ void goto_instrument_parse_optionst::instrument_goto_program()
15231531
if(cmdline.isset("property"))
15241532
property_slicer(goto_model, cmdline.get_values("property"));
15251533
else
1534+
{
1535+
// full_slicer requires that the model has unique location numbers:
1536+
goto_model.goto_functions.update();
15261537
full_slicer(goto_model);
1538+
}
15271539
}
15281540

15291541
// splice option
@@ -1544,6 +1556,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
15441556
{
15451557
do_indirect_call_and_rtti_removal();
15461558

1559+
// reachability_slicer requires that the model has unique location numbers:
1560+
goto_model.goto_functions.update();
1561+
15471562
log.status() << "Slicing away initializations of unused global variables"
15481563
<< messaget::eom;
15491564
slice_global_inits(goto_model);
@@ -1572,6 +1587,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
15721587

15731588
aggressive_slicer.doit();
15741589

1590+
goto_model.goto_functions.update();
1591+
15751592
log.status() << "Performing a reachability slice" << messaget::eom;
15761593
if(cmdline.isset("property"))
15771594
reachability_slicer(goto_model, cmdline.get_values("property"));

Diff for: src/goto-instrument/points_to.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,9 @@ void points_tot::fixedpoint()
2121
{
2222
added=false;
2323

24-
for(const auto &instruction_and_entry : cfg.entries())
24+
for(const auto &key : cfg.keys())
2525
{
26-
if(transform(cfg[instruction_and_entry.second]))
26+
if(transform(cfg.get_node(key)))
2727
added=true;
2828
}
2929
}

Diff for: src/goto-instrument/reachability_slicer.cpp

+5-4
Original file line numberDiff line numberDiff line change
@@ -39,12 +39,13 @@ reachability_slicert::get_sources(
3939
const slicing_criteriont &criterion)
4040
{
4141
std::vector<cfgt::node_indext> sources;
42-
for(const auto &e_it : cfg.entries())
42+
for(const auto &instruction : cfg.keys())
4343
{
44+
const auto cfg_node_index = cfg.get_node_index(instruction);
4445
if(
45-
criterion(cfg[e_it.second].function_id, e_it.first) ||
46-
is_threaded(e_it.first))
47-
sources.push_back(e_it.second);
46+
criterion(cfg[cfg_node_index].function_id, instruction) ||
47+
is_threaded(instruction))
48+
sources.push_back(cfg_node_index);
4849
}
4950

5051
if(sources.empty())

Diff for: src/goto-programs/cfg.h

+74-26
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_GOTO_PROGRAMS_CFG_H
1313
#define CPROVER_GOTO_PROGRAMS_CFG_H
1414

15-
#include <util/std_expr.h>
15+
#include <util/dense_integer_map.h>
1616
#include <util/graph.h>
17+
#include <util/std_expr.h>
1718

1819
#include "goto_functions.h"
1920

@@ -31,6 +32,29 @@ struct cfg_base_nodet:public graph_nodet<empty_edget>, public T
3132
I PC;
3233
};
3334

35+
/// Functor to convert cfg nodes into dense integers, used by \ref cfg_baset.
36+
/// Default implementation: the identity function.
37+
template <class T>
38+
class cfg_instruction_to_dense_integert
39+
{
40+
public:
41+
std::size_t operator()(T &&t) const
42+
{
43+
return std::forward<T>(identity_functort<T>{}(t));
44+
}
45+
};
46+
47+
/// GOTO-instruction to location number functor.
48+
template <>
49+
class cfg_instruction_to_dense_integert<goto_programt::const_targett>
50+
{
51+
public:
52+
std::size_t operator()(const goto_programt::const_targett &t) const
53+
{
54+
return t->location_number;
55+
}
56+
};
57+
3458
/// A multi-procedural control flow graph (CFG) whose nodes store references to
3559
/// instructions in a GOTO program.
3660
///
@@ -69,28 +93,16 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
6993

7094
class entry_mapt final
7195
{
72-
typedef std::map<goto_programt::const_targett, entryt> data_typet;
96+
typedef dense_integer_mapt<
97+
goto_programt::const_targett,
98+
entryt,
99+
cfg_instruction_to_dense_integert<goto_programt::const_targett>>
100+
data_typet;
73101
data_typet data;
74102

75103
public:
76104
grapht< cfg_base_nodet<T, I> > &container;
77105

78-
// NOLINTNEXTLINE(readability/identifiers)
79-
typedef typename data_typet::iterator iterator;
80-
// NOLINTNEXTLINE(readability/identifiers)
81-
typedef typename data_typet::const_iterator const_iterator;
82-
83-
template <typename U>
84-
const_iterator find(U &&u) const { return data.find(std::forward<U>(u)); }
85-
86-
iterator begin() { return data.begin(); }
87-
const_iterator begin() const { return data.begin(); }
88-
const_iterator cbegin() const { return data.cbegin(); }
89-
90-
iterator end() { return data.end(); }
91-
const_iterator end() const { return data.end(); }
92-
const_iterator cend() const { return data.cend(); }
93-
94106
explicit entry_mapt(grapht< cfg_base_nodet<T, I> > &_container):
95107
container(_container)
96108
{
@@ -100,10 +112,10 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
100112
{
101113
auto e=data.insert(std::make_pair(t, 0));
102114

103-
if(e.second)
104-
e.first->second=container.add_node();
115+
if(e)
116+
data.at(t) = container.add_node();
105117

106-
return e.first->second;
118+
return data.at(t);
107119
}
108120

109121
entryt &at(const goto_programt::const_targett &t)
@@ -114,6 +126,25 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
114126
{
115127
return data.at(t);
116128
}
129+
130+
std::size_t count(const goto_programt::const_targett &t) const
131+
{
132+
return data.count(t);
133+
}
134+
135+
typedef typename data_typet::possible_keyst keyst;
136+
const keyst &keys() const
137+
{
138+
// We always define exactly the keys the entry map was set up for, so
139+
// data's possible key set is exactly our key set
140+
return data.possible_keys();
141+
}
142+
143+
template <class Iter>
144+
void setup_for_keys(Iter begin, Iter end)
145+
{
146+
data.setup_for_keys(begin, end);
147+
}
117148
};
118149
entry_mapt entry_map;
119150

@@ -173,12 +204,30 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
173204
void operator()(
174205
const goto_functionst &goto_functions)
175206
{
207+
std::vector<goto_programt::const_targett> possible_keys;
208+
for(const auto &id_and_function : goto_functions.function_map)
209+
{
210+
const auto &instructions = id_and_function.second.body.instructions;
211+
possible_keys.reserve(
212+
possible_keys.size() +
213+
std::distance(instructions.begin(), instructions.end()));
214+
for(auto it = instructions.begin(); it != instructions.end(); ++it)
215+
possible_keys.push_back(it);
216+
}
217+
entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
176218
compute_edges(goto_functions);
177219
}
178220

179221
void operator()(P &goto_program)
180222
{
181223
goto_functionst goto_functions;
224+
std::vector<goto_programt::const_targett> possible_keys;
225+
const auto &instructions = goto_program.instructions;
226+
possible_keys.reserve(
227+
std::distance(instructions.begin(), instructions.end()));
228+
for(auto it = instructions.begin(); it != instructions.end(); ++it)
229+
possible_keys.push_back(it);
230+
entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
182231
compute_edges(goto_functions, goto_program);
183232
}
184233

@@ -204,12 +253,11 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
204253
return (*this)[get_node_index(program_point)];
205254
}
206255

207-
/// Get a map from program points to their corresponding node indices. Use
208-
/// the indices with `operator[]` similar to those returned by
209-
/// \ref get_node_index.
210-
const entry_mapt &entries() const
256+
/// Get a vector of keys present in this cfg. Use these with \ref get_node or
257+
/// \ref get_node_index to get the corresponding CFG nodes.
258+
const typename entry_mapt::keyst &keys() const
211259
{
212-
return entry_map;
260+
return entry_map.keys();
213261
}
214262

215263
static I get_first_node(P &program)

0 commit comments

Comments
 (0)