#include "utils.h"
#include <util/c_types.h>
#include <util/fresh_symbol.h>
#include <util/graph.h>
#include <util/mathematical_expr.h>
#include <util/message.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/symbol.h>
#include <goto-programs/cfg.h>
#include <analyses/natural_loops.h>
#include <ansi-c/c_expr.h>
#include <langapi/language_util.h>

Include dependency graph for utils.cpp:

Functions
static void	append_safe_havoc_code_for_expr (const source_locationt location, const namespacet &ns, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl)

exprt	all_dereferences_are_valid (const exprt &expr, const namespacet &ns)
	Generate a validity check over all dereferences in an expression. More...

exprt	generate_lexicographic_less_than_check (const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
	Generate a lexicographic less-than comparison over ordered tuples. More...

void	insert_before_swap_and_advance (goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
	Insert a goto program before a target instruction iterator and advance the iterator. More...

void	insert_before_and_update_jumps (goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
	Insert a goto instruction before a target instruction iterator and update targets of all jumps that points to the iterator to jumping to the inserted instruction. More...

void	simplify_gotos (goto_programt &goto_program, const namespacet &ns)
	Turns goto instructions `IF cond GOTO label` where the condition statically simplifies to `false` into SKIP instructions. More...

bool	is_loop_free (const goto_programt &goto_program, const namespacet &ns, messaget &log)
	Returns true iff the given program is loop-free, i.e. More...

irep_idt	make_assigns_clause_replacement_tracking_comment (const exprt &target, const irep_idt &function_id, const namespacet &ns)
	Returns an irep_idt that essentially says that `target` was assigned by the contract of `function_id`. More...

bool	is_assigns_clause_replacement_tracking_comment (const irep_idt &comment)
	Returns true if the given comment matches the type of comments created by make_assigns_clause_replacement_tracking_comment. More...

void	infer_loop_assigns (const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
	Infer loop assigns using alias analysis result `local_may_alias`. More...

void	widen_assigns (assignst &assigns, const namespacet &ns)
	Widen expressions in `assigns` with the following strategy. More...

static void	replace_history_parameter_rec (symbol_table_baset &symbol_table, exprt &expr, std::unordered_map< exprt, symbol_exprt, irep_hash > &parameter2history, const source_locationt &location, const irep_idt &mode, goto_programt &history, const irep_idt &history_id)

replace_history_parametert	replace_history_old (symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
	This function recursively identifies the "old" expressions within `expr` and replaces them with corresponding history variables. More...

replace_history_parametert	replace_history_loop_entry (symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
	This function recursively identifies the "loop_entry" expressions within `expr` and replaces them with corresponding history variables. More...

void	generate_history_variables_initialization (symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
	This function generates all the instructions required to initialize history variables. More...

bool	is_transformed_loop_head (const goto_programt::const_targett &target)
	Return true if `target` is the head of some transformed loop. More...

bool	is_transformed_loop_end (const goto_programt::const_targett &target)
	Return true if `target` is the end of some transformed loop. More...

bool	is_assignment_to_instrumented_variable (const goto_programt::const_targett &target, std::string var_name)
	Return true if `target` is an assignment to an instrumented variable with name `var_name`. More...

unsigned	get_suffix_unsigned (const std::string &str, const std::string &prefix)
	Convert the suffix digits right after `prefix` of `str` into unsigned. More...

goto_programt::const_targett	get_loop_end_from_loop_head_and_content (const goto_programt::const_targett &loop_head, const loop_templatet< goto_programt::const_targett, goto_programt::target_less_than > &loop)

goto_programt::targett	get_loop_end_from_loop_head_and_content_mutable (const goto_programt::targett &loop_head, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &loop)
	Find the goto instruction of `loop` that jumps to `loop_head` More...

goto_programt::targett	get_loop_head_or_end (const unsigned int target_loop_number, goto_functiont &function, bool finding_head)
	Return loop head if `finding_head` is true, Otherwise return loop end. More...

goto_programt::targett	get_loop_end (const unsigned int target_loop_number, goto_functiont &function)
	Find and return the last instruction of the natural loop with `loop_number` in `function`. More...

goto_programt::targett	get_loop_head (const unsigned int target_loop_number, goto_functiont &function)
	Find and return the first instruction of the natural loop with `loop_number` in `function`. More...

static exprt	extract_loop_invariants (const goto_programt::const_targett &loop_end)
	Extract loop invariants from loop end without any checks. More...

static exprt	extract_loop_assigns (const goto_programt::const_targett &loop_end)

static exprt	extract_loop_decreases (const goto_programt::const_targett &loop_end)

exprt	get_loop_invariants (const goto_programt::const_targett &loop_end, const bool check_side_effect)
	Extract loop invariants from annotated loop end. More...

exprt	get_loop_assigns (const goto_programt::const_targett &loop_end)
	Extract loop assigns from annotated loop end. More...

exprt	get_loop_decreases (const goto_programt::const_targett &loop_end, const bool check_side_effect)
	Extract loop decreases from annotated loop end. More...

void	annotate_invariants (const invariant_mapt &invariant_map, goto_modelt &goto_model)
	Annotate the invariants in `invariant_map` to their corresponding loops. More...

void	annotate_assigns (const std::map< loop_idt, std::set< exprt >> &assigns_map, goto_modelt &goto_model)
	Annotate the assigns in `assigns_map` to their corresponding loops. More...

void	annotate_assigns (const std::map< loop_idt, exprt > &assigns_map, goto_modelt &goto_model)

void	annotate_decreases (const std::map< loop_idt, std::vector< exprt >> &decreases_map, goto_modelt &goto_model)
	Annotate the decreases in `decreases_map` to their corresponding loops. More...

Variables
static const char	ASSIGNS_CLAUSE_REPLACEMENT_TRACKING []
	Prefix for comments added to track assigns clause replacement. More...

Function Documentation

◆ all_dereferences_are_valid()

exprt all_dereferences_are_valid	(	const exprt &	expr,
		const namespacet &	ns
	)

Generate a validity check over all dereferences in an expression.

This function generates a formula:

r_ok_exprt(pexpr_1, sizeof(*pexpr_1)) && r_ok_exprt(pexpr_2, sizeof(*pexpr_1)) && ...

over all dereferenced pointer expressions *(pexpr_1), *(pexpr_2), ... found in the AST of expr.

Parameters

expr	The expression that contains dereferences to be validated.
ns	The namespace that defines all symbols appearing in `expr`.

Returns: A conjunctive expression that checks validity of all pointers that are dereferenced within expr.

Definition at line 175 of file utils.cpp.

◆ annotate_assigns() [1/2]

void annotate_assigns	(	const std::map< loop_idt, exprt > &	assigns_map,
		goto_modelt &	goto_model
	)

Definition at line 747 of file utils.cpp.

◆ annotate_assigns() [2/2]

void annotate_assigns	(	const std::map< loop_idt, std::set< exprt >> &	assigns_map,
		goto_modelt &	goto_model
	)

Annotate the assigns in assigns_map to their corresponding loops.

Corresponding loops are specified by keys of assigns_map

Definition at line 725 of file utils.cpp.

◆ annotate_decreases()

void annotate_decreases	(	const std::map< loop_idt, std::vector< exprt >> &	decreases_map,
		goto_modelt &	goto_model
	)

Annotate the decreases in decreases_map to their corresponding loops.

Corresponding loops are specified by keys of decreases_map

Definition at line 766 of file utils.cpp.

◆ annotate_invariants()

void annotate_invariants	(	const invariant_mapt &	invariant_map,
		goto_modelt &	goto_model
	)

Annotate the invariants in invariant_map to their corresponding loops.

Corresponding loops are specified by keys of invariant_map

Definition at line 705 of file utils.cpp.

◆ append_safe_havoc_code_for_expr()

static void append_safe_havoc_code_for_expr	(	const source_locationt	location,
		const namespacet &	ns,
		const exprt &	expr,
		goto_programt &	dest,
		const std::function< void()> &	havoc_code_impl
	)

static

Definition at line 31 of file utils.cpp.

◆ extract_loop_assigns()

static exprt extract_loop_assigns ( const goto_programt::const_targett & loop_end )

static

Definition at line 653 of file utils.cpp.

◆ extract_loop_decreases()

static exprt extract_loop_decreases ( const goto_programt::const_targett & loop_end )

static

Definition at line 660 of file utils.cpp.

◆ extract_loop_invariants()

static exprt extract_loop_invariants ( const goto_programt::const_targett & loop_end )

static

Extract loop invariants from loop end without any checks.

Definition at line 647 of file utils.cpp.

◆ generate_history_variables_initialization()

void generate_history_variables_initialization	(	symbol_table_baset &	symbol_table,
		exprt &	clause,
		const irep_idt &	mode,
		goto_programt &	program
	)

This function generates all the instructions required to initialize history variables.

Definition at line 494 of file utils.cpp.

◆ generate_lexicographic_less_than_check()

exprt generate_lexicographic_less_than_check	(	const std::vector< symbol_exprt > &	lhs,
		const std::vector< symbol_exprt > &	rhs
	)

Generate a lexicographic less-than comparison over ordered tuples.

This function creates an expression representing a lexicographic less-than comparison, lhs < rhs, between two ordered tuples of variables. This is used in instrumentation of decreases clauses.

Parameters

lhs	A vector of variables representing the LHS of the comparison.
rhs	A vector of variables representing the RHS of the comparison.

Returns: A lexicographic less-than comparison expression: LHS < RHS.

Definition at line 193 of file utils.cpp.

◆ get_loop_assigns()

exprt get_loop_assigns ( const goto_programt::const_targett & loop_end )

Extract loop assigns from annotated loop end.

Definition at line 683 of file utils.cpp.

◆ get_loop_decreases()

exprt get_loop_decreases	(	const goto_programt::const_targett &	loop_end,
		const bool	check_side_effect = `true`
	)

Extract loop decreases from annotated loop end.

Will check if the loop decreases is side-effect free if check_side_effect` is set.

Definition at line 688 of file utils.cpp.

◆ get_loop_end()

goto_programt::targett get_loop_end	(	const unsigned int	loop_number,
		goto_functiont &	function
	)

Find and return the last instruction of the natural loop with loop_number in function.

loop_end -> loop_head

Definition at line 634 of file utils.cpp.

◆ get_loop_end_from_loop_head_and_content()

goto_programt::const_targett get_loop_end_from_loop_head_and_content	(	const goto_programt::const_targett &	loop_head,
		const loop_templatet< goto_programt::const_targett, goto_programt::target_less_than > &	loop
	)

Definition at line 560 of file utils.cpp.

◆ get_loop_end_from_loop_head_and_content_mutable()

goto_programt::targett get_loop_end_from_loop_head_and_content_mutable	(	const goto_programt::targett &	loop_head,
		const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &	loop
	)

Find the goto instruction of loop that jumps to loop_head

Definition at line 584 of file utils.cpp.

◆ get_loop_head()

goto_programt::targett get_loop_head	(	const unsigned int	loop_number,
		goto_functiont &	function
	)

Find and return the first instruction of the natural loop with loop_number in function.

loop_end -> loop_head

Definition at line 640 of file utils.cpp.

◆ get_loop_head_or_end()

goto_programt::targett get_loop_head_or_end	(	const unsigned int	target_loop_number,
		goto_functiont &	function,
		bool	finding_head
	)

Return loop head if finding_head is true, Otherwise return loop end.

Definition at line 607 of file utils.cpp.

◆ get_loop_invariants()

exprt get_loop_invariants	(	const goto_programt::const_targett &	loop_end,
		const bool	check_side_effect = `true`
	)

Extract loop invariants from annotated loop end.

Will check if the loop invariant is side-effect free if check_side_effect` is set.

Definition at line 666 of file utils.cpp.

◆ get_suffix_unsigned()

unsigned get_suffix_unsigned	(	const std::string &	str,
		const std::string &	prefix
	)

Convert the suffix digits right after prefix of str into unsigned.

Definition at line 546 of file utils.cpp.

◆ infer_loop_assigns()

void infer_loop_assigns	(	const local_may_aliast &	local_may_alias,
		const loopt &	loop,
		assignst &	assigns
	)

Infer loop assigns using alias analysis result local_may_alias.

Definition at line 344 of file utils.cpp.

◆ insert_before_and_update_jumps()

void insert_before_and_update_jumps	(	goto_programt &	destination,
		goto_programt::targett &	target,
		const goto_programt::instructiont &	i
	)

Insert a goto instruction before a target instruction iterator and update targets of all jumps that points to the iterator to jumping to the inserted instruction.

This method is intended to keep external instruction::targett stable, i.e. they will still point to the same instruction after inserting the new one

This function inserts a instruction i into a destination program destination immediately before a specified instruction iterator target. After insertion, update all jumps that pointing to target to jumping to i instead.

Different from insert_before_swap_and_advance, this function doesn't invalidate the iterator target after insertion. That is, target and all other instruction iterators same as target will still point to the same instruction after insertion.

Parameters

destination	The destination program for inserting the `i`.
target	The instruction iterator at which to insert the `i`.
i	The goto instruction to be inserted into the `destination`.

Definition at line 247 of file utils.cpp.

◆ insert_before_swap_and_advance()

void insert_before_swap_and_advance	(	goto_programt &	destination,
		goto_programt::targett &	target,
		goto_programt &	payload
	)

Insert a goto program before a target instruction iterator and advance the iterator.

This function inserts all instruction from a goto program payload into a destination program destination immediately before a specified instruction iterator target. After insertion, target is advanced by the size of the payload, and payload is destroyed.

Parameters

destination	The destination program for inserting the `payload`.
target	The instruction iterator at which to insert the `payload`.
payload	The goto program to be inserted into the `destination`.

Definition at line 237 of file utils.cpp.

◆ is_assignment_to_instrumented_variable()

bool is_assignment_to_instrumented_variable	(	const goto_programt::const_targett &	target,
		std::string	var_name
	)

Return true if target is an assignment to an instrumented variable with name var_name.

Definition at line 524 of file utils.cpp.

◆ is_assigns_clause_replacement_tracking_comment()

bool is_assigns_clause_replacement_tracking_comment ( const irep_idt & comment )

Returns true if the given comment matches the type of comments created by make_assigns_clause_replacement_tracking_comment.

Definition at line 338 of file utils.cpp.

◆ is_loop_free()

bool is_loop_free	(	const goto_programt &	goto_program,
		const namespacet &	ns,
		messaget &	log
	)

Returns true iff the given program is loop-free, i.e.

if each SCC of its CFG contains a single element.

Definition at line 271 of file utils.cpp.

◆ is_transformed_loop_end()

bool is_transformed_loop_end ( const goto_programt::const_targett & target )

Return true if target is the end of some transformed loop.

Definition at line 516 of file utils.cpp.

◆ is_transformed_loop_head()

bool is_transformed_loop_head ( const goto_programt::const_targett & target )

Return true if target is the head of some transformed loop.

Definition at line 508 of file utils.cpp.

◆ make_assigns_clause_replacement_tracking_comment()

irep_idt make_assigns_clause_replacement_tracking_comment	(	const exprt &	target,
		const irep_idt &	function_id,
		const namespacet &	ns
	)

Returns an irep_idt that essentially says that target was assigned by the contract of function_id.

Definition at line 329 of file utils.cpp.

◆ replace_history_loop_entry()

replace_history_parametert replace_history_loop_entry	(	symbol_table_baset &	symbol_table,
		const exprt &	expr,
		const source_locationt &	location,
		const irep_idt &	mode
	)

This function recursively identifies the "loop_entry" expressions within expr and replaces them with corresponding history variables.

Definition at line 475 of file utils.cpp.

◆ replace_history_old()

replace_history_parametert replace_history_old	(	symbol_table_baset &	symbol_table,
		const exprt &	expr,
		const source_locationt &	location,
		const irep_idt &	mode
	)

This function recursively identifies the "old" expressions within expr and replaces them with corresponding history variables.

Definition at line 456 of file utils.cpp.

◆ replace_history_parameter_rec()

static void replace_history_parameter_rec	(	symbol_table_baset &	symbol_table,
		exprt &	expr,
		std::unordered_map< exprt, symbol_exprt, irep_hash > &	parameter2history,
		const source_locationt &	location,
		const irep_idt &	mode,
		goto_programt &	history,
		const irep_idt &	history_id
	)

static

Definition at line 386 of file utils.cpp.

◆ simplify_gotos()

void simplify_gotos	(	goto_programt &	goto_program,
		const namespacet &	ns
	)

Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SKIP instructions.

Definition at line 260 of file utils.cpp.

◆ widen_assigns()

void widen_assigns	(	assignst &	assigns,
		const namespacet &	ns
	)

Widen expressions in assigns with the following strategy.

If an expression is an array index or object dereference expression, with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant i, then replace it by the entire underlying object. Otherwise, e.g. for a[i] or *(b+i) when i is a known constant, keep the expression in the result.

Definition at line 360 of file utils.cpp.

Variable Documentation

◆ ASSIGNS_CLAUSE_REPLACEMENT_TRACKING

const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[]

static

Initial value:

=

" (assigned by the contract of "

Prefix for comments added to track assigns clause replacement.

Definition at line 326 of file utils.cpp.

Functions

Variables

Function Documentation

◆ all_dereferences_are_valid()

◆ annotate_assigns() [1/2]

◆ annotate_assigns() [2/2]

◆ annotate_decreases()

◆ annotate_invariants()

◆ append_safe_havoc_code_for_expr()

◆ extract_loop_assigns()

◆ extract_loop_decreases()

◆ extract_loop_invariants()

◆ generate_history_variables_initialization()

◆ generate_lexicographic_less_than_check()

◆ get_loop_assigns()

◆ get_loop_decreases()

◆ get_loop_end()

◆ get_loop_end_from_loop_head_and_content()

◆ get_loop_end_from_loop_head_and_content_mutable()

◆ get_loop_head()

◆ get_loop_head_or_end()

◆ get_loop_invariants()

◆ get_suffix_unsigned()

◆ infer_loop_assigns()

◆ insert_before_and_update_jumps()

◆ insert_before_swap_and_advance()

◆ is_assignment_to_instrumented_variable()

◆ is_assigns_clause_replacement_tracking_comment()

◆ is_loop_free()

◆ is_transformed_loop_end()

◆ is_transformed_loop_head()

◆ make_assigns_clause_replacement_tracking_comment()

◆ replace_history_loop_entry()

◆ replace_history_old()

◆ replace_history_parameter_rec()

◆ simplify_gotos()

◆ widen_assigns()

Variable Documentation

◆ ASSIGNS_CLAUSE_REPLACEMENT_TRACKING