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

#include <limits>
#include <solvers/strings/string_constraint.h>
#include <util/constexpr.def>
#include <util/deprecate.h>
#include <util/namespace.h>
#include <util/refined_string_type.h>
#include <util/replace_expr.h>
#include <util/string_expr.h>
#include "array_pool.h"

Include dependency graph for string_constraint_generator.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	string_constraintst
	Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation). More...

class	string_constraint_generatort

struct	string_constraint_generatort::parseint_argumentst
	Argument block for parseInt and cousins, common to parseInt itself and CProverString.isValidInt. More...

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

exprt	length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1, array_poolt &array_pool)
	Add axioms enforcing that the length of `res` is that of the concatenation of `s1` with. More...

exprt	length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, array_poolt &array_pool)
	Add axioms enforcing that the length of `res` is that of the concatenation of `s1` with `s2` More...

exprt	length_constraint_for_concat_substr (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start, const exprt &end, array_poolt &array_pool)
	Add axioms enforcing that the length of `res` is that of the concatenation of `s1` with the substring of `s2` starting at index ‘start’ `and ending at index`end'‘. More...

size_t	max_printed_string_length (const typet &type, unsigned long ul_radix)
	Calculate the string length needed to represent any value of the given type using the given radix. More...

exprt	is_positive (const exprt &x)

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

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

exprt	sum_overflows (const plus_exprt &sum)

signedbv_typet	get_return_code_type ()

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

exprt	is_digit_with_radix (const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul)
	Check if a character is a digit with respect to the given radix, e.g. More...

exprt	get_numeric_value_from_character (const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, unsigned long radix_ul)
	Get the numeric value of a character, assuming that the radix is large enough. 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.h.

Function Documentation

◆ get_numeric_value_from_character()

exprt get_numeric_value_from_character	(	const exprt &	chr,
		const typet &	char_type,
		const typet &	type,
		const bool	strict_formatting,
		const unsigned long	radix_ul
	)

Get the numeric value of a character, assuming that the radix is large enough.

'+' and '-' yield 0.

Parameters

chr	the character to get the numeric value of
char_type	the type to use for characters
type	the type to use for the return value
strict_formatting	if true, don't allow upper case characters
radix_ul	the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix

Returns: an integer expression of the given type with the numeric value of the char

There are four cases, which occur in ASCII in the following order: '+' and '-', digits, upper case letters, lower case letters

return char >= '0' ? (char - '0') : 0

return char >= 'a' ? (char - 'a' + 10) : char >= '0' ? (char - '0') : 0

return char >= 'a' ? (char - 'a' + 10) : char >= 'A' ? (char - 'A' + 10) : char >= '0' ? (char - '0') : 0

Definition at line 623 of file string_constraint_generator_valueof.cpp.

◆ get_return_code_type()

signedbv_typet get_return_code_type ( )

Definition at line 182 of file string_constraint_generator_main.cpp.

◆ is_digit_with_radix()

exprt is_digit_with_radix	(	const exprt &	chr,
		const bool	strict_formatting,
		const exprt &	radix_as_char,
		const unsigned long	radix_ul
	)

Check if a character is a digit with respect to the given radix, e.g.

if the radix is 10 then check if the character is in the range 0-9.

Parameters

chr	the character
strict_formatting	if true, don't allow upper case characters
radix_as_char	the radix as an expression of the same type as chr
radix_ul	the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix

Returns: an expression for the condition

Definition at line 555 of file string_constraint_generator_valueof.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 341 of file string_constraint_generator_main.cpp.

◆ length_constraint_for_concat()

exprt length_constraint_for_concat	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2,
		array_poolt &	array_pool
	)

Add axioms enforcing that the length of res is that of the concatenation of s1 with s2

Definition at line 125 of file string_concatenation_builtin_function.cpp.

◆ length_constraint_for_concat_char()

exprt length_constraint_for_concat_char	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		array_poolt &	array_pool
	)

Add axioms enforcing that the length of res is that of the concatenation of s1 with.

Definition at line 140 of file string_concatenation_builtin_function.cpp.

◆ length_constraint_for_concat_substr()

exprt length_constraint_for_concat_substr	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2,
		const exprt &	start,
		const exprt &	end,
		array_poolt &	array_pool
	)

Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at indexend'‘.

Where start_index’ is max(0, start) and end' is max(min(end, s2.length), start')

Definition at line 102 of file string_concatenation_builtin_function.cpp.

◆ max_printed_string_length()

size_t max_printed_string_length	(	const typet &	type,
		unsigned long	radix_ul
	)

Calculate the string length needed to represent any value of the given type using the given radix.

Due to floating point rounding errors we sometimes return a value 1 larger than needed, which is fine for our purposes.

Parameters

type	the type that we are considering values of
radix_ul	the radix we are using, or 0, in which case the return value will work for any radix

Returns: the maximum string length

We want to calculate max, the maximum number of characters needed to represent any value of the given type.

For signed types, the longest string will be for -2^(n_bits-1), so max = 1 + min{k: 2^(n_bits-1) < radix^k} (the 1 is for the minus sign) = 1 + min{k: n_bits-1 < k log_2(radix)} = 1 + min{k: k > (n_bits-1) / log_2(radix)} = 1 + min{k: k > floor((n_bits-1) / log_2(radix))} = 1 + (1 + floor((n_bits-1) / log_2(radix))) = 2 + floor((n_bits-1) / log_2(radix))

For unsigned types, the longest string will be for (2^n_bits)-1, so max = min{k: (2^n_bits)-1 < radix^k} = min{k: 2^n_bits <= radix^k} = min{k: n_bits <= k log_2(radix)} = min{k: k >= n_bits / log_2(radix)} = min{k: k >= ceil(n_bits / log_2(radix))} = ceil(n_bits / log_2(radix))

Definition at line 697 of file string_constraint_generator_valueof.cpp.

◆ maximum()

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

Returns: expression representing the maximum of two expressions

Definition at line 404 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 101 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 399 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 40 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 412 of file string_constraint_generator_main.cpp.

Classes

Functions

Detailed Description

Function Documentation

◆ get_numeric_value_from_character()

◆ get_return_code_type()

◆ is_digit_with_radix()

◆ is_positive()

◆ length_constraint_for_concat()

◆ length_constraint_for_concat_char()

◆ length_constraint_for_concat_substr()

◆ max_printed_string_length()

◆ maximum()

◆ merge()

◆ minimum()

◆ sum_overflows()

◆ zero_if_negative()