33 static const char LOG_HEADER[] =
"assigns clause checking: ";
37 "contracts:propagate-static-local";
41 const auto &pragmas = source_location.
get_pragmas();
52 "contracts:disable:assigns-check";
57 location.
add_pragma(
"disable:pointer-primitive-check");
58 location.
add_pragma(
"disable:pointer-overflow-check");
59 location.
add_pragma(
"disable:signed-overflow-check");
60 location.
add_pragma(
"disable:unsigned-overflow-check");
61 location.
add_pragma(
"disable:conversion-check");
69 const auto &pragmas = target->source_location().get_pragmas();
96 if(
auto target = expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
122 "symbol is not tracked :" +
from_expr(
ns,
"", symbol_expr));
154 lhs.
id() == ID_symbol &&
170 "the instrumented function must exist in the model");
183 std::unordered_set<symbol_exprt, irep_hash> symbols;
186 for(
const auto &expr : propagated)
189 for(
const auto &sym : symbols)
202 std::unordered_set<symbol_exprt, irep_hash> symbols;
205 for(
const auto &sym : symbols)
208 for(
const auto &expr : propagated)
219 for(; it != end; it++)
221 const auto &loc = it->source_location();
222 const auto &loc_fun = loc.get_function();
225 auto &itv = covered_locations[loc_fun];
226 if(loc_fun == ambient_function_id)
239 log.
debug() <<
"Ignoring instruction without function attribute"
252 "Expected an assignment of the form `symbol_exprt := "
253 "side_effect_expr_nondett`");
259 if(it->is_function_call())
261 const auto &fun_expr = it->call_function();
264 fun_expr.id() == ID_symbol,
265 "Local static search requires function pointer removal");
271 "Function " +
id2string(fun_id) +
"not in function map");
274 if(covered_locations.find(fun_id) == covered_locations.end())
277 covered_locations[fun_id].anywhere();
295 std::unordered_set<symbol_exprt, irep_hash> &dest)
297 for(
const auto &sym_pair :
st)
299 const auto &sym = sym_pair.second;
300 if(sym.is_static_lifetime)
302 const auto &loc = sym.location;
303 if(!loc.get_function().empty())
305 const auto &itv = covered_locations.find(loc.get_function());
306 if(itv != covered_locations.end() && itv->second.contains(sym.location))
307 dest.insert(sym.symbol_expr());
338 while(instruction_it != instruction_end)
343 (pred && !pred(instruction_it)))
356 const auto &decl_symbol = instruction_it->decl_symbol();
372 else if(instruction_it->is_function_call())
378 const auto &symbol = instruction_it->dead_symbol();
394 log.
warning() <<
"Found a `DEAD` variable " << symbol.get_identifier()
395 <<
" without corresponding `DECL`, at: "
400 instruction_it->is_other() &&
401 instruction_it->get_other().get_statement() == ID_havoc_object)
403 auto havoc_argument = instruction_it->get_other().operands().front();
405 havoc_object.add_source_location() = instruction_it->source_location();
423 std::list<irep_idt> new_vars;
425 new_vars = cleaner.
clean(condition, dest,
mode);
428 for(
const auto &target : group.
targets())
460 const std::string &suffix,
477 const exprt &condition,
478 const exprt &target)
const
481 const auto &valid_var =
490 if(target.
id() == ID_pointer_object)
517 "call to function '" +
id2string(ident) +
518 "' in assigns clause not supported yet");
522 const auto &ptr = funcall.arguments().at(0);
542 const auto &ptr = funcall.arguments().at(0);
543 const auto &size = funcall.arguments().at(1);
558 const auto &ptr = funcall.arguments().at(0);
575 const auto &ptr = funcall.arguments().at(0);
576 const auto &size = funcall.arguments().at(1);
577 const auto &is_ptr_to_ptr = funcall.arguments().at(2);
599 "no definite size for lvalue target:\n" + target.
pretty());
652 bool allow_null_target)
const
663 if(allow_null_target)
671 bool allow_null_target,
685 std::string
comment =
"Check that ";
703 bool include_stack_allocated,
718 const auto &orig_comment = source_location.
get_comment();
719 std::string
comment =
"Check that ";
732 exprt inclusion_check =
735 auto &checked_assigns =
736 static_cast<exprt &
>(inclusion_check.
add(ID_checked_assigns));
737 checked_assigns = car.
target();
754 pointer_offset(car.lower_bound_var())},
756 pointer_offset(car.upper_bound_var()),
757 pointer_offset(candidate_car.upper_bound_var())}}},
764 bool include_stack_allocated)
const
767 (!include_stack_allocated ||
804 if(include_stack_allocated)
834 const exprt &condition,
841 log.
warning() <<
"Ignored duplicate expression '"
843 <<
"' in assigns clause spec at "
845 return found->second;
862 log.
warning() <<
"Ignored duplicate stack-allocated target '"
865 return found->second;
891 log.
warning() <<
"Ignored duplicate static local var target '"
894 return found->second;
917 not_exprt{same_object(
918 tracked_car.lower_bound_var(), freed_car.lower_bound_var())}},
946 <<
"skipping checking on assignment to local symbol "
984 <<
"skipping check on assignment to local composite member expression "
1009 <<
format(target->decl_symbol()) <<
" as assignable"
1016 <<
format(target->decl_symbol())
1034 auto lhs = instruction_it->assign_lhs();
1035 lhs.add_source_location() = instruction_it->source_location();
1046 instruction_it->is_function_call(),
1047 "The first argument of instrument_call_statement should always be "
1050 const auto &callee_name =
1053 if(callee_name ==
"malloc")
1056 if(function_call.lhs().is_not_nil())
1060 object.add_source_location() = function_call.source_location();
1072 else if(callee_name ==
"free")
1074 const auto &ptr = instruction_it->call_arguments().front();
1076 object.add_source_location() = instruction_it->source_location();
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
signedbv_typet signed_size_type()
bitvector_typet char_type()
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
Operator to return the address of an object.
Class that represents a normalized conditional address range, with:
const exprt & target_size() const
Size of the target in bytes.
const symbol_exprt & upper_bound_var() const
Identifier of the upper address bound snapshot variable.
const exprt & condition() const
Condition expression. When this condition holds the target is allowed.
const symbol_exprt & valid_var() const
Identifier of the validity snapshot variable.
const exprt & target() const
The target expression.
const symbol_exprt & lower_bound_var() const
Identifier of the lower address bound snapshot variable.
const exprt & target_start_address() const
Start address of the target.
virtual bool is_not_local_or_dirty_local(const irep_idt &ident) const =0
Returns true iff the given ident is either non-locally declared or is locally-declared but dirty.
virtual bool is_local(const irep_idt &ident) const =0
Returns true iff ident is locally declared.
bool is_local_composite_access(const exprt &expr) const
Returns true iff expr is an access to a locally declared symbol and does not contain dereference or a...
Class that allows to clean expressions of side effects and to generate havoc_slice expressions.
std::list< irep_idt > clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Class that represents a single conditional target.
A class for an expression that represents a conditional target or a list of targets sharing a common ...
const exprt & condition() const
const exprt::operandst & targets() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
source_locationt & source_location_nonconst()
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
bool empty() const
Is the program empty?
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
bool must_track_dead(const goto_programt::const_targett &target) const
Returns true iff a DEAD x must be processed to update the write set.
void invalidate_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Generate instructions to invalidate a stack-allocated object that goes DEAD in dest.
std::unordered_set< symbol_exprt, irep_hash > propagated_static_localst
const goto_functionst & functions
Other functions of the model.
void collect_static_symbols(covered_locationst &covered_locations, std::unordered_set< symbol_exprt, irep_hash > &dest)
Collects static symbols from the symbol table that have a source location included in one of the cove...
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
bool must_check_assign(const goto_programt::const_targett &target)
Returns true iff an ASSIGN lhs := rhs instruction must be instrumented.
symbol_exprt_to_car_mapt from_stack_alloc
Map from DECL symbols to corresponding conditional address ranges.
void inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, goto_programt &dest) const
Returns an inclusion check assertion of lhs over all tracked cars.
void track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Track a stack-allocated object and generate snaphsot instructions in dest.
cond_target_exprt_to_car_mapt from_spec_assigns
Map from conditional target expressions of assigns clauses to corresponding conditional address range...
void instrument_assign_statement(goto_programt::targett &instruction_it, goto_programt &body) const
Inserts an assertion in body immediately before the assignment at instruction_it, to ensure that the ...
const car_exprt & create_car_from_static_local(const symbol_exprt &target)
void track_heap_allocated(const exprt &expr, goto_programt &dest)
Track a whole heap-alloc object and generate snaphsot instructions in dest.
symbol_table_baset & st
Program symbol table.
symbol_exprt_to_car_mapt from_static_local
Map to from detected or propagated static local symbols to corresponding conditional address ranges.
const car_exprt & create_car_from_spec_assigns(const exprt &condition, const exprt &target)
const irep_idt & mode
Language mode.
void invalidate_car(const car_exprt &tracked_car, const car_exprt &freed_car, goto_programt &result) const
Adds an assignment in dest to invalidate the tracked car if was valid before and was pointing to the ...
car_expr_listt from_heap_alloc
car_exprt create_car_expr(const exprt &condition, const exprt &target) const
Creates a conditional address range expression from a cleaned-up condition and target expression.
void track_spec_target_group(const conditional_target_group_exprt &group, goto_programt &dest)
Track and generate snaphsot instructions and target validity checking assertions for a conditional ta...
bool must_track_decl_or_dead(const irep_idt &ident) const
Returns true iff a function-local symbol must be tracked.
void target_validity_assertion(const car_exprt &car, bool allow_null_target, goto_programt &dest) const
Generates the target validity assertion for the given car and adds it to dest.
void track_static_locals(goto_programt &dest)
Searches the goto instructions reachable from the start to the end of the instrumented function's ins...
void instrument_call_statement(goto_programt::targett &instruction_it, goto_programt &body)
Inserts an assertion in body immediately before the function call at instruction_it,...
void instrument_instructions(goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, const std::function< bool(const goto_programt::targett &)> &pred={})
Instruments a sequence of instructions with inclusion checks.
void track_plain_spec_target(const exprt &expr, goto_programt &dest)
Track and generate snaphsot instructions and target validity checking assertions for a conditional ta...
void check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, goto_programt &dest)
Generates inclusion check instructions for an argument passed to free.
void invalidate_heap_and_spec_aliases(const car_exprt &freed_car, goto_programt &dest) const
Generates instructions to invalidate all targets aliased with a car that was passed to free,...
void traverse_instructions(const irep_idt ambient_function_id, goto_programt::const_targett it, const goto_programt::const_targett end, covered_locationst &covered_locations, propagated_static_localst &propagated) const
Traverses the given list of instructions, updating the given coverage map, recursing into function ca...
void track_static_locals_between(goto_programt::const_targett it, const goto_programt::const_targett end, goto_programt &dest)
Searches the goto instructions reachable between the given it and end target instructions to identify...
bool must_track_decl(const goto_programt::const_targett &target) const
Returns true iff a DECL x must be explicitly added to the write set.
const car_exprt & create_car_from_stack_alloc(const symbol_exprt &target)
exprt inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated) const
Returns an inclusion check expression of lhs over all tracked cars.
const car_exprt & create_car_from_heap_alloc(const exprt &target)
exprt inclusion_check_single(const car_exprt &lhs, const car_exprt &candidate_car) const
Returns inclusion check expression for a single candidate location.
const namespacet ns
Program namespace.
exprt target_validity_expr(const car_exprt &car, bool allow_null_target) const
Returns the target validity expression for a car_exprt.
void check_inclusion_assignment(const exprt &lhs, goto_programt &dest) const
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.
cfg_infot & cfg_info
CFG information for simplification.
void create_snapshot(const car_exprt &car, goto_programt &dest) const
Returns snapshot instructions for a car_exprt.
const irep_idt & function_id
Name of the instrumented function.
bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const
Returns true if the expression is tracked.
std::unordered_map< irep_idt, location_intervalt > covered_locationst
Map type from function identifiers to covered locations.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
irept & add(const irep_idt &name)
Binary less than or equal operator expression.
source_locationt source_location
mstreamt & warning() const
message_handlert & get_message_handler()
The plus expression Associativity is not specified.
const irep_idt & get_function() const
void set_comment(const irep_idt &comment)
const irep_idt & get_comment() const
void set_property_class(const irep_idt &property_class)
const irept::named_subt & get_pragmas() const
void add_pragma(const irep_idt &pragma)
std::string as_string() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
A predicate that indicates that an address range is ok to write.
bool has_prefix(const std::string &s, const std::string &prefix)
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
#define Forall_goto_program_instructions(it, program)
static const char PROPAGATE_STATIC_LOCAL_PRAGMA[]
Pragma used to mark assignments to static locals that need to be propagated.
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
bool has_disable_assigns_check_pragma(const goto_programt::const_targett &target)
Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' prag...
bool has_propagate_static_local_pragma(const source_locationt &source_location)
const char CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK[]
A local pragma used to keep track and skip already instrumented instructions.
static const char LOG_HEADER[]
header for log messages
void add_propagate_static_local_pragma(source_locationt &source_location)
Sets a pragma to mark assignments to static local variables that need to be propagated upwards in the...
static symbol_exprt create_fresh_symbol(const std::string &suffix, const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symbol_table)
Creates a fresh symbolt with given suffix, scoped to the function of location.
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define UNREACHABLE
This should be used to mark dead code.
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool can_cast_expr< symbol_exprt >(const exprt &base)
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
Returns true if the given comment matches the type of comments created by make_assigns_clause_replace...
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.