Skip to content

Commit 45104b6

Browse files
smowtonsmowton
committed
Remove unused dereference mode parameter
Both implementations currently disregard whether they're looking at an LHS or RHS expression.
1 parent 51d7363 commit 45104b6

File tree

8 files changed

+53
-96
lines changed

8 files changed

+53
-96
lines changed

‎src/goto-symex/goto_symex.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -222,11 +222,11 @@ class goto_symext
222222

223223
void trigger_auto_object(const exprt &, statet &);
224224
void initialize_auto_object(const exprt &, statet &);
225-
void process_array_expr(statet &, exprt &, bool);
225+
void process_array_expr(statet &, exprt &);
226226
exprt make_auto_object(const typet &, statet &);
227-
virtual void dereference(exprt &, statet &, bool write);
227+
virtual void dereference(exprt &, statet &);
228228

229-
void dereference_rec(exprt &, statet &, guardt &, bool write);
229+
void dereference_rec(exprt &, statet &, guardt &);
230230
exprt address_arithmetic(
231231
const exprt &,
232232
statet &,

‎src/goto-symex/symex_clean_expr.cpp

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -120,18 +120,14 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
120120
}
121121
}
122122

123-
void goto_symext::process_array_expr(statet &state, exprt &expr, bool is_lhs)
123+
void goto_symext::process_array_expr(statet &state, exprt &expr)
124124
{
125125
symex_dereference_statet symex_dereference_state(*this, state);
126126

127127
value_set_dereferencet dereference(
128128
ns, state.symbol_table, symex_dereference_state, language_mode, false);
129129

130-
expr = dereference.dereference(
131-
expr,
132-
guardt{true_exprt()},
133-
is_lhs ? value_set_dereferencet::modet::WRITE
134-
: value_set_dereferencet::modet::READ);
130+
expr = dereference.dereference(expr, guardt{true_exprt()});
135131

136132
::process_array_expr(expr, symex_config.simplify_opt, ns);
137133
}
@@ -180,7 +176,7 @@ void goto_symext::clean_expr(
180176
const bool write)
181177
{
182178
replace_nondet(expr, path_storage.build_symex_nondet);
183-
dereference(expr, state, write);
179+
dereference(expr, state);
184180

185181
// make sure all remaining byte extract operations use the root
186182
// object to avoid nesting of with/update and byte_update when on

‎src/goto-symex/symex_dereference.cpp

Lines changed: 13 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ exprt goto_symext::address_arithmetic(
5959

6060
// there could be further dereferencing in the offset
6161
exprt offset=be.offset();
62-
dereference_rec(offset, state, guard, false);
62+
dereference_rec(offset, state, guard);
6363

6464
result=plus_exprt(result, offset);
6565

@@ -95,14 +95,14 @@ exprt goto_symext::address_arithmetic(
9595
// just grab the pointer, but be wary of further dereferencing
9696
// in the pointer itself
9797
result=to_dereference_expr(expr).pointer();
98-
dereference_rec(result, state, guard, false);
98+
dereference_rec(result, state, guard);
9999
}
100100
else if(expr.id()==ID_if)
101101
{
102102
if_exprt if_expr=to_if_expr(expr);
103103

104104
// the condition is not an address
105-
dereference_rec(if_expr.cond(), state, guard, false);
105+
dereference_rec(if_expr.cond(), state, guard);
106106

107107
// recursive call
108108
if_expr.true_case()=
@@ -119,7 +119,7 @@ exprt goto_symext::address_arithmetic(
119119
{
120120
// give up, just dereference
121121
result=expr;
122-
dereference_rec(result, state, guard, false);
122+
dereference_rec(result, state, guard);
123123

124124
// turn &array into &array[0]
125125
if(result.type().id() == ID_array && !keep_array)
@@ -179,11 +179,7 @@ exprt goto_symext::address_arithmetic(
179179
return result;
180180
}
181181

182-
void goto_symext::dereference_rec(
183-
exprt &expr,
184-
statet &state,
185-
guardt &guard,
186-
const bool write)
182+
void goto_symext::dereference_rec(exprt &expr, statet &state, guardt &guard)
187183
{
188184
if(expr.id()==ID_dereference)
189185
{
@@ -207,7 +203,7 @@ void goto_symext::dereference_rec(
207203
tmp1.swap(to_dereference_expr(expr).pointer());
208204

209205
// first make sure there are no dereferences in there
210-
dereference_rec(tmp1, state, guard, false);
206+
dereference_rec(tmp1, state, guard);
211207

212208
// we need to set up some elaborate call-backs
213209
symex_dereference_statet symex_dereference_state(*this, state);
@@ -220,13 +216,7 @@ void goto_symext::dereference_rec(
220216
expr_is_not_null);
221217

222218
// std::cout << "**** " << format(tmp1) << '\n';
223-
exprt tmp2=
224-
dereference.dereference(
225-
tmp1,
226-
guard,
227-
write?
228-
value_set_dereferencet::modet::WRITE:
229-
value_set_dereferencet::modet::READ);
219+
exprt tmp2 = dereference.dereference(tmp1, guard);
230220
// std::cout << "**** " << format(tmp2) << '\n';
231221

232222
expr.swap(tmp2);
@@ -252,7 +242,7 @@ void goto_symext::dereference_rec(
252242
tmp.add_source_location()=expr.source_location();
253243

254244
// recursive call
255-
dereference_rec(tmp, state, guard, write);
245+
dereference_rec(tmp, state, guard);
256246

257247
expr.swap(tmp);
258248
}
@@ -292,24 +282,21 @@ void goto_symext::dereference_rec(
292282
to_address_of_expr(tc_op).object(),
293283
from_integer(0, index_type())));
294284

295-
dereference_rec(expr, state, guard, write);
285+
dereference_rec(expr, state, guard);
296286
}
297287
else
298288
{
299-
dereference_rec(tc_op, state, guard, write);
289+
dereference_rec(tc_op, state, guard);
300290
}
301291
}
302292
else
303293
{
304294
Forall_operands(it, expr)
305-
dereference_rec(*it, state, guard, write);
295+
dereference_rec(*it, state, guard);
306296
}
307297
}
308298

309-
void goto_symext::dereference(
310-
exprt &expr,
311-
statet &state,
312-
const bool write)
299+
void goto_symext::dereference(exprt &expr, statet &state)
313300
{
314301
// The expression needs to be renamed to level 1
315302
// in order to distinguish addresses of local variables
@@ -320,7 +307,7 @@ void goto_symext::dereference(
320307

321308
// start the recursion!
322309
guardt guard{true_exprt{}};
323-
dereference_rec(expr, state, guard, write);
310+
dereference_rec(expr, state, guard);
324311
// dereferencing may introduce new symbol_exprt
325312
// (like __CPROVER_memory)
326313
state.rename(expr, ns, goto_symex_statet::L1);

‎src/goto-symex/symex_other.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -145,8 +145,8 @@ void goto_symext::symex_other(
145145
clean_expr(src_array, state, false);
146146

147147
// obtain the actual arrays
148-
process_array_expr(state, dest_array, true);
149-
process_array_expr(state, src_array, false);
148+
process_array_expr(state, dest_array);
149+
process_array_expr(state, src_array);
150150

151151
// check for size (or type) mismatch and adjust
152152
if(!base_type_eq(dest_array.type(), src_array.type(), ns))
@@ -195,7 +195,7 @@ void goto_symext::symex_other(
195195
clean_expr(array_expr, state, false);
196196

197197
// obtain the actual array(s)
198-
process_array_expr(state, array_expr, true);
198+
process_array_expr(state, array_expr);
199199

200200
// prepare to build the array_of
201201
exprt value = code.op1();
@@ -244,8 +244,8 @@ void goto_symext::symex_other(
244244
clean_expr(array2, state, false);
245245

246246
// obtain the actual arrays
247-
process_array_expr(state, array1, false);
248-
process_array_expr(state, array2, false);
247+
process_array_expr(state, array1);
248+
process_array_expr(state, array2);
249249

250250
code_assignt assignment(code.op2(), equal_exprt(array1, array2));
251251

@@ -274,7 +274,7 @@ void goto_symext::symex_other(
274274
exprt object(code.op0());
275275
clean_expr(object, state, false);
276276

277-
process_array_expr(state, object, true);
277+
process_array_expr(state, object);
278278
havoc_rec(state, guardt(true_exprt()), object);
279279
}
280280
else

‎src/pointer-analysis/goto_program_dereference.cpp

Lines changed: 22 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -101,10 +101,7 @@ void goto_program_dereferencet::dereference_failure(
101101
/// \param expr: expression in which to remove dereferences
102102
/// \param guard: boolean expression assumed to hold when dereferencing
103103
/// \param mode: unused
104-
void goto_program_dereferencet::dereference_rec(
105-
exprt &expr,
106-
guardt &guard,
107-
const value_set_dereferencet::modet mode)
104+
void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
108105
{
109106
if(!has_subexpr(expr, ID_dereference))
110107
return;
@@ -124,7 +121,7 @@ void goto_program_dereferencet::dereference_rec(
124121
op.pretty();
125122

126123
if(has_subexpr(op, ID_dereference))
127-
dereference_rec(op, guard, value_set_dereferencet::modet::READ);
124+
dereference_rec(op, guard);
128125

129126
if(expr.id()==ID_or)
130127
guard.add(boolean_negate(op));
@@ -148,7 +145,7 @@ void goto_program_dereferencet::dereference_rec(
148145
throw msg;
149146
}
150147

151-
dereference_rec(expr.op0(), guard, value_set_dereferencet::modet::READ);
148+
dereference_rec(expr.op0(), guard);
152149

153150
bool o1 = has_subexpr(expr.op1(), ID_dereference);
154151
bool o2 = has_subexpr(expr.op2(), ID_dereference);
@@ -157,15 +154,15 @@ void goto_program_dereferencet::dereference_rec(
157154
{
158155
guardt old_guard=guard;
159156
guard.add(expr.op0());
160-
dereference_rec(expr.op1(), guard, mode);
157+
dereference_rec(expr.op1(), guard);
161158
guard = std::move(old_guard);
162159
}
163160

164161
if(o2)
165162
{
166163
guardt old_guard=guard;
167164
guard.add(boolean_negate(expr.op0()));
168-
dereference_rec(expr.op2(), guard, mode);
165+
dereference_rec(expr.op2(), guard);
169166
guard = std::move(old_guard);
170167
}
171168

@@ -185,7 +182,7 @@ void goto_program_dereferencet::dereference_rec(
185182
}
186183

187184
Forall_operands(it, expr)
188-
dereference_rec(*it, guard, mode);
185+
dereference_rec(*it, guard);
189186

190187
if(expr.id()==ID_dereference)
191188
{
@@ -194,8 +191,7 @@ void goto_program_dereferencet::dereference_rec(
194191

195192
dereference_location=expr.find_source_location();
196193

197-
exprt tmp=dereference.dereference(
198-
expr.op0(), guard, mode);
194+
exprt tmp = dereference.dereference(expr.op0(), guard);
199195

200196
expr.swap(tmp);
201197
}
@@ -213,7 +209,7 @@ void goto_program_dereferencet::dereference_rec(
213209
exprt tmp1(ID_plus, expr.op0().type());
214210
tmp1.operands().swap(expr.operands());
215211

216-
exprt tmp2=dereference.dereference(tmp1, guard, mode);
212+
exprt tmp2 = dereference.dereference(tmp1, guard);
217213
tmp2.swap(expr);
218214
}
219215
}
@@ -235,21 +231,19 @@ void goto_program_dereferencet::get_value_set(
235231
/// \param checks_only: when true, execute the substitution on a copy of expr
236232
/// so that `expr` stays unchanged. In that case the only observable effect
237233
/// is whether an exception would be thrown.
238-
/// \param mode: unused
239234
void goto_program_dereferencet::dereference_expr(
240235
exprt &expr,
241-
const bool checks_only,
242-
const value_set_dereferencet::modet mode)
236+
const bool checks_only)
243237
{
244238
guardt guard{true_exprt{}};
245239

246240
if(checks_only)
247241
{
248242
exprt tmp(expr);
249-
dereference_rec(tmp, guard, mode);
243+
dereference_rec(tmp, guard);
250244
}
251245
else
252-
dereference_rec(expr, guard, mode);
246+
dereference_rec(expr, guard);
253247
}
254248

255249
void goto_program_dereferencet::dereference_program(
@@ -301,38 +295,29 @@ void goto_program_dereferencet::dereference_instruction(
301295
#endif
302296
goto_programt::instructiont &i=*target;
303297

304-
dereference_expr(i.guard, checks_only, value_set_dereferencet::modet::READ);
298+
dereference_expr(i.guard, checks_only);
305299

306300
if(i.is_assign())
307301
{
308302
auto &assignment = i.get_assign();
309303

310-
dereference_expr(
311-
assignment.lhs(), checks_only, value_set_dereferencet::modet::WRITE);
312-
dereference_expr(
313-
assignment.rhs(), checks_only, value_set_dereferencet::modet::READ);
304+
dereference_expr(assignment.lhs(), checks_only);
305+
dereference_expr(assignment.rhs(), checks_only);
314306
}
315307
else if(i.is_function_call())
316308
{
317309
code_function_callt &function_call = i.get_function_call();
318310

319311
if(function_call.lhs().is_not_nil())
320-
dereference_expr(
321-
function_call.lhs(),
322-
checks_only,
323-
value_set_dereferencet::modet::WRITE);
324-
325-
dereference_expr(
326-
function_call.function(),
327-
checks_only,
328-
value_set_dereferencet::modet::READ);
329-
dereference_expr(
330-
function_call.op2(), checks_only, value_set_dereferencet::modet::READ);
312+
dereference_expr(function_call.lhs(), checks_only);
313+
314+
dereference_expr(function_call.function(), checks_only);
315+
dereference_expr(function_call.op2(), checks_only);
331316
}
332317
else if(i.is_return())
333318
{
334319
Forall_operands(it, i.get_return())
335-
dereference_expr(*it, checks_only, value_set_dereferencet::modet::READ);
320+
dereference_expr(*it, checks_only);
336321
}
337322
else if(i.is_other())
338323
{
@@ -344,13 +329,12 @@ void goto_program_dereferencet::dereference_instruction(
344329
if(code.operands().size() != 1)
345330
throw "expression expects one operand";
346331

347-
dereference_expr(
348-
code.op0(), checks_only, value_set_dereferencet::modet::READ);
332+
dereference_expr(code.op0(), checks_only);
349333
}
350334
else if(statement==ID_printf)
351335
{
352336
for(auto &op : code.operands())
353-
dereference_expr(op, checks_only, value_set_dereferencet::modet::READ);
337+
dereference_expr(op, checks_only);
354338
}
355339
}
356340
}
@@ -367,7 +351,7 @@ void goto_program_dereferencet::dereference_expression(
367351
valid_local_variables=&target->local_variables;
368352
#endif
369353

370-
dereference_expr(expr, false, value_set_dereferencet::modet::READ);
354+
dereference_expr(expr, false);
371355
}
372356

373357
/// Throw an exception in case removing dereferences from the program would

‎src/pointer-analysis/goto_program_dereference.h

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -86,12 +86,8 @@ class goto_program_dereferencet:protected dereference_callbackt
8686
bool checks_only=false);
8787

8888
protected:
89-
void dereference_rec(
90-
exprt &expr, guardt &guard, const value_set_dereferencet::modet mode);
91-
void dereference_expr(
92-
exprt &expr,
93-
const bool checks_only,
94-
const value_set_dereferencet::modet mode);
89+
void dereference_rec(exprt &expr, guardt &guard);
90+
void dereference_expr(exprt &expr, const bool checks_only);
9591

9692
#if 0
9793
const std::set<irep_idt> *valid_local_variables;

0 commit comments

Comments
 (0)