cprover
Loading...
Searching...
No Matches
string_constraint_generator_main.cpp
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
22
23#include <iterator>
24
25#include <util/arith_tools.h>
26#include <util/deprecate.h>
29#include <util/simplify_expr.h>
30#include <util/ssa_expr.h>
32
34 : array_pool(fresh_symbol), ns(ns)
35{
36}
37
39{
40 PRECONDITION(sum.operands().size() == 2);
41 const exprt zero = from_integer(0, sum.op0().type());
42 const binary_relation_exprt op0_negative(sum.op0(), ID_lt, zero);
43 const binary_relation_exprt op1_negative(sum.op1(), ID_lt, zero);
45
46 // overflow happens when we add two values of same sign but their sum has a
47 // different sign
48 return and_exprt(
51}
52
62 const exprt &return_code,
64{
65 PRECONDITION(f.arguments().size() == 2);
66
70 f.arguments()[0].id() == ID_index ? to_index_expr(f.arguments()[0]).array()
71 : f.arguments()[0]);
72
73 const exprt &pointer_expr = f.arguments()[1];
75 // created_strings.emplace(to_array_string_expr(array_expr));
76 return equal_exprt{return_code, from_integer(0, f.type())};
77}
78
86 const exprt &return_code,
88{
89 PRECONDITION(f.arguments().size() == 2);
91 const exprt &new_length = f.arguments()[1];
92
93 const auto &length = array_pool.get_or_create_length(array_expr);
94 return and_exprt{equal_exprt{return_code, from_integer(0, f.type())},
95 equal_exprt(length, new_length)};
96}
97
100{
101 std::move(
102 other.existential.begin(),
103 other.existential.end(),
104 std::back_inserter(result.existential));
105 std::move(
106 other.universal.begin(),
107 other.universal.end(),
108 std::back_inserter(result.universal));
109 std::move(
110 other.not_contains.begin(),
111 other.not_contains.end(),
112 std::back_inserter(result.not_contains));
113}
114
128 const array_string_exprt &s,
129 const exprt &start,
130 const exprt &end,
131 const std::string &char_set)
132{
133 // Parse char_set
134 PRECONDITION(char_set.length() == 3);
135 PRECONDITION(char_set[1] == '-');
137
138 // Add constraint
139 const symbol_exprt qvar = fresh_symbol("char_constr", s.length_type());
140 const exprt chr = s[qvar];
142 qvar,
144 zero_if_negative(end),
146 return {{}, {sc}, {}};
147}
148
159std::pair<exprt, string_constraintst>
162{
163 const auto &args = f.arguments();
164 PRECONDITION(3 <= args.size() && args.size() <= 5);
165 PRECONDITION(args[2].type().id() == ID_string);
166 PRECONDITION(args[2].id() == ID_constant);
167
168 const array_string_exprt s = array_pool.find(args[1], args[0]);
170 const exprt &start =
171 args.size() >= 4 ? args[3] : from_integer(0, s.length_type());
172 const exprt &end =
173 args.size() >= 5 ? args[4] : array_pool.get_or_create_length(s);
174 auto constraints =
176 return {from_integer(0, get_return_code_type()), std::move(constraints)};
177}
178
183
185{
186 const exprt &name = expr.function();
187 PRECONDITION(name.id() == ID_symbol);
189 return to_symbol_expr(name).get_identifier();
190}
191
193 const exprt &return_code,
194 const function_application_exprt &expr)
195{
196 const irep_idt &id = get_function_name(expr);
198 return associate_array_to_pointer(return_code, expr);
200 return associate_length_to_array(return_code, expr);
201 return {};
202}
203
209std::pair<exprt, string_constraintst>
211 const function_application_exprt &expr)
212{
213 const irep_idt &id = get_function_name(expr);
214
216 return add_axioms_for_char_literal(expr);
217 else if(id == ID_cprover_string_length_func)
218 return add_axioms_for_length(expr);
219 else if(id == ID_cprover_string_equal_func)
220 return add_axioms_for_equals(expr);
224 return add_axioms_for_is_empty(expr);
225 else if(id == ID_cprover_string_char_at_func)
226 return add_axioms_for_char_at(expr);
228 return add_axioms_for_is_prefix(expr, false);
230 return add_axioms_for_is_suffix(expr, false);
232 return add_axioms_for_is_prefix(expr, true);
234 return add_axioms_for_is_suffix(expr, true);
236 return add_axioms_for_contains(expr);
238 return add_axioms_for_index_of(expr);
240 return add_axioms_for_last_index_of(expr);
241 else if(
244 return add_axioms_for_is_valid_int(expr);
246 return add_axioms_for_parse_int(expr);
248 return add_axioms_for_code_point_at(expr);
256 return add_axioms_for_compare_to(expr);
257 else if(id == ID_cprover_string_literal_func)
258 return add_axioms_from_literal(expr);
262 return add_axioms_for_substring(expr);
263 else if(id == ID_cprover_string_trim_func)
264 return add_axioms_for_trim(expr);
266 return add_axioms_for_empty_string(expr);
267 else if(id == ID_cprover_string_copy_func)
268 return add_axioms_for_copy(expr);
270 return add_axioms_from_int_hex(expr);
276 return add_axioms_from_double(expr);
277 else if(id == ID_cprover_string_of_long_func)
278 return add_axioms_from_long(expr);
280 return add_axioms_for_set_length(expr);
281 else if(id == ID_cprover_string_delete_func)
282 return add_axioms_for_delete(expr);
285 else if(id == ID_cprover_string_replace_func)
286 return add_axioms_for_replace(expr);
289 else
290 {
291 std::string msg(
292 "string_constraint_generator::function_application: unknown symbol :");
293 msg += id2string(id);
295 }
297}
298
305DEPRECATED(SINCE(2017, 10, 5, "should use substring instead"))
307string_constraint_generatort::add_axioms_for_copy(
309{
310 const auto &args = f.arguments();
311 PRECONDITION(args.size() == 3 || args.size() == 5);
312 const array_string_exprt res = array_pool.find(args[1], args[0]);
313 const array_string_exprt str = get_string_expr(array_pool, args[2]);
314 const typet &index_type = str.length_type();
315 const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3];
316 const exprt count =
317 args.size() == 3 ? array_pool.get_or_create_length(str) : args[4];
318 return add_axioms_for_substring(res, str, offset, plus_exprt(offset, count));
319}
320
326std::pair<exprt, string_constraintst>
334
338{
339 return binary_relation_exprt(x, ID_ge, from_integer(0, x.type()));
340}
341
345std::pair<exprt, string_constraintst>
348{
351 args.size() == 1); // there should be exactly 1 arg to char literal
352
353 const exprt &arg = args[0];
354 // for C programs argument to char literal should be one string constant
355 // of size 1.
356 if(
357 arg.operands().size() == 1 &&
358 to_unary_expr(arg).op().operands().size() == 1 &&
359 to_unary_expr(to_unary_expr(arg).op()).op().operands().size() == 2 &&
360 to_binary_expr(to_unary_expr(to_unary_expr(arg).op()).op()).op0().id() ==
362 {
364 to_binary_expr(to_unary_expr(to_unary_expr(arg).op()).op()).op0());
365 const std::string &sval = id2string(s.get_value());
366 CHECK_RETURN(sval.size() == 1);
367 return {from_integer(unsigned(sval[0]), arg.type()), {}};
368 }
369 else
370 {
372 }
373}
374
382std::pair<exprt, string_constraintst>
385{
386 PRECONDITION(f.arguments().size() == 2);
388 symbol_exprt char_sym = fresh_symbol("char", str.type().subtype());
389 string_constraintst constraints;
390 constraints.existential = {equal_exprt(char_sym, str[f.arguments()[1]])};
391 return {std::move(char_sym), std::move(constraints)};
392}
393
394exprt minimum(const exprt &a, const exprt &b)
395{
397}
398
399exprt maximum(const exprt &a, const exprt &b)
400{
402}
403
408{
409 return maximum(from_integer(0, expr.type()), expr);
410}
411
414std::pair<exprt, string_constraintst>
416 std::pair<exprt, string_constraintst> result1,
417 std::pair<exprt, string_constraintst> result2)
418{
419 const exprt return_code = maximum(result1.first, result2.first);
420 merge(result2.second, std::move(result1.second));
421 return {simplify_expr(return_code, ns), std::move(result2.second)};
422}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
bitvector_typet index_type()
Definition c_types.cpp:22
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
void insert(const exprt &pointer_expr, const array_string_exprt &array)
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
const typet & length_type() const
Definition string_expr.h:69
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
const irep_idt & get_value() const
Definition std_expr.h:2815
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
Application of (mathematical) function.
The trinary if-then-else operator.
Definition std_expr.h:2226
exprt & array()
Definition std_expr.h:1353
const irep_idt & id() const
Definition irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Disequality.
Definition std_expr.h:1283
The plus expression Associativity is not specified.
Definition std_expr.h:914
Fixed-width bit-vector with two's complement interpretation.
const irep_idt & get_value() const
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_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_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.
optionalt< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
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_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_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.
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.
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_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 ...
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
exprt interval_constraint(const exprt &expr, const integer_intervalt &interval)
Given an exprt and an integer interval return an exprt that represents restricting the expression to ...
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for 'mathematical' expressions.
STL namespace.
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define UNIMPLEMENTED
Definition invariant.h:525
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const string_constantt & to_string_constant(const exprt &expr)
Generates string constraints to link results from string functions with their arguments.
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 zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
signedbv_typet get_return_code_type()
exprt is_positive(const exprt &x)
static irep_idt get_function_name(const function_application_exprt &expr)
exprt sum_overflows(const plus_exprt &sum)
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 minimum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
signedbv_typet get_return_code_type()
array_string_exprt & to_array_string_expr(exprt &expr)
Definition string_expr.h:95
#define string_refinement_invariantt(reason)
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