Skip to content

Commit 112bd5b

Browse files
NlightNFotisNlightNFotis
committed
Add changes suggested during code review.
1 parent 526945e commit 112bd5b

15 files changed

+78
-47
lines changed

‎src/goto-symex/build_goto_trace.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -222,7 +222,7 @@ void build_goto_trace(
222222
else if(it->is_atomic_end() && current_time<0)
223223
current_time*=-1;
224224

225-
PRECONDITION(current_time>=0);
225+
INVARIANT(current_time>=0, "time keeping inconsistency");
226226
// move any steps gathered in an atomic section
227227

228228
if(time_before<0)

‎src/goto-symex/goto_symex_state.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -493,9 +493,10 @@ void goto_symex_statet::rename(
493493
}
494494
else if(expr.id()==ID_address_of)
495495
{
496-
PRECONDITION(expr.operands().size() == 1);
497-
rename_address(expr.op0(), ns, level);
498496
PRECONDITION(expr.type().id() == ID_pointer);
497+
DATA_INVARIANT(
498+
expr.operands().size() == 1, "address_of should have a single operand");
499+
rename_address(expr.op0(), ns, level);
499500
expr.type().subtype()=expr.op0().type();
500501
}
501502
else

‎src/goto-symex/postcondition.cpp

+12-5
Original file line numberDiff line numberDiff line change
@@ -76,19 +76,22 @@ bool postconditiont::is_used_address_of(
7676
}
7777
else if(expr.id()==ID_index)
7878
{
79-
PRECONDITION(expr.operands().size() == 2);
79+
DATA_INVARIANT(
80+
expr.operands().size() == 2, "index expression should have two operands");
8081
return
8182
is_used_address_of(expr.op0(), identifier) ||
8283
is_used(expr.op1(), identifier);
8384
}
8485
else if(expr.id()==ID_member)
8586
{
86-
PRECONDITION(expr.operands().size() == 1);
87+
DATA_INVARIANT(
88+
expr.operands().size() == 1, "member expression should only have one operand");
8789
return is_used_address_of(expr.op0(), identifier);
8890
}
8991
else if(expr.id()==ID_dereference)
9092
{
91-
PRECONDITION(expr.operands().size() == 1);
93+
DATA_INVARIANT(
94+
expr.operands().size() == 1, "dereference expression should only have one operand");
9295
return is_used(expr.op0(), identifier);
9396
}
9497

@@ -154,7 +157,9 @@ bool postconditiont::is_used(
154157
if(expr.id()==ID_address_of)
155158
{
156159
// only do index!
157-
PRECONDITION(expr.operands().size() == 1);
160+
DATA_INVARIANT(
161+
expr.operands().size() == 1,
162+
"address_of expression expected to have one operand at this point");
158163
return is_used_address_of(expr.op0(), identifier);
159164
}
160165
else if(expr.id()==ID_symbol &&
@@ -168,7 +173,9 @@ bool postconditiont::is_used(
168173
}
169174
else if(expr.id()==ID_dereference)
170175
{
171-
PRECONDITION(expr.operands().size() == 1);
176+
DATA_INVARIANT(
177+
expr.operands().size() == 1,
178+
"dereference expression expected to have one operand");
172179

173180
// aliasing may happen here
174181

‎src/goto-symex/precondition.cpp

+12-5
Original file line numberDiff line numberDiff line change
@@ -78,18 +78,21 @@ void preconditiont::compute_address_of(exprt &dest)
7878
}
7979
else if(dest.id()==ID_index)
8080
{
81-
PRECONDITION(dest.operands().size() == 2);
81+
DATA_INVARIANT(
82+
dest.operands().size() == 2, "index expression expected to have two operands");
8283
compute_address_of(dest.op0());
8384
compute(dest.op1());
8485
}
8586
else if(dest.id()==ID_member)
8687
{
87-
PRECONDITION(dest.operands().size() == 1);
88+
DATA_INVARIANT(
89+
dest.operands().size() == 1, "member expression expected to have one operand");
8890
compute_address_of(dest.op0());
8991
}
9092
else if(dest.id()==ID_dereference)
9193
{
92-
PRECONDITION(dest.operands().size() == 1);
94+
DATA_INVARIANT(
95+
dest.operands().size() == 1, "dereference expression expected to have 1 operand");
9396
compute(dest.op0());
9497
}
9598
}
@@ -104,12 +107,16 @@ void preconditiont::compute_rec(exprt &dest)
104107
if(dest.id()==ID_address_of)
105108
{
106109
// only do index!
107-
PRECONDITION(dest.operands().size() == 1);
110+
DATA_INVARIANT(
111+
dest.operands().size() == 1,
112+
"address_of expression expected to have one operand at this point");
108113
compute_address_of(dest.op0());
109114
}
110115
else if(dest.id()==ID_dereference)
111116
{
112-
PRECONDITION(dest.operands().size() == 1);
117+
DATA_INVARIANT(
118+
dest.operands().size() == 1,
119+
"dereference expression expected to have one operand at this point");
113120

114121
const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
115122

‎src/goto-symex/slice_by_trace.cpp

-4
Original file line numberDiff line numberDiff line change
@@ -99,10 +99,6 @@ void symex_slice_by_tracet::slice_by_trace(
9999
simplify(copy_last, ns);
100100
implications.insert(copy_last);
101101
}
102-
else if(!(g_copy.id()==ID_constant))
103-
{
104-
UNHANDLED_CASE;
105-
}
106102
}
107103

108104
slice_SSA_steps(equation, implications); // Slice based on implications

‎src/goto-symex/symex_assign.cpp

+13-7
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,9 @@ void goto_symext::symex_assign(
5555
symex_allocate(state, lhs, side_effect_expr);
5656
else if(statement==ID_printf)
5757
{
58-
if(lhs.is_not_nil())
59-
throw "printf: unexpected assignment";
58+
PRECONDITION(!lhs.is_not_nil());
59+
// if(lhs.is_not_nil())
60+
// throw "printf: unexpected assignment";
6061
symex_printf(state, side_effect_expr);
6162
}
6263
else if(statement==ID_gcc_builtin_va_arg_next)
@@ -106,12 +107,15 @@ exprt goto_symext::add_to_lhs(
106107

107108
while(p->is_not_nil())
108109
{
109-
PRECONDITION(p->id()!=ID_symbol);
110-
PRECONDITION(p->operands().size()>=1);
110+
INVARIANT(
111+
p->id() != ID_symbol, "expected pointed-to expression to be a symbol");
112+
INVARIANT(
113+
p->operands().size() >= 1,
114+
"expected pointed-to expression to have at least one operand");
111115
p=&p->op0();
112116
}
113117

114-
PRECONDITION(p->is_nil());
118+
INVARIANT(p->is_nil(), "expected pointed-to expression to be nil at this point");
115119

116120
*p=tmp_what;
117121
return new_lhs;
@@ -366,7 +370,9 @@ void goto_symext::symex_assign_struct_member(
366370
// typecasts involved? C++ does that for inheritance.
367371
if(lhs_struct.id()==ID_typecast)
368372
{
369-
PRECONDITION(lhs_struct.operands().size() == 1);
373+
DATA_INVARIANT(
374+
lhs_struct.operands().size() == 1,
375+
"typecast expression expected to have one operand");
370376

371377
if(lhs_struct.op0().id() == ID_null_object)
372378
{
@@ -445,7 +451,7 @@ void goto_symext::symex_assign_if(
445451
guard.swap(old_guard);
446452
}
447453

448-
if(!renamed_guard.is_true())
454+
if(!renamed_guard.is_true())
449455
{
450456
guard.add(not_exprt(renamed_guard));
451457
symex_assign_rec(

‎src/goto-symex/symex_atomic_section.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,9 @@ void goto_symext::symex_atomic_begin(statet &state)
1616
if(state.guard.is_false())
1717
return;
1818

19-
// we don't allow any nesting of atomic sections
20-
INVARIANT(state.atomic_section_id == 0,
21-
"nested atomic section detected at " +
22-
state.source.pc->source_location.as_string());
19+
INVARIANT(
20+
state.atomic_section_id == 0,
21+
"we don't support nesting of atomic sections");
2322

2423
state.atomic_section_id=++atomic_section_counter;
2524
state.read_in_atomic_section.clear();

‎src/goto-symex/symex_builtin_functions.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -174,7 +174,7 @@ void goto_symext::symex_allocate(
174174
ns,
175175
null_message);
176176

177-
PRECONDITION(zero_value.is_not_nil())
177+
CHECK_RETURN(zero_value.is_not_nil());
178178
code_assignt assignment(value_symbol.symbol_expr(), zero_value);
179179
symex_assign(state, assignment);
180180
}
@@ -229,7 +229,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
229229
const exprt &lhs,
230230
const side_effect_exprt &code)
231231
{
232-
PRECONDITION(code.operands().size() != 1);
232+
PRECONDITION(code.operands().size() == 1);
233233

234234
if(lhs.is_nil())
235235
return; // ignore
@@ -518,7 +518,7 @@ void goto_symext::symex_macro(
518518
{
519519
const irep_idt &identifier=code.op0().get(ID_identifier);
520520

521-
PRECONDITION(identifier == CPROVER_MACRO_PREFIX "waitfor")
521+
PRECONDITION(identifier == CPROVER_MACRO_PREFIX "waitfor");
522522
#if 0
523523
exprt new_fc("waitfor", fc.type());
524524

‎src/goto-symex/symex_dead.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,8 @@ void goto_symext::symex_dead(statet &state)
2323

2424
const codet &code=to_code(instruction.code);
2525

26-
PRECONDITION(code.operands().size()!=1);
27-
PRECONDITION(code.op0().id()!=ID_symbol);
26+
PRECONDITION(code.operands().size()==1);
27+
PRECONDITION(code.op0().id()==ID_symbol);
2828

2929
// We increase the L2 renaming to make these non-deterministic.
3030
// We also prevent propagation of old values.

‎src/goto-symex/symex_decl.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,6 @@ void goto_symext::symex_decl(statet &state)
2626
const codet &code=to_code(instruction.code);
2727

2828
// two-operand decl not supported here
29-
PRECONDITION(code.operands().size()!=2);
3029
// we handle the decl with only one operand
3130
PRECONDITION(code.operands().size()==1);
3231
PRECONDITION(code.op0().id()!=ID_symbol);

‎src/goto-symex/symex_dereference.cpp

+6-2
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,9 @@ exprt goto_symext::address_arithmetic(
155155
}
156156
else if(expr.id()==ID_dereference)
157157
{
158-
PRECONDITION(expr.operands().size()==1);
158+
DATA_INVARIANT(
159+
expr.operands().size() == 1,
160+
"dereference expression expected to have one operand");
159161
// ANSI-C guarantees &*p == p no matter what p is,
160162
// even if it's complete garbage
161163
// just grab the pointer, but be wary of further dereferencing
@@ -234,7 +236,9 @@ void goto_symext::dereference_rec(
234236
{
235237
if(expr.id()==ID_dereference)
236238
{
237-
PRECONDITION(expr.operands().size()==1);
239+
DATA_INVARIANT(
240+
expr.operands().size() == 1,
241+
"dereference expression expected to have one operand");
238242

239243
bool expr_is_not_null = false;
240244

‎src/goto-symex/symex_function_call.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -173,7 +173,7 @@ void goto_symext::symex_function_call(
173173
// expression ids(), like ID_Dereference, please expand the
174174
// precondition appropriately.
175175
PRECONDITION(function.id() == ID_symbol);
176-
symex_function_call_symbol(get_goto_function, state, code);
176+
symex_function_call_symbol(get_goto_function, state, code);
177177
}
178178

179179
void goto_symext::symex_function_call_symbol(
@@ -427,7 +427,9 @@ void goto_symext::return_assignment(statet &state)
427427

428428
target.location(state.guard.as_expr(), state.source);
429429

430-
PRECONDITION(code.operands().size() == 1);
430+
PRECONDITION(
431+
code.operands().size() == 1 ||
432+
frame.return_value.is_nil());
431433

432434
exprt value=code.op0();
433435

@@ -441,6 +443,4 @@ void goto_symext::return_assignment(statet &state)
441443

442444
symex_assign(state, assignment);
443445
}
444-
445-
POSTCONDITION(!frame.return_value.is_not_nil());
446446
}

‎src/goto-symex/symex_goto.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ void goto_symext::symex_goto(statet &state)
4949

5050
// we only do deterministic gotos for now
5151
DATA_INVARIANT(
52-
instruction.targets.size()!=1, "no support for non-deterministic gotos");
52+
instruction.targets.size() == 1, "no support for non-deterministic gotos");
5353

5454
goto_programt::const_targett goto_target=
5555
instruction.get_target();

‎src/goto-symex/symex_main.cpp

+6-2
Original file line numberDiff line numberDiff line change
@@ -107,8 +107,12 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
107107
{
108108
// forall X. P -> P
109109
// we keep the quantified variable unique by means of L2 renaming
110-
PRECONDITION(expr.operands().size() == 2);
111-
PRECONDITION(expr.op0().id() == ID_symbol);
110+
DATA_INVARIANT(
111+
expr.operands().size() == 2,
112+
"for_all expression expected to have two operands");
113+
DATA_INVARIANT(
114+
expr.op0().id() == ID_symbol,
115+
"first operand of for_all expression expected to be a symbol");
112116
symbol_exprt tmp0=
113117
to_symbol_expr(to_ssa_expr(expr.op0()).get_original_expr());
114118
symex_decl(state, tmp0);

‎src/goto-symex/symex_other.cpp

+12-4
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,9 @@ void goto_symext::symex_other(
137137
// 3. build an assignment where the type on lhs and rhs is:
138138
// - array_copy: the type of the first array (even if the second is smaller)
139139
// - array_replace: the type of the second array (even if it is smaller)
140-
PRECONDITION(code.operands().size() == 2);
140+
DATA_INVARIANT(
141+
code.operands().size() == 2,
142+
"expected statement to have two operands at this point");
141143

142144
// we need to add dereferencing for both operands
143145
dereference_exprt dest_array(code.op0());
@@ -185,7 +187,9 @@ void goto_symext::symex_other(
185187
// process_array_expr)
186188
// 3. use the type of the resulting array to construct an array_of
187189
// expression
188-
PRECONDITION(code.operands().size() == 2);
190+
DATA_INVARIANT(
191+
code.operands().size() == 2,
192+
"expected statement to have two operands at this point");
189193

190194
// we need to add dereferencing for the first operand
191195
exprt array_expr = dereference_exprt(code.op0());
@@ -230,7 +234,9 @@ void goto_symext::symex_other(
230234
// 3. build an assignment where the lhs is the previous third argument, and
231235
// the right-hand side is an equality over the arrays, if their types match;
232236
// if the types don't match the result trivially is false
233-
PRECONDITION(code.operands().size() == 3);
237+
DATA_INVARIANT(
238+
code.operands().size() == 3,
239+
"expected statement to have three operands at this point");
234240

235241
// we need to add dereferencing for the first two
236242
dereference_exprt array1(code.op0());
@@ -262,7 +268,9 @@ void goto_symext::symex_other(
262268
}
263269
else if(statement==ID_havoc_object)
264270
{
265-
PRECONDITION(code.operands().size()==1);
271+
DATA_INVARIANT(
272+
code.operands().size() == 1,
273+
"expected statement to have one operand at this point");
266274

267275
// we need to add dereferencing for the first operand
268276
dereference_exprt object(code.op0(), empty_typet());

0 commit comments

Comments
 (0)