replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

avoid access to exprt::opX 

This prevents out-of-bounds accesses to the operands() vector.
This commit is contained in:
Daniel Kroening 2019-04-18 15:21:38 +01:00
parent 65e6b6a495
commit dc67638cfc
9 changed files with 91 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
src/goto-instrument/accelerate/acceleration_utils.cpp
View File

@ -331,8 +331,7 @@ void acceleration_utilst::push_nondet(exprt &expr)
push_nondet(*it);
}
if(expr.id()==ID_not &&
expr.op0().id()==ID_nondet)
if(expr.id() == ID_not && to_not_expr(expr).op().id() == ID_nondet)
{
expr = side_effect_expr_nondett(expr.type(), expr.source_location());
}
@ -342,8 +341,8 @@ void acceleration_utilst::push_nondet(exprt &expr)
expr.id()==ID_le ||
expr.id()==ID_ge)
{
if(expr.op0().id()==ID_nondet ||
expr.op1().id()==ID_nondet)
const auto &rel_expr = to_binary_relation_expr(expr);
if(rel_expr.lhs().id() == ID_nondet || rel_expr.rhs().id() == ID_nondet)
{
expr = side_effect_expr_nondett(expr.type(), expr.source_location());
}
@ -887,7 +886,7 @@ bool acceleration_utilst::do_nonrecursive(
// for these variables by just forward simulating the path and
// taking the expressions we get at the end.
replace_mapt state;
expr_sett array_writes;
std::unordered_set<index_exprt, irep_hash> array_writes;
expr_sett arrays_written;
expr_sett arrays_read;
@ -938,21 +937,22 @@ bool acceleration_utilst::do_nonrecursive(
if(lhs.id()==ID_index)
{
replace_expr(state, lhs.op1());
array_writes.insert(lhs);
auto &lhs_index_expr = to_index_expr(lhs);
replace_expr(state, lhs_index_expr.index());
array_writes.insert(lhs_index_expr);
if(arrays_written.find(lhs.op0())!=arrays_written.end())
if(arrays_written.find(lhs_index_expr.array()) != arrays_written.end())
{
// We've written to this array before -- be conservative and bail
// out now.
#ifdef DEBUG
std::cout << "Bailing out on array written to twice in loop: " <<
expr2c(lhs.op0(), ns) << '\n';
std::cout << "Bailing out on array written to twice in loop: "
<< expr2c(lhs_index_expr.array(), ns) << '\n';
#endif
return false;
}
arrays_written.insert(lhs.op0());
arrays_written.insert(lhs_index_expr.array());
}
replace_expr(state, rhs);
@ -992,12 +992,10 @@ bool acceleration_utilst::do_nonrecursive(
}
}
for(expr_sett::iterator it=array_writes.begin();
it!=array_writes.end();
++it)
for(auto it = array_writes.begin(); it != array_writes.end(); ++it)
{
const exprt &lhs=*it;
const exprt &rhs=state[*it];
const auto &lhs = *it;
const auto &rhs = state[*it];
if(!assign_array(lhs, rhs, program))
{
@ -1013,7 +1011,7 @@ bool acceleration_utilst::do_nonrecursive(
}
bool acceleration_utilst::assign_array(
const exprt &lhs,
const index_exprt &lhs,
const exprt &rhs,
scratch_programt &program)
{
@ -1081,7 +1079,7 @@ bool acceleration_utilst::assign_array(
{
if(idx.id()==ID_pointer_offset)
{
poly.from_expr(idx.op0());
poly.from_expr(to_unary_expr(idx).op());
}
else
{
@ -1204,10 +1202,13 @@ void acceleration_utilst::gather_array_accesses(
const exprt &e,
expr_sett &arrays)
{
if(e.id()==ID_index ||
e.id()==ID_dereference)
if(e.id() == ID_index)
{
arrays.insert(e.op0());
arrays.insert(to_index_expr(e).array());
}
else if(e.id() == ID_dereference)
{
arrays.insert(to_dereference_expr(e).pointer());
}
forall_operands(it, e)

2
src/goto-instrument/accelerate/acceleration_utils.h
View File

@ -128,7 +128,7 @@ public:
expr_sett &nonrecursive,
scratch_programt &program);
bool assign_array(
const exprt &lhs,
const index_exprt &lhs,
const exprt &rhs,
scratch_programt &program);

68
src/goto-instrument/accelerate/overflow_instrumenter.cpp
View File

@ -104,12 +104,12 @@ void overflow_instrumentert::overflow_expr(
if(expr.id()==ID_typecast)
{
if(expr.op0().id()==ID_constant)
{
return;
}
const auto &typecast_expr = to_typecast_expr(expr);
const typet &old_type = expr.op0().type();
if(typecast_expr.op().id() == ID_constant)
return;
const typet &old_type = typecast_expr.op().type();
const std::size_t new_width = to_bitvector_type(expr.type()).get_width();
const std::size_t old_width = to_bitvector_type(old_type).get_width();
@ -124,13 +124,15 @@ void overflow_instrumentert::overflow_expr(
return;
}
cases.insert(
binary_relation_exprt(expr.op0(), ID_gt,
from_integer(power(2, new_width - 1) - 1, old_type)));
cases.insert(binary_relation_exprt(
typecast_expr.op(),
ID_gt,
from_integer(power(2, new_width - 1) - 1, old_type)));
cases.insert(
binary_relation_exprt(expr.op0(), ID_lt,
from_integer(-power(2, new_width - 1), old_type)));
cases.insert(binary_relation_exprt(
typecast_expr.op(),
ID_lt,
from_integer(-power(2, new_width - 1), old_type)));
}
else if(old_type.id()==ID_unsignedbv)
{
@ -141,9 +143,10 @@ void overflow_instrumentert::overflow_expr(
return;
}
cases.insert(
binary_relation_exprt(expr.op0(), ID_gt,
from_integer(power(2, new_width - 1) - 1, old_type)));
cases.insert(binary_relation_exprt(
typecast_expr.op(),
ID_gt,
from_integer(power(2, new_width - 1) - 1, old_type)));
}
}
else if(type.id()==ID_unsignedbv)
@ -151,15 +154,15 @@ void overflow_instrumentert::overflow_expr(
if(old_type.id()==ID_signedbv)
{
// signed -> unsigned
cases.insert(
binary_relation_exprt(expr.op0(), ID_lt,
from_integer(0, old_type)));
cases.insert(binary_relation_exprt(
typecast_expr.op(), ID_lt, from_integer(0, old_type)));
if(new_width < old_width - 1)
{
// Need to check for overflow as well as signedness.
cases.insert(
binary_relation_exprt(expr.op0(), ID_gt,
from_integer(power(2, new_width - 1) - 1, old_type)));
cases.insert(binary_relation_exprt(
typecast_expr.op(),
ID_gt,
from_integer(power(2, new_width - 1) - 1, old_type)));
}
}
else if(old_type.id()==ID_unsignedbv)
@ -171,20 +174,23 @@ void overflow_instrumentert::overflow_expr(
return;
}
cases.insert(
binary_relation_exprt(expr.op0(), ID_gt,
from_integer(power(2, new_width - 1) - 1, old_type)));
cases.insert(binary_relation_exprt(
typecast_expr.op(),
ID_gt,
from_integer(power(2, new_width - 1) - 1, old_type)));
}
}
}
else if(expr.id()==ID_div)
{
const auto &div_expr = to_div_expr(expr);
// Undefined for signed INT_MIN / -1
if(type.id()==ID_signedbv)
{
equal_exprt int_min_eq(
expr.op0(), to_signedbv_type(type).smallest_expr());
equal_exprt minus_one_eq(expr.op1(), from_integer(-1, type));
div_expr.dividend(), to_signedbv_type(type).smallest_expr());
equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
cases.insert(and_exprt(int_min_eq, minus_one_eq));
}
@ -195,9 +201,9 @@ void overflow_instrumentert::overflow_expr(
{
// Overflow on unary- can only happen with the smallest
// representable number.
cases.insert(
equal_exprt(expr.op0(),
to_signedbv_type(type).smallest_expr()));
cases.insert(equal_exprt(
to_unary_minus_expr(expr).op(),
to_signedbv_type(type).smallest_expr()));
}
}
else if(expr.id()==ID_plus ||
@ -229,14 +235,14 @@ void overflow_instrumentert::overflow_expr(
overflow.op0()=tmp;
overflow.op1()=expr.operands()[i];
fix_types(overflow);
fix_types(to_binary_expr(overflow));
cases.insert(overflow);
}
}
else
{
fix_types(overflow);
fix_types(to_binary_expr(overflow));
cases.insert(overflow);
}
}
@ -265,7 +271,7 @@ void overflow_instrumentert::overflow_expr(const exprt &expr, exprt &overflow)
}
}
void overflow_instrumentert::fix_types(exprt &overflow)
void overflow_instrumentert::fix_types(binary_exprt &overflow)
{
typet &t1=overflow.op0().type();
typet &t2=overflow.op1().type();

2
src/goto-instrument/accelerate/overflow_instrumenter.h
View File

@ -51,7 +51,7 @@ class overflow_instrumentert
void accumulate_overflow(goto_programt::targett t, const exprt &expr,
goto_programt::targetst &added);
void fix_types(exprt &overflow);
void fix_types(binary_exprt &overflow);
goto_programt &program;
symbol_tablet &symbol_table;

7
src/goto-instrument/accelerate/scratch_program.cpp
View File

@ -112,13 +112,14 @@ static void fix_types(exprt &expr)
expr.id()==ID_ge ||
expr.id()==ID_le)
{
exprt &lhs=expr.op0();
exprt &rhs=expr.op1();
auto &rel_expr = to_binary_relation_expr(expr);
exprt &lhs = rel_expr.lhs();
exprt &rhs = rel_expr.rhs();
if(lhs.type()!=rhs.type())
{
typecast_exprt typecast(rhs, lhs.type());
expr.op1().swap(typecast);
rel_expr.rhs().swap(typecast);
}
}
}

4
src/goto-instrument/cover_instrument_mcdc.cpp
View File

@ -208,7 +208,7 @@ collect_mcdc_controlling_nested(const std::set<exprt> &decisions)
// expansion of such an operand is stored in ''res''.
if(operands[i].id() == ID_not)
{
exprt no = operands[i].op0();
exprt no = to_not_expr(operands[i]).op();
if(!is_condition(no))
{
changed = true;
@ -271,7 +271,7 @@ std::set<signed> sign_of_expr(const exprt &e, const exprt &E)
// or, ''E'' is the negation of ''e''?
if(E.id() == ID_not)
{
if(e == E.op0())
if(e == to_not_expr(E).op())
{
signs.insert(-1);
return signs;

2
src/goto-instrument/cover_util.cpp
View File

@ -92,7 +92,7 @@ void collect_decisions_rec(const exprt &src, std::set<exprt> &dest)
}
else if(src.id() == ID_not)
{
collect_decisions_rec(src.op0(), dest);
collect_decisions_rec(to_not_expr(src).op(), dest);
}
else
{

7
src/goto-instrument/dump_c.cpp
View File

@ -1277,10 +1277,11 @@ void dump_ct::cleanup_expr(exprt &expr)
}
}
else if(
expr.id() == ID_typecast && expr.op0().id() == ID_typecast &&
expr.type() == expr.op0().type())
expr.id() == ID_typecast &&
to_typecast_expr(expr).op().id() == ID_typecast &&
expr.type() == to_typecast_expr(expr).op().type())
{
exprt tmp=expr.op0();
exprt tmp = to_typecast_expr(expr).op();
expr.swap(tmp);
}
else if(expr.id()==ID_code &&

35
src/goto-instrument/rw_set.cpp
View File

@ -113,23 +113,27 @@ void _rw_set_loct::read_write_rec(
}
else if(expr.id()==ID_member)
{
assert(expr.operands().size()==1);
const std::string &component_name=expr.get_string(ID_component_name);
const auto &member_expr = to_member_expr(expr);
const std::string &component_name =
id2string(member_expr.get_component_name());
read_write_rec(
expr.op0(), r, w, "." + component_name + suffix, guard_conjuncts);
member_expr.compound(),
r,
w,
"." + component_name + suffix,
guard_conjuncts);
}
else if(expr.id()==ID_index)
{
// we don't distinguish the array elements for now
assert(expr.operands().size()==2);
read_write_rec(expr.op0(), r, w, "[]" + suffix, guard_conjuncts);
read(expr.op1(), guard_conjuncts);
const auto &index_expr = to_index_expr(expr);
read_write_rec(index_expr.array(), r, w, "[]" + suffix, guard_conjuncts);
read(index_expr.index(), guard_conjuncts);
}
else if(expr.id()==ID_dereference)
{
assert(expr.operands().size()==1);
set_track_deref();
read(expr.op0(), guard_conjuncts);
read(to_dereference_expr(expr).pointer(), guard_conjuncts);
exprt tmp=expr;
#ifdef LOCAL_MAY
@ -166,8 +170,7 @@ void _rw_set_loct::read_write_rec(
}
else if(expr.id()==ID_typecast)
{
assert(expr.operands().size()==1);
read_write_rec(expr.op0(), r, w, suffix, guard_conjuncts);
read_write_rec(to_typecast_expr(expr).op(), r, w, suffix, guard_conjuncts);
}
else if(expr.id()==ID_address_of)
{
@ -175,16 +178,16 @@ void _rw_set_loct::read_write_rec(
}
else if(expr.id()==ID_if)
{
assert(expr.operands().size()==3);
read(expr.op0(), guard_conjuncts);
const auto &if_expr = to_if_expr(expr);
read(if_expr.cond(), guard_conjuncts);
exprt::operandst true_guard = guard_conjuncts;
true_guard.push_back(expr.op0());
read_write_rec(expr.op1(), r, w, suffix, true_guard);
true_guard.push_back(if_expr.cond());
read_write_rec(if_expr.true_case(), r, w, suffix, true_guard);
exprt::operandst false_guard = guard_conjuncts;
false_guard.push_back(not_exprt(expr.op0()));
read_write_rec(expr.op2(), r, w, suffix, false_guard);
false_guard.push_back(not_exprt(if_expr.cond()));
read_write_rec(if_expr.false_case(), r, w, suffix, false_guard);
}
else
{