Skip to content

Commit b8a4382

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 b867245 commit b8a4382

File tree

3 files changed

+74
-2
lines changed

3 files changed

+74
-2
lines changed

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/goto_instrument_parse_options.cpp

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -692,6 +692,10 @@ int goto_instrument_parse_optionst::doit()
692692
// applied
693693
restore_returns(goto_model);
694694

695+
// dump_c (actually goto_program2code) requires valid instruction
696+
// location numbers:
697+
goto_model.goto_functions.update();
698+
695699
if(cmdline.args.size()==2)
696700
{
697701
#ifdef _MSC_VER
@@ -1520,6 +1524,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
15201524
do_indirect_call_and_rtti_removal();
15211525

15221526
log.status() << "Performing a reachability slice" << messaget::eom;
1527+
1528+
// reachability_slicer requires that the model has unique location numbers:
1529+
goto_model.goto_functions.update();
1530+
15231531
if(cmdline.isset("property"))
15241532
reachability_slicer(goto_model, cmdline.get_values("property"));
15251533
else
@@ -1546,7 +1554,11 @@ void goto_instrument_parse_optionst::instrument_goto_program()
15461554
if(cmdline.isset("property"))
15471555
property_slicer(goto_model, cmdline.get_values("property"));
15481556
else
1557+
{
1558+
// full_slicer requires that the model has unique location numbers:
1559+
goto_model.goto_functions.update();
15491560
full_slicer(goto_model);
1561+
}
15501562
}
15511563

15521564
// splice option
@@ -1567,6 +1579,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
15671579
{
15681580
do_indirect_call_and_rtti_removal();
15691581

1582+
// reachability_slicer requires that the model has unique location numbers:
1583+
goto_model.goto_functions.update();
1584+
15701585
log.status() << "Slicing away initializations of unused global variables"
15711586
<< messaget::eom;
15721587
slice_global_inits(goto_model);
@@ -1595,6 +1610,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
15951610

15961611
aggressive_slicer.doit();
15971612

1613+
goto_model.goto_functions.update();
1614+
15981615
log.status() << "Performing a reachability slice" << messaget::eom;
15991616
if(cmdline.isset("property"))
16001617
reachability_slicer(goto_model, cmdline.get_values("property"));

src/goto-programs/cfg.h

Lines changed: 54 additions & 2 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));
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,7 +93,11 @@ 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:
@@ -114,6 +142,12 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
114142
{
115143
return data.at(t);
116144
}
145+
146+
template <class Iter>
147+
void setup_for_keys(Iter begin, Iter end)
148+
{
149+
data.setup_for_keys(begin, end);
150+
}
117151
};
118152
entry_mapt entry_map;
119153

@@ -173,12 +207,30 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
173207
void operator()(
174208
const goto_functionst &goto_functions)
175209
{
210+
std::vector<goto_programt::const_targett> possible_keys;
211+
for(const auto &id_and_function : goto_functions.function_map)
212+
{
213+
const auto &instructions = id_and_function.second.body.instructions;
214+
possible_keys.reserve(
215+
possible_keys.size() +
216+
std::distance(instructions.begin(), instructions.end()));
217+
for(auto it = instructions.begin(); it != instructions.end(); ++it)
218+
possible_keys.push_back(it);
219+
}
220+
entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
176221
compute_edges(goto_functions);
177222
}
178223

179224
void operator()(P &goto_program)
180225
{
181226
goto_functionst goto_functions;
227+
std::vector<goto_programt::const_targett> possible_keys;
228+
const auto &instructions = goto_program.instructions;
229+
possible_keys.reserve(
230+
std::distance(instructions.begin(), instructions.end()));
231+
for(auto it = instructions.begin(); it != instructions.end(); ++it)
232+
possible_keys.push_back(it);
233+
entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
182234
compute_edges(goto_functions, goto_program);
183235
}
184236

0 commit comments

Comments
 (0)