Skip to content

Commit

Permalink
fix enum-range check for LHSs
Browse files Browse the repository at this point in the history 
The check_rec recursion now distinguishes values that are assigned to,
enabling a fix of #8543.
  • Loading branch information
@kroening
kroening committed Dec 23, 2024
1 parent fbee5c1 commit bb2ec84
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 41 deletions.
2 changes: 1 addition & 1 deletion regression/cbmc/enum_is_in_range/enum_lhs.desc
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE
enum_lhs.c
--enum-range-check
^\[main\.enum-range-check\.2\] line 14 enum range check in \(my_enumt\)4: FAILURE$
Expand Down
78 changes: 38 additions & 40 deletions src/ansi-c/goto-conversion/goto_check_c.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,11 +157,13 @@ class goto_check_ct
/// guard.
/// \param expr: the expression to be checked
/// \param guard: the condition for when the check should be made
void check_rec(const exprt &expr, const guardt &guard);
/// \param is_assigned: the expression is assigned to
void check_rec(const exprt &expr, const guardt &guard, bool is_assigned);

/// Initiate the recursively analysis of \p expr with its `guard' set to TRUE.
/// \param expr: the expression to be checked
void check(const exprt &expr);
/// \param is_assigned: the expression is assigned to
void check(const exprt &expr, bool is_assigned);

struct conditiont
{
Expand All @@ -183,7 +185,7 @@ class goto_check_ct
void float_div_by_zero_check(const div_exprt &, const guardt &);
void mod_by_zero_check(const mod_exprt &, const guardt &);
void mod_overflow_check(const mod_exprt &, const guardt &);
void enum_range_check(const exprt &, const guardt &);
void enum_range_check(const exprt &, const guardt &, bool is_assigned);
void undefined_shift_check(const shift_exprt &, const guardt &);
void pointer_rel_check(const binary_exprt &, const guardt &);
void pointer_overflow_check(const exprt &, const guardt &);
Expand Down Expand Up @@ -537,11 +539,17 @@ void goto_check_ct::float_div_by_zero_check(
guard);
}

void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
void goto_check_ct::enum_range_check(
const exprt &expr,
const guardt &guard,
bool is_assigned)
{
if(!enable_enum_range_check)
return;

if(is_assigned)
return; // not in range yet

// we might be looking at a lowered enum_is_in_range_exprt, skip over these
const auto &pragmas = expr.source_location().get_pragmas();
for(const auto &d : pragmas)
Expand Down Expand Up @@ -1807,13 +1815,13 @@ void goto_check_ct::check_rec_address(const exprt &expr, const guardt &guard)

if(expr.id() == ID_dereference)
{
check_rec(to_dereference_expr(expr).pointer(), guard);
check_rec(to_dereference_expr(expr).pointer(), guard, false);
}
else if(expr.id() == ID_index)
{
const index_exprt &index_expr = to_index_expr(expr);
check_rec_address(index_expr.array(), guard);
check_rec(index_expr.index(), guard);
check_rec(index_expr.index(), guard, false);
}
else
{
Expand Down Expand Up @@ -1843,7 +1851,7 @@ void goto_check_ct::check_rec_logical_op(const exprt &expr, const guardt &guard)
return guard(implication(conjunction(constraints), expr));
};

check_rec(op, new_guard);
check_rec(op, new_guard, false);

constraints.push_back(expr.id() == ID_or ? boolean_negate(op) : op);
}
Expand All @@ -1855,20 +1863,20 @@ void goto_check_ct::check_rec_if(const if_exprt &if_expr, const guardt &guard)
if_expr.cond().is_boolean(),
"first argument of if must be boolean, but got " + if_expr.cond().pretty());

check_rec(if_expr.cond(), guard);
check_rec(if_expr.cond(), guard, false);

{
auto new_guard = [&guard, &if_expr](exprt expr) {
return guard(implication(if_expr.cond(), std::move(expr)));
};
check_rec(if_expr.true_case(), new_guard);
check_rec(if_expr.true_case(), new_guard, false);
}

{
auto new_guard = [&guard, &if_expr](exprt expr) {
return guard(implication(not_exprt(if_expr.cond()), std::move(expr)));
};
check_rec(if_expr.false_case(), new_guard);
check_rec(if_expr.false_case(), new_guard, false);
}
}

Expand All @@ -1878,7 +1886,7 @@ bool goto_check_ct::check_rec_member(
{
const dereference_exprt &deref = to_dereference_expr(member.struct_op());

check_rec(deref.pointer(), guard);
check_rec(deref.pointer(), guard, false);

// avoid building the following expressions when pointer_validity_check
// would return immediately anyway
Expand Down Expand Up @@ -1969,7 +1977,10 @@ void goto_check_ct::check_rec_arithmetic_op(
}
}

void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
void goto_check_ct::check_rec(
const exprt &expr,
const guardt &guard,
bool is_assigned)
{
if(expr.id() == ID_exists || expr.id() == ID_forall)
{
Expand All @@ -1980,7 +1991,7 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
return guard(forall_exprt(quantifier_expr.symbol(), expr));
};

check_rec(quantifier_expr.where(), new_guard);
check_rec(quantifier_expr.where(), new_guard, false);
return;
}
else if(expr.id() == ID_address_of)
Expand All @@ -2007,10 +2018,10 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
}

for(const auto &op : expr.operands())
check_rec(op, guard);
check_rec(op, guard, false);

if(expr.type().id() == ID_c_enum_tag)
enum_range_check(expr, guard);
enum_range_check(expr, guard, is_assigned);

if(expr.id() == ID_index)
{
Expand Down Expand Up @@ -2059,9 +2070,9 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
}
}

void goto_check_ct::check(const exprt &expr)
void goto_check_ct::check(const exprt &expr, bool is_assigned)
{
check_rec(expr, identity);
check_rec(expr, identity, is_assigned);
}

void goto_check_ct::memory_leak_check(const irep_idt &function_id)
Expand Down Expand Up @@ -2151,7 +2162,7 @@ void goto_check_ct::goto_check(

if(i.has_condition())
{
check(i.condition());
check(i.condition(), false);
}

// magic ERROR label?
Expand Down Expand Up @@ -2184,45 +2195,32 @@ void goto_check_ct::goto_check(

if(statement == ID_expression)
{
check(code);
check(code, false);
}
else if(statement == ID_printf)
{
for(const auto &op : code.operands())
check(op);
check(op, false);
}
}
else if(i.is_assign())
{
const exprt &assign_lhs = i.assign_lhs();
const exprt &assign_rhs = i.assign_rhs();

// Disable enum range checks for left-hand sides as their values are yet
// to be set (by this assignment).
{
flag_overridet resetter(i.source_location());
resetter.disable_flag(enable_enum_range_check, "enum_range_check");
check(assign_lhs);
}

check(assign_rhs);
check(assign_lhs, true);
check(assign_rhs, false);

// the LHS might invalidate any assertion
invalidate(assign_lhs);
}
else if(i.is_function_call())
{
// Disable enum range checks for left-hand sides as their values are yet
// to be set (by this function call).
{
flag_overridet resetter(i.source_location());
resetter.disable_flag(enable_enum_range_check, "enum_range_check");
check(i.call_lhs());
}
check(i.call_function());
check(i.call_lhs(), true);
check(i.call_function(), false);

for(const auto &arg : i.call_arguments())
check(arg);
check(arg, false);

check_shadow_memory_api_calls(i);

Expand All @@ -2231,7 +2229,7 @@ void goto_check_ct::goto_check(
}
else if(i.is_set_return_value())
{
check(i.return_value());
check(i.return_value(), false);
// the return value invalidate any assertion
invalidate(i.return_value());
}
Expand Down Expand Up @@ -2342,7 +2340,7 @@ void goto_check_ct::check_shadow_memory_api_calls(
{
const exprt &expr = i.call_arguments()[0];
PRECONDITION(expr.type().id() == ID_pointer);
check(dereference_exprt(expr));
check(dereference_exprt(expr), false);
}
}

Expand Down

0 comments on commit bb2ec84

Please sign in to comment.