#include "utils.h"
#include <goto-programs/cfg.h>
#include <util/fresh_symbol.h>
#include <util/graph.h>
#include <util/message.h>
#include <util/pointer_expr.h>
#include <util/pointer_predicates.h>
#include <util/simplify_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...

const symbolt &	new_tmp_symbol (const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix, bool is_auxiliary)
	Adds a fresh and uniquely named symbol to the symbol table. 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...

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:

good_pointer_def(pexpr_1, ns) && good_pointer_def(pexpr_2, n2) && ...

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 80 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 24 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 94 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 138 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 240 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 173 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 231 of file utils.cpp.

◆ new_tmp_symbol()

const symbolt& new_tmp_symbol	(	const typet &	type,
		const source_locationt &	location,
		const irep_idt &	mode,
		symbol_table_baset &	symtab,
		std::string	suffix = `"tmp_cc"`,
		bool	is_auxiliary = `true`
	)

Adds a fresh and uniquely named symbol to the symbol table.

Parameters

type	The type of the new symbol.
location	The source location for the new symbol.
mode	The mode for the new symbol, e.g. ID_C, ID_java.
symtab	The symbol table to which the new symbol is to be added.
suffix	Suffix to use to generate the unique name
is_auxiliary	Do not print symbol in traces if true (default = true)

Returns: The new symbolt object.

Definition at line 148 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 162 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 228 of file utils.cpp.

Functions

Variables

Function Documentation

◆ all_dereferences_are_valid()

◆ append_safe_havoc_code_for_expr()

◆ generate_lexicographic_less_than_check()

◆ insert_before_swap_and_advance()

◆ is_assigns_clause_replacement_tracking_comment()

◆ is_loop_free()

◆ make_assigns_clause_replacement_tracking_comment()

◆ new_tmp_symbol()

◆ simplify_gotos()

Variable Documentation

◆ ASSIGNS_CLAUSE_REPLACEMENT_TRACKING