Skip to content

Commit 6fe6e9f

Browse files
tautschnigtautschnig
authored
Merge pull request #3863 from tautschnig/function-rw_set
rw_set: store function identifier alongside instruction reference [blocks: #3126]
2 parents 07fa10e + d939de9 commit 6fe6e9f

10 files changed

+163
-84
lines changed

Diff for: ‎src/goto-instrument/interrupt.cpp

+20-11
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ Date: September 2011
1919
#include <analyses/local_may_alias.h>
2020
#endif
2121

22-
bool potential_race_on_read(
22+
static bool potential_race_on_read(
2323
const rw_set_baset &code_rw_set,
2424
const rw_set_baset &isr_rw_set)
2525
{
@@ -33,7 +33,7 @@ bool potential_race_on_read(
3333
return false;
3434
}
3535

36-
bool potential_race_on_write(
36+
static bool potential_race_on_write(
3737
const rw_set_baset &code_rw_set,
3838
const rw_set_baset &isr_rw_set)
3939
{
@@ -50,9 +50,10 @@ bool potential_race_on_write(
5050
return false;
5151
}
5252

53-
void interrupt(
53+
static void interrupt(
5454
value_setst &value_sets,
5555
const symbol_tablet &symbol_table,
56+
const irep_idt &function_id,
5657
#ifdef LOCAL_MAY
5758
const goto_functionst::goto_functiont &goto_function,
5859
#endif
@@ -69,11 +70,16 @@ void interrupt(
6970
#ifdef LOCAL_MAY
7071
local_may_aliast local_may(goto_function);
7172
#endif
72-
rw_set_loct rw_set(ns, value_sets, i_it
73+
rw_set_loct rw_set(
74+
ns,
75+
value_sets,
76+
function_id,
77+
i_it
7378
#ifdef LOCAL_MAY
74-
, local_may
79+
,
80+
local_may
7581
#endif
76-
); // NOLINT(whitespace/parens)
82+
); // NOLINT(whitespace/parens)
7783

7884
// potential race?
7985
bool race_on_read=potential_race_on_read(rw_set, isr_rw_set);
@@ -143,9 +149,8 @@ void interrupt(
143149
}
144150
}
145151

146-
symbol_exprt get_isr(
147-
const symbol_tablet &symbol_table,
148-
const irep_idt &interrupt_handler)
152+
static symbol_exprt
153+
get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
149154
{
150155
std::list<symbol_exprt> matches;
151156

@@ -197,11 +202,15 @@ void interrupt(
197202
f_it->first!=goto_functionst::entry_point() &&
198203
f_it->first!=isr.get_identifier())
199204
interrupt(
200-
value_sets, goto_model.symbol_table,
205+
value_sets,
206+
goto_model.symbol_table,
207+
f_it->first,
201208
#ifdef LOCAL_MAY
202209
f_it->second,
203210
#endif
204-
f_it->second.body, isr, isr_rw_set);
211+
f_it->second.body,
212+
isr,
213+
isr_rw_set);
205214

206215
goto_model.goto_functions.update();
207216
}

Diff for: ‎src/goto-instrument/mmio.cpp

+13-4
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,10 @@ Date: September 2011
2121
#include <analyses/local_may_alias.h>
2222
#endif
2323

24-
void mmio(
24+
static void mmio(
2525
value_setst &value_sets,
2626
const symbol_tablet &symbol_table,
27+
const irep_idt &function_id,
2728
#ifdef LOCAL_MAY
2829
const goto_functionst::goto_functiont &goto_function,
2930
#endif
@@ -41,9 +42,14 @@ void mmio(
4142

4243
if(instruction.is_assign())
4344
{
44-
rw_set_loct rw_set(ns, value_sets, i_it
45+
rw_set_loct rw_set(
46+
ns,
47+
value_sets,
48+
function_id,
49+
i_it
4550
#ifdef LOCAL_MAY
46-
, local_may
51+
,
52+
local_may
4753
#endif
4854
); // NOLINT(whitespace/parens)
4955

@@ -159,7 +165,10 @@ void mmio(
159165
Forall_goto_functions(f_it, goto_model.goto_functions)
160166
if(f_it->first != INITIALIZE_FUNCTION &&
161167
f_it->first!=goto_functionst::entry_point())
162-
mmio(value_sets, goto_model.symbol_table,
168+
mmio(
169+
value_sets,
170+
goto_model.symbol_table,
171+
f_it->first,
163172
#ifdef LOCAL_MAY
164173
f_it->second,
165174
#endif

Diff for: ‎src/goto-instrument/race_check.cpp

+16-13
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ void w_guardst::add_initialization(goto_programt &goto_program) const
104104
}
105105
}
106106

107-
std::string comment(const rw_set_baset::entryt &entry, bool write)
107+
static std::string comment(const rw_set_baset::entryt &entry, bool write)
108108
{
109109
std::string result;
110110
if(write)
@@ -117,9 +117,7 @@ std::string comment(const rw_set_baset::entryt &entry, bool write)
117117
return result;
118118
}
119119

120-
bool is_shared(
121-
const namespacet &ns,
122-
const symbol_exprt &symbol_expr)
120+
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
123121
{
124122
const irep_idt &identifier=symbol_expr.get_identifier();
125123

@@ -137,9 +135,7 @@ bool is_shared(
137135
return symbol.is_shared();
138136
}
139137

140-
bool has_shared_entries(
141-
const namespacet &ns,
142-
const rw_set_baset &rw_set)
138+
static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
143139
{
144140
for(rw_set_baset::entriest::const_iterator
145141
it=rw_set.r_entries.begin();
@@ -158,12 +154,17 @@ bool has_shared_entries(
158154
return false;
159155
}
160156

161-
void race_check(
157+
// clang-format off
158+
// clang-format is confused by the L_M_ARG macro and wants to indent the line
159+
// after
160+
static void race_check(
162161
value_setst &value_sets,
163162
symbol_tablet &symbol_table,
163+
const irep_idt &function_id,
164164
L_M_ARG(const goto_functionst::goto_functiont &goto_function)
165165
goto_programt &goto_program,
166166
w_guardst &w_guards)
167+
// clang-format on
167168
{
168169
namespacet ns(symbol_table);
169170

@@ -177,7 +178,8 @@ void race_check(
177178

178179
if(instruction.is_assign())
179180
{
180-
rw_set_loct rw_set(ns, value_sets, i_it L_M_LAST_ARG(local_may));
181+
rw_set_loct rw_set(
182+
ns, value_sets, function_id, i_it L_M_LAST_ARG(local_may));
181183

182184
if(!has_shared_entries(ns, rw_set))
183185
continue;
@@ -266,6 +268,7 @@ void race_check(
266268
void race_check(
267269
value_setst &value_sets,
268270
symbol_tablet &symbol_table,
271+
const irep_idt &function_id,
269272
#ifdef LOCAL_MAY
270273
const goto_functionst::goto_functiont &goto_function,
271274
#endif
@@ -276,8 +279,8 @@ void race_check(
276279
race_check(
277280
value_sets,
278281
symbol_table,
279-
L_M_ARG(goto_function)
280-
goto_program,
282+
function_id,
283+
L_M_ARG(goto_function) goto_program,
281284
w_guards);
282285

283286
w_guards.add_initialization(goto_program);
@@ -296,8 +299,8 @@ void race_check(
296299
race_check(
297300
value_sets,
298301
goto_model.symbol_table,
299-
L_M_ARG(f_it->second)
300-
f_it->second.body,
302+
f_it->first,
303+
L_M_ARG(f_it->second) f_it->second.body,
301304
w_guards);
302305

303306
// get "main"

Diff for: ‎src/goto-instrument/race_check.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,11 @@ Date: February 2006
2020
void race_check(
2121
value_setst &,
2222
class symbol_tablet &,
23+
const irep_idt &function_id,
2324
#ifdef LOCAL_MAY
2425
const goto_functionst::goto_functiont &goto_function,
2526
#endif
26-
goto_programt &goto_program
27-
);
27+
goto_programt &goto_program);
2828

2929
void race_check(value_setst &, goto_modelt &);
3030

Diff for: ‎src/goto-instrument/rw_set.cpp

+10-5
Original file line numberDiff line numberDiff line change
@@ -199,10 +199,10 @@ void rw_set_functiont::compute_rec(const exprt &function)
199199
{
200200
if(function.id()==ID_symbol)
201201
{
202-
const irep_idt &id=to_symbol_expr(function).get_identifier();
202+
const irep_idt &function_id = to_symbol_expr(function).get_identifier();
203203

204-
goto_functionst::function_mapt::const_iterator f_it=
205-
goto_functions.function_map.find(id);
204+
goto_functionst::function_mapt::const_iterator f_it =
205+
goto_functions.function_map.find(function_id);
206206

207207
if(f_it!=goto_functions.function_map.end())
208208
{
@@ -220,9 +220,14 @@ void rw_set_functiont::compute_rec(const exprt &function)
220220

221221
forall_goto_program_instructions(i_it, body)
222222
{
223-
*this+=rw_set_loct(ns, value_sets, i_it
223+
*this += rw_set_loct(
224+
ns,
225+
value_sets,
226+
function_id,
227+
i_it
224228
#ifdef LOCAL_MAY
225-
, local_may
229+
,
230+
local_may
226231
#endif
227232
); // NOLINT(whitespace/parens)
228233
}

Diff for: ‎src/goto-instrument/rw_set.h

+28-19
Original file line numberDiff line numberDiff line change
@@ -121,26 +121,31 @@ class _rw_set_loct:public rw_set_baset
121121
_rw_set_loct(
122122
const namespacet &_ns,
123123
value_setst &_value_sets,
124+
const irep_idt &_function_id,
124125
goto_programt::const_targett _target,
125-
local_may_aliast &may):
126-
rw_set_baset(_ns),
127-
value_sets(_value_sets),
128-
target(_target),
129-
local_may(may)
126+
local_may_aliast &may)
127+
: rw_set_baset(_ns),
128+
value_sets(_value_sets),
129+
function_id(_function_id),
130+
target(_target),
131+
local_may(may)
130132
#else
131133
_rw_set_loct(
132134
const namespacet &_ns,
133135
value_setst &_value_sets,
134-
goto_programt::const_targett _target):
135-
rw_set_baset(_ns),
136-
value_sets(_value_sets),
137-
target(_target)
136+
const irep_idt &_function_id,
137+
goto_programt::const_targett _target)
138+
: rw_set_baset(_ns),
139+
value_sets(_value_sets),
140+
function_id(_function_id),
141+
target(_target)
138142
#endif
139143
{
140144
}
141145

142146
protected:
143147
value_setst &value_sets;
148+
const irep_idt function_id;
144149
const goto_programt::const_targett target;
145150

146151
#ifdef LOCAL_MAY
@@ -180,15 +185,17 @@ class rw_set_loct:public _rw_set_loct
180185
rw_set_loct(
181186
const namespacet &_ns,
182187
value_setst &_value_sets,
188+
const irep_idt &_function_id,
183189
goto_programt::const_targett _target,
184-
local_may_aliast &may):
185-
_rw_set_loct(_ns, _value_sets, _target, may)
190+
local_may_aliast &may)
191+
: _rw_set_loct(_ns, _value_sets, _function_id, _target, may)
186192
#else
187193
rw_set_loct(
188194
const namespacet &_ns,
189195
value_setst &_value_sets,
190-
goto_programt::const_targett _target):
191-
_rw_set_loct(_ns, _value_sets, _target)
196+
const irep_idt &_function_id,
197+
goto_programt::const_targett _target)
198+
: _rw_set_loct(_ns, _value_sets, _function_id, _target)
192199
#endif
193200
{
194201
compute();
@@ -239,17 +246,19 @@ class rw_set_with_trackt:public _rw_set_loct
239246
rw_set_with_trackt(
240247
const namespacet &_ns,
241248
value_setst &_value_sets,
249+
const irep_idt &_function_id,
242250
goto_programt::const_targett _target,
243-
local_may_aliast &may):
244-
_rw_set_loct(_ns, _value_sets, _target, may),
245-
dereferencing(false)
251+
local_may_aliast &may)
252+
: _rw_set_loct(_ns, _value_sets, _function_id, _target, may),
253+
dereferencing(false)
246254
#else
247255
rw_set_with_trackt(
248256
const namespacet &_ns,
249257
value_setst &_value_sets,
250-
goto_programt::const_targett _target):
251-
_rw_set_loct(_ns, _value_sets, _target),
252-
dereferencing(false)
258+
const irep_idt &_function_id,
259+
goto_programt::const_targett _target)
260+
: _rw_set_loct(_ns, _value_sets, _function_id, _target),
261+
dereferencing(false)
253262
#endif
254263
{
255264
compute();

0 commit comments

Comments
 (0)