cprover
Loading...
Searching...
No Matches
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, const source_locationt &_source_location, symbol_tablet &_st, message_handlert &_message_handler)
 
void get_instructions (goto_programt &dest)
 Generates the assigns clause replacement instructions in dest.
 
- Public Member Functions inherited from instrument_spec_assignst
 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 dest.
 
void track_stack_allocated (const symbol_exprt &symbol_expr, goto_programt &dest)
 Track a stack-allocated object and generate snaphsot instructions in dest.
 
bool stack_allocated_is_tracked (const symbol_exprt &symbol_expr) const
 Returns true if the expression is tracked.
 
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.
 
void track_heap_allocated (const exprt &expr, goto_programt &dest)
 Track a whole heap-alloc object and generate snaphsot instructions in dest.
 
void track_static_locals (goto_programt &dest)
 Search the call graph reachable from the instrumented function to identify local static variables used directly or indirectly, add them to the stack-allocated tracked locations, and generate corresponding snapshot instructions in dest.
 
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.
 
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.
 

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.
 

Private Attributes

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

Additional Inherited Members

- Protected Types inherited from instrument_spec_assignst
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 >
 
- Protected Member Functions inherited from instrument_spec_assignst
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.
 
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.
 
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 create_snapshot (const car_exprt &car, goto_programt &dest) const
 Returns snapshot instructions for a car_exprt.
 
exprt target_validity_expr (const car_exprt &car, bool allow_null_target) const
 Returns the target validity expression for a car_exprt.
 
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_single (const car_exprt &lhs, const car_exprt &candidate_car) const
 Returns inclusion check expression for a single candidate location.
 
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 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.
 
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.
 
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.
 
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)
 
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.
 
- Protected Attributes inherited from instrument_spec_assignst
const irep_idtfunction_id
 Name of the instrumented function.
 
const goto_functionstfunctions
 Other functions of the model.
 
symbol_tabletst
 Program symbol table.
 
const namespacet ns
 Program namespace.
 
messaget log
 Logger.
 
cond_target_exprt_to_car_mapt from_spec_assigns
 Map to from conditional target expressions of assigns clauses to corresponding conditional address ranges.
 
symbol_exprt_to_car_mapt from_stack_alloc
 Map to from DECL symbols to corresponding conditional address ranges.
 
exprt_to_car_mapt from_heap_alloc
 Map to from malloc'd symbols to corresponding conditional address ranges.
 

Detailed Description

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

Parameters
replaced_function_idName of the replaced function
goto_functionsOther functions forming the GOTO model
targetsAssigns clause targets for the replaced function
source_locationSource location of the replaced function call (added to all generated instructions)
modeLanguage mode to use for newly generated symbols
nsNamespace of the model
stSymbol table of the model (new symbols will be added)
message_handlerhandler used to log translation warnings/errors

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 *)

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 54 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,
const source_locationt _source_location,
symbol_tablet _st,
message_handlert _message_handler 
)
inline

Definition at line 57 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 31 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
@ SKIP
@ OTHER
@ GOTO

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

Where target_type is the type of the target expression.

Definition at line 59 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 105 of file havoc_assigns_clause_targets.h.

◆ targets

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

Definition at line 104 of file havoc_assigns_clause_targets.h.


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