Skip to content

Commit 6e06a40

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 ef6980f commit 6e06a40

File tree

7 files changed

+128
-83
lines changed

7 files changed

+128
-83
lines changed

src/goto-analyzer/unreachable_instructions.cpp

Lines changed: 3 additions & 7 deletions
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.entry_map.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

src/goto-instrument/dump_c.cpp

Lines changed: 3 additions & 0 deletions
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);

src/goto-instrument/full_slicer.cpp

Lines changed: 25 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -46,13 +46,10 @@ void full_slicert::add_function_calls(
4646
goto_programt::const_targett begin_function=
4747
f_it->second.body.instructions.begin();
4848

49-
cfgt::entry_mapt::const_iterator entry=
50-
cfg.entry_map.find(begin_function);
51-
assert(entry!=cfg.entry_map.end());
49+
const auto &entry = cfg.entry_map.at(begin_function);
5250

53-
for(cfgt::edgest::const_iterator
54-
it=cfg[entry->second].in.begin();
55-
it!=cfg[entry->second].in.end();
51+
for(cfgt::edgest::const_iterator it = cfg[entry].in.begin();
52+
it != cfg[entry].in.end();
5653
++it)
5754
add_to_queue(queue, it->first, node.PC);
5855
}
@@ -135,11 +132,9 @@ void full_slicert::add_jumps(
135132
goto_programt::const_targett lex_succ=j.PC;
136133
for( ; !lex_succ->is_end_function(); ++lex_succ)
137134
{
138-
cfgt::entry_mapt::const_iterator entry=
139-
cfg.entry_map.find(lex_succ);
140-
assert(entry!=cfg.entry_map.end());
135+
const auto &entry = cfg.entry_map.at(lex_succ);
141136

142-
if(cfg[entry->second].node_required)
137+
if(cfg[entry].node_required)
143138
break;
144139
}
145140
if(lex_succ->is_end_function())
@@ -170,13 +165,10 @@ void full_slicert::add_jumps(
170165
d_it!=j_PC_node.dominators.end();
171166
++d_it)
172167
{
173-
cfgt::entry_mapt::const_iterator entry=
174-
cfg.entry_map.find(*d_it);
175-
assert(entry!=cfg.entry_map.end());
176-
177-
if(cfg[entry->second].node_required)
168+
const auto &entry = cfg.entry_map.at(*d_it);
169+
if(cfg[entry].node_required)
178170
{
179-
const irep_idt &id2 = cfg[entry->second].function_id;
171+
const irep_idt &id2 = cfg[entry].function_id;
180172
INVARIANT(id==id2,
181173
"goto/jump expected to be within a single function");
182174

@@ -211,11 +203,8 @@ void full_slicert::fixedpoint(
211203
dep_node_to_cfg.reserve(dep_graph.size());
212204
for(dependence_grapht::node_indext i=0; i<dep_graph.size(); ++i)
213205
{
214-
cfgt::entry_mapt::const_iterator entry=
215-
cfg.entry_map.find(dep_graph[i].PC);
216-
assert(entry!=cfg.entry_map.end());
217-
218-
dep_node_to_cfg.push_back(entry->second);
206+
const auto &entry = cfg.entry_map.at(dep_graph[i].PC);
207+
dep_node_to_cfg.push_back(entry);
219208
}
220209

221210
// process queue until empty
@@ -289,28 +278,26 @@ void full_slicert::operator()(
289278
// declarations or dead instructions may be necessary as well
290279
decl_deadt decl_dead;
291280

292-
for(cfgt::entry_mapt::iterator
293-
e_it=cfg.entry_map.begin();
294-
e_it!=cfg.entry_map.end();
295-
e_it++)
281+
for(const auto &instruction : cfg.entry_map.keys())
296282
{
297-
if(criterion(cfg[e_it->second].function_id, e_it->first))
298-
add_to_queue(queue, e_it->second, e_it->first);
299-
else if(implicit(e_it->first))
300-
add_to_queue(queue, e_it->second, e_it->first);
283+
const auto &instruction_node_index = cfg.entry_map.at(instruction);
284+
if(criterion(cfg[instruction_node_index].function_id, instruction))
285+
add_to_queue(queue, instruction_node_index, instruction);
286+
else if(implicit(instruction))
287+
add_to_queue(queue, instruction_node_index, instruction);
301288
else if(
302-
(e_it->first->is_goto() && e_it->first->get_condition().is_true()) ||
303-
e_it->first->is_throw())
304-
jumps.push_back(e_it->second);
305-
else if(e_it->first->is_decl())
289+
(instruction->is_goto() && instruction->get_condition().is_true()) ||
290+
instruction->is_throw())
291+
jumps.push_back(instruction_node_index);
292+
else if(instruction->is_decl())
306293
{
307-
const auto &s = to_code_decl(e_it->first->code).symbol();
308-
decl_dead[s.get_identifier()].push(e_it->second);
294+
const auto &s = to_code_decl(instruction->code).symbol();
295+
decl_dead[s.get_identifier()].push(instruction_node_index);
309296
}
310-
else if(e_it->first->is_dead())
297+
else if(instruction->is_dead())
311298
{
312-
const auto &s = to_code_dead(e_it->first->code).symbol();
313-
decl_dead[s.get_identifier()].push(e_it->second);
299+
const auto &s = to_code_dead(instruction->code).symbol();
300+
decl_dead[s.get_identifier()].push(instruction_node_index);
314301
}
315302
}
316303

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 17 additions & 0 deletions
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"));

src/goto-instrument/points_to.cpp

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -21,14 +21,9 @@ void points_tot::fixedpoint()
2121
{
2222
added=false;
2323

24-
for(cfgt::entry_mapt::iterator
25-
e_it=cfg.entry_map.begin();
26-
e_it!=cfg.entry_map.end();
27-
e_it++)
28-
{
29-
if(transform(cfg[e_it->second]))
24+
for(const auto &key : cfg.entry_map.keys())
25+
if(transform(cfg[cfg.entry_map.at(key)]))
3026
added=true;
31-
}
3227
}
3328
while(added);
3429
}

src/goto-instrument/reachability_slicer.cpp

Lines changed: 8 additions & 10 deletions
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.entry_map)
42+
for(const auto &instruction : cfg.entry_map.keys())
4343
{
44+
const auto cfg_node_index = cfg.entry_map.at(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())
@@ -64,12 +65,9 @@ bool reachability_slicert::is_same_target(
6465
{
6566
// Avoid comparing iterators belonging to different functions, and therefore
6667
// different std::lists.
67-
cfgt::entry_mapt::const_iterator it1_entry = cfg.entry_map.find(it1);
68-
cfgt::entry_mapt::const_iterator it2_entry = cfg.entry_map.find(it2);
69-
return it1_entry != cfg.entry_map.end() && it2_entry != cfg.entry_map.end() &&
70-
cfg[it1_entry->second].function_id ==
71-
cfg[it2_entry->second].function_id &&
72-
it1 == it2;
68+
const auto &it1_entry = cfg.entry_map.at(it1);
69+
const auto &it2_entry = cfg.entry_map.at(it2);
70+
return cfg[it1_entry].function_id == cfg[it2_entry].function_id && it1 == it2;
7371
}
7472

7573
/// Perform backward depth-first search of the control-flow graph of the

src/goto-programs/cfg.h

Lines changed: 70 additions & 21 deletions
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
///
@@ -66,28 +90,16 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
6690

6791
class entry_mapt final
6892
{
69-
typedef std::map<goto_programt::const_targett, entryt> data_typet;
93+
typedef dense_integer_mapt<
94+
goto_programt::const_targett,
95+
entryt,
96+
cfg_instruction_to_dense_integert<goto_programt::const_targett>>
97+
data_typet;
7098
data_typet data;
7199

72100
public:
73101
grapht< cfg_base_nodet<T, I> > &container;
74102

75-
// NOLINTNEXTLINE(readability/identifiers)
76-
typedef data_typet::iterator iterator;
77-
// NOLINTNEXTLINE(readability/identifiers)
78-
typedef data_typet::const_iterator const_iterator;
79-
80-
template <typename U>
81-
const_iterator find(U &&u) const { return data.find(std::forward<U>(u)); }
82-
83-
iterator begin() { return data.begin(); }
84-
const_iterator begin() const { return data.begin(); }
85-
const_iterator cbegin() const { return data.cbegin(); }
86-
87-
iterator end() { return data.end(); }
88-
const_iterator end() const { return data.end(); }
89-
const_iterator cend() const { return data.cend(); }
90-
91103
explicit entry_mapt(grapht< cfg_base_nodet<T, I> > &_container):
92104
container(_container)
93105
{
@@ -97,10 +109,10 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
97109
{
98110
auto e=data.insert(std::make_pair(t, 0));
99111

100-
if(e.second)
101-
e.first->second=container.add_node();
112+
if(e)
113+
data.at(t) = container.add_node();
102114

103-
return e.first->second;
115+
return data.at(t);
104116
}
105117

106118
entryt &at(const goto_programt::const_targett &t)
@@ -111,6 +123,25 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
111123
{
112124
return data.at(t);
113125
}
126+
127+
std::size_t count(const goto_programt::const_targett &t) const
128+
{
129+
return data.count(t);
130+
}
131+
132+
typedef data_typet::possible_keyst keyst;
133+
const keyst &keys() const
134+
{
135+
// We always define exactly the keys the entry map was set up for, so
136+
// data's possible key set is exactly our key set
137+
return data.possible_keys();
138+
}
139+
140+
template <class Iter>
141+
void setup_for_keys(Iter begin, Iter end)
142+
{
143+
data.setup_for_keys(begin, end);
144+
}
114145
};
115146
entry_mapt entry_map;
116147

@@ -170,12 +201,30 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
170201
void operator()(
171202
const goto_functionst &goto_functions)
172203
{
204+
std::vector<goto_programt::const_targett> possible_keys;
205+
for(const auto &id_and_function : goto_functions.function_map)
206+
{
207+
const auto &instructions = id_and_function.second.body.instructions;
208+
possible_keys.reserve(
209+
possible_keys.size() +
210+
std::distance(instructions.begin(), instructions.end()));
211+
for(auto it = instructions.begin(); it != instructions.end(); ++it)
212+
possible_keys.push_back(it);
213+
}
214+
entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
173215
compute_edges(goto_functions);
174216
}
175217

176218
void operator()(P &goto_program)
177219
{
178220
goto_functionst goto_functions;
221+
std::vector<goto_programt::const_targett> possible_keys;
222+
const auto &instructions = goto_program.instructions;
223+
possible_keys.reserve(
224+
std::distance(instructions.begin(), instructions.end()));
225+
for(auto it = instructions.begin(); it != instructions.end(); ++it)
226+
possible_keys.push_back(it);
227+
entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
179228
compute_edges(goto_functions, goto_program);
180229
}
181230

0 commit comments

Comments
 (0)