Skip to content

Commit c260acd

Browse files
committed
Move goto_programt::(const_)targett comparison to a struct
This makes sure no one can inadvertently use less-than comparison on those iterators, which may lead to non-reproducible behaviour (see diffblue#6782).
1 parent 87e992b commit c260acd

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

51 files changed

+252
-117
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -240,7 +240,23 @@ class java_bytecode_convert_methodt
240240

241241
public:
242242
typedef std::map<method_offsett, converted_instructiont> address_mapt;
243-
typedef std::pair<const methodt &, const address_mapt &> method_with_amapt;
243+
struct method_with_amapt
244+
{
245+
method_with_amapt(const methodt &m, const address_mapt &a)
246+
: method_with_amap(m, a)
247+
{
248+
}
249+
250+
std::pair<const methodt &, const address_mapt &> method_with_amap;
251+
252+
struct target_less_than // NOLINT(readability/identifiers)
253+
{
254+
bool operator()(const method_offsett &a, const method_offsett &b) const
255+
{
256+
return a < b;
257+
}
258+
};
259+
};
244260
typedef cfg_dominators_templatet<method_with_amapt, method_offsett, false>
245261
java_cfg_dominatorst;
246262

jbmc/src/java_bytecode/java_local_variable_table.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,8 @@ struct procedure_local_cfg_baset<
4646

4747
void operator()(const method_with_amapt &args)
4848
{
49-
const auto &method=args.first;
50-
const auto &amap=args.second;
49+
const auto &method = args.method_with_amap.first;
50+
const auto &amap = args.method_with_amap.second;
5151
for(const auto &inst : amap)
5252
{
5353
// Map instruction PCs onto node indices:
@@ -109,18 +109,18 @@ struct procedure_local_cfg_baset<
109109
static java_bytecode_convert_methodt::method_offsett
110110
get_first_node(const method_with_amapt &args)
111111
{
112-
return args.second.begin()->first;
112+
return args.method_with_amap.second.begin()->first;
113113
}
114114

115115
static java_bytecode_convert_methodt::method_offsett
116116
get_last_node(const method_with_amapt &args)
117117
{
118-
return (--args.second.end())->first;
118+
return (--args.method_with_amap.second.end())->first;
119119
}
120120

121121
static bool nodes_empty(const method_with_amapt &args)
122122
{
123-
return args.second.empty();
123+
return args.method_with_amap.second.empty();
124124
}
125125
};
126126

src/analyses/ai_storage.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,8 @@ class ai_storage_baset
100100
class trace_map_storaget : public ai_storage_baset
101101
{
102102
protected:
103-
typedef std::map<locationt, trace_set_ptrt> trace_mapt;
103+
typedef std::map<locationt, trace_set_ptrt, goto_programt::target_less_than>
104+
trace_mapt;
104105
trace_mapt trace_map;
105106

106107
// This retains one part of a shared_ptr to the history object

src/analyses/call_graph.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@ class call_grapht
9898
typedef goto_programt::const_targett locationt;
9999

100100
/// Type of a set of callsites
101-
typedef std::set<locationt> locationst;
101+
typedef std::set<locationt, goto_programt::target_less_than> locationst;
102102

103103
/// Type mapping from call-graph edges onto the set of call instructions
104104
/// that make that call.

src/analyses/cfg_dominators.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ template <class P, class T, bool post_dom>
3636
class cfg_dominators_templatet
3737
{
3838
public:
39-
typedef std::set<T> target_sett;
39+
typedef std::set<T, typename P::target_less_than> target_sett;
4040

4141
struct nodet
4242
{
@@ -218,12 +218,12 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
218218
{
219219
if(*n_it==current)
220220
++n_it;
221-
else if(*n_it<*o_it)
221+
else if(typename P::target_less_than()(*n_it, *o_it))
222222
{
223223
changed=true;
224224
node.dominators.erase(n_it++);
225225
}
226-
else if(*o_it<*n_it)
226+
else if(typename P::target_less_than()(*o_it, *n_it))
227227
++o_it;
228228
else
229229
{

src/analyses/dependence_graph.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -172,7 +172,9 @@ class dep_graph_domaint:public ai_domain_baset
172172
node_indext node_id;
173173
bool has_changed;
174174

175-
typedef std::set<goto_programt::const_targett> depst;
175+
typedef std::
176+
set<goto_programt::const_targett, goto_programt::target_less_than>
177+
depst;
176178

177179
// Set of locations with control instructions on which the instruction at this
178180
// location has a control dependency on

src/analyses/flow_insensitive_analysis.h

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -93,9 +93,9 @@ class flow_insensitive_analysis_baset
9393
typedef flow_insensitive_abstract_domain_baset statet;
9494
typedef goto_programt::const_targett locationt;
9595

96-
std::set<locationt> seen_locations;
96+
std::set<locationt, goto_programt::target_less_than> seen_locations;
9797

98-
std::map<locationt, unsigned> statistics;
98+
std::map<locationt, unsigned, goto_programt::target_less_than> statistics;
9999

100100
bool seen(const locationt &l)
101101
{
@@ -155,7 +155,11 @@ class flow_insensitive_analysis_baset
155155
protected:
156156
const namespacet &ns;
157157

158-
typedef std::priority_queue<locationt> working_sett;
158+
typedef std::priority_queue<
159+
locationt,
160+
std::vector<locationt>,
161+
goto_programt::target_less_than>
162+
working_sett;
159163

160164
locationt get_next(working_sett &working_set);
161165

src/analyses/is_threaded.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,9 @@ class is_threadedt
4444
}
4545

4646
protected:
47-
typedef std::set<goto_programt::const_targett> is_threaded_sett;
47+
typedef std::
48+
set<goto_programt::const_targett, goto_programt::target_less_than>
49+
is_threaded_sett;
4850
is_threaded_sett is_threaded_set;
4951

5052
void compute(

src/analyses/lexical_loops.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -152,7 +152,7 @@ bool lexical_loops_templatet<P, T>::compute_lexical_loop(
152152
"loop header should come lexically before the tail");
153153

154154
std::stack<T> stack;
155-
std::set<T> loop_instructions;
155+
std::set<T, typename P::target_less_than> loop_instructions;
156156

157157
loop_instructions.insert(loop_head);
158158
loop_instructions.insert(loop_tail);

src/analyses/local_cfg.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,9 @@ class local_cfgt
2929
successorst successors;
3030
};
3131

32-
typedef std::map<goto_programt::const_targett, node_nrt> loc_mapt;
32+
typedef std::
33+
map<goto_programt::const_targett, node_nrt, goto_programt::target_less_than>
34+
loc_mapt;
3335
loc_mapt loc_map;
3436

3537
typedef std::vector<nodet> nodest;

src/analyses/local_may_alias.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,9 @@ class local_may_alias_factoryt
140140
typedef std::map<irep_idt, std::unique_ptr<local_may_aliast> > fkt_mapt;
141141
fkt_mapt fkt_map;
142142

143-
typedef std::map<goto_programt::const_targett, irep_idt > target_mapt;
143+
typedef std::
144+
map<goto_programt::const_targett, irep_idt, goto_programt::target_less_than>
145+
target_mapt;
144146
target_mapt target_map;
145147
};
146148

src/analyses/loop_analysis.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ class loop_analysist;
2222
template <class T>
2323
class loop_templatet
2424
{
25-
typedef std::set<T> loop_instructionst;
25+
typedef std::set<T, goto_programt::target_less_than> loop_instructionst;
2626
loop_instructionst loop_instructions;
2727

2828
friend loop_analysist<T>;
@@ -83,7 +83,7 @@ class loop_analysist
8383
public:
8484
typedef loop_templatet<T> loopt;
8585
// map loop headers to loops
86-
typedef std::map<T, loopt> loop_mapt;
86+
typedef std::map<T, loopt, goto_programt::target_less_than> loop_mapt;
8787

8888
loop_mapt loop_map;
8989

src/analyses/reaching_definitions.h

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -114,9 +114,9 @@ inline bool operator<(
114114
const reaching_definitiont &a,
115115
const reaching_definitiont &b)
116116
{
117-
if(a.definition_at<b.definition_at)
117+
if(goto_programt::target_less_than()(a.definition_at, b.definition_at))
118118
return true;
119-
if(b.definition_at<a.definition_at)
119+
if(goto_programt::target_less_than()(b.definition_at, a.definition_at))
120120
return false;
121121

122122
if(a.bit_begin.is_unknown() != b.bit_begin.is_unknown())
@@ -250,7 +250,8 @@ class rd_range_domaint:public ai_domain_baset
250250

251251
// each element x represents a range of bits [x.first, x.second)
252252
typedef std::multimap<range_spect, range_spect> rangest;
253-
typedef std::map<locationt, rangest> ranges_at_loct;
253+
typedef std::map<locationt, rangest, goto_programt::target_less_than>
254+
ranges_at_loct;
254255

255256
const ranges_at_loct &get(const irep_idt &identifier) const;
256257
void clear_cache(const irep_idt &identifier) const

src/analyses/static_analysis.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -317,7 +317,7 @@ class static_analysist:public static_analysis_baset
317317
}
318318

319319
protected:
320-
typedef std::map<locationt, T> state_mapt;
320+
typedef std::map<locationt, T, goto_programt::target_less_than> state_mapt;
321321
state_mapt state_map;
322322

323323
virtual statet &get_state(locationt l)

src/analyses/variable-sensitivity/context_abstract_object.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ class context_abstract_objectt : public abstract_objectt
132132

133133
exprt to_predicate_internal(const exprt &name) const override;
134134

135-
typedef std::set<locationt> locationst;
135+
typedef std::set<locationt, goto_programt::target_less_than> locationst;
136136

137137
virtual context_abstract_object_ptrt
138138
update_location_context_internal(const locationst &locations) const = 0;

src/analyses/variable-sensitivity/data_dependency_context.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -327,10 +327,11 @@ data_dependency_contextt::abstract_object_merge_internal(
327327
*
328328
* \return set of data dependencies
329329
*/
330-
std::set<goto_programt::const_targett>
330+
std::set<goto_programt::const_targett, goto_programt::target_less_than>
331331
data_dependency_contextt::get_data_dependencies() const
332332
{
333-
std::set<goto_programt::const_targett> result;
333+
std::set<goto_programt::const_targett, goto_programt::target_less_than>
334+
result;
334335
for(const auto &d : data_deps)
335336
result.insert(d);
336337
return result;
@@ -341,10 +342,11 @@ data_dependency_contextt::get_data_dependencies() const
341342
*
342343
* \return set of data dominators
343344
*/
344-
std::set<goto_programt::const_targett>
345+
std::set<goto_programt::const_targett, goto_programt::target_less_than>
345346
data_dependency_contextt::get_data_dominators() const
346347
{
347-
std::set<goto_programt::const_targett> result;
348+
std::set<goto_programt::const_targett, goto_programt::target_less_than>
349+
result;
348350
for(const auto &d : data_dominators)
349351
result.insert(d);
350352
return result;

src/analyses/variable-sensitivity/data_dependency_context.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -56,8 +56,10 @@ class data_dependency_contextt : public write_location_contextt
5656

5757
bool has_been_modified(const abstract_object_pointert &before) const override;
5858

59-
std::set<goto_programt::const_targett> get_data_dependencies() const;
60-
std::set<goto_programt::const_targett> get_data_dominators() const;
59+
std::set<goto_programt::const_targett, goto_programt::target_less_than>
60+
get_data_dependencies() const;
61+
std::set<goto_programt::const_targett, goto_programt::target_less_than>
62+
get_data_dominators() const;
6163

6264
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
6365
const override;

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -326,10 +326,13 @@ bool variable_sensitivity_dependence_domaint::merge_control_dependencies(
326326
for(const auto &c_dep : other_control_deps)
327327
{
328328
// find position to insert
329-
while(it != control_deps.end() && it->first < c_dep.first)
329+
while(it != control_deps.end() &&
330+
goto_programt::target_less_than()(it->first, c_dep.first))
330331
++it;
331332

332-
if(it == control_deps.end() || c_dep.first < it->first)
333+
if(
334+
it == control_deps.end() ||
335+
goto_programt::target_less_than()(c_dep.first, it->first))
333336
{
334337
// hint points at position that will follow the new element
335338
control_deps.insert(it, c_dep);
@@ -340,9 +343,11 @@ bool variable_sensitivity_dependence_domaint::merge_control_dependencies(
340343
INVARIANT(
341344
it != control_deps.end(), "Property of branch needed for safety");
342345
INVARIANT(
343-
!(it->first < c_dep.first), "Property of loop needed for safety");
346+
!(goto_programt::target_less_than()(it->first, c_dep.first)),
347+
"Property of loop needed for safety");
344348
INVARIANT(
345-
!(c_dep.first < it->first), "Property of loop needed for safety");
349+
!(goto_programt::target_less_than()(c_dep.first, it->first)),
350+
"Property of loop needed for safety");
346351

347352
tvt &branch1 = it->second;
348353
const tvt &branch2 = c_dep.second;

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -179,13 +179,19 @@ class variable_sensitivity_dependence_domaint
179179
data_depst;
180180
data_depst domain_data_deps;
181181

182-
typedef std::map<goto_programt::const_targett, tvt> control_depst;
182+
typedef std::
183+
map<goto_programt::const_targett, tvt, goto_programt::target_less_than>
184+
control_depst;
183185
control_depst control_deps;
184186

185-
typedef std::set<goto_programt::const_targett> control_dep_candidatest;
187+
typedef std::
188+
set<goto_programt::const_targett, goto_programt::target_less_than>
189+
control_dep_candidatest;
186190
control_dep_candidatest control_dep_candidates;
187191

188-
typedef std::set<goto_programt::const_targett> control_dep_callst;
192+
typedef std::
193+
set<goto_programt::const_targett, goto_programt::target_less_than>
194+
control_dep_callst;
189195
control_dep_callst control_dep_calls;
190196
control_dep_callst control_dep_call_candidates;
191197

src/cprover/state_encoding.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,8 @@ class state_encodingt
9292
loct first_loc;
9393
symbol_exprt entry_state = symbol_exprt(irep_idt(), typet());
9494
exprt return_lhs = nil_exprt();
95-
using incomingt = std::map<loct, std::vector<loct>>;
95+
using incomingt =
96+
std::map<loct, std::vector<loct>, goto_programt::target_less_than>;
9697
incomingt incoming;
9798

9899
static symbol_exprt va_args(irep_idt function);

src/goto-checker/fault_localization_provider.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,11 @@ class namespacet;
2121

2222
struct fault_location_infot
2323
{
24-
typedef std::map<goto_programt::const_targett, std::size_t> score_mapt;
24+
typedef std::map<
25+
goto_programt::const_targett,
26+
std::size_t,
27+
goto_programt::target_less_than>
28+
score_mapt;
2529
score_mapt scores;
2630
};
2731

src/goto-checker/symex_coverage.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,11 @@ class goto_program_coverage_recordt : public coverage_recordt
8080
}
8181

8282
unsigned hits;
83-
std::map<goto_programt::const_targett, coverage_conditiont> conditions;
83+
std::map<
84+
goto_programt::const_targett,
85+
coverage_conditiont,
86+
goto_programt::target_less_than>
87+
conditions;
8488
};
8589

8690
typedef std::map<unsigned, coverage_linet> coverage_lines_mapt;

src/goto-checker/symex_coverage.h

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -64,9 +64,16 @@ class symex_coveraget
6464
goto_programt::const_targett succ;
6565
};
6666

67-
typedef std::map<goto_programt::const_targett, coverage_infot>
67+
typedef std::map<
68+
goto_programt::const_targett,
69+
coverage_infot,
70+
goto_programt::target_less_than>
6871
coverage_innert;
69-
typedef std::map<goto_programt::const_targett, coverage_innert> coveraget;
72+
typedef std::map<
73+
goto_programt::const_targett,
74+
coverage_innert,
75+
goto_programt::target_less_than>
76+
coveraget;
7077
coveraget coverage;
7178

7279
bool

src/goto-diff/change_impact.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -236,8 +236,9 @@ class change_impactt
236236
DEL_CTRL_DEP=1<<5
237237
};
238238

239-
typedef std::map<goto_programt::const_targett, unsigned>
240-
goto_program_change_impactt;
239+
typedef std::
240+
map<goto_programt::const_targett, unsigned, goto_programt::target_less_than>
241+
goto_program_change_impactt;
241242
typedef std::map<irep_idt, goto_program_change_impactt>
242243
goto_functions_change_impactt;
243244

0 commit comments

Comments
 (0)