Skip to content

Commit 2d63171

Browse files
tautschnigtautschnig
authored
Merge pull request #2910 from sonodtt/invariant-cleanup-util_dir-s_files-part2
Cleanup asserts & throws - replace with invariants - dir util/s* (part2)
2 parents 92efd4c + 69e5c2d commit 2d63171

7 files changed

+114
-104
lines changed

‎src/util/simplify_expr_int.cpp

Lines changed: 81 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,10 @@ bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
4343
mp_integer new_value=0;
4444
for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
4545
{
46-
assert(!bytes.empty());
46+
INVARIANT(
47+
!bytes.empty(),
48+
"bytes is not empty because we just pushed just as many elements on "
49+
"top of it as we are popping now");
4750
new_value+=bytes.back()<<bit;
4851
bytes.pop_back();
4952
}
@@ -180,7 +183,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
180183
exprt::operandst::iterator constant;
181184

182185
// true if we have found a constant
183-
bool found = false;
186+
bool constant_found = false;
184187

185188
typet c_sizeof_type=nil_typet();
186189

@@ -212,7 +215,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
212215
c_sizeof_type=
213216
static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
214217

215-
if(found)
218+
if(constant_found)
216219
{
217220
// update the constant factor
218221
if(!mul_expr(to_constant_expr(*constant), to_constant_expr(*it)))
@@ -222,7 +225,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
222225
{
223226
// set it as the constant factor if this is the first
224227
constant=it;
225-
found=true;
228+
constant_found = true;
226229
}
227230
}
228231

@@ -238,7 +241,10 @@ bool simplify_exprt::simplify_mult(exprt &expr)
238241

239242
if(c_sizeof_type.is_not_nil())
240243
{
241-
assert(found);
244+
INVARIANT(
245+
constant_found,
246+
"c_sizeof_type is only set to a non-nil value "
247+
"if a constant has been found");
242248
constant->set(ID_C_c_sizeof_type, c_sizeof_type);
243249
}
244250

@@ -252,7 +258,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
252258
else
253259
{
254260
// if the constant is a one and there are other factors
255-
if(found && constant->is_one())
261+
if(constant_found && constant->is_one())
256262
{
257263
// just delete it
258264
operands.erase(constant);
@@ -440,20 +446,18 @@ bool simplify_exprt::simplify_mod(exprt &expr)
440446

441447
bool simplify_exprt::simplify_plus(exprt &expr)
442448
{
443-
if(!is_number(expr.type()) &&
444-
expr.type().id()!=ID_pointer)
449+
auto const &plus_expr = to_plus_expr(expr);
450+
if(!is_number(plus_expr.type()) && plus_expr.type().id() != ID_pointer)
445451
return true;
446452

447453
bool result=true;
448454

449455
exprt::operandst &operands=expr.operands();
450456

451-
assert(expr.id()==ID_plus);
452-
453457
// floating-point addition is _NOT_ associative; thus,
454458
// there is special case for float
455459

456-
if(ns.follow(expr.type()).id()==ID_floatbv)
460+
if(ns.follow(plus_expr.type()).id() == ID_floatbv)
457461
{
458462
// we only merge neighboring constants!
459463
Forall_expr(it, operands)
@@ -476,14 +480,13 @@ bool simplify_exprt::simplify_plus(exprt &expr)
476480
else
477481
{
478482
// ((T*)p+a)+b -> (T*)p+(a+b)
479-
if(expr.type().id()==ID_pointer &&
480-
expr.operands().size()==2 &&
481-
expr.op0().id()==ID_plus &&
482-
expr.op0().operands().size()==2)
483+
if(
484+
plus_expr.type().id() == ID_pointer && plus_expr.operands().size() == 2 &&
485+
plus_expr.op0().id() == ID_plus && plus_expr.op0().operands().size() == 2)
483486
{
484-
exprt op0=expr.op0();
487+
exprt op0 = plus_expr.op0();
485488

486-
if(expr.op0().op1().id()==ID_plus)
489+
if(plus_expr.op0().op1().id() == ID_plus)
487490
op0.op1().copy_to_operands(expr.op1());
488491
else
489492
op0.op1()=plus_exprt(op0.op1(), expr.op1());
@@ -498,7 +501,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
498501

499502
// count the constants
500503
size_t count=0;
501-
forall_operands(it, expr)
504+
forall_operands(it, plus_expr)
502505
if(is_number(it->type()) && it->is_constant())
503506
count++;
504507

@@ -523,7 +526,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
523526
to_constant_expr(*it)))
524527
{
525528
*it=from_integer(0, it->type());
526-
assert(it->is_not_nil());
529+
CHECK_RETURN(it->is_not_nil());
527530
result=false;
528531
}
529532
}
@@ -556,7 +559,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
556559
{
557560
*(itm->second)=from_integer(0, expr.type());
558561
*it=from_integer(0, expr.type());
559-
assert(it->is_not_nil());
562+
CHECK_RETURN(it->is_not_nil());
560563
expr_map.erase(itm);
561564
result=false;
562565
}
@@ -582,8 +585,8 @@ bool simplify_exprt::simplify_plus(exprt &expr)
582585

583586
if(operands.empty())
584587
{
585-
expr=from_integer(0, expr.type());
586-
assert(expr.is_not_nil());
588+
expr = from_integer(0, plus_expr.type());
589+
CHECK_RETURN(expr.is_not_nil());
587590
return false;
588591
}
589592
else if(operands.size()==1)
@@ -598,55 +601,53 @@ bool simplify_exprt::simplify_plus(exprt &expr)
598601

599602
bool simplify_exprt::simplify_minus(exprt &expr)
600603
{
601-
if(!is_number(expr.type()) &&
602-
expr.type().id()!=ID_pointer)
604+
auto const &minus_expr = to_minus_expr(expr);
605+
if(!is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
603606
return true;
604607

605-
exprt::operandst &operands=expr.operands();
606-
607-
assert(expr.id()==ID_minus);
608+
const exprt::operandst &operands = minus_expr.operands();
608609

609610
if(operands.size()!=2)
610611
return true;
611612

612-
if(is_number(expr.type()) &&
613-
is_number(operands[0].type()) &&
614-
is_number(operands[1].type()))
613+
if(
614+
is_number(minus_expr.type()) && is_number(operands[0].type()) &&
615+
is_number(operands[1].type()))
615616
{
616617
// rewrite "a-b" to "a+(-b)"
617-
unary_minus_exprt tmp2(operands[1]);
618-
simplify_unary_minus(tmp2);
618+
unary_minus_exprt rhs_negated(operands[1]);
619+
simplify_unary_minus(rhs_negated);
619620

620-
plus_exprt tmp(operands[0], tmp2);
621-
simplify_node(tmp);
621+
plus_exprt plus_expr(operands[0], rhs_negated);
622+
simplify_node(plus_expr);
622623

623-
expr.swap(tmp);
624+
expr.swap(plus_expr);
624625
return false;
625626
}
626-
else if(expr.type().id()==ID_pointer &&
627-
operands[0].type().id()==ID_pointer &&
628-
is_number(operands[1].type()))
627+
else if(
628+
minus_expr.type().id() == ID_pointer &&
629+
operands[0].type().id() == ID_pointer && is_number(operands[1].type()))
629630
{
630631
// pointer arithmetic: rewrite "p-i" to "p+(-i)"
631-
unary_minus_exprt tmp2(operands[1]);
632-
simplify_unary_minus(tmp2);
632+
unary_minus_exprt negated_pointer_offset(operands[1]);
633+
simplify_unary_minus(negated_pointer_offset);
633634

634-
plus_exprt tmp(operands[0], tmp2);
635-
simplify_plus(tmp);
635+
plus_exprt pointer_offset_expr(operands[0], negated_pointer_offset);
636+
simplify_plus(pointer_offset_expr);
636637

637-
expr.swap(tmp);
638+
expr.swap(pointer_offset_expr);
638639
return false;
639640
}
640-
else if(is_number(expr.type()) &&
641-
operands[0].type().id()==ID_pointer &&
642-
operands[1].type().id()==ID_pointer)
641+
else if(
642+
is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
643+
operands[1].type().id() == ID_pointer)
643644
{
644645
// pointer arithmetic: rewrite "p-p" to "0"
645646

646647
if(operands[0]==operands[1])
647648
{
648-
exprt zero=from_integer(0, expr.type());
649-
assert(zero.is_not_nil());
649+
exprt zero = from_integer(0, minus_expr.type());
650+
CHECK_RETURN(zero.is_not_nil());
650651
expr=zero;
651652
return false;
652653
}
@@ -741,7 +742,9 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
741742
if(expr.op1().type()!=expr.type())
742743
break;
743744

744-
assert(a_str.size()==b_str.size());
745+
INVARIANT(
746+
a_str.size() == b_str.size(),
747+
"bitvectors of the same type have the same size");
745748

746749
std::string new_value;
747750
new_value.resize(width);
@@ -847,32 +850,40 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
847850

848851
bool simplify_exprt::simplify_extractbit(exprt &expr)
849852
{
850-
const typet &op0_type=expr.op0().type();
853+
PRECONDITION(expr.id() == ID_extractbit);
854+
const auto &extractbit_expr = to_extractbit_expr(expr);
851855

852-
if(!is_bitvector_type(op0_type))
853-
return true;
856+
const typet &src_type = extractbit_expr.src().type();
854857

855-
std::size_t width=to_bitvector_type(op0_type).get_width();
856-
857-
assert(expr.operands().size()==2);
858+
if(!is_bitvector_type(src_type))
859+
return true;
858860

859-
mp_integer i;
861+
const std::size_t src_bit_width = to_bitvector_type(src_type).get_width();
860862

861-
if(to_integer(expr.op1(), i))
863+
const auto index_converted_to_int =
864+
numeric_cast<mp_integer>(extractbit_expr.index());
865+
if(!index_converted_to_int.has_value())
866+
{
862867
return true;
863-
864-
if(!expr.op0().is_constant())
868+
}
869+
const mp_integer index_as_int = index_converted_to_int.value();
870+
if(!extractbit_expr.src().is_constant())
865871
return true;
866872

867-
if(i<0 || i>=width)
873+
if(index_as_int < 0 || index_as_int >= src_bit_width)
868874
return true;
869875

870-
const irep_idt &value=expr.op0().get(ID_value);
876+
const irep_idt &src_value =
877+
to_constant_expr(extractbit_expr.src()).get_value();
878+
879+
std::string src_value_as_string = id2string(src_value);
871880

872-
if(value.size()!=width)
881+
if(src_value_as_string.size() != src_bit_width)
873882
return true;
874883

875-
bool bit=(id2string(value)[width-integer2size_t(i)-1]=='1');
884+
const bool bit =
885+
(src_value_as_string[src_bit_width -
886+
numeric_cast_v<std::size_t>(index_as_int) - 1] == '1');
876887

877888
expr.make_bool(bit);
878889

@@ -1581,7 +1592,9 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
15811592

15821593
// now we only have >=, =
15831594

1584-
assert(expr.id()==ID_ge || expr.id()==ID_equal);
1595+
INVARIANT(
1596+
expr.id() == ID_ge || expr.id() == ID_equal,
1597+
"we previously converted all other cases to >= or ==");
15851598

15861599
// syntactically equal?
15871600

@@ -1663,7 +1676,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
16631676
bool simplify_exprt::simplify_inequality_constant(exprt &expr)
16641677
{
16651678
// the constant is always on the RHS
1666-
assert(expr.op1().is_constant());
1679+
PRECONDITION(expr.op1().is_constant());
16671680

16681681
if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
16691682
{
@@ -1767,7 +1780,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
17671780
{
17681781
constant+=i;
17691782
*it=from_integer(0, it->type());
1770-
assert(it->is_not_nil());
1783+
CHECK_RETURN(it->is_not_nil());
17711784
changed=true;
17721785
}
17731786
}
@@ -1907,9 +1920,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
19071920
}
19081921
else if(expr.id()==ID_gt)
19091922
{
1910-
mp_integer i;
1911-
if(to_integer(expr.op1(), i))
1912-
throw "bit-vector constant unexpectedly non-integer";
1923+
mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
19131924

19141925
if(i==max)
19151926
{
@@ -1933,9 +1944,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
19331944
}
19341945
else if(expr.id()==ID_le)
19351946
{
1936-
mp_integer i;
1937-
if(to_integer(expr.op1(), i))
1938-
throw "bit-vector constant unexpectedly non-integer";
1947+
mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
19391948

19401949
if(i==max)
19411950
{

‎src/util/simplify_expr_pointer.cpp

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -200,9 +200,8 @@ bool simplify_exprt::simplify_address_of(exprt &expr)
200200
else if(object.id()==ID_dereference)
201201
{
202202
// simplify &*p to p
203-
assert(object.operands().size()==1);
204-
exprt tmp=object.op0();
205-
expr=tmp;
203+
auto const &object_as_dereference_expr = to_dereference_expr(object);
204+
expr = object_as_dereference_expr.pointer();
206205
return false;
207206
}
208207

@@ -412,9 +411,10 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
412411

413412
bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
414413
{
415-
assert(expr.type().id()==ID_bool);
416-
assert(expr.operands().size()==2);
417-
assert(expr.id()==ID_equal || expr.id()==ID_notequal);
414+
PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
415+
PRECONDITION(expr.type().id() == ID_bool);
416+
DATA_INVARIANT(
417+
expr.operands().size() == 2, "(in)equalities have two operands");
418418

419419
exprt tmp0=expr.op0();
420420
if(tmp0.id()==ID_typecast)
@@ -428,8 +428,8 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
428428
if(tmp1.op0().id()==ID_index &&
429429
to_index_expr(tmp1.op0()).index().is_zero())
430430
tmp1=address_of_exprt(to_index_expr(tmp1.op0()).array());
431-
assert(tmp0.id()==ID_address_of);
432-
assert(tmp1.id()==ID_address_of);
431+
INVARIANT(tmp0.id() == ID_address_of, "id must be ID_address_of");
432+
INVARIANT(tmp1.id() == ID_address_of, "id must be ID_address_of");
433433

434434
if(tmp0.operands().size()!=1)
435435
return true;
@@ -452,14 +452,15 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
452452

453453
bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
454454
{
455-
assert(expr.type().id()==ID_bool);
456-
assert(expr.operands().size()==2);
457-
assert(expr.id()==ID_equal || expr.id()==ID_notequal);
455+
PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
456+
PRECONDITION(expr.type().id() == ID_bool);
457+
DATA_INVARIANT(
458+
expr.operands().size() == 2, "(in)equalities have two operands");
458459

459460
forall_operands(it, expr)
460461
{
461-
assert(it->id()==ID_pointer_object);
462-
assert(it->operands().size()==1);
462+
PRECONDITION(it->id() == ID_pointer_object);
463+
PRECONDITION(it->operands().size() == 1);
463464
const exprt &op=it->op0();
464465

465466
if(op.id()==ID_address_of)

0 commit comments

Comments
 (0)