Skip to content

Commit e08a951

Browse files
committed
Dirty locals analysis: consume goto_programt instead of goto_functiont
The analysis does not use any information contained in a `goto_functiont` that's not already available in a `goto_programt`. Using this more specific type avoids any (future) use building unnecessary wrappers.
1 parent deaa5ee commit e08a951

File tree

10 files changed

+29
-31
lines changed

10 files changed

+29
-31
lines changed

src/analyses/constant_propagator.h

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -188,9 +188,8 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
188188

189189
explicit constant_propagator_ait(
190190
const goto_functiont &goto_function,
191-
should_track_valuet should_track_value = track_all_values):
192-
dirty(goto_function),
193-
should_track_value(should_track_value)
191+
should_track_valuet should_track_value = track_all_values)
192+
: dirty(goto_function.body), should_track_value(should_track_value)
194193
{
195194
}
196195

@@ -210,7 +209,7 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
210209
goto_functionst::goto_functiont &goto_function,
211210
const namespacet &ns,
212211
should_track_valuet should_track_value = track_all_values)
213-
: dirty(goto_function), should_track_value(should_track_value)
212+
: dirty(goto_function.body), should_track_value(should_track_value)
214213
{
215214
operator()(function_identifier, goto_function, ns);
216215
replace(goto_function, ns);

src/analyses/dirty.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@ Date: March 2013
1616
#include <util/pointer_expr.h>
1717
#include <util/std_expr.h>
1818

19-
void dirtyt::build(const goto_functiont &goto_function)
19+
void dirtyt::build(const goto_programt &goto_program)
2020
{
21-
for(const auto &i : goto_function.body.instructions)
21+
for(const auto &i : goto_program.instructions)
2222
{
2323
if(i.is_other())
2424
{
@@ -108,12 +108,12 @@ void dirtyt::output(std::ostream &out) const
108108

109109
/// Analyse the given function with dirtyt if it hasn't been seen before
110110
/// \param id: function id to analyse
111-
/// \param function: function to analyse
111+
/// \param goto_program: body of function to analyse
112112
void incremental_dirtyt::populate_dirty_for_function(
113113
const irep_idt &id,
114-
const goto_functionst::goto_functiont &function)
114+
const goto_programt &goto_program)
115115
{
116116
auto insert_result = dirty_processed_functions.insert(id);
117117
if(insert_result.second)
118-
dirty.add_function(function);
118+
dirty.add_function(goto_program);
119119
}

src/analyses/dirty.h

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,6 @@ class dirtyt
3838

3939
public:
4040
bool initialized;
41-
typedef goto_functionst::goto_functiont goto_functiont;
4241

4342
/// \post dirtyt objects that are created through this constructor are not
4443
/// safe to use. If you copied a dirtyt (for example, by adding an object
@@ -48,9 +47,9 @@ class dirtyt
4847
{
4948
}
5049

51-
explicit dirtyt(const goto_functiont &goto_function) : initialized(false)
50+
explicit dirtyt(const goto_programt &goto_program) : initialized(false)
5251
{
53-
build(goto_function);
52+
build(goto_program);
5453
initialized = true;
5554
}
5655

@@ -81,9 +80,9 @@ class dirtyt
8180
return dirty;
8281
}
8382

84-
void add_function(const goto_functiont &goto_function)
83+
void add_function(const goto_programt &goto_program)
8584
{
86-
build(goto_function);
85+
build(goto_program);
8786
initialized = true;
8887
}
8988

@@ -92,12 +91,12 @@ class dirtyt
9291
// dirtyts should not be initialized twice
9392
PRECONDITION(!initialized);
9493
for(const auto &gf_entry : goto_functions.function_map)
95-
build(gf_entry.second);
94+
build(gf_entry.second.body);
9695
initialized = true;
9796
}
9897

9998
protected:
100-
void build(const goto_functiont &goto_function);
99+
void build(const goto_programt &);
101100

102101
// variables whose address is taken
103102
std::unordered_set<irep_idt> dirty;
@@ -119,7 +118,7 @@ class incremental_dirtyt
119118
public:
120119
void populate_dirty_for_function(
121120
const irep_idt &id,
122-
const goto_functionst::goto_functiont &function);
121+
const goto_programt &goto_program);
123122

124123
bool operator()(const irep_idt &id) const
125124
{

src/analyses/local_bitvector_analysis.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ class local_bitvector_analysist
2727
local_bitvector_analysist(
2828
const goto_functiont &_goto_function,
2929
const namespacet &ns)
30-
: dirty(_goto_function),
30+
: dirty(_goto_function.body),
3131
locals(_goto_function),
3232
cfg(_goto_function.body),
3333
ns(ns)

src/analyses/local_may_alias.h

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -27,11 +27,10 @@ class local_may_aliast
2727
public:
2828
typedef goto_functionst::goto_functiont goto_functiont;
2929

30-
explicit local_may_aliast(
31-
const goto_functiont &_goto_function):
32-
dirty(_goto_function),
33-
locals(_goto_function),
34-
cfg(_goto_function.body)
30+
explicit local_may_aliast(const goto_functiont &_goto_function)
31+
: dirty(_goto_function.body),
32+
locals(_goto_function),
33+
cfg(_goto_function.body)
3534
{
3635
build(_goto_function);
3736
}

src/goto-instrument/contracts/cfg_info.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -111,7 +111,7 @@ class function_cfg_infot : public cfg_infot
111111
{
112112
public:
113113
explicit function_cfg_infot(const goto_functiont &_goto_function)
114-
: is_dirty(_goto_function), locals(_goto_function)
114+
: is_dirty(_goto_function.body), locals(_goto_function)
115115
{
116116
parameters.insert(
117117
_goto_function.parameter_identifiers.begin(),
@@ -143,7 +143,7 @@ class loop_cfg_infot : public cfg_infot
143143
{
144144
public:
145145
loop_cfg_infot(goto_functiont &_goto_function, const loopt &loop)
146-
: is_dirty(_goto_function)
146+
: is_dirty(_goto_function.body)
147147
{
148148
for(const auto &t : loop)
149149
{

src/goto-symex/symex_function_call.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -230,7 +230,8 @@ void goto_symext::symex_function_call_post_clean(
230230
const goto_functionst::goto_functiont &goto_function =
231231
get_goto_function(identifier);
232232

233-
path_storage.dirty.populate_dirty_for_function(identifier, goto_function);
233+
path_storage.dirty.populate_dirty_for_function(
234+
identifier, goto_function.body);
234235

235236
auto emplace_safe_pointers_result =
236237
path_storage.safe_pointers.emplace(identifier, local_safe_pointerst{});

src/goto-symex/symex_main.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -448,7 +448,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
448448
emplace_safe_pointers_result.first->second(start_function->body);
449449

450450
path_storage.dirty.populate_dirty_for_function(
451-
entry_point_id, *start_function);
451+
entry_point_id, start_function->body);
452452
state->dirty = &path_storage.dirty;
453453

454454
// Only enable loop analysis when complexity is enabled.

unit/goto-symex/goto_symex_state.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,8 @@ SCENARIO(
4848

4949
// Initialize dirty field of state
5050
incremental_dirtyt dirty;
51-
goto_functiont function;
52-
dirty.populate_dirty_for_function("fun", function);
51+
goto_programt function_body;
52+
dirty.populate_dirty_for_function("fun", function_body);
5353
state.dirty = &dirty;
5454

5555
GIVEN("An L1 lhs and an L2 rhs of type int")

unit/goto-symex/symex_assign.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,8 @@ SCENARIO(
5959

6060
// Initialize dirty field of state
6161
incremental_dirtyt dirty;
62-
goto_functiont function;
63-
dirty.populate_dirty_for_function("fun", function);
62+
goto_programt function_body;
63+
dirty.populate_dirty_for_function("fun", function_body);
6464
state.dirty = &dirty;
6565

6666
// Initialize symbol table with an integer symbol `foo`, and a boolean g

0 commit comments

Comments
 (0)