cprover
string_constraint_generator_main.cpp File Reference

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

#include "string_constraint_generator.h"
#include "string_refinement_invariant.h"
#include <iterator>
#include <limits>
#include <util/arith_tools.h>
#include <util/deprecate.h>
#include <util/pointer_predicates.h>
#include <util/simplify_expr.h>
#include <util/ssa_expr.h>
#include <util/string_constant.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)
 
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, array_poolt &array_pool)
 Add constraint on characters of a string. More...
 
std::pair< exprt, string_constraintstadd_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...
 
signedbv_typet get_return_code_type ()
 
static irep_idt get_function_name (const function_application_exprt &expr)
 
std::pair< exprt, string_constraintstadd_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_constraintstadd_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_constraintstadd_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_constraintstadd_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_constraintstcombine_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_symbolgenerator of fresh symbols
ffunction application with arguments string str and integer i
array_poolpool of arrays representing strings
Returns
character expression char

Definition at line 409 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
ffunction application with one character argument
Returns
a new character expression

Definition at line 375 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_symbolgenerator of fresh symbols
fa function application with arguments: integer |s|, character pointer &s[0], string char_set_string, optional integers start and end
array_poolpool of arrays representing strings
Returns
integer expression whose value is zero

Definition at line 168 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_symbolgenerator of fresh symbols
ffunction application with one argument, which is a string, or three arguments: string, integer offset and count
array_poolpool of arrays representing strings
Returns
a new string expression
Deprecated:
SINCE(2017, 10, 5, "should use substring instead")

Definition at line 332 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
ffunction application with argument string str
array_poolpool of arrays representing strings
Returns
expression |str|

Definition at line 355 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,
array_poolt array_pool 
)

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_symbolgenerator of fresh symbols
sa string expression
startindex of the first character to constrain
endindex at which we stop adding constraints
char_seta 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.
array_poolpool of arrays representing strings
Returns
a string expression that is linked to the argument through axioms that are added to the list

Definition at line 131 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 442 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 194 of file string_constraint_generator_main.cpp.

◆ get_return_code_type()

signedbv_typet get_return_code_type ( )

Definition at line 189 of file string_constraint_generator_main.cpp.

◆ is_positive()

exprt is_positive ( const exprt x)
Parameters
xan expression
Returns
a Boolean expression true exactly when x is positive

Definition at line 366 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 427 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 422 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 38 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
exprexpression of which we want a non-negative version
Returns
max(0, expr)

Definition at line 435 of file string_constraint_generator_main.cpp.