CBMC
havoc_assigns_clause_targetst Class Reference

Class to generate havocking instructions for target expressions of a function contract's assign clause (replacement). More...

#include <havoc_assigns_clause_targets.h>

+ Inheritance diagram for havoc_assigns_clause_targetst:
+ Collaboration diagram for havoc_assigns_clause_targetst:

Public Member Functions

 havoc_assigns_clause_targetst (const irep_idt &_function_id, const std::vector< exprt > &_targets, const goto_functionst &_functions, cfg_infot &_cfg_info, const source_locationt &_source_location, symbol_table_baset &_st, message_handlert &_message_handler)
 
void get_instructions (goto_programt &dest)
 Generates the assigns clause replacement instructions in dest. More...
 
- Public Member Functions inherited from instrument_spec_assignst
 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. More...
 
void track_spec_target (const exprt &expr, goto_programt &dest)
 Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in dest. More...
 
void track_stack_allocated (const symbol_exprt &symbol_expr, goto_programt &dest)
 Track a stack-allocated object and generate snaphsot instructions in dest. More...
 
bool stack_allocated_is_tracked (const symbol_exprt &symbol_expr) const
 Returns true if the expression is tracked. More...
 
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. More...
 
void track_heap_allocated (const exprt &expr, goto_programt &dest)
 Track a whole heap-alloc object and generate snaphsot instructions in dest. More...
 
void track_static_locals (goto_programt &dest)
 Searches the goto instructions reachable from the start to the end of the instrumented function's instruction to identify local static variables, declared directly in the function or indirectly in the functions it calls, add them to the stack-allocated set of tracked locations, and generates corresponding snapshot instructions in dest. More...
 
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 local static variables, declared directly in the function or indirectly in the functions it calls, add them to the stack-allocated set of tracked locations, and generates corresponding snapshot instructions in dest. More...
 
void check_inclusion_assignment (const exprt &lhs, goto_programt &dest) const
 Generates inclusion check instructions for an assignment, havoc or havoc_object instruction. More...
 
void check_inclusion_heap_allocated_and_invalidate_aliases (const exprt &expr, goto_programt &dest)
 Generates inclusion check instructions for an argument passed to free. More...
 
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. More...
 
template<typename C >
void get_static_locals (std::insert_iterator< C > inserter) const
 Inserts the detected static local symbols into a target container. More...
 

Private Member Functions

void havoc_if_valid (car_exprt car, goto_programt &dest)
 Generates instructions to conditionally havoc the given conditional address range expression car, adding results to dest. More...
 
void havoc_static_local (car_exprt car, goto_programt &dest)
 Havoc a static local expression. More...
 

Private Attributes

const std::vector< exprt > & targets
 
const source_locationtsource_location
 

Additional Inherited Members

- Protected Types inherited from instrument_spec_assignst
typedef std::unordered_map< irep_idt, location_intervaltcovered_locationst
 Map type from function identifiers to covered locations. More...
 
typedef std::unordered_set< symbol_exprt, irep_hashpropagated_static_localst
 
using cond_target_exprt_to_car_mapt = std::unordered_map< const conditional_target_exprt, const car_exprt, irep_hash >
 
using symbol_exprt_to_car_mapt = std::unordered_map< const symbol_exprt, const car_exprt, irep_hash >
 
using exprt_to_car_mapt = std::unordered_map< const exprt, const car_exprt, irep_hash >
 
using car_expr_listt = std::list< car_exprt >
 List of malloc'd conditional address ranges. More...
 
- Protected Member Functions inherited from instrument_spec_assignst
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 calls only once. More...
 
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 covered_locations and writes them into dest. More...
 
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 target group from an assigns clause. More...
 
void track_plain_spec_target (const exprt &expr, goto_programt &dest)
 Track and generate snaphsot instructions and target validity checking assertions for a conditional target group from an assigns clause. More...
 
void create_snapshot (const car_exprt &car, goto_programt &dest) const
 Returns snapshot instructions for a car_exprt. More...
 
exprt target_validity_expr (const car_exprt &car, bool allow_null_target) const
 Returns the target validity expression for a car_exprt. More...
 
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. More...
 
exprt inclusion_check_single (const car_exprt &lhs, const car_exprt &candidate_car) const
 Returns inclusion check expression for a single candidate location. More...
 
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. More...
 
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. More...
 
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 same object as the freed car. More...
 
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, assuming the inclusion check passes, ie. More...
 
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. More...
 
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. More...
 
bool must_track_decl_or_dead (const irep_idt &ident) const
 Returns true iff a function-local symbol must be tracked. More...
 
bool must_check_assign (const goto_programt::const_targett &target)
 Returns true iff an ASSIGN lhs := rhs instruction must be instrumented. More...
 
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 LHS of the assignment is included in the set of currently tracked CARs. More...
 
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, to ensure that all memory locations written to by the called function are included in the set of currently tracked CARs. More...
 
const car_exprtcreate_car_from_spec_assigns (const exprt &condition, const exprt &target)
 
const car_exprtcreate_car_from_stack_alloc (const symbol_exprt &target)
 
const car_exprtcreate_car_from_heap_alloc (const exprt &target)
 
const car_exprtcreate_car_from_static_local (const symbol_exprt &target)
 
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. More...
 
- Protected Attributes inherited from instrument_spec_assignst
const irep_idtfunction_id
 Name of the instrumented function. More...
 
const goto_functionstfunctions
 Other functions of the model. More...
 
cfg_infotcfg_info
 CFG information for simplification. More...
 
symbol_table_basetst
 Program symbol table. More...
 
const namespacet ns
 Program namespace. More...
 
messaget log
 Logger. More...
 
const irep_idtmode
 Language mode. More...
 
cond_target_exprt_to_car_mapt from_spec_assigns
 Map from conditional target expressions of assigns clauses to corresponding conditional address ranges. More...
 
symbol_exprt_to_car_mapt from_stack_alloc
 Map from DECL symbols to corresponding conditional address ranges. More...
 
car_expr_listt from_heap_alloc
 
symbol_exprt_to_car_mapt from_static_local
 Map to from detected or propagated static local symbols to corresponding conditional address ranges. More...
 

Detailed Description

Class to generate havocking instructions for target expressions of a function contract's assign clause (replacement).

Assigns clause targets can be interdependent as shown in this example:

typedef struct vect { int *arr; int size; } vect;
void resize(vect *v)
__CPROVER_assigns(v->arr, v->size, __CPROVER_POINTER_OBJECT(v->arr))
{
free(v->arr);
v->size += 10 * sizeof(int);
v->arr = malloc(v->size);
}
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *)
void * malloc(__CPROVER_size_t malloc_size)
Definition: stdlib.c:212
void free(void *ptr)
Definition: stdlib.c:317

To havoc these dependent targets simultaneously, we first take snapshots of their addresses, and havoc them in a second time. Snapshotting and havocking are both guarded by the validity of the target.

Definition at line 42 of file havoc_assigns_clause_targets.h.

Constructor & Destructor Documentation

◆ havoc_assigns_clause_targetst()

havoc_assigns_clause_targetst::havoc_assigns_clause_targetst ( const irep_idt _function_id,
const std::vector< exprt > &  _targets,
const goto_functionst _functions,
cfg_infot _cfg_info,
const source_locationt _source_location,
symbol_table_baset _st,
message_handlert _message_handler 
)
inline
Parameters
_function_idName of the replaced function
_targetsAssigns clause targets of the replaced function
_functionsOther functions forming the GOTO model
_cfg_infoCFG-based information on function symbols (not used)
_source_locationSource location of the replaced function call (added to all generated instructions)
_stSymbol table of the model (new symbols will be added)
_message_handlerhandler used to log translation warnings/errors

Definition at line 54 of file havoc_assigns_clause_targets.h.

Member Function Documentation

◆ get_instructions()

void havoc_assigns_clause_targetst::get_instructions ( goto_programt dest)

Generates the assigns clause replacement instructions in dest.

Definition at line 22 of file havoc_assigns_clause_targets.cpp.

◆ havoc_if_valid()

void havoc_assigns_clause_targetst::havoc_if_valid ( car_exprt  car,
goto_programt dest 
)
private

Generates instructions to conditionally havoc the given conditional address range expression car, adding results to dest.

Adds a special comment on the havoc instructions in order to trace back the origin of the havoc expressions to the function being replaced.

Generates these instructions for a __CPROVER_POINTER_OBJECT(...) target:

IF !__car_writable GOTO skip_target
OTHER havoc_object(_car_lb)
skip_target: SKIP
DEAD __car_writable
DEAD __car_lb
DEAD __car_ub
@ DEAD
Definition: goto_program.h:48
@ SKIP
Definition: goto_program.h:38
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34

Generates these instructions for an object slice target:

IF !__car_writable GOTO skip_target
__CPROVER_havoc_slize(__car_lb, car.target_size)
skip_target: SKIP
DEAD __car_writable
DEAD __car_lb
DEAD __car_ub

And generate these instructions otherwise:

IF !__car_writable GOTO skip_target
ASSIGN *((target_type *) _car_lb) = nondet(target_type);
skip_target: SKIP
DEAD __car_writable
DEAD __car_lb
DEAD __car_ub
@ ASSIGN
Definition: goto_program.h:46

Where target_type is the type of the target expression.

Definition at line 55 of file havoc_assigns_clause_targets.cpp.

◆ havoc_static_local()

void havoc_assigns_clause_targetst::havoc_static_local ( car_exprt  car,
goto_programt dest 
)
private

Havoc a static local expression.

Definition at line 125 of file havoc_assigns_clause_targets.cpp.

Member Data Documentation

◆ source_location

const source_locationt& havoc_assigns_clause_targetst::source_location
private

Definition at line 121 of file havoc_assigns_clause_targets.h.

◆ targets

const std::vector<exprt>& havoc_assigns_clause_targetst::targets
private

Definition at line 120 of file havoc_assigns_clause_targets.h.


The documentation for this class was generated from the following files: