Skip to content

Commit 040a00e

Browse files
committed
fix enum-range check for LHSs
The check_rec recursion now distinguishes values that are assigned to, enabling a fix of #8543.
1 parent fbee5c1 commit 040a00e

File tree

2 files changed

+36
-41
lines changed

2 files changed

+36
-41
lines changed

regression/cbmc/enum_is_in_range/enum_lhs.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
enum_lhs.c
33
--enum-range-check
44
^\[main\.enum-range-check\.2\] line 14 enum range check in \(my_enumt\)4: FAILURE$

src/ansi-c/goto-conversion/goto_check_c.cpp

Lines changed: 35 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -157,11 +157,13 @@ class goto_check_ct
157157
/// guard.
158158
/// \param expr: the expression to be checked
159159
/// \param guard: the condition for when the check should be made
160-
void check_rec(const exprt &expr, const guardt &guard);
160+
/// \param is_assigned: the expression is assigned to
161+
void check_rec(const exprt &expr, const guardt &guard, bool is_assigned);
161162

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

166168
struct conditiont
167169
{
@@ -183,7 +185,7 @@ class goto_check_ct
183185
void float_div_by_zero_check(const div_exprt &, const guardt &);
184186
void mod_by_zero_check(const mod_exprt &, const guardt &);
185187
void mod_overflow_check(const mod_exprt &, const guardt &);
186-
void enum_range_check(const exprt &, const guardt &);
188+
void enum_range_check(const exprt &, const guardt &, bool is_assigned);
187189
void undefined_shift_check(const shift_exprt &, const guardt &);
188190
void pointer_rel_check(const binary_exprt &, const guardt &);
189191
void pointer_overflow_check(const exprt &, const guardt &);
@@ -537,11 +539,14 @@ void goto_check_ct::float_div_by_zero_check(
537539
guard);
538540
}
539541

540-
void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
542+
void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard, bool is_assigned)
541543
{
542544
if(!enable_enum_range_check)
543545
return;
544546

547+
if(is_assigned)
548+
return; // not in range yet
549+
545550
// we might be looking at a lowered enum_is_in_range_exprt, skip over these
546551
const auto &pragmas = expr.source_location().get_pragmas();
547552
for(const auto &d : pragmas)
@@ -1807,13 +1812,13 @@ void goto_check_ct::check_rec_address(const exprt &expr, const guardt &guard)
18071812

18081813
if(expr.id() == ID_dereference)
18091814
{
1810-
check_rec(to_dereference_expr(expr).pointer(), guard);
1815+
check_rec(to_dereference_expr(expr).pointer(), guard, false);
18111816
}
18121817
else if(expr.id() == ID_index)
18131818
{
18141819
const index_exprt &index_expr = to_index_expr(expr);
18151820
check_rec_address(index_expr.array(), guard);
1816-
check_rec(index_expr.index(), guard);
1821+
check_rec(index_expr.index(), guard, false);
18171822
}
18181823
else
18191824
{
@@ -1843,7 +1848,7 @@ void goto_check_ct::check_rec_logical_op(const exprt &expr, const guardt &guard)
18431848
return guard(implication(conjunction(constraints), expr));
18441849
};
18451850

1846-
check_rec(op, new_guard);
1851+
check_rec(op, new_guard, false);
18471852

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

1858-
check_rec(if_expr.cond(), guard);
1863+
check_rec(if_expr.cond(), guard, false);
18591864

18601865
{
18611866
auto new_guard = [&guard, &if_expr](exprt expr) {
18621867
return guard(implication(if_expr.cond(), std::move(expr)));
18631868
};
1864-
check_rec(if_expr.true_case(), new_guard);
1869+
check_rec(if_expr.true_case(), new_guard, false);
18651870
}
18661871

18671872
{
18681873
auto new_guard = [&guard, &if_expr](exprt expr) {
18691874
return guard(implication(not_exprt(if_expr.cond()), std::move(expr)));
18701875
};
1871-
check_rec(if_expr.false_case(), new_guard);
1876+
check_rec(if_expr.false_case(), new_guard, false);
18721877
}
18731878
}
18741879

@@ -1878,7 +1883,7 @@ bool goto_check_ct::check_rec_member(
18781883
{
18791884
const dereference_exprt &deref = to_dereference_expr(member.struct_op());
18801885

1881-
check_rec(deref.pointer(), guard);
1886+
check_rec(deref.pointer(), guard, false);
18821887

18831888
// avoid building the following expressions when pointer_validity_check
18841889
// would return immediately anyway
@@ -1969,7 +1974,10 @@ void goto_check_ct::check_rec_arithmetic_op(
19691974
}
19701975
}
19711976

1972-
void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
1977+
void goto_check_ct::check_rec(
1978+
const exprt &expr,
1979+
const guardt &guard,
1980+
bool is_assigned)
19731981
{
19741982
if(expr.id() == ID_exists || expr.id() == ID_forall)
19751983
{
@@ -1980,7 +1988,7 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
19801988
return guard(forall_exprt(quantifier_expr.symbol(), expr));
19811989
};
19821990

1983-
check_rec(quantifier_expr.where(), new_guard);
1991+
check_rec(quantifier_expr.where(), new_guard, false);
19841992
return;
19851993
}
19861994
else if(expr.id() == ID_address_of)
@@ -2007,10 +2015,10 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
20072015
}
20082016

20092017
for(const auto &op : expr.operands())
2010-
check_rec(op, guard);
2018+
check_rec(op, guard, false);
20112019

20122020
if(expr.type().id() == ID_c_enum_tag)
2013-
enum_range_check(expr, guard);
2021+
enum_range_check(expr, guard, is_assigned);
20142022

20152023
if(expr.id() == ID_index)
20162024
{
@@ -2059,9 +2067,9 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
20592067
}
20602068
}
20612069

2062-
void goto_check_ct::check(const exprt &expr)
2070+
void goto_check_ct::check(const exprt &expr, bool is_assigned)
20632071
{
2064-
check_rec(expr, identity);
2072+
check_rec(expr, identity, is_assigned);
20652073
}
20662074

20672075
void goto_check_ct::memory_leak_check(const irep_idt &function_id)
@@ -2151,7 +2159,7 @@ void goto_check_ct::goto_check(
21512159

21522160
if(i.has_condition())
21532161
{
2154-
check(i.condition());
2162+
check(i.condition(), false);
21552163
}
21562164

21572165
// magic ERROR label?
@@ -2184,45 +2192,32 @@ void goto_check_ct::goto_check(
21842192

21852193
if(statement == ID_expression)
21862194
{
2187-
check(code);
2195+
check(code, false);
21882196
}
21892197
else if(statement == ID_printf)
21902198
{
21912199
for(const auto &op : code.operands())
2192-
check(op);
2200+
check(op, false);
21932201
}
21942202
}
21952203
else if(i.is_assign())
21962204
{
21972205
const exprt &assign_lhs = i.assign_lhs();
21982206
const exprt &assign_rhs = i.assign_rhs();
21992207

2200-
// Disable enum range checks for left-hand sides as their values are yet
2201-
// to be set (by this assignment).
2202-
{
2203-
flag_overridet resetter(i.source_location());
2204-
resetter.disable_flag(enable_enum_range_check, "enum_range_check");
2205-
check(assign_lhs);
2206-
}
2207-
2208-
check(assign_rhs);
2208+
check(assign_lhs, true);
2209+
check(assign_rhs, false);
22092210

22102211
// the LHS might invalidate any assertion
22112212
invalidate(assign_lhs);
22122213
}
22132214
else if(i.is_function_call())
22142215
{
2215-
// Disable enum range checks for left-hand sides as their values are yet
2216-
// to be set (by this function call).
2217-
{
2218-
flag_overridet resetter(i.source_location());
2219-
resetter.disable_flag(enable_enum_range_check, "enum_range_check");
2220-
check(i.call_lhs());
2221-
}
2222-
check(i.call_function());
2216+
check(i.call_lhs(), true);
2217+
check(i.call_function(), false);
22232218

22242219
for(const auto &arg : i.call_arguments())
2225-
check(arg);
2220+
check(arg, false);
22262221

22272222
check_shadow_memory_api_calls(i);
22282223

@@ -2231,7 +2226,7 @@ void goto_check_ct::goto_check(
22312226
}
22322227
else if(i.is_set_return_value())
22332228
{
2234-
check(i.return_value());
2229+
check(i.return_value(), false);
22352230
// the return value invalidate any assertion
22362231
invalidate(i.return_value());
22372232
}
@@ -2342,7 +2337,7 @@ void goto_check_ct::check_shadow_memory_api_calls(
23422337
{
23432338
const exprt &expr = i.call_arguments()[0];
23442339
PRECONDITION(expr.type().id() == ID_pointer);
2345-
check(dereference_exprt(expr));
2340+
check(dereference_exprt(expr), false);
23462341
}
23472342
}
23482343

0 commit comments

Comments
 (0)