Skip to content

Commit b39c559

Browse files
kroeningkroening
committed
avoid access to exprt::op0 and op1
1 parent e1e96d3 commit b39c559

File tree

4 files changed

+89
-97
lines changed

4 files changed

+89
-97
lines changed

‎src/analyses/flow_insensitive_analysis.cpp‎

Lines changed: 5 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -317,24 +317,15 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
317317
}
318318
else if(function.id()==ID_if)
319319
{
320-
if(function.operands().size()!=3)
321-
throw "if takes three arguments";
320+
const auto &if_expr = to_if_expr(function);
322321

323-
new_data =
324-
do_function_call_rec(
325-
l_call,
326-
function.op1(),
327-
arguments,
328-
state,
329-
goto_functions);
322+
new_data = do_function_call_rec(
323+
l_call, if_expr.true_case(), arguments, state, goto_functions);
330324

331325
new_data =
332326
do_function_call_rec(
333-
l_call,
334-
function.op2(),
335-
arguments,
336-
state,
337-
goto_functions) || new_data;
327+
l_call, if_expr.false_case(), arguments, state, goto_functions) ||
328+
new_data;
338329
}
339330
else if(function.id()==ID_dereference)
340331
{

‎src/analyses/interval_domain.cpp‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -339,25 +339,25 @@ void interval_domaint::assume_rec(
339339
cond.id()==ID_gt || cond.id()==ID_ge ||
340340
cond.id()==ID_equal || cond.id()==ID_notequal)
341341
{
342-
assert(cond.operands().size()==2);
342+
const auto &rel = to_binary_relation_expr(cond);
343343

344344
if(negation) // !x<y ---> x>=y
345345
{
346-
if(cond.id()==ID_lt)
347-
assume_rec(cond.op0(), ID_ge, cond.op1());
348-
else if(cond.id()==ID_le)
349-
assume_rec(cond.op0(), ID_gt, cond.op1());
350-
else if(cond.id()==ID_gt)
351-
assume_rec(cond.op0(), ID_le, cond.op1());
352-
else if(cond.id()==ID_ge)
353-
assume_rec(cond.op0(), ID_lt, cond.op1());
354-
else if(cond.id()==ID_equal)
355-
assume_rec(cond.op0(), ID_notequal, cond.op1());
356-
else if(cond.id()==ID_notequal)
357-
assume_rec(cond.op0(), ID_equal, cond.op1());
346+
if(rel.id() == ID_lt)
347+
assume_rec(rel.op0(), ID_ge, rel.op1());
348+
else if(rel.id() == ID_le)
349+
assume_rec(rel.op0(), ID_gt, rel.op1());
350+
else if(rel.id() == ID_gt)
351+
assume_rec(rel.op0(), ID_le, rel.op1());
352+
else if(rel.id() == ID_ge)
353+
assume_rec(rel.op0(), ID_lt, rel.op1());
354+
else if(rel.id() == ID_equal)
355+
assume_rec(rel.op0(), ID_notequal, rel.op1());
356+
else if(rel.id() == ID_notequal)
357+
assume_rec(rel.op0(), ID_equal, rel.op1());
358358
}
359359
else
360-
assume_rec(cond.op0(), cond.id(), cond.op1());
360+
assume_rec(rel.op0(), rel.id(), rel.op1());
361361
}
362362
else if(cond.id()==ID_not)
363363
{

‎src/analyses/invariant_set.cpp‎

Lines changed: 65 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -95,21 +95,24 @@ std::string inv_object_storet::build_string(const exprt &expr) const
9595
// we ignore some casts
9696
if(expr.id()==ID_typecast)
9797
{
98-
assert(expr.operands().size()==1);
98+
const auto &typecast_expr = to_typecast_expr(expr);
9999

100-
if(expr.type().id()==ID_signedbv ||
101-
expr.type().id()==ID_unsignedbv)
100+
if(
101+
typecast_expr.type().id() == ID_signedbv ||
102+
typecast_expr.type().id() == ID_unsignedbv)
102103
{
103-
if(expr.op0().type().id()==ID_signedbv ||
104-
expr.op0().type().id()==ID_unsignedbv)
104+
if(
105+
typecast_expr.op().type().id() == ID_signedbv ||
106+
typecast_expr.op().type().id() == ID_unsignedbv)
105107
{
106-
if(to_bitvector_type(expr.type()).get_width()>=
107-
to_bitvector_type(expr.op0().type()).get_width())
108-
return build_string(expr.op0());
108+
if(
109+
to_bitvector_type(typecast_expr.type()).get_width() >=
110+
to_bitvector_type(typecast_expr.op().type()).get_width())
111+
return build_string(typecast_expr.op());
109112
}
110-
else if(expr.op0().type().id()==ID_bool)
113+
else if(typecast_expr.op().type().id() == ID_bool)
111114
{
112-
return build_string(expr.op0());
115+
return build_string(typecast_expr.op());
113116
}
114117
}
115118
}
@@ -137,8 +140,8 @@ std::string inv_object_storet::build_string(const exprt &expr) const
137140

138141
if(expr.id()==ID_member)
139142
{
140-
assert(expr.operands().size()==1);
141-
return build_string(expr.op0())+"."+expr.get_string(ID_component_name);
143+
return build_string(to_member_expr(expr).struct_op()) + "." +
144+
expr.get_string(ID_component_name);
142145
}
143146

144147
if(expr.id()==ID_symbol)
@@ -158,8 +161,7 @@ bool invariant_sett::get_object(
158161
bool inv_object_storet::is_constant_address(const exprt &expr)
159162
{
160163
if(expr.id()==ID_address_of)
161-
if(expr.operands().size()==1)
162-
return is_constant_address_rec(expr.op0());
164+
return is_constant_address_rec(to_address_of_expr(expr).object());
163165

164166
return false;
165167
}
@@ -169,15 +171,12 @@ bool inv_object_storet::is_constant_address_rec(const exprt &expr)
169171
if(expr.id()==ID_symbol)
170172
return true;
171173
else if(expr.id()==ID_member)
172-
{
173-
assert(expr.operands().size()==1);
174-
return is_constant_address_rec(expr.op0());
175-
}
174+
return is_constant_address_rec(to_member_expr(expr).struct_op());
176175
else if(expr.id()==ID_index)
177176
{
178-
assert(expr.operands().size()==2);
179-
if(expr.op1().is_constant())
180-
return is_constant_address_rec(expr.op0());
177+
const auto &index_expr = to_index_expr(expr);
178+
if(index_expr.index().is_constant())
179+
return is_constant_address_rec(index_expr.array());
181180
}
182181

183182
return false;
@@ -429,14 +428,14 @@ void invariant_sett::strengthen_rec(const exprt &expr)
429428
else if(expr.id()==ID_le ||
430429
expr.id()==ID_lt)
431430
{
432-
assert(expr.operands().size()==2);
431+
const auto &rel = to_binary_relation_expr(expr);
433432

434433
// special rule: x <= (a & b)
435434
// implies: x<=a && x<=b
436435

437-
if(expr.op1().id()==ID_bitand)
436+
if(rel.op1().id() == ID_bitand)
438437
{
439-
const exprt &bitand_op=expr.op1();
438+
const exprt &bitand_op = rel.op1();
440439

441440
forall_operands(it, bitand_op)
442441
{
@@ -450,12 +449,11 @@ void invariant_sett::strengthen_rec(const exprt &expr)
450449

451450
std::pair<unsigned, unsigned> p;
452451

453-
if(get_object(expr.op0(), p.first) ||
454-
get_object(expr.op1(), p.second))
452+
if(get_object(rel.op0(), p.first) || get_object(rel.op1(), p.second))
455453
return;
456454

457-
const auto i0 = numeric_cast<mp_integer>(expr.op0());
458-
const auto i1 = numeric_cast<mp_integer>(expr.op1());
455+
const auto i0 = numeric_cast<mp_integer>(rel.op0());
456+
const auto i1 = numeric_cast<mp_integer>(rel.op1());
459457

460458
if(expr.id()==ID_le)
461459
{
@@ -483,9 +481,9 @@ void invariant_sett::strengthen_rec(const exprt &expr)
483481
}
484482
else if(expr.id()==ID_equal)
485483
{
486-
assert(expr.operands().size()==2);
484+
const auto &equal_expr = to_equal_expr(expr);
487485

488-
const typet &op_type=ns->follow(expr.op0().type());
486+
const typet &op_type = ns->follow(equal_expr.op0().type());
489487

490488
if(op_type.id()==ID_struct)
491489
{
@@ -495,9 +493,9 @@ void invariant_sett::strengthen_rec(const exprt &expr)
495493
for(const auto &comp : struct_type.components())
496494
{
497495
const member_exprt lhs_member_expr(
498-
expr.op0(), comp.get_name(), comp.type());
496+
equal_expr.op0(), comp.get_name(), comp.type());
499497
const member_exprt rhs_member_expr(
500-
expr.op1(), comp.get_name(), comp.type());
498+
equal_expr.op1(), comp.get_name(), comp.type());
501499

502500
const equal_exprt equality(lhs_member_expr, rhs_member_expr);
503501

@@ -511,48 +509,49 @@ void invariant_sett::strengthen_rec(const exprt &expr)
511509
// special rule: x = (a & b)
512510
// implies: x<=a && x<=b
513511

514-
if(expr.op1().id()==ID_bitand)
512+
if(equal_expr.op1().id() == ID_bitand)
515513
{
516-
const exprt &bitand_op=expr.op1();
514+
const exprt &bitand_op = equal_expr.op1();
517515

518516
forall_operands(it, bitand_op)
519517
{
520-
exprt tmp(expr);
518+
exprt tmp(equal_expr);
521519
tmp.op1()=*it;
522520
tmp.id(ID_le);
523521
strengthen_rec(tmp);
524522
}
525523

526524
return;
527525
}
528-
else if(expr.op0().id()==ID_bitand)
526+
else if(equal_expr.op0().id() == ID_bitand)
529527
{
530-
exprt tmp(expr);
528+
exprt tmp(equal_expr);
531529
std::swap(tmp.op0(), tmp.op1());
532530
strengthen_rec(tmp);
533531
return;
534532
}
535533

536534
// special rule: x = (type) y
537-
if(expr.op1().id()==ID_typecast)
535+
if(equal_expr.op1().id() == ID_typecast)
538536
{
539-
assert(expr.op1().operands().size()==1);
540-
add_type_bounds(expr.op0(), expr.op1().op0().type());
537+
assert(equal_expr.op1().operands().size() == 1);
538+
add_type_bounds(equal_expr.op0(), equal_expr.op1().op0().type());
541539
}
542-
else if(expr.op0().id()==ID_typecast)
540+
else if(equal_expr.op0().id() == ID_typecast)
543541
{
544-
assert(expr.op0().operands().size()==1);
545-
add_type_bounds(expr.op1(), expr.op0().op0().type());
542+
assert(equal_expr.op0().operands().size() == 1);
543+
add_type_bounds(equal_expr.op1(), equal_expr.op0().op0().type());
546544
}
547545

548546
std::pair<unsigned, unsigned> p, s;
549547

550-
if(get_object(expr.op0(), p.first) ||
551-
get_object(expr.op1(), p.second))
548+
if(
549+
get_object(equal_expr.op0(), p.first) ||
550+
get_object(equal_expr.op1(), p.second))
552551
return;
553552

554-
const auto i0 = numeric_cast<mp_integer>(expr.op0());
555-
const auto i1 = numeric_cast<mp_integer>(expr.op1());
553+
const auto i0 = numeric_cast<mp_integer>(equal_expr.op0());
554+
const auto i1 = numeric_cast<mp_integer>(equal_expr.op1());
556555
if(i0.has_value())
557556
add_bounds(p.second, boundst(*i0));
558557
else if(i1.has_value())
@@ -569,12 +568,13 @@ void invariant_sett::strengthen_rec(const exprt &expr)
569568
}
570569
else if(expr.id()==ID_notequal)
571570
{
572-
assert(expr.operands().size()==2);
571+
const auto &notequal_expr = to_notequal_expr(expr);
573572

574573
std::pair<unsigned, unsigned> p;
575574

576-
if(get_object(expr.op0(), p.first) ||
577-
get_object(expr.op1(), p.second))
575+
if(
576+
get_object(notequal_expr.op0(), p.first) ||
577+
get_object(notequal_expr.op1(), p.second))
578578
return;
579579

580580
// check if this is a contradiction
@@ -629,19 +629,19 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
629629
expr.id()==ID_equal ||
630630
expr.id()==ID_notequal)
631631
{
632-
assert(expr.operands().size()==2);
632+
const auto &rel = to_binary_relation_expr(expr);
633633

634634
std::pair<unsigned, unsigned> p;
635635

636-
bool ob0=get_object(expr.op0(), p.first);
637-
bool ob1=get_object(expr.op1(), p.second);
636+
bool ob0 = get_object(rel.op0(), p.first);
637+
bool ob1 = get_object(rel.op1(), p.second);
638638

639639
if(ob0 || ob1)
640640
return tvt::unknown();
641641

642642
tvt r;
643643

644-
if(expr.id()==ID_le)
644+
if(rel.id() == ID_le)
645645
{
646646
r=is_le(p);
647647
if(!r.is_unknown())
@@ -653,7 +653,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
653653

654654
return b0<=b1;
655655
}
656-
else if(expr.id()==ID_lt)
656+
else if(rel.id() == ID_lt)
657657
{
658658
r=is_lt(p);
659659
if(!r.is_unknown())
@@ -665,9 +665,9 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
665665

666666
return b0<b1;
667667
}
668-
else if(expr.id()==ID_equal)
668+
else if(rel.id() == ID_equal)
669669
return is_eq(p);
670-
else if(expr.id()==ID_notequal)
670+
else if(rel.id() == ID_notequal)
671671
return is_ne(p);
672672
else
673673
UNREACHABLE;
@@ -717,10 +717,9 @@ void invariant_sett::nnf(exprt &expr, bool negate)
717717
}
718718
else if(expr.id()==ID_not)
719719
{
720-
assert(expr.operands().size()==1);
721-
nnf(expr.op0(), !negate);
720+
nnf(to_not_expr(expr).op(), !negate);
722721
exprt tmp;
723-
tmp.swap(expr.op0());
722+
tmp.swap(to_not_expr(expr).op());
724723
expr.swap(tmp);
725724
}
726725
else if(expr.id()==ID_and)
@@ -741,14 +740,15 @@ void invariant_sett::nnf(exprt &expr, bool negate)
741740
}
742741
else if(expr.id()==ID_typecast)
743742
{
744-
assert(expr.operands().size()==1);
743+
const auto &typecast_expr = to_typecast_expr(expr);
745744

746-
if(expr.op0().type().id()==ID_unsignedbv ||
747-
expr.op0().type().id()==ID_signedbv)
745+
if(
746+
typecast_expr.op().type().id() == ID_unsignedbv ||
747+
typecast_expr.op().type().id() == ID_signedbv)
748748
{
749749
equal_exprt tmp;
750-
tmp.lhs()=expr.op0();
751-
tmp.rhs()=from_integer(0, expr.op0().type());
750+
tmp.lhs() = typecast_expr.op();
751+
tmp.rhs() = from_integer(0, typecast_expr.op().type());
752752
nnf(tmp, !negate);
753753
expr.swap(tmp);
754754
}

‎src/goto-symex/symex_builtin_functions.cpp‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -281,12 +281,13 @@ irep_idt get_string_argument_rec(const exprt &src)
281281
PRECONDITION(src.operands().size() == 1);
282282
if(src.op0().id()==ID_index)
283283
{
284-
PRECONDITION(src.op0().operands().size() == 2);
284+
const auto &index_expr = to_index_expr(src.op0());
285285

286-
if(src.op0().op0().id()==ID_string_constant &&
287-
src.op0().op1().is_zero())
286+
if(
287+
index_expr.array().id() == ID_string_constant &&
288+
index_expr.index().is_zero())
288289
{
289-
const exprt &fmt_str=src.op0().op0();
290+
const exprt &fmt_str = index_expr.array();
290291
return fmt_str.get_string(ID_value);
291292
}
292293
}

0 commit comments

Comments
 (0)