Skip to content

Commit

Permalink
uninitialized check
Browse files Browse the repository at this point in the history 
Uninitialized local or dynamically allocated variables have an indeterminate
initial value.

Reading an indeterminate value _may_ be undefined behavior, or may yield an
unspecific value.

This adds a check for uninitialized local variables.  The check is not added
as a standard check.
  • Loading branch information
@kroening
kroening committed Dec 23, 2024
1 parent c4aaafd commit 1e08a57
Show file tree
Hide file tree
Showing 2 changed files with 58 additions and 24 deletions.
77 changes: 53 additions & 24 deletions src/ansi-c/goto-conversion/goto_check_c.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,8 @@ class goto_check_ct
{
enable_bounds_check = _options.get_bool_option("bounds-check");
enable_pointer_check = _options.get_bool_option("pointer-check");
enable_uninitialized_check =
_options.get_bool_option("uninitialized-check");
enable_memory_leak_check = _options.get_bool_option("memory-leak-check");
enable_memory_cleanup_check =
_options.get_bool_option("memory-cleanup-check");
Expand Down Expand Up @@ -157,11 +159,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_lhs: the expression is the LHS of an assignment
void check_rec(const exprt &, const guardt &, bool is_lhs);

/// 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_lhs: the expression is the LHS of an assignment
void check(const exprt &expr, bool is_lhs);

struct conditiont
{
Expand All @@ -187,6 +191,7 @@ class goto_check_ct
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 &);
void uninitialized_check(const symbol_exprt &, const guardt &);
void memory_leak_check(const irep_idt &function_id);

/// Generates VCCs for the validity of the given dereferencing operation.
Expand Down Expand Up @@ -263,6 +268,7 @@ class goto_check_ct

bool enable_bounds_check;
bool enable_pointer_check;
bool enable_uninitialized_check;
bool enable_memory_leak_check;
bool enable_memory_cleanup_check;
bool enable_div_by_zero_check;
Expand All @@ -284,6 +290,7 @@ class goto_check_ct
std::map<irep_idt, bool *> name_to_flag{
{"bounds-check", &enable_bounds_check},
{"pointer-check", &enable_pointer_check},
{"uninitialized-check", &enable_uninitialized_check},
{"memory-leak-check", &enable_memory_leak_check},
{"memory-cleanup-check", &enable_memory_cleanup_check},
{"div-by-zero-check", &enable_div_by_zero_check},
Expand Down Expand Up @@ -1331,6 +1338,23 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
guard);
}

void goto_check_ct::uninitialized_check(
const symbol_exprt &expr,
const guardt &guard)
{
if(!enable_uninitialized_check)
return;

add_guarded_property(
false_exprt{},
"reading uninitialized local",
"uninitialized",
true, // not fatal
expr.find_source_location(),
expr,
guard);
}

void goto_check_ct::pointer_rel_check(
const binary_exprt &expr,
const guardt &guard)
Expand Down Expand Up @@ -1807,13 +1831,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 +1867,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 +1879,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 +1902,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 +1993,7 @@ 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_lhs)
{
if(expr.id() == ID_exists || expr.id() == ID_forall)
{
Expand All @@ -1980,7 +2004,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,7 +2031,7 @@ 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);
Expand Down Expand Up @@ -2048,6 +2072,10 @@ void goto_check_ct::check_rec(const exprt &expr, const guardt &guard)
{
pointer_validity_check(to_dereference_expr(expr), expr, guard);
}
else if(expr.id() == ID_symbol)
{
uninitialized_check(to_symbol_expr(expr), guard);
}
else if(requires_pointer_primitive_check(expr))
{
pointer_primitive_check(expr, guard);
Expand All @@ -2059,9 +2087,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_lhs)
{
check_rec(expr, identity);
check_rec(expr, identity, is_lhs);
}

void goto_check_ct::memory_leak_check(const irep_idt &function_id)
Expand Down Expand Up @@ -2151,7 +2179,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,12 +2212,12 @@ 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())
Expand All @@ -2202,10 +2230,10 @@ void goto_check_ct::goto_check(
{
flag_overridet resetter(i.source_location());
resetter.disable_flag(enable_enum_range_check, "enum_range_check");
check(assign_lhs);
check(assign_lhs, true);
}

check(assign_rhs);
check(assign_rhs, false);

// the LHS might invalidate any assertion
invalidate(assign_lhs);
Expand All @@ -2217,12 +2245,13 @@ void goto_check_ct::goto_check(
{
flag_overridet resetter(i.source_location());
resetter.disable_flag(enable_enum_range_check, "enum_range_check");
check(i.call_lhs());
check(i.call_lhs(), true);
}
check(i.call_function());

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 +2260,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 +2371,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
5 changes: 5 additions & 0 deletions src/ansi-c/goto-conversion/goto_check_c.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ void goto_check_c(

#define OPT_GOTO_CHECK \
"(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)" \
"(uninitialized-check)" \
"(div-by-zero-check)(float-div-by-zero-check)" \
"(enum-range-check)" \
"(signed-overflow-check)(unsigned-overflow-check)" \
Expand All @@ -51,6 +52,7 @@ void goto_check_c(
"(assert-to-assume)" \
"(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)" \
"(no-pointer-primitive-check)(no-undefined-shift-check)" \
"(no-uninitialized-check)" \
"(no-div-by-zero-check)"

// clang-format off
Expand All @@ -59,6 +61,8 @@ void goto_check_c(
" {y--bounds-check} \t enable array bounds checks (default on)\n" \
" {y--no-bounds-check} \t disable array bounds checks\n" \
" {y--pointer-check} \t enable pointer checks (default on)\n" \
" {y--uninitialized-check} \t enable checks for uninitialized data (default off)\n" \
" {y--no-uninitialized-check} \t disable checks for uninitialized data\n" \
" {y--no-pointer-check} \t disable pointer checks\n" \
" {y--memory-leak-check} \t enable memory leak checks\n" \
" {y--memory-cleanup-check} \t enable memory cleanup checks\n" \
Expand Down Expand Up @@ -126,6 +130,7 @@ void goto_check_c(
options.set_option("error-label", cmdline.get_values("error-label")); \
PARSE_OPTION_OVERRIDE(cmdline, options, "bounds-check"); \
PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-check"); \
PARSE_OPTION_OVERRIDE(cmdline, options, "uninitialized-check"); \
PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \
PARSE_OPTION_OVERRIDE(cmdline, options, "float-div-by-zero-check"); \
PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \
Expand Down

0 comments on commit 1e08a57

Please sign in to comment.