14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
25 #include <unordered_map>
26 #include <unordered_set>
42 "condition must have no side_effect sub-expression");
77 const exprt &_condition,
79 const exprt &_target_start_address,
80 const exprt &_target_size,
90 _target_start_address,
207 log(_message_handler),
267 min_line = std::numeric_limits<std::size_t>::max();
268 min_col = std::numeric_limits<std::size_t>::max();
269 max_line = std::numeric_limits<std::size_t>::min();
270 max_col = std::numeric_limits<std::size_t>::min();
277 min_line = std::numeric_limits<std::size_t>::min();
278 min_col = std::numeric_limits<std::size_t>::min();
279 max_line = std::numeric_limits<std::size_t>::max();
280 max_col = std::numeric_limits<std::size_t>::max();
290 source_location, std::numeric_limits<std::size_t>::min()),
292 source_location, std::numeric_limits<std::size_t>::min()));
297 source_location, std::numeric_limits<std::size_t>::max()),
299 source_location, std::numeric_limits<std::size_t>::max()));
313 source_location, std::numeric_limits<std::size_t>::max()),
315 source_location, std::numeric_limits<std::size_t>::max())) &&
319 source_location, std::numeric_limits<std::size_t>::min()),
321 source_location, std::numeric_limits<std::size_t>::min()),
335 std::size_t default_value)
341 return default_value;
355 std::size_t default_value)
359 return default_value;
371 static bool is_lte(
size_t line0,
size_t col0,
size_t line1,
size_t col1)
373 return (line0 < line1) || ((line0 == line1) && (col0 <= col1));
426 std::unordered_set<symbol_exprt, irep_hash> &dest);
461 template <
typename C>
469 [](
const symbol_exprt_to_car_mapt::value_type &s) { return s.first; });
517 bool allow_null_target,
533 bool include_stack_allocated)
const;
544 bool include_stack_allocated,
598 unordered_map<const conditional_target_exprt, const car_exprt, irep_hash>;
608 std::unordered_map<const symbol_exprt, const car_exprt, irep_hash>;
616 std::unordered_map<const exprt, const car_exprt, irep_hash>;
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Class that represents a normalized conditional address range, with:
const car_havoc_methodt havoc_method
Method to use to havod the target.
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.
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 car_havoc_methodt _havoc_method)
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.
Stores information about a goto function computed from its CFG.
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.
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
Represents an interval of source locations covered by the static local variable search.
bool contains(const source_locationt &source_location)
True iff the interval contains the given location.
void anywhere()
Grows the interval cover the maximum range [(size_t::min, size_t::min), (size_t::min,...
void update_min(size_t line, size_t col)
Updates the min_line and min_col in place using the given values iff they are smaller.
location_intervalt()
Initializes to the empty interval.
static bool is_lte(size_t line0, size_t col0, size_t line1, size_t col1)
True iff (line0, col0) <= (line1, col1) in lexicographic ordering.
std::size_t col_to_size_t(const source_locationt &source_location, std::size_t default_value)
If line or col is missing use default.
void update(const source_locationt &source_location)
Grows the interval to include the given (line, col) location.
std::size_t line_to_size_t(const source_locationt &source_location, std::size_t default_value)
If line is missing use default.
void update_max(size_t line, size_t col)
Updates the max_line and max_col in place using the given values iff they are larger.
A class that generates instrumentation for assigns clause checking.
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.
std::unordered_map< const symbol_exprt, const car_exprt, irep_hash > symbol_exprt_to_car_mapt
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
std::list< car_exprt > car_expr_listt
List of malloc'd 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...
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.
std::unordered_map< const exprt, const car_exprt, irep_hash > exprt_to_car_mapt
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,...
instrument_spec_assignst(const irep_idt &_function_id, const goto_functionst &_functions, cfg_infot &_cfg_info, symbol_table_baset &_st, message_handlert &_message_handler)
Class constructor.
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)
std::unordered_map< const conditional_target_exprt, const car_exprt, irep_hash > cond_target_exprt_to_car_mapt
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.
void get_static_locals(std::insert_iterator< C > inserter) const
Inserts the detected static local symbols into a target container.
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...
const irep_idt & get_column() const
const irep_idt & get_line() const
Expression to hold a symbol (variable)
The symbol table base class interface.
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
Deprecated expression utility functions.
void add_pragma_disable_pointer_checks(source_locationt &source_location)
Adds a pragma on a source location disable all pointer checks.
bool has_propagate_static_local_pragma(source_locationt &source_location)
True iff the pragma to mark assignments to static local variables that need to be propagated upwards ...
void add_pragma_disable_assigns_check(source_locationt &source_location)
Adds a pragma on a source_locationt to disable inclusion checking.
car_havoc_methodt
method to use to havoc a target
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...
const std::string & id2string(const irep_idt &d)
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.