Skip to content

Commit 526945e

Browse files
NlightNFotisNlightNFotis
committed
Translate asserts and throws to PRECONDITIONS and INVARIANTS
1 parent 16d03d7 commit 526945e

17 files changed

+120
-175
lines changed

‎src/goto-symex/build_goto_trace.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -92,9 +92,7 @@ exprt build_full_lhs_rec(
9292
id==ID_byte_extract_big_endian)
9393
{
9494
exprt tmp=src_original;
95-
DATA_INVARIANT(
96-
tmp.operands().size() == 2,
97-
"byte_extract_exprt should have two operands.");
95+
PRECONDITION(tmp.operands().size() == 2);
9896
tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());
9997

10098
// re-write into big case-split
@@ -224,7 +222,7 @@ void build_goto_trace(
224222
else if(it->is_atomic_end() && current_time<0)
225223
current_time*=-1;
226224

227-
assert(current_time>=0);
225+
PRECONDITION(current_time>=0);
228226
// move any steps gathered in an atomic section
229227

230228
if(time_before<0)

‎src/goto-symex/goto_symex_state.cpp

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -51,8 +51,7 @@ void goto_symex_statet::level0t::operator()(
5151

5252
const symbolt *s;
5353
const bool found_l0 = !ns.lookup(obj_identifier, s);
54-
DATA_INVARIANT(
55-
found_l0, "level0: failed to find " + id2string(obj_identifier));
54+
INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
5655

5756
// don't rename shared variables or functions
5857
if(s->type.id()==ID_code ||
@@ -187,8 +186,7 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
187186
}
188187
else if(expr.id()==ID_member)
189188
{
190-
DATA_INVARIANT(
191-
expr.operands().size() == 1, "member_exprt takes one operand.");
189+
PRECONDITION(expr.operands().size() == 1);
192190

193191
return constant_propagation_reference(expr.op0());
194192
}
@@ -495,12 +493,9 @@ void goto_symex_statet::rename(
495493
}
496494
else if(expr.id()==ID_address_of)
497495
{
498-
DATA_INVARIANT(
499-
expr.operands().size() == 1, "address_of should have a single operand");
496+
PRECONDITION(expr.operands().size() == 1);
500497
rename_address(expr.op0(), ns, level);
501-
DATA_INVARIANT(
502-
expr.type().id() == ID_pointer,
503-
"type of address_of should be ID_pointer");
498+
PRECONDITION(expr.type().id() == ID_pointer);
504499
expr.type().subtype()=expr.op0().type();
505500
}
506501
else

‎src/goto-symex/partial_order_concurrency.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -198,7 +198,7 @@ exprt partial_order_concurrencyt::before(
198198
binary_relation_exprt(clock(e1, ax), ID_lt, clock(e2, ax)));
199199
}
200200

201-
assert(!ops.empty());
201+
POSTCONDITION(!ops.empty());
202202

203203
return conjunction(ops);
204204
}

‎src/goto-symex/postcondition.cpp

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -76,23 +76,19 @@ bool postconditiont::is_used_address_of(
7676
}
7777
else if(expr.id()==ID_index)
7878
{
79-
DATA_INVARIANT(
80-
expr.operands().size() == 2, "index_exprt takes two operands.");
81-
79+
PRECONDITION(expr.operands().size() == 2);
8280
return
8381
is_used_address_of(expr.op0(), identifier) ||
8482
is_used(expr.op1(), identifier);
8583
}
8684
else if(expr.id()==ID_member)
8785
{
88-
DATA_INVARIANT(
89-
expr.operands().size() == 1, "member_exprt takes one operand.");
86+
PRECONDITION(expr.operands().size() == 1);
9087
return is_used_address_of(expr.op0(), identifier);
9188
}
9289
else if(expr.id()==ID_dereference)
9390
{
94-
DATA_INVARIANT(
95-
expr.operands().size() == 1, "dereference_exprt takes one operand.");
91+
PRECONDITION(expr.operands().size() == 1);
9692
return is_used(expr.op0(), identifier);
9793
}
9894

@@ -158,8 +154,7 @@ bool postconditiont::is_used(
158154
if(expr.id()==ID_address_of)
159155
{
160156
// only do index!
161-
DATA_INVARIANT(
162-
expr.operands().size() == 1, "address_of_exprt takes one operand.");
157+
PRECONDITION(expr.operands().size() == 1);
163158
return is_used_address_of(expr.op0(), identifier);
164159
}
165160
else if(expr.id()==ID_symbol &&
@@ -173,8 +168,7 @@ bool postconditiont::is_used(
173168
}
174169
else if(expr.id()==ID_dereference)
175170
{
176-
DATA_INVARIANT(
177-
expr.operands().size() == 1, "dereference_exprt takes one operand.");
171+
PRECONDITION(expr.operands().size() == 1);
178172

179173
// aliasing may happen here
180174

‎src/goto-symex/precondition.cpp

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -78,21 +78,18 @@ void preconditiont::compute_address_of(exprt &dest)
7878
}
7979
else if(dest.id()==ID_index)
8080
{
81-
DATA_INVARIANT(
82-
dest.operands().size() == 2, "index_exprt takes two operands.");
81+
PRECONDITION(dest.operands().size() == 2);
8382
compute_address_of(dest.op0());
8483
compute(dest.op1());
8584
}
8685
else if(dest.id()==ID_member)
8786
{
88-
DATA_INVARIANT(
89-
dest.operands().size() == 1, "member_exprt takes one operand.");
87+
PRECONDITION(dest.operands().size() == 1);
9088
compute_address_of(dest.op0());
9189
}
9290
else if(dest.id()==ID_dereference)
9391
{
94-
DATA_INVARIANT(
95-
dest.operands().size() == 1, "dereference_exprt takes one operand.");
92+
PRECONDITION(dest.operands().size() == 1);
9693
compute(dest.op0());
9794
}
9895
}
@@ -107,14 +104,12 @@ void preconditiont::compute_rec(exprt &dest)
107104
if(dest.id()==ID_address_of)
108105
{
109106
// only do index!
110-
DATA_INVARIANT(
111-
dest.operands().size() == 1, "address_of_exprt takes one operand.");
107+
PRECONDITION(dest.operands().size() == 1);
112108
compute_address_of(dest.op0());
113109
}
114110
else if(dest.id()==ID_dereference)
115111
{
116-
DATA_INVARIANT(
117-
dest.operands().size() == 1, "dereference_exprt takes one operand.");
112+
PRECONDITION(dest.operands().size() == 1);
118113

119114
const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
120115

‎src/goto-symex/slice_by_trace.cpp

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,13 @@ void symex_slice_by_tracet::slice_by_trace(
7979
{
8080
exprt g_copy(*i);
8181

82+
INVARIANT(
83+
g_copy.id() == ID_symbol ||
84+
g_copy.id() == ID_not ||
85+
g_copy.id() == ID_and ||
86+
g_copy.id() == ID_constant,
87+
"guards should only be and, symbol, constant, or `not'");
88+
8289
if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
8390
{
8491
g_copy.make_not();
@@ -94,7 +101,7 @@ void symex_slice_by_tracet::slice_by_trace(
94101
}
95102
else if(!(g_copy.id()==ID_constant))
96103
{
97-
throw "guards should only be and, symbol, constant, or `not'";
104+
UNHANDLED_CASE;
98105
}
99106
}
100107

@@ -219,9 +226,9 @@ void symex_slice_by_tracet::parse_events(std::string read_line)
219226
const std::string::size_type vnext=read_line.find(",", vidx);
220227
std::string event=read_line.substr(vidx, vnext - vidx);
221228
eis.insert(event);
222-
if((!alphabet.empty()) &&
223-
((alphabet.count(event)!=0)!=alphabet_parity))
224-
throw "trace uses symbol not in alphabet: "+event;
229+
PRECONDITION(!alphabet.empty());
230+
INVARIANT((alphabet.count(event) != 0) == alphabet_parity,
231+
"trace uses symbol not in alphabet: " + event);
225232
if(vnext==std::string::npos)
226233
break;
227234
vidx=vnext;

‎src/goto-symex/symex_assign.cpp

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ void goto_symext::symex_assign(
3737

3838
if(statement==ID_function_call)
3939
{
40-
assert(!side_effect_expr.operands().empty());
40+
PRECONDITION(!side_effect_expr.operands().empty());
4141

4242
if(side_effect_expr.op0().id()!=ID_symbol)
4343
throw "symex_assign: expected symbol as function";
@@ -96,7 +96,7 @@ exprt goto_symext::add_to_lhs(
9696

9797
if(tmp_what.id()!=ID_symbol)
9898
{
99-
assert(tmp_what.operands().size()>=1);
99+
PRECONDITION(tmp_what.operands().size() >= 1);
100100
tmp_what.op0().make_nil();
101101
}
102102

@@ -106,12 +106,12 @@ exprt goto_symext::add_to_lhs(
106106

107107
while(p->is_not_nil())
108108
{
109-
assert(p->id()!=ID_symbol);
110-
assert(p->operands().size()>=1);
109+
PRECONDITION(p->id()!=ID_symbol);
110+
PRECONDITION(p->operands().size()>=1);
111111
p=&p->op0();
112112
}
113113

114-
assert(p->is_nil());
114+
PRECONDITION(p->is_nil());
115115

116116
*p=tmp_what;
117117
return new_lhs;
@@ -172,9 +172,7 @@ void goto_symext::symex_assign_rec(
172172
lhs.id()==ID_complex_imag)
173173
{
174174
// this is stuff like __real__ x = 1;
175-
DATA_INVARIANT(
176-
lhs.operands().size() == 1,
177-
"exprts with id ID_complex_real or ID_complex_imag take one operand.");
175+
PRECONDITION(lhs.operands().size() == 1);
178176

179177
exprt new_rhs=exprt(ID_complex, lhs.op0().type());
180178
new_rhs.operands().resize(2);
@@ -284,7 +282,6 @@ void goto_symext::symex_assign_typecast(
284282
assignment_typet assignment_type)
285283
{
286284
// these may come from dereferencing on the lhs
287-
288285
PRECONDITION(lhs.operands().size() == 1);
289286

290287
exprt rhs_typecasted=rhs;
@@ -307,7 +304,8 @@ void goto_symext::symex_assign_array(
307304
// lhs must be index operand
308305
// that takes two operands: the first must be an array
309306
// the second is the index
310-
DATA_INVARIANT(lhs.operands().size() == 2, "index_exprt takes two operands");
307+
DATA_INVARIANT(lhs.operands().size() == 2,
308+
"index_exprt takes two operands: first must be array; second must be the index");
311309

312310
const exprt &lhs_array=lhs.array();
313311
const exprt &lhs_index=lhs.index();
@@ -368,8 +366,7 @@ void goto_symext::symex_assign_struct_member(
368366
// typecasts involved? C++ does that for inheritance.
369367
if(lhs_struct.id()==ID_typecast)
370368
{
371-
DATA_INVARIANT(
372-
lhs_struct.operands().size() == 1, "typecast_exprt takes one operand.");
369+
PRECONDITION(lhs_struct.operands().size() == 1);
373370

374371
if(lhs_struct.op0().id() == ID_null_object)
375372
{

‎src/goto-symex/symex_atomic_section.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,9 @@ void goto_symext::symex_atomic_begin(statet &state)
1717
return;
1818

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

2424
state.atomic_section_id=++atomic_section_counter;
2525
state.read_in_atomic_section.clear();
@@ -36,8 +36,7 @@ void goto_symext::symex_atomic_end(statet &state)
3636
if(state.guard.is_false())
3737
return;
3838

39-
if(state.atomic_section_id==0)
40-
throw "ATOMIC_END unmatched"; // NOLINT(readability/throw)
39+
INVARIANT(state.atomic_section_id != 0, "ATOMIC_END unmatched");
4140

4241
const unsigned atomic_section_id=state.atomic_section_id;
4342
state.atomic_section_id=0;
@@ -51,7 +50,7 @@ void goto_symext::symex_atomic_end(statet &state)
5150
r.set_level_2(r_it->second.first);
5251

5352
// guard is the disjunction over reads
54-
assert(!r_it->second.second.empty());
53+
PRECONDITION(!r_it->second.second.empty());
5554
guardt read_guard(r_it->second.second.front());
5655
for(std::list<guardt>::const_iterator
5756
it=++(r_it->second.second.begin());
@@ -77,7 +76,7 @@ void goto_symext::symex_atomic_end(statet &state)
7776
w.set_level_2(state.level2.current_count(w.get_identifier()));
7877

7978
// guard is the disjunction over writes
80-
assert(!w_it->second.empty());
79+
PRECONDITION(!w_it->second.empty());
8180
guardt write_guard(w_it->second.front());
8281
for(std::list<guardt>::const_iterator
8382
it=++(w_it->second.begin());

0 commit comments

Comments
 (0)