Skip to content

Commit 9b0133d

Browse files
committed
cfgt: introduce and use a public interface when interacting with the entry map
This eliminates many uses of the cfg[cfg.entry_map[instruction]] pattern, and makes it easier to refactor / change the implementation of cfgt.
1 parent 82d0ea2 commit 9b0133d

File tree

8 files changed

+136
-109
lines changed

8 files changed

+136
-109
lines changed

jbmc/src/java_bytecode/java_local_variable_table.cpp

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,10 @@ struct procedure_local_cfg_baset<
3232
: public grapht<
3333
cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>
3434
{
35+
typedef grapht<
36+
cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>
37+
base_grapht;
38+
typedef typename base_grapht::nodet nodet;
3539
typedef java_bytecode_convert_methodt::method_with_amapt method_with_amapt;
3640
typedef std::map<java_bytecode_convert_methodt::method_offsett,
3741
java_bytecode_convert_methodt::method_offsett>
@@ -85,6 +89,23 @@ struct procedure_local_cfg_baset<
8589
}
8690
}
8791

92+
java_bytecode_convert_methodt::method_offsett get_node_index(
93+
const java_bytecode_convert_methodt::method_offsett &instruction) const
94+
{
95+
return entry_map.at(instruction);
96+
}
97+
98+
nodet &
99+
get_node(const java_bytecode_convert_methodt::method_offsett &instruction)
100+
{
101+
return (*this)[get_node_index(instruction)];
102+
}
103+
const nodet &get_node(
104+
const java_bytecode_convert_methodt::method_offsett &instruction) const
105+
{
106+
return (*this)[get_node_index(instruction)];
107+
}
108+
88109
static java_bytecode_convert_methodt::method_offsett
89110
get_first_node(const method_with_amapt &args)
90111
{

src/analyses/cfg_dominators.h

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -53,14 +53,14 @@ class cfg_dominators_templatet
5353
/// for \p program_point
5454
const typename cfgt::nodet &get_node(const T &program_point) const
5555
{
56-
return cfg[cfg.entry_map.at(program_point)];
56+
return cfg.get_node(program_point);
5757
}
5858

5959
/// Get the graph node (which gives dominators, predecessors and successors)
6060
/// for \p program_point
6161
typename cfgt::nodet &get_node(const T &program_point)
6262
{
63-
return cfg[cfg.entry_map.at(program_point)];
63+
return cfg.get_node(program_point);
6464
}
6565

6666
/// Returns true if the program point corresponding to \p rhs_node is
@@ -149,7 +149,7 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
149149
entry_node = cfgt::get_last_node(program);
150150
else
151151
entry_node = cfgt::get_first_node(program);
152-
typename cfgt::nodet &n=cfg[cfg.entry_map[entry_node]];
152+
typename cfgt::nodet &n = cfg.get_node(entry_node);
153153
n.dominators.insert(entry_node);
154154

155155
for(typename cfgt::edgest::const_iterator
@@ -165,7 +165,7 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
165165
worklist.pop_front();
166166

167167
bool changed=false;
168-
typename cfgt::nodet &node=cfg[cfg.entry_map[current]];
168+
typename cfgt::nodet &node = cfg.get_node(current);
169169
if(node.dominators.empty())
170170
{
171171
for(const auto &edge : (post_dom ? node.out : node.in))
@@ -248,7 +248,7 @@ 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.entry_map)
251+
for(const auto &node : cfg.entries())
252252
{
253253
auto n=node.first;
254254

src/goto-diff/change_impact.cpp

Lines changed: 23 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -66,27 +66,26 @@ void full_slicert::operator()(
6666
// declarations or dead instructions may be necessary as well
6767
decl_deadt decl_dead;
6868

69-
for(cfgt::entry_mapt::iterator
70-
e_it=cfg.entry_map.begin();
71-
e_it!=cfg.entry_map.end();
72-
e_it++)
69+
for(const auto &entry : cfg.entries())
7370
{
74-
if(criterion(e_it->first))
75-
add_to_queue(queue, e_it->second, e_it->first);
76-
else if(implicit(e_it->first))
77-
add_to_queue(queue, e_it->second, e_it->first);
78-
else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
79-
e_it->first->is_throw())
80-
jumps.push_back(e_it->second);
81-
else if(e_it->first->is_decl())
71+
const auto &instruction = instruction_and_index.first;
72+
const auto instruction_node_index = instruction_and_index.second;
73+
if(criterion(instruction))
74+
add_to_queue(queue, instruction_node_index, instruction);
75+
else if(implicit(instruction))
76+
add_to_queue(queue, instruction_node_index, instruction);
77+
else if((instruction->is_goto() && instruction->guard.is_true()) ||
78+
instruction->is_throw())
79+
jumps.push_back(instruction_node_index);
80+
else if(instruction->is_decl())
8281
{
83-
const auto &s=to_code_decl(e_it->first->code).symbol();
84-
decl_dead[s.get_identifier()].push(e_it->second);
82+
const auto &s=to_code_decl(instruction->code).symbol();
83+
decl_dead[s.get_identifier()].push(instruction_node_index);
8584
}
86-
else if(e_it->first->is_dead())
85+
else if(instruction->is_dead())
8786
{
88-
const auto &s=to_code_dead(e_it->first->code).symbol();
89-
decl_dead[s.get_identifier()].push(e_it->second);
87+
const auto &s=to_code_dead(instruction->code).symbol();
88+
decl_dead[s.get_identifier()].push(instruction_node_index);
9089
}
9190
}
9291

@@ -105,21 +104,21 @@ void full_slicert::operator()(
105104
{
106105
Forall_goto_program_instructions(i_it, f_it->second.body)
107106
{
108-
const cfgt::entryt &e=cfg.entry_map[i_it];
107+
const auto &node = cfg.get_node(i_it);
109108
if(!i_it->is_end_function() && // always retained
110-
!cfg[e].node_required)
109+
!node.node_required)
111110
i_it->make_skip();
112111
#ifdef DEBUG_FULL_SLICERT
113112
else
114113
{
115114
std::string c="ins:"+std::to_string(i_it->location_number);
116115
c+=" req by:";
117116
for(std::set<unsigned>::const_iterator
118-
req_it=cfg[e].required_by.begin();
119-
req_it!=cfg[e].required_by.end();
117+
req_it=node.required_by.begin();
118+
req_it!=node.required_by.end();
120119
++req_it)
121120
{
122-
if(req_it!=cfg[e].required_by.begin())
121+
if(req_it!=node.required_by.begin())
123122
c+=",";
124123
c+=std::to_string(*req_it);
125124
}
@@ -144,13 +143,10 @@ void full_slicert::fixedpoint(
144143
{
145144
std::vector<cfgt::entryt> dep_node_to_cfg;
146145
dep_node_to_cfg.reserve(dep_graph.size());
146+
147147
for(unsigned i=0; i<dep_graph.size(); ++i)
148148
{
149-
cfgt::entry_mapt::const_iterator entry=
150-
cfg.entry_map.find(dep_graph[i].PC);
151-
assert(entry!=cfg.entry_map.end());
152-
153-
dep_node_to_cfg.push_back(entry->second);
149+
dep_node_to_cfg.push_back(cfg.get_node_index(dep_graph[i].PC));
154150
}
155151

156152
// process queue until empty

src/goto-instrument/count_eloc.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -106,10 +106,10 @@ void print_path_lengths(const goto_modelt &goto_model)
106106

107107
const goto_programt &start_program=start->second.body;
108108

109-
const cfgt::entryt &start_node=
110-
cfg.entry_map[start_program.instructions.begin()];
111-
const cfgt::entryt &last_node=
112-
cfg.entry_map[--start_program.instructions.end()];
109+
const cfgt::entryt &start_node =
110+
cfg.get_node_index(start_program.instructions.begin());
111+
const cfgt::entryt &last_node =
112+
cfg.get_node_index(--start_program.instructions.end());
113113

114114
cfgt::patht shortest_path;
115115
cfg.shortest_path(start_node, last_node, shortest_path);
@@ -123,7 +123,7 @@ void print_path_lengths(const goto_modelt &goto_model)
123123
if(i_it->is_backwards_goto() ||
124124
i_it==gf_it->second.body.instructions.begin())
125125
{
126-
const cfgt::entryt &node=cfg.entry_map[i_it];
126+
const cfgt::entryt &node = cfg.get_node_index(i_it);
127127
cfgt::patht loop;
128128
cfg.shortest_loop(node, loop);
129129

src/goto-instrument/full_slicer.cpp

Lines changed: 34 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -46,15 +46,9 @@ 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());
52-
53-
for(cfgt::edgest::const_iterator
54-
it=cfg[entry->second].in.begin();
55-
it!=cfg[entry->second].in.end();
56-
++it)
57-
add_to_queue(queue, it->first, node.PC);
49+
const auto &entry = cfg.get_node(begin_function);
50+
for(const auto &in_edge : entry.in)
51+
add_to_queue(queue, in_edge.first, node.PC);
5852
}
5953

6054
void full_slicert::add_decl_dead(
@@ -135,11 +129,7 @@ void full_slicert::add_jumps(
135129
goto_programt::const_targett lex_succ=j.PC;
136130
for( ; !lex_succ->is_end_function(); ++lex_succ)
137131
{
138-
cfgt::entry_mapt::const_iterator entry=
139-
cfg.entry_map.find(lex_succ);
140-
assert(entry!=cfg.entry_map.end());
141-
142-
if(cfg[entry->second].node_required)
132+
if(cfg.get_node(lex_succ).node_required)
143133
break;
144134
}
145135
if(lex_succ->is_end_function())
@@ -170,13 +160,10 @@ void full_slicert::add_jumps(
170160
d_it != j_PC_node.dominators.end();
171161
++d_it)
172162
{
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)
163+
const auto &node = cfg.get_node(*d_it);
164+
if(node.node_required)
178165
{
179-
const irep_idt &id2 = cfg[entry->second].function_id;
166+
const irep_idt &id2 = node.function_id;
180167
INVARIANT(id==id2,
181168
"goto/jump expected to be within a single function");
182169

@@ -209,14 +196,9 @@ void full_slicert::fixedpoint(
209196
{
210197
std::vector<cfgt::entryt> dep_node_to_cfg;
211198
dep_node_to_cfg.reserve(dep_graph.size());
212-
for(dependence_grapht::node_indext i=0; i<dep_graph.size(); ++i)
213-
{
214-
cfgt::entry_mapt::const_iterator entry=
215-
cfg.entry_map.find(dep_graph[i].PC);
216-
assert(entry!=cfg.entry_map.end());
217199

218-
dep_node_to_cfg.push_back(entry->second);
219-
}
200+
for(dependence_grapht::node_indext i = 0; i < dep_graph.size(); ++i)
201+
dep_node_to_cfg.push_back(cfg.get_node_index(dep_graph[i].PC));
220202

221203
// process queue until empty
222204
while(!queue.empty())
@@ -279,7 +261,7 @@ void full_slicert::operator()(
279261
forall_goto_functions(f_it, goto_functions)
280262
{
281263
forall_goto_program_instructions(i_it, f_it->second.body)
282-
cfg[cfg.entry_map[i_it]].function_id = f_it->first;
264+
cfg.get_node(i_it).function_id = f_it->first;
283265
}
284266

285267
// fill queue with according to slicing criterion
@@ -289,28 +271,27 @@ void full_slicert::operator()(
289271
// declarations or dead instructions may be necessary as well
290272
decl_deadt decl_dead;
291273

292-
for(cfgt::entry_mapt::iterator
293-
e_it=cfg.entry_map.begin();
294-
e_it!=cfg.entry_map.end();
295-
e_it++)
274+
for(const auto &instruction_and_index : cfg.entries())
296275
{
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);
276+
const auto &instruction = instruction_and_index.first;
277+
const auto instruction_node_index = instruction_and_index.second;
278+
if(criterion(cfg[instruction_node_index].function_id, instruction))
279+
add_to_queue(queue, instruction_node_index, instruction);
280+
else if(implicit(instruction))
281+
add_to_queue(queue, instruction_node_index, instruction);
301282
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())
283+
(instruction->is_goto() && instruction->get_condition().is_true()) ||
284+
instruction->is_throw())
285+
jumps.push_back(instruction_node_index);
286+
else if(instruction->is_decl())
306287
{
307-
const auto &s = to_code_decl(e_it->first->code).symbol();
308-
decl_dead[s.get_identifier()].push(e_it->second);
288+
const auto &s = to_code_decl(instruction->code).symbol();
289+
decl_dead[s.get_identifier()].push(instruction_node_index);
309290
}
310-
else if(e_it->first->is_dead())
291+
else if(instruction->is_dead())
311292
{
312-
const auto &s = to_code_dead(e_it->first->code).symbol();
313-
decl_dead[s.get_identifier()].push(e_it->second);
293+
const auto &s = to_code_dead(instruction->code).symbol();
294+
decl_dead[s.get_identifier()].push(instruction_node_index);
314295
}
315296
}
316297

@@ -329,9 +310,10 @@ void full_slicert::operator()(
329310
{
330311
Forall_goto_program_instructions(i_it, f_it->second.body)
331312
{
332-
const cfgt::entryt &e=cfg.entry_map[i_it];
333-
if(!i_it->is_end_function() && // always retained
334-
!cfg[e].node_required)
313+
const auto &cfg_node = cfg.get_node(i_it);
314+
if(
315+
!i_it->is_end_function() && // always retained
316+
!cfg_node.node_required)
335317
{
336318
i_it->turn_into_skip();
337319
}
@@ -340,12 +322,12 @@ void full_slicert::operator()(
340322
{
341323
std::string c="ins:"+std::to_string(i_it->location_number);
342324
c+=" req by:";
343-
for(std::set<unsigned>::const_iterator
344-
req_it=cfg[e].required_by.begin();
345-
req_it!=cfg[e].required_by.end();
325+
for(std::set<unsigned>::const_iterator req_it =
326+
cfg_node.required_by.begin();
327+
req_it != cfg_node.required_by.end();
346328
++req_it)
347329
{
348-
if(req_it!=cfg[e].required_by.begin())
330+
if(req_it != cfg_node.required_by.begin())
349331
c+=",";
350332
c+=std::to_string(*req_it);
351333
}

src/goto-instrument/points_to.cpp

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -21,12 +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++)
24+
for(const auto &instruction_and_entry : cfg.entries())
2825
{
29-
if(transform(cfg[e_it->second]))
26+
if(transform(cfg[instruction_and_entry.second]))
3027
added=true;
3128
}
3229
}

0 commit comments

Comments
 (0)