cprover
string_constraint_generator_main.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: 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 
9 Author: Romain Brenguier, romain.brenguier@diffblue.com
10 
11 \*******************************************************************/
12 
19 
22 
23 #include <iterator>
24 #include <limits>
25 
26 #include <util/arith_tools.h>
27 #include <util/deprecate.h>
30 #include <util/simplify_expr.h>
31 #include <util/ssa_expr.h>
32 #include <util/string_constant.h>
33 
35  : array_pool(fresh_symbol), ns(ns)
36 {
37 }
38 
40 {
41  PRECONDITION(sum.operands().size() == 2);
42  const exprt zero = from_integer(0, sum.op0().type());
43  const binary_relation_exprt op0_negative(sum.op0(), ID_lt, zero);
44  const binary_relation_exprt op1_negative(sum.op1(), ID_lt, zero);
45  const binary_relation_exprt sum_negative(sum, ID_lt, zero);
46 
47  // overflow happens when we add two values of same sign but their sum has a
48  // different sign
49  return and_exprt(
50  equal_exprt(op0_negative, op1_negative),
51  notequal_exprt(op1_negative, sum_negative));
52 }
53 
63  const exprt &return_code,
65 {
66  PRECONDITION(f.arguments().size() == 2);
67 
71  f.arguments()[0].id() == ID_index ? to_index_expr(f.arguments()[0]).array()
72  : f.arguments()[0]);
73 
74  const exprt &pointer_expr = f.arguments()[1];
75  array_pool.insert(simplify_expr(pointer_expr, ns), array_expr);
76  // created_strings.emplace(to_array_string_expr(array_expr));
77  return equal_exprt{return_code, from_integer(0, f.type())};
78 }
79 
87  const exprt &return_code,
89 {
90  PRECONDITION(f.arguments().size() == 2);
92  const exprt &new_length = f.arguments()[1];
93 
94  const auto &length = array_pool.get_or_create_length(array_expr);
95  return and_exprt{equal_exprt{return_code, from_integer(0, f.type())},
96  equal_exprt(length, new_length)};
97 }
98 
101 {
102  std::move(
103  other.existential.begin(),
104  other.existential.end(),
105  std::back_inserter(result.existential));
106  std::move(
107  other.universal.begin(),
108  other.universal.end(),
109  std::back_inserter(result.universal));
110  std::move(
111  other.not_contains.begin(),
112  other.not_contains.end(),
113  std::back_inserter(result.not_contains));
114 }
115 
129  const array_string_exprt &s,
130  const exprt &start,
131  const exprt &end,
132  const std::string &char_set)
133 {
134  // Parse char_set
135  PRECONDITION(char_set.length() == 3);
136  PRECONDITION(char_set[1] == '-');
137  const integer_intervalt char_range(char_set[0], char_set[2]);
138 
139  // Add constraint
140  const symbol_exprt qvar = fresh_symbol("char_constr", s.length_type());
141  const exprt chr = s[qvar];
142  const string_constraintt sc(
143  qvar,
144  zero_if_negative(start),
145  zero_if_negative(end),
146  interval_constraint(chr, char_range));
147  return {{}, {sc}, {}};
148 }
149 
160 std::pair<exprt, string_constraintst>
163 {
164  const auto &args = f.arguments();
165  PRECONDITION(3 <= args.size() && args.size() <= 5);
166  PRECONDITION(args[2].type().id() == ID_string);
167  PRECONDITION(args[2].id() == ID_constant);
168 
169  const array_string_exprt s = array_pool.find(args[1], args[0]);
170  const irep_idt &char_set_string = to_constant_expr(args[2]).get_value();
171  const exprt &start =
172  args.size() >= 4 ? args[3] : from_integer(0, s.length_type());
173  const exprt &end =
174  args.size() >= 5 ? args[4] : array_pool.get_or_create_length(s);
175  auto constraints =
176  add_constraint_on_characters(s, start, end, char_set_string.c_str());
177  return {from_integer(0, get_return_code_type()), std::move(constraints)};
178 }
179 
181 {
182  return signedbv_typet(32);
183 }
184 
186 {
187  const exprt &name = expr.function();
188  PRECONDITION(name.id() == ID_symbol);
189  PRECONDITION(!is_ssa_expr(name));
190  return to_symbol_expr(name).get_identifier();
191 }
192 
194  const exprt &return_code,
195  const function_application_exprt &expr)
196 {
197  const irep_idt &id = get_function_name(expr);
198  if(id == ID_cprover_associate_array_to_pointer_func)
199  return associate_array_to_pointer(return_code, expr);
200  else if(id == ID_cprover_associate_length_to_array_func)
201  return associate_length_to_array(return_code, expr);
202  return {};
203 }
204 
210 std::pair<exprt, string_constraintst>
212  const function_application_exprt &expr)
213 {
214  const irep_idt &id = get_function_name(expr);
215 
216  if(id == ID_cprover_char_literal_func)
217  return add_axioms_for_char_literal(expr);
218  else if(id == ID_cprover_string_length_func)
219  return add_axioms_for_length(expr);
220  else if(id == ID_cprover_string_equal_func)
221  return add_axioms_for_equals(expr);
222  else if(id == ID_cprover_string_equals_ignore_case_func)
224  else if(id == ID_cprover_string_is_empty_func)
225  return add_axioms_for_is_empty(expr);
226  else if(id == ID_cprover_string_char_at_func)
227  return add_axioms_for_char_at(expr);
228  else if(id == ID_cprover_string_is_prefix_func)
229  return add_axioms_for_is_prefix(expr, false);
230  else if(id == ID_cprover_string_is_suffix_func)
231  return add_axioms_for_is_suffix(expr, false);
232  else if(id == ID_cprover_string_startswith_func)
233  return add_axioms_for_is_prefix(expr, true);
234  else if(id == ID_cprover_string_endswith_func)
235  return add_axioms_for_is_suffix(expr, true);
236  else if(id == ID_cprover_string_contains_func)
237  return add_axioms_for_contains(expr);
238  else if(id == ID_cprover_string_index_of_func)
239  return add_axioms_for_index_of(expr);
240  else if(id == ID_cprover_string_last_index_of_func)
241  return add_axioms_for_last_index_of(expr);
242  else if(
243  id == ID_cprover_string_is_valid_int_func ||
244  id == ID_cprover_string_is_valid_long_func)
245  return add_axioms_for_is_valid_int(expr);
246  else if(id == ID_cprover_string_parse_int_func)
247  return add_axioms_for_parse_int(expr);
248  else if(id == ID_cprover_string_code_point_at_func)
249  return add_axioms_for_code_point_at(expr);
250  else if(id == ID_cprover_string_code_point_before_func)
252  else if(id == ID_cprover_string_code_point_count_func)
253  return add_axioms_for_code_point_count(expr);
254  else if(id == ID_cprover_string_offset_by_code_point_func)
256  else if(id == ID_cprover_string_compare_to_func)
257  return add_axioms_for_compare_to(expr);
258  else if(id == ID_cprover_string_literal_func)
259  return add_axioms_from_literal(expr);
260  else if(id == ID_cprover_string_concat_code_point_func)
262  else if(id == ID_cprover_string_substring_func)
263  return add_axioms_for_substring(expr);
264  else if(id == ID_cprover_string_trim_func)
265  return add_axioms_for_trim(expr);
266  else if(id == ID_cprover_string_empty_string_func)
267  return add_axioms_for_empty_string(expr);
268  else if(id == ID_cprover_string_copy_func)
269  return add_axioms_for_copy(expr);
270  else if(id == ID_cprover_string_of_int_hex_func)
271  return add_axioms_from_int_hex(expr);
272  else if(id == ID_cprover_string_of_float_func)
273  return add_axioms_for_string_of_float(expr);
274  else if(id == ID_cprover_string_of_float_scientific_notation_func)
276  else if(id == ID_cprover_string_of_double_func)
277  return add_axioms_from_double(expr);
278  else if(id == ID_cprover_string_of_long_func)
279  return add_axioms_from_long(expr);
280  else if(id == ID_cprover_string_set_length_func)
281  return add_axioms_for_set_length(expr);
282  else if(id == ID_cprover_string_delete_func)
283  return add_axioms_for_delete(expr);
284  else if(id == ID_cprover_string_delete_char_at_func)
285  return add_axioms_for_delete_char_at(expr);
286  else if(id == ID_cprover_string_replace_func)
287  return add_axioms_for_replace(expr);
288  else if(id == ID_cprover_string_constrain_characters_func)
290  else
291  {
292  std::string msg(
293  "string_constraint_generator::function_application: unknown symbol :");
294  msg += id2string(id);
296  }
297  UNREACHABLE;
298 }
299 
306 DEPRECATED(SINCE(2017, 10, 5, "should use substring instead"))
307 std::pair<exprt, string_constraintst>
308 string_constraint_generatort::add_axioms_for_copy(
310 {
311  const auto &args = f.arguments();
312  PRECONDITION(args.size() == 3 || args.size() == 5);
313  const array_string_exprt res = array_pool.find(args[1], args[0]);
314  const array_string_exprt str = get_string_expr(array_pool, args[2]);
315  const typet &index_type = str.length_type();
316  const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3];
317  const exprt count =
318  args.size() == 3 ? array_pool.get_or_create_length(str) : args[4];
319  return add_axioms_for_substring(res, str, offset, plus_exprt(offset, count));
320 }
321 
327 std::pair<exprt, string_constraintst>
330 {
331  PRECONDITION(f.arguments().size() == 1);
333  return {array_pool.get_or_create_length(str), {}};
334 }
335 
339 {
340  return binary_relation_exprt(x, ID_ge, from_integer(0, x.type()));
341 }
342 
346 std::pair<exprt, string_constraintst>
349 {
351  PRECONDITION(
352  args.size() == 1); // there should be exactly 1 arg to char literal
353 
354  const exprt &arg = args[0];
355  // for C programs argument to char literal should be one string constant
356  // of size 1.
357  if(
358  arg.operands().size() == 1 &&
359  to_unary_expr(arg).op().operands().size() == 1 &&
360  to_unary_expr(to_unary_expr(arg).op()).op().operands().size() == 2 &&
361  to_binary_expr(to_unary_expr(to_unary_expr(arg).op()).op()).op0().id() ==
362  ID_string_constant)
363  {
365  to_binary_expr(to_unary_expr(to_unary_expr(arg).op()).op()).op0());
366  const std::string &sval = id2string(s.get_value());
367  CHECK_RETURN(sval.size() == 1);
368  return {from_integer(unsigned(sval[0]), arg.type()), {}};
369  }
370  else
371  {
373  }
374 }
375 
383 std::pair<exprt, string_constraintst>
386 {
387  PRECONDITION(f.arguments().size() == 2);
389  symbol_exprt char_sym = fresh_symbol("char", str.type().subtype());
390  string_constraintst constraints;
391  constraints.existential = {equal_exprt(char_sym, str[f.arguments()[1]])};
392  return {std::move(char_sym), std::move(constraints)};
393 }
394 
395 exprt minimum(const exprt &a, const exprt &b)
396 {
397  return if_exprt(binary_relation_exprt(a, ID_le, b), a, b);
398 }
399 
400 exprt maximum(const exprt &a, const exprt &b)
401 {
402  return if_exprt(binary_relation_exprt(a, ID_le, b), b, a);
403 }
404 
409 {
410  return maximum(from_integer(0, expr.type()), expr);
411 }
412 
415 std::pair<exprt, string_constraintst>
417  std::pair<exprt, string_constraintst> result1,
418  std::pair<exprt, string_constraintst> result2)
419 {
420  const exprt return_code = maximum(result1.first, result2.first);
421  merge(result2.second, std::move(result1.second));
422  return {simplify_expr(return_code, ns), std::move(result2.second)};
423 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
get_function_name
static irep_idt get_function_name(const function_application_exprt &expr)
Definition: string_constraint_generator_main.cpp:185
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:221
dstringt::c_str
const char * c_str() const
Definition: dstring.h:99
string_constraint_generatort::add_axioms_from_literal
std::pair< exprt, string_constraintst > add_axioms_from_literal(const function_application_exprt &f)
String corresponding to an internal cprover string.
Definition: string_constraint_generator_constants.cpp:111
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
array_string_exprt::length_type
const typet & length_type() const
Definition: string_expr.h:69
typet::subtype
const typet & subtype() const
Definition: type.h:47
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:523
string_constraint_generatort::add_axioms_for_code_point_count
std::pair< exprt, string_constraintst > add_axioms_for_code_point_count(const function_application_exprt &f)
Add axioms corresponding the String.codePointCount java function.
Definition: string_constraint_generator_code_points.cpp:189
string_constraint_generatort::add_axioms_for_index_of
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...
Definition: string_constraint_generator_indexof.cpp:38
is_positive
exprt is_positive(const exprt &x)
Definition: string_constraint_generator_main.cpp:338
string_constraint_generatort::add_axioms_for_substring
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,...
Definition: string_constraint_generator_transformation.cpp:122
arith_tools.h
array_poolt::find
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: array_pool.cpp:182
string_constraint_generatort::add_axioms_from_long
std::pair< exprt, string_constraintst > add_axioms_from_long(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(J) java function.
Definition: string_constraint_generator_valueof.cpp:45
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
typet
The type of an expression, extends irept.
Definition: type.h:29
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
string_constraintt
Definition: string_constraint.h:60
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
pointer_predicates.h
Various predicates over pointers in programs.
string_constraint_generatort::add_axioms_for_char_at
std::pair< exprt, string_constraintst > add_axioms_for_char_at(const function_application_exprt &f)
Character at a given position.
Definition: string_constraint_generator_main.cpp:384
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:56
string_constraint_generatort::add_axioms_for_delete
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...
Definition: string_constraint_generator_transformation.cpp:375
string_constraint_generatort::add_axioms_for_contains
std::pair< exprt, string_constraintst > add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
Definition: string_constraint_generator_testing.cpp:248
string_constraint_generatort::add_axioms_for_trim
std::pair< exprt, string_constraintst > add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
Definition: string_constraint_generator_transformation.cpp:180
and_exprt
Boolean AND.
Definition: std_expr.h:2137
array_poolt::get_or_create_length
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition: array_pool.cpp:24
get_string_expr
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
Definition: array_pool.cpp:196
string_refinement_invariant.h
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:36
string_constraint_generatort::string_constraint_generatort
string_constraint_generatort(const namespacet &ns)
Definition: string_constraint_generator_main.cpp:34
minimum
exprt minimum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:395
string_constraint_generatort::add_axioms_for_string_of_float
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
Definition: string_constraint_generator_float.cpp:159
string_constraint_generatort::add_axioms_for_equals
std::pair< exprt, string_constraintst > add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
Definition: string_constraint_generator_comparison.cpp:31
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
string_constantt
Definition: string_constant.h:16
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1190
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: mathematical_expr.h:193
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:58
string_constraint_generatort
Definition: string_constraint_generator.h:45
notequal_exprt
Disequality.
Definition: std_expr.h:1248
string_constraint_generatort::add_axioms_for_offset_by_code_point
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.
Definition: string_constraint_generator_code_points.cpp:215
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
interval_templatet
Definition: interval_template.h:20
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
string_constraint_generatort::add_constraint_on_characters
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.
Definition: string_constraint_generator_main.cpp:128
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
string_constraint_generatort::add_axioms_for_concat_code_point
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.
Definition: string_concatenation_builtin_function.cpp:173
string_constraint_generatort::add_axioms_for_compare_to
std::pair< exprt, string_constraintst > add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
Definition: string_constraint_generator_comparison.cpp:207
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:128
merge
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Definition: string_constraint_generator_main.cpp:100
string_constraint_generatort::add_axioms_for_replace
std::pair< exprt, string_constraintst > add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
Definition: string_constraint_generator_transformation.cpp:306
string_constraint_generatort::ns
const namespacet ns
Definition: string_constraint_generator.h:60
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
deprecate.h
string_constraint_generatort::add_axioms_for_parse_int
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
Definition: string_constraint_generator_valueof.cpp:525
string_constraint_generatort::add_axioms_for_is_empty
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.
Definition: string_constraint_generator_testing.cpp:129
interval_constraint.h
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:817
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
string_constraint_generatort::associate_length_to_array
exprt associate_length_to_array(const exprt &return_code, const function_application_exprt &f)
Associate an integer length to a char array.
Definition: string_constraint_generator_main.cpp:86
string_constraint_generatort::add_axioms_for_is_valid_int
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.
Definition: string_constraint_generator_valueof.cpp:490
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
string_constraint_generatort::add_axioms_for_is_suffix
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.
Definition: string_constraint_generator_testing.cpp:170
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
string_constraint_generatort::add_axioms_for_delete_char_at
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
Definition: string_constraint_generator_transformation.cpp:348
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
string_constraint_generatort::add_axioms_from_double
std::pair< exprt, string_constraintst > add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
Definition: string_constraint_generator_float.cpp:171
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
string_constraint_generatort::add_axioms_for_function_application
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.
Definition: string_constraint_generator_main.cpp:211
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
string_constraint_generatort::add_axioms_for_set_length
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.
Definition: string_constraint_generator_transformation.cpp:39
to_array_string_expr
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:95
string_constraint_generatort::make_array_pointer_association
optionalt< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
Definition: string_constraint_generator_main.cpp:193
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
string_constraint_generatort::add_axioms_for_last_index_of
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 ...
Definition: string_constraint_generator_indexof.cpp:356
string_constraint_generatort::add_axioms_for_equals_ignore_case
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
Definition: string_constraint_generator_comparison.cpp:135
string_constraint_generatort::add_axioms_for_constrain_characters
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.
Definition: string_constraint_generator_main.cpp:161
string_constraint_generatort::add_axioms_for_is_prefix
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...
Definition: string_constraint_generator_testing.cpp:38
simplify_expr.h
ssa_expr.h
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
interval_constraint
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 ...
Definition: interval_constraint.cpp:12
string_constraint_generatort::add_axioms_for_length
std::pair< exprt, string_constraintst > add_axioms_for_length(const function_application_exprt &f)
Length of a string.
Definition: string_constraint_generator_main.cpp:328
string_constraint_generatort::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
Definition: string_constraint_generator_main.cpp:347
function_application_exprt::function
exprt & function()
Definition: mathematical_expr.h:211
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
string_refinement_invariantt
#define string_refinement_invariantt(reason)
Definition: string_refinement_invariant.h:12
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:408
string_constraint_generatort::add_axioms_for_copy
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...
Definition: string_constraint_generator_main.cpp:308
string_constraint_generatort::add_axioms_from_int_hex
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.
Definition: string_constraint_generator_valueof.cpp:201
get_return_code_type
signedbv_typet get_return_code_type()
Definition: string_constraint_generator_main.cpp:180
string_constraint_generatort::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 ...
Definition: string_constraint_generator_main.cpp:416
string_constraint_generatort::associate_array_to_pointer
exprt associate_array_to_pointer(const exprt &return_code, const function_application_exprt &f)
Associate a char array to a char pointer.
Definition: string_constraint_generator_main.cpp:62
string_constraint_generatort::add_axioms_from_float_scientific_notation
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.
Definition: string_constraint_generator_float.cpp:335
string_constraintst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_constraint_generator.h:39
string_constraint_generatort::add_axioms_for_code_point_at
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
Definition: string_constraint_generator_code_points.cpp:122
exprt::operands
operandst & operands()
Definition: expr.h:95
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:400
array_poolt::insert
void insert(const exprt &pointer_expr, const array_string_exprt &array)
Definition: array_pool.cpp:158
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
string_constraint_generator.h
Generates string constraints to link results from string functions with their arguments.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
string_constraint_generatort::add_axioms_for_code_point_before
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
Definition: string_constraint_generator_code_points.cpp:154
array_string_exprt
Definition: string_expr.h:67
string_constantt::get_value
const irep_idt & get_value() const
Definition: string_constant.h:22
sum_overflows
exprt sum_overflows(const plus_exprt &sum)
Definition: string_constraint_generator_main.cpp:39
string_constraint_generatort::add_axioms_for_empty_string
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.
Definition: string_constraint_generator_constants.cpp:64
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:37
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:38