dfcc_infer_loop_assigns.cpp File Reference

#include "dfcc_infer_loop_assigns.h"
#include <util/expr.h>
#include <util/find_symbols.h>
#include <util/message.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <goto-programs/goto_inline.h>
#include <analyses/goto_rw.h>
#include <goto-instrument/contracts/utils.h>
#include <goto-instrument/havoc_utils.h>
#include "dfcc_loop_nesting_graph.h"
#include "dfcc_root_object.h"

Include dependency graph for dfcc_infer_loop_assigns.cpp:

Go to the source code of this file.

Functions
static exprt	make_object_whole_call_expr (const exprt &expr, const namespacet &ns)
	Builds a call expression object_whole(expr) More...
static bool	depends_on (const exprt &expr, std::unordered_set< irep_idt > identifiers)
	Returns true iff expr contains at least one identifier found in identifiers. More...
std::unordered_set< irep_idt >	gen_loop_locals_set (const irep_idt &function_id, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop_node, message_handlert &message_handler, const namespacet &ns)
	Collect identifiers that are local to this loop. More...
static std::unordered_set< irep_idt >	find_symbol_identifiers (const goto_programt &src)
	Find all identifiers in src. More...
static assignst	dfcc_infer_loop_assigns_for_loop (const local_may_aliast &local_may_alias, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop, const std::unordered_set< irep_idt > &candidate_targets, message_handlert &message_handler, const namespacet &ns)
	Infer loop assigns in the given loop. More...
static void	remove_dead_object_assignment (goto_functiont &goto_function)
	Remove assignments to __CPROVER_dead_object to avoid aliasing all targets that are assigned to __CPROVER_dead_object. More...
void	dfcc_infer_loop_assigns_for_function (std::map< std::size_t, assignst > &inferred_loop_assigns_map, goto_functionst &goto_functions, const goto_functiont &goto_function, message_handlert &message_handler, const namespacet &ns)
	Infer assigns clause targets for loops in goto_function from their instructions and an alias analysis at the function level (with inlining), and store the result in inferred_loop_assigns_map, a map from loop numbers to the set of inferred assigns targets. More...

Function Documentation

depends_on()

static bool depends_on ( const exprt &  expr, std::unordered_set< irep_idt >  identifiers  )

static

Returns true iff expr contains at least one identifier found in identifiers.

Definition at line 42 of file dfcc_infer_loop_assigns.cpp.

dfcc_infer_loop_assigns_for_function()

void dfcc_infer_loop_assigns_for_function	(	std::map< std::size_t, assignst > &	inferred_loop_assigns_map,
		goto_functionst &	goto_functions,
		const goto_functiont &	goto_function,
		message_handlert &	message_handler,
		const namespacet &	ns
	)

Infer assigns clause targets for loops in goto_function from their instructions and an alias analysis at the function level (with inlining), and store the result in inferred_loop_assigns_map, a map from loop numbers to the set of inferred assigns targets.

Definition at line 302 of file dfcc_infer_loop_assigns.cpp.

dfcc_infer_loop_assigns_for_loop()

static assignst dfcc_infer_loop_assigns_for_loop ( const local_may_aliast &  local_may_alias, goto_functiont &  goto_function, const dfcc_loop_nesting_graph_nodet &  loop, const std::unordered_set< irep_idt > &  candidate_targets, message_handlert &  message_handler, const namespacet &  ns  )

static

Infer loop assigns in the given loop.

Loop assigns should depend on some identifiers in candidate_targets. function_assigns_map contains the function contracts used to infer loop assigns of function_call instructions.

Definition at line 216 of file dfcc_infer_loop_assigns.cpp.

find_symbol_identifiers()

static std::unordered_set<irep_idt> find_symbol_identifiers ( const goto_programt &  src )

static

Find all identifiers in src.

Definition at line 162 of file dfcc_infer_loop_assigns.cpp.

gen_loop_locals_set()

std::unordered_set<irep_idt> gen_loop_locals_set	(	const irep_idt &	function_id,
		goto_functiont &	goto_function,
		const dfcc_loop_nesting_graph_nodet &	loop_node,
		message_handlert &	message_handler,
		const namespacet &	ns
	)

Collect identifiers that are local to this loop.

Collect identifiers that are local to loop.

A identifier is or is equivalent to a loop local if

1. it is declared inside the loop, or
2. there is no write or read of it outside the loop.
3. it is not used in loop contracts.

Definition at line 58 of file dfcc_infer_loop_assigns.cpp.

make_object_whole_call_expr()

static exprt make_object_whole_call_expr ( const exprt &  expr, const namespacet &  ns  )

static

Builds a call expression object_whole(expr)

Definition at line 27 of file dfcc_infer_loop_assigns.cpp.

remove_dead_object_assignment()

static void remove_dead_object_assignment ( goto_functiont &  goto_function )

static

Remove assignments to __CPROVER_dead_object to avoid aliasing all targets that are assigned to __CPROVER_dead_object.

Definition at line 284 of file dfcc_infer_loop_assigns.cpp.