#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/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, 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, 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	widen_assigns (assignst &assigns, const namespacet &ns)
	Widen expressions in `assigns` with the following strategy. More...

void	add_quantified_variable (symbol_table_baset &symbol_table, exprt &expression, const irep_idt &mode)
	This function recursively searches `expression` to find nested or non-nested quantified expressions. 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...

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

◆ add_quantified_variable()

void add_quantified_variable	(	symbol_table_baset &	symbol_table,
		exprt &	expression,
		const irep_idt &	mode
	)

This function recursively searches expression to find nested or non-nested quantified expressions.

When a quantified expression is found, a fresh quantified variable is added to the symbol table and expression is updated to use this fresh variable.

Definition at line 367 of file utils.cpp.

◆ 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 172 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 742 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 720 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 761 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 700 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 30 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 549 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 190 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 689 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 615 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 639 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 695 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 662 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 601 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 244 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 234 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 579 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 335 of file utils.cpp.

◆ is_loop_free()

bool is_loop_free	(	const goto_programt &	goto_program,
		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 268 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 571 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 563 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 326 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 530 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 511 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 441 of file utils.cpp.

◆ simplify_gotos()

void simplify_gotos	(	goto_programt &	goto_program,
		namespacet &	ns
	)

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

Definition at line 257 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 341 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 323 of file utils.cpp.

Functions

Variables

Function Documentation

◆ add_quantified_variable()

◆ all_dereferences_are_valid()

◆ annotate_assigns() [1/2]

◆ annotate_assigns() [2/2]

◆ annotate_decreases()

◆ annotate_invariants()

◆ append_safe_havoc_code_for_expr()

◆ generate_history_variables_initialization()

◆ generate_lexicographic_less_than_check()

◆ 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_suffix_unsigned()

◆ 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