Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

uninitialized check #8545

Draft
wants to merge 1 commit into
base: develop
Choose a base branch
from
Draft

uninitialized check #8545

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
86 changes: 79 additions & 7 deletions src/ansi-c/goto-conversion/goto_check_c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,13 +46,15 @@ class goto_check_ct
{
public:
goto_check_ct(
const namespacet &_ns,
symbol_table_baset &_symbol_table,
const optionst &_options,
message_handlert &_message_handler)
: ns(_ns), local_bitvector_analysis(nullptr), log(_message_handler)
: ns(_symbol_table), symbol_table(_symbol_table), local_bitvector_analysis(nullptr), log(_message_handler)
{
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 @@ -94,7 +96,8 @@ class goto_check_ct
void collect_allocations(const goto_functionst &goto_functions);

protected:
const namespacet &ns;
const namespacet ns;
symbol_table_baset &symbol_table;
std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
goto_programt::const_targett current_target;
messaget log;
Expand Down Expand Up @@ -189,6 +192,8 @@ 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 &, bool is_assigned);
void memory_leak_check(const irep_idt &function_id);

/// Generates VCCs for the validity of the given dereferencing operation.
Expand Down Expand Up @@ -265,6 +270,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 @@ -286,6 +292,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 @@ -1341,6 +1348,66 @@ 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,
bool is_assigned)
{
if(!enable_uninitialized_check)
return;

// Ignore C function symbols.
if(expr.type().id() == ID_code)
return;

// Don't check the LHS of an assignment -- these do not
// have to be initialized
if(is_assigned)
return;

// Look up the symbol
auto &symbol = ns.lookup(expr);

// Anything with static lifetime is initialized by the runtime,
// and is hence never uninitialized.
if(symbol.is_static_lifetime)
return;

// Is the address taken? If so, uninitialized accesses are merely
// intederminate, but not undefined.
if(local_bitvector_analysis->dirty(expr))
return;

// Ignore structs/union/arrays for now
if(
symbol.type.id() == ID_struct || symbol.type.id() == ID_union ||
symbol.type.id() == ID_array)
{
return;
}

// Look up the bits that track initialization
auto init_bit_id = id2string(symbol.name) + "$init";

if(!symbol_table.has_symbol(init_bit_id))
{
auxiliary_symbolt new_init_symbol{init_bit_id, bool_typet{}, symbol.mode};
new_init_symbol.is_static_lifetime = false;
symbol_table.add(new_init_symbol);
}

const symbolt &init_symbol = ns.lookup(init_bit_id);

add_guarded_property(
init_symbol.symbol_expr(),
"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 @@ -2061,6 +2128,10 @@ void goto_check_ct::check_rec(
{
pointer_validity_check(to_dereference_expr(expr), expr, guard);
}
else if(expr.id() == ID_symbol)
{
uninitialized_check(to_symbol_expr(expr), guard, is_assigned);
}
else if(requires_pointer_primitive_check(expr))
{
pointer_primitive_check(expr, guard);
Expand Down Expand Up @@ -2469,6 +2540,7 @@ exprt goto_check_ct::is_in_bounds_of_some_explicit_allocation(
return disjunction(alloc_disjuncts);
}

#if 0
void goto_check_c(
const irep_idt &function_identifier,
goto_functionst::goto_functiont &goto_function,
Expand All @@ -2479,14 +2551,15 @@ void goto_check_c(
goto_check_ct goto_check(ns, options, message_handler);
goto_check.goto_check(function_identifier, goto_function);
}
#endif

void goto_check_c(
const namespacet &ns,
const optionst &options,
symbol_table_baset &symbol_table,
goto_functionst &goto_functions,
message_handlert &message_handler)
{
goto_check_ct goto_check(ns, options, message_handler);
goto_check_ct goto_check(symbol_table, options, message_handler);

goto_check.collect_allocations(goto_functions);

Expand All @@ -2501,8 +2574,7 @@ void goto_check_c(
goto_modelt &goto_model,
message_handlert &message_handler)
{
const namespacet ns(goto_model.symbol_table);
goto_check_c(ns, options, goto_model.goto_functions, message_handler);
goto_check_c(options, goto_model.symbol_table, goto_model.goto_functions, message_handler);
}

void goto_check_ct::add_active_named_check_pragmas(
Expand Down
7 changes: 7 additions & 0 deletions src/ansi-c/goto-conversion/goto_check_c.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ class namespacet;
class optionst;
class message_handlert;

#if 0
void goto_check_c(
const namespacet &ns,
const optionst &options,
Expand All @@ -31,6 +32,7 @@ void goto_check_c(
const namespacet &ns,
const optionst &options,
message_handlert &message_handler);
#endif

void goto_check_c(
const optionst &options,
Expand All @@ -39,6 +41,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 +54,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 +63,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 +132,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
Loading