cprover
string_constraint_generator.h File Reference

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

#include <limits>
#include <util/string_expr.h>
#include <util/replace_expr.h>
#include <util/refined_string_type.h>
#include <util/constexpr.def>
#include <util/deprecate.h>
#include <solvers/refinement/string_constraint.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

class  symbol_generatort
 Generation of fresh symbols of a given type. More...
 
class  array_poolt
 Correspondance between arrays and pointers string representations. More...
 
class  string_constraint_generatort
 

Functions

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...
 
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...
 
std::string utf16_constant_array_to_java (const array_exprt &arr, std::size_t length)
 Construct a string from a constant array. More...
 
exprt minimum (const exprt &a, const exprt &b)
 
exprt maximum (const exprt &a, const exprt &b)
 
exprt sum_overflows (const plus_exprt &sum)
 
exprt length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1)
 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)
 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_index, const exprt &end_index)
 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'`. More...
 
exprt length_constraint_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
 Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset. 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
chrthe character to get the numeric value of
char_typethe type to use for characters
typethe type to use for the return value
strict_formattingif true, don't allow upper case characters
radix_ulthe 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 628 of file string_constraint_generator_valueof.cpp.

References char_type(), and from_integer().

Referenced by string_constraint_generatort::add_axioms_for_characters_in_integer_string().

◆ 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
chrthe character
strict_formattingif true, don't allow upper case characters
radix_as_charthe radix as an expression of the same type as chr
radix_ulthe 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 558 of file string_constraint_generator_valueof.cpp.

References char_type(), exprt::copy_to_operands(), from_integer(), PRECONDITION, and exprt::type().

Referenced by string_constraint_generatort::add_axioms_for_correct_number_format().

◆ length_constraint_for_concat()

exprt length_constraint_for_concat ( const array_string_exprt res,
const array_string_exprt s1,
const array_string_exprt s2 
)

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

Definition at line 95 of file string_constraint_generator_concat.cpp.

References array_string_exprt::length().

Referenced by string_concatenation_builtin_functiont::length_constraint().

◆ length_constraint_for_concat_char()

exprt length_constraint_for_concat_char ( const array_string_exprt res,
const array_string_exprt s1 
)

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

Definition at line 135 of file string_constraint_generator_concat.cpp.

References from_integer(), and array_string_exprt::length().

Referenced by string_constraint_generatort::add_axioms_for_concat_char(), and string_concat_char_builtin_functiont::length_constraint().

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

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 77 of file string_constraint_generator_concat.cpp.

References from_integer(), irept::id(), array_string_exprt::length(), maximum(), minimum(), PRECONDITION, sum_overflows(), to_signedbv_type(), and exprt::type().

Referenced by string_constraint_generatort::add_axioms_for_concat_substr(), and string_concatenation_builtin_functiont::length_constraint().

◆ length_constraint_for_insert()

exprt length_constraint_for_insert ( const array_string_exprt res,
const array_string_exprt s1,
const array_string_exprt s2,
const exprt offset 
)

Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset.

Definition at line 74 of file string_constraint_generator_insert.cpp.

References array_string_exprt::length().

Referenced by string_constraint_generatort::add_axioms_for_insert(), and string_insertion_builtin_functiont::length_constraint().

◆ 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
typethe type that we are considering values of
radix_ulthe 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 702 of file string_constraint_generator_valueof.cpp.

References bitvector_typet::get_width(), irept::id(), and to_bitvector_type().

Referenced by string_constraint_generatort::add_axioms_for_parse_int(), and string_constraint_generatort::add_axioms_from_int_with_radix().

◆ maximum()

◆ minimum()

◆ sum_overflows()

exprt sum_overflows ( const plus_exprt sum)
Returns
Boolean true when the sum of the two expressions overflows

Definition at line 132 of file string_constraint_generator_main.cpp.

References from_integer(), exprt::op0(), exprt::op1(), exprt::operands(), PRECONDITION, and exprt::type().

Referenced by length_constraint_for_concat_substr().

◆ utf16_constant_array_to_java()

std::string utf16_constant_array_to_java ( const array_exprt arr,
std::size_t  length 
)

Construct a string from a constant array.

Parameters
arran array expression containing only constants
lengthan unsigned value representing the length of the array
Returns
String of length length represented by the array assuming each field in arr represents a character.

Definition at line 435 of file string_constraint_generator_format.cpp.

References INVARIANT, exprt::operands(), PRECONDITION, to_constant_expr(), to_unsigned_integer(), and utf16_little_endian_to_java().

Referenced by string_constraint_generatort::add_axioms_for_format(), and string_of_array().