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_locationt &	source_location

Additional Inherited Members
Protected Types inherited from instrument_spec_assignst
typedef std::unordered_map< irep_idt, location_intervalt >	covered_locationst
	Map type from function identifiers to covered locations. More...

typedef std::unordered_set< symbol_exprt, irep_hash >	propagated_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_exprt &	create_car_from_spec_assigns (const exprt &condition, const exprt &target)

const car_exprt &	create_car_from_stack_alloc (const symbol_exprt &target)

const car_exprt &	create_car_from_heap_alloc (const exprt &target)

const car_exprt &	create_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_idt &	function_id
	Name of the instrumented function. More...

const goto_functionst &	functions
	Other functions of the model. More...

cfg_infot &	cfg_info
	CFG information for simplification. More...

symbol_table_baset &	st
	Program symbol table. More...

const namespacet	ns
	Program namespace. More...

messaget	log
	Logger. More...

const irep_idt &	mode
	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);
}

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_id	Name of the replaced function
_targets	Assigns clause targets of the replaced function
_functions	Other functions forming the GOTO model
_cfg_info	CFG-based information on function symbols (not used)
_source_location	Source location of the replaced function call (added to all generated instructions)
_st	Symbol table of the model (new symbols will be added)
_message_handler	handler 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

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

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:

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/havoc_assigns_clause_targets.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ havoc_assigns_clause_targetst()

Member Function Documentation

◆ get_instructions()

◆ havoc_if_valid()

◆ havoc_static_local()

Member Data Documentation

◆ source_location

◆ targets