14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
18 #include <unordered_map>
19 #include <unordered_set>
43 "condition must have no side_effect sub-expression");
70 const exprt &_condition,
72 const exprt &_target_start_address,
73 const exprt &_target_size,
82 _target_start_address,
160 log(_message_handler)
248 const std::string &suffix,
265 bool allow_null_target,
283 bool include_stack_allocated,
297 bool include_stack_allocated,
316 unordered_map<const conditional_target_exprt, const car_exprt, irep_hash>;
326 std::unordered_map<const symbol_exprt, const car_exprt, irep_hash>;
334 std::unordered_map<const exprt, const car_exprt, irep_hash>;
API to expression classes that are internal to the C frontend.
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.
car_exprt(const exprt &_condition, const exprt &_target, const exprt &_target_start_address, const exprt &_target_size, const symbol_exprt &_validity_var, const symbol_exprt &_lower_bound_var, const symbol_exprt &_upper_bound_var)
const exprt & target_start_address() const
Start address of the target.
Class that represents a single conditional target.
const exprt & target() const
Target expression.
conditional_target_exprt(const exprt &_condition, const exprt &_target)
const exprt & condition() const
Condition expression.
A class for an expression that represents a conditional target or a list of targets sharing a common ...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
source_locationt & add_source_location()
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
A class that generates instrumentation for assigns clause checking.
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.
const goto_functionst & functions
Other functions of the model.
instrument_spec_assignst(const irep_idt &_function_id, const goto_functionst &_functions, symbol_tablet &_st, message_handlert &_message_handler)
Class constructor.
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
symbol_exprt_to_car_mapt from_stack_alloc
Map to from DECL symbols to corresponding conditional address ranges.
void track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Track a stack-allocated object and generate snaphsot instructions in dest.
void inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest) const
Returns an inclusion check assertion of lhs over all tracked cars.
cond_target_exprt_to_car_mapt from_spec_assigns
Map to from conditional target expressions of assigns clauses to corresponding conditional address ra...
void track_heap_allocated(const exprt &expr, goto_programt &dest)
Track a whole heap-alloc object and generate snaphsot instructions in dest.
std::unordered_map< const symbol_exprt, const car_exprt, irep_hash > symbol_exprt_to_car_mapt
const car_exprt & create_car_from_spec_assigns(const exprt &condition, const exprt &target)
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 ...
exprt_to_car_mapt from_heap_alloc
Map to from malloc'd symbols to corresponding conditional address ranges.
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...
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.
exprt inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt) const
Returns an inclusion check expression of lhs over all tracked cars.
void track_static_locals(goto_programt &dest)
Search the call graph reachable from the instrumented function to identify local static variables use...
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...
std::unordered_map< const exprt, const car_exprt, irep_hash > exprt_to_car_mapt
const symbolt create_fresh_symbol(const std::string &suffix, const typet &type, const source_locationt &location) const
Creates a fresh symbolt with given suffix, scoped to function_id.
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,...
const car_exprt & create_car_from_stack_alloc(const symbol_exprt &target)
std::unordered_map< const conditional_target_exprt, const car_exprt, irep_hash > cond_target_exprt_to_car_mapt
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 create_snapshot(const car_exprt &car, goto_programt &dest) const
Returns snapshot instructions for a car_exprt.
symbol_tablet & st
Program symbol table.
const irep_idt & function_id
Name of the instrumented function.
void check_inclusion_assignment(const exprt &lhs, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.
bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const
Returns true if the expression is tracked.
void check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an argument passed to free.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a symbol (variable)
The type of an expression, extends irept.
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
nonstd::optional< T > optionalt
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.