cprover
Loading...
Searching...
No Matches
string_constraint_generator.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generates string constraints to link results from string functions
4 with their arguments. This is inspired by the PASS paper at HVC'13:
5 "PASS: String Solving with Parameterized Array and Interval Automaton"
6 by Guodong Li and Indradeep Ghosh, which gives examples of constraints
7 for several functions.
8
9Author: Romain Brenguier, romain.brenguier@diffblue.com
10
11\*******************************************************************/
12
19
20#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
21#define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
22
23#include <limits>
25#include <util/constexpr.def>
26#include <util/deprecate.h>
27#include <util/namespace.h>
29#include <util/replace_expr.h>
30#include <util/string_expr.h>
31
32#include "array_pool.h"
33
35
39{
40 std::vector<exprt> existential;
41 std::vector<string_constraintt> universal;
42 std::vector<string_not_contains_constraintt> not_contains;
43};
44
46
48{
49public:
50 // This module keeps a list of axioms. It has methods which generate
51 // string constraints for different string functions and add them
52 // to the axiom list.
53
55
56 std::pair<exprt, string_constraintst>
58
60
62
64
69 const exprt &return_code,
70 const function_application_exprt &expr);
71
72private:
74 const exprt &return_code,
76
78 const exprt &return_code,
80
81public:
82 std::pair<exprt, string_constraintst> add_axioms_for_concat(
85 const array_string_exprt &s2);
86
87 std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
91 const exprt &start_index,
92 const exprt &end_index);
93 std::pair<exprt, string_constraintst> add_axioms_for_insert(
97 const exprt &offset);
98 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
100 const exprt &input_int,
101 const exprt &radix,
102 size_t max_size);
103
105 const array_string_exprt &s,
106 const exprt &start,
107 const exprt &end,
108 const std::string &char_set);
109 std::pair<exprt, string_constraintst>
111
112 // The following functions add axioms for the returned value
113 // to be equal to the result of the function given as argument.
114 // They are not accessed directly from other classes: they call
115 // `add_axioms_for_function_application` which determines which of
116 // these methods should be called.
117
118 std::pair<exprt, string_constraintst>
120 std::pair<exprt, string_constraintst>
122
123 std::pair<exprt, string_constraintst>
125 std::pair<exprt, string_constraintst>
127 std::pair<exprt, string_constraintst>
129 std::pair<exprt, string_constraintst>
131
132 std::pair<exprt, string_constraintst>
134 std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
135 const array_string_exprt &prefix,
136 const array_string_exprt &str,
137 const exprt &offset);
138 std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
140 bool swap_arguments);
141
142 std::pair<exprt, string_constraintst> add_axioms_for_is_suffix(
144 bool swap_arguments);
145 std::pair<exprt, string_constraintst>
147 std::pair<exprt, string_constraintst>
149
150 std::pair<exprt, string_constraintst>
152
153 std::pair<exprt, string_constraintst>
155 std::pair<exprt, string_constraintst> add_axioms_for_constant(
156 const array_string_exprt &res,
158 const exprt &guard = true_exprt());
159
160 std::pair<exprt, string_constraintst> add_axioms_for_delete(
161 const array_string_exprt &res,
162 const array_string_exprt &str,
163 const exprt &start,
164 const exprt &end);
165 std::pair<exprt, string_constraintst>
167 std::pair<exprt, string_constraintst>
169
170 std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
171 const array_string_exprt &res,
172 const exprt &arg,
173 const exprt &guard);
174 std::pair<exprt, string_constraintst>
176
177 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int(
178 const array_string_exprt &res,
179 const exprt &input_int,
180 size_t max_size);
181 std::pair<exprt, string_constraintst>
183 std::pair<exprt, string_constraintst>
185 std::pair<exprt, string_constraintst>
187 std::pair<exprt, string_constraintst>
189 std::pair<exprt, string_constraintst>
191 std::pair<exprt, string_constraintst>
193 std::pair<exprt, string_constraintst>
195 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
196 const array_string_exprt &str,
197 const exprt &c,
198 const exprt &from_index);
199 std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
202 const exprt &from_index);
203 std::pair<exprt, string_constraintst>
205 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
208 const exprt &from_index);
209 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
210 const array_string_exprt &str,
211 const exprt &c,
212 const exprt &from_index);
213
214 std::pair<exprt, string_constraintst>
216
222 std::pair<exprt, string_constraintst>
224 std::pair<exprt, string_constraintst>
226 std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
227 const array_string_exprt &res,
228 const exprt &int_expr,
229 size_t max_size);
230 std::pair<exprt, string_constraintst>
232 const array_string_exprt &res,
233 const exprt &f);
234 std::pair<exprt, string_constraintst>
237
240 std::pair<exprt, string_constraintst>
242
243 std::pair<exprt, string_constraintst>
245 std::pair<exprt, string_constraintst>
247
251 std::pair<exprt, string_constraintst> add_axioms_for_substring(
252 const array_string_exprt &res,
253 const array_string_exprt &str,
254 const exprt &start,
255 const exprt &end);
256 std::pair<exprt, string_constraintst>
258
259 std::pair<exprt, string_constraintst>
261
262 std::pair<exprt, string_constraintst> add_axioms_for_code_point(
263 const array_string_exprt &res,
264 const exprt &code_point);
265 std::pair<exprt, string_constraintst>
267
272 DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
275
285
287 const exprt &input_int,
288 const typet &type,
289 const bool strict_formatting,
290 const array_string_exprt &str,
291 const std::size_t max_string_length,
292 const exprt &radix,
293 const unsigned long radix_ul);
295 const array_string_exprt &str,
296 const exprt &radix_as_char,
297 const unsigned long radix_ul,
298 const std::size_t max_size,
299 const bool strict_formatting);
306
310
314 {
320 unsigned long radix_ul;
322 // (or pessimistic assumption of base-2 if unknown) and result type. For
323 // example, the longest possible decimal int64 is 16 characters long in hex.
324 std::size_t max_string_length;
325 };
326
329 const typet &target_int_type);
330};
331
333 const array_string_exprt &res,
334 const array_string_exprt &s1,
335 array_poolt &array_pool);
337 const array_string_exprt &res,
338 const array_string_exprt &s1,
339 const array_string_exprt &s2,
340 array_poolt &array_pool);
342 const array_string_exprt &res,
343 const array_string_exprt &s1,
344 const array_string_exprt &s2,
345 const exprt &start,
346 const exprt &end,
347 array_poolt &array_pool);
348
349size_t max_printed_string_length(const typet &type, unsigned long ul_radix);
350
351exprt is_positive(const exprt &x);
352
354exprt minimum(const exprt &a, const exprt &b);
355
357exprt maximum(const exprt &a, const exprt &b);
358
361
362// Type used by primitives to signal errors
364
365exprt zero_if_negative(const exprt &expr);
366
368 const exprt &chr,
369 const bool strict_formatting,
370 const exprt &radix_as_char,
371 const unsigned long radix_ul);
372
374 const exprt &chr,
375 const typet &char_type,
376 const typet &type,
377 const bool strict_formatting,
378 unsigned long radix_ul);
379
380#endif
Associates arrays and length to pointers, so that the string refinement can transform builtin functio...
bitvector_typet char_type()
Definition c_types.cpp:124
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Correspondance between arrays and pointers string representations.
Definition array_pool.h:42
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
Application of (mathematical) function.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The plus expression Associativity is not specified.
Definition std_expr.h:914
Fixed-width bit-vector with two's complement interpretation.
std::pair< exprt, string_constraintst > add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
std::pair< exprt, string_constraintst > add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f)
std::pair< exprt, string_constraintst > add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the last occurrence ...
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f)
std::pair< exprt, string_constraintst > add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
exprt associate_array_to_pointer(const exprt &return_code, const function_application_exprt &f)
Associate a char array to a char pointer.
std::pair< exprt, string_constraintst > add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start,...
std::pair< exprt, string_constraintst > add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
std::pair< exprt, string_constraintst > add_axioms_for_is_valid_int(const function_application_exprt &f)
Check a string is a valid integer, using the same rules as Java Integer.parseInt.
std::pair< exprt, string_constraintst > add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal.
std::pair< exprt, string_constraintst > add_axioms_for_is_empty(const function_application_exprt &f)
Add axioms stating that the returned value is true exactly when the argument string is empty.
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack of the last occurrence of nee...
std::pair< exprt, string_constraintst > add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
std::vector< exprt > get_conjuncts_for_correct_number_format(const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting)
Add axioms making the return value true if the given string is a correct number in the given radix.
std::pair< exprt, string_constraintst > add_axioms_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 res is the concatenation of s1 with the substring of s2 starting at index ‘...
std::pair< exprt, string_constraintst > add_axioms_for_cprover_string(const array_string_exprt &res, const exprt &arg, const exprt &guard)
Convert an expression of type string_typet to a string_exprt.
optionalt< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
parseint_argumentst unpack_parseint_arguments(const function_application_exprt &f, const typet &target_int_type)
std::pair< exprt, string_constraintst > add_axioms_for_fractional_part(const array_string_exprt &res, const exprt &int_expr, size_t max_size)
Add axioms for representing the fractional part of a floating point starting with a dot.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
std::pair< exprt, string_constraintst > add_axioms_for_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the first occurrence...
std::pair< exprt, string_constraintst > add_axioms_for_constrain_characters(const function_application_exprt &f)
Add axioms to ensure all characters of a string belong to a given set.
std::pair< exprt, string_constraintst > add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
std::pair< exprt, string_constraintst > add_axioms_for_set_length(const function_application_exprt &f)
Reduce or extend a string to have the given length.
std::pair< exprt, string_constraintst > add_axioms_for_offset_by_code_point(const function_application_exprt &f)
Add axioms corresponding the String.offsetByCodePointCount java function.
std::pair< exprt, string_constraintst > add_axioms_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
std::pair< exprt, string_constraintst > add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
Add axioms stating that the returned expression is true exactly when the offset is greater or equal t...
std::pair< exprt, string_constraintst > add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
string_constraintst add_axioms_for_characters_in_integer_string(const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, const unsigned long radix_ul)
Add axioms connecting the characters in the input string to the value of the output integer.
std::pair< exprt, string_constraintst > add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
exprt associate_length_to_array(const exprt &return_code, const function_application_exprt &f)
Associate an integer length to a char array.
std::pair< exprt, string_constraintst > add_axioms_from_literal(const function_application_exprt &f)
String corresponding to an internal cprover string.
std::pair< exprt, string_constraintst > add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments)
Test if the target is a suffix of the string.
std::pair< exprt, string_constraintst > add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
std::pair< exprt, string_constraintst > add_axioms_for_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value index is the index within haystack of the first occurrence...
std::pair< exprt, string_constraintst > add_axioms_for_code_point(const array_string_exprt &res, const exprt &code_point)
add axioms for the conversion of an integer representing a java code point to a utf-16 string
string_constraintst add_constraint_on_characters(const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set)
Add constraint on characters of a string.
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
std::pair< exprt, string_constraintst > add_axioms_for_copy(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the argument of the function applic...
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
std::pair< exprt, string_constraintst > add_axioms_from_long(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(J) java function.
std::pair< exprt, string_constraintst > add_axioms_for_code_point_count(const function_application_exprt &f)
Add axioms corresponding the String.codePointCount java function.
std::pair< exprt, string_constraintst > add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
std::pair< exprt, string_constraintst > add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
std::pair< exprt, string_constraintst > add_axioms_for_char_at(const function_application_exprt &f)
Character at a given position.
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
std::pair< exprt, string_constraintst > add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
std::pair< exprt, string_constraintst > add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
std::pair< exprt, string_constraintst > add_axioms_for_length(const function_application_exprt &f)
Length of a string.
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
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 ...
std::pair< exprt, string_constraintst > add_axioms_from_char(const array_string_exprt &res, const exprt &c)
Generation of fresh symbols of a given type.
Definition array_pool.h:22
The Boolean constant true.
Definition std_expr.h:2856
The type of an expression, extends irept.
Definition type.h:29
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
STL namespace.
Type for string expressions used by the string solver.
Defines string constraints.
exprt is_positive(const exprt &x)
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
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.
exprt sum_overflows(const plus_exprt &sum)
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 ...
exprt maximum(const exprt &a, const exprt &b)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
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.
exprt minimum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
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.
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.
signedbv_typet get_return_code_type()
String expressions for the string solver.
Argument block for parseInt and cousins, common to parseInt itself and CProverString....
unsigned long radix_ul
Radix as an unsigned long (or 0 if unknown)
std::size_t max_string_length
Max string length (assuming no leading zeroes) considering the radix.
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< string_not_contains_constraintt > not_contains
std::vector< exprt > existential
std::vector< string_constraintt > universal