Generates string constraints to link results from string functions with their arguments. More...

#include <solvers/refinement/string_constraint_generator.h>
#include <iterator>
#include <limits>
#include <solvers/refinement/string_refinement_invariant.h>
#include <util/arith_tools.h>
#include <util/pointer_predicates.h>
#include <util/ssa_expr.h>
#include <util/string_constant.h>
#include <util/deprecate.h>

Include dependency graph for string_constraint_generator_main.cpp:

Go to the source code of this file.

Functions
exprt	sum_overflows (const plus_exprt &sum)

array_string_exprt	get_string_expr (array_poolt &pool, const exprt &expr)
	casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbol. More...

void	merge (string_constraintst &result, string_constraintst other)
	Merge two sets of constraints by appending to the first one. More...

string_constraintst	add_constraint_on_characters (symbol_generatort &fresh_symbol, const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set)
	Add constraint on characters of a string. More...

std::pair< exprt, string_constraintst >	add_axioms_for_constrain_characters (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
	Add axioms to ensure all characters of a string belong to a given set. More...

const array_string_exprt &	char_array_of_pointer (array_poolt &pool, const exprt &pointer, const exprt &length)
	Adds creates a new array if it does not already exists. More...

array_string_exprt	of_argument (array_poolt &array_pool, const exprt &arg)
	Converts a struct containing a length and pointer to an array. More...

signedbv_typet	get_return_code_type ()

static irep_idt	get_function_name (const function_application_exprt &expr)

std::pair< exprt, string_constraintst >	add_axioms_for_copy (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
	add axioms to say that the returned string expression is equal to the argument of the function application More...

std::pair< exprt, string_constraintst >	add_axioms_for_length (const function_application_exprt &f, array_poolt &array_pool)
	Length of a string. More...

exprt	is_positive (const exprt &x)

std::pair< exprt, string_constraintst >	add_axioms_for_char_literal (const function_application_exprt &f)
	add axioms stating that the returned value is equal to the argument More...

std::pair< exprt, string_constraintst >	add_axioms_for_char_at (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
	Character at a given position. More...

exprt	minimum (const exprt &a, const exprt &b)

exprt	maximum (const exprt &a, const exprt &b)

exprt	zero_if_negative (const exprt &expr)
	Returns a non-negative version of the argument. More...

std::pair< exprt, string_constraintst >	combine_results (std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
	Combine the results of two `add_axioms` function by taking the maximum of the return codes and merging the constraints. More...

Detailed Description

Generates string constraints to link results from string functions with their arguments.

This is inspired by the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh, which gives examples of constraints for several functions.

Definition in file string_constraint_generator_main.cpp.

Function Documentation

◆ add_axioms_for_char_at()

std::pair<exprt, string_constraintst> add_axioms_for_char_at	(	symbol_generatort &	fresh_symbol,
		const function_application_exprt &	f,
		array_poolt &	array_pool
	)

Character at a given position.

Add axioms stating that the character of the string at position given by second argument is equal to the returned value. This axiom is \( char = str[i] \).

Parameters

fresh_symbol	generator of fresh symbols
f	function application with arguments string `str` and integer `i`
array_pool	pool of arrays representing strings

Returns: character expression char

Definition at line 566 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_char_literal()

std::pair<exprt, string_constraintst> add_axioms_for_char_literal ( const function_application_exprt & f )

add axioms stating that the returned value is equal to the argument

Parameters

f	function application with one character argument

Returns: a new character expression

Definition at line 532 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_constrain_characters()

std::pair<exprt, string_constraintst> add_axioms_for_constrain_characters	(	symbol_generatort &	fresh_symbol,
		const function_application_exprt &	f,
		array_poolt &	array_pool
	)

Add axioms to ensure all characters of a string belong to a given set.

The axiom is: \(\forall i \in [start, end).\ s[i] \in char_set \), where char_set is given by the string char_set_string composed of three characters low_char, - and high_char. Character c belongs to char_set if \(low_char \le c \le high_char\).

Parameters

fresh_symbol	generator of fresh symbols
f	a function application with arguments: integer `\|s\|`, character pointer `&s[0]`, string `char_set_string`, optional integers `start` and `end`
array_pool	pool of arrays representing strings

Returns: integer expression whose value is zero

Definition at line 290 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_copy()

std::pair<exprt, string_constraintst> add_axioms_for_copy	(	symbol_generatort &	fresh_symbol,
		const function_application_exprt &	f,
		array_poolt &	array_pool
	)

add axioms to say that the returned string expression is equal to the argument of the function application

Deprecated:: should use substring instead

Parameters

fresh_symbol	generator of fresh symbols
f	function application with one argument, which is a string, or three arguments: string, integer offset and count
array_pool	pool of arrays representing strings

Returns: a new string expression

Definition at line 490 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_length()

std::pair<exprt, string_constraintst> add_axioms_for_length	(	const function_application_exprt &	f,
		array_poolt &	array_pool
	)

Length of a string.

Returns the length of the string argument of the given function application

Parameters

f	function application with argument string `str`
array_pool	pool of arrays representing strings

Returns: expression |str|

Definition at line 513 of file string_constraint_generator_main.cpp.

◆ add_constraint_on_characters()

string_constraintst add_constraint_on_characters	(	symbol_generatort &	fresh_symbol,
		const array_string_exprt &	s,
		const exprt &	start,
		const exprt &	end,
		const std::string &	char_set
	)

Add constraint on characters of a string.

This constraint is \( \forall i \in [start, end), low\_char \le s[i] \le high\_char \)

Parameters

fresh_symbol	generator of fresh symbols
s	a string expression
start	index of the first character to constrain
end	index at which we stop adding constraints
char_set	a string of the form "<low_char>-<high_char>" where `<low_char>` and `<high_char>` are two characters, which represents the set of characters that are between `low_char` and `high_char`.

Returns: a string expression that is linked to the argument through axioms that are added to the list

Definition at line 254 of file string_constraint_generator_main.cpp.

◆ char_array_of_pointer()

const array_string_exprt& char_array_of_pointer	(	array_poolt &	pool,
		const exprt &	pointer,
		const exprt &	length
	)

Adds creates a new array if it does not already exists.

Definition at line 325 of file string_constraint_generator_main.cpp.

◆ combine_results()

std::pair<exprt, string_constraintst> combine_results	(	std::pair< exprt, string_constraintst >	result1,
		std::pair< exprt, string_constraintst >	result2
	)

Combine the results of two add_axioms function by taking the maximum of the return codes and merging the constraints.

Definition at line 598 of file string_constraint_generator_main.cpp.

◆ get_function_name()

static irep_idt get_function_name ( const function_application_exprt & expr )

static

Definition at line 344 of file string_constraint_generator_main.cpp.

◆ get_return_code_type()

signedbv_typet get_return_code_type ( )

Definition at line 339 of file string_constraint_generator_main.cpp.

◆ get_string_expr()

array_string_exprt get_string_expr	(	array_poolt &	pool,
		const exprt &	expr
	)

casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbol.

Parameters

pool	pool of arrays representing strings
expr	an expression of refined string type

Returns: a string expression

Definition at line 210 of file string_constraint_generator_main.cpp.

◆ is_positive()

exprt is_positive ( const exprt & x )

Parameters

x	an expression

Returns: a Boolean expression true exactly when x is positive

Definition at line 524 of file string_constraint_generator_main.cpp.

◆ maximum()

exprt maximum	(	const exprt &	a,
		const exprt &	b
	)

Returns: expression representing the maximum of two expressions

Definition at line 583 of file string_constraint_generator_main.cpp.

◆ merge()

void merge	(	string_constraintst &	result,
		string_constraintst	other
	)

Merge two sets of constraints by appending to the first one.

Definition at line 225 of file string_constraint_generator_main.cpp.

◆ minimum()

exprt minimum	(	const exprt &	a,
		const exprt &	b
	)

Returns: expression representing the minimum of two expressions

Definition at line 578 of file string_constraint_generator_main.cpp.

◆ of_argument()

array_string_exprt of_argument	(	array_poolt &	array_pool,
		const exprt &	arg
	)

Converts a struct containing a length and pointer to an array.

This allows to get a string expression from arguments of a string builtion function, because string arguments in these function calls are given as a struct containing a length and pointer to an array.

Definition at line 333 of file string_constraint_generator_main.cpp.

◆ sum_overflows()

exprt sum_overflows ( const plus_exprt & sum )

Returns: Boolean true when the sum of the two expressions overflows

Definition at line 54 of file string_constraint_generator_main.cpp.

◆ zero_if_negative()

exprt zero_if_negative ( const exprt & expr )

Returns a non-negative version of the argument.

Parameters

expr	expression of which we want a non-negative version

Returns: max(0, expr)

Definition at line 591 of file string_constraint_generator_main.cpp.

Functions

Detailed Description

Function Documentation

◆ add_axioms_for_char_at()

◆ add_axioms_for_char_literal()

◆ add_axioms_for_constrain_characters()

◆ add_axioms_for_copy()

◆ add_axioms_for_length()

◆ add_constraint_on_characters()

◆ char_array_of_pointer()

◆ combine_results()

◆ get_function_name()

◆ get_return_code_type()

◆ get_string_expr()

◆ is_positive()

◆ maximum()

◆ merge()

◆ minimum()

◆ of_argument()

◆ sum_overflows()

◆ zero_if_negative()