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 
21 
22 #include <limits>
24 
25 #include <util/arith_tools.h>
27 #include <util/ssa_expr.h>
28 #include <util/string_constant.h>
29 #include <util/deprecate.h>
30 
32  : array_pool(fresh_symbol), ns(ns)
33 {
34 }
35 
36 const std::vector<exprt> &string_constraint_generatort::get_lemmas() const
37 {
38  return lemmas;
39 }
40 
42 {
43  lemmas.push_back(expr);
44 }
45 
46 const std::vector<string_constraintt> &
48 {
49  return constraints;
50 }
51 
52 const std::vector<string_not_contains_constraintt> &
54 {
56 }
57 
58 const std::vector<symbol_exprt> &
60 {
61  return index_symbols;
62 }
63 
64 const std::vector<symbol_exprt> &
66 {
67  return boolean_symbols;
68 }
69 
70 const std::set<array_string_exprt> &
72 {
73  return created_strings;
74 }
75 
83  int i, const typet &char_type)
84 {
85  return from_integer(i, char_type);
86 }
87 
93 operator()(const irep_idt &prefix, const typet &type)
94 {
95  std::ostringstream buf;
96  buf << "string_refinement#" << prefix << "#" << ++symbol_count;
97  irep_idt name(buf.str());
98  return symbol_exprt(name, type);
99 }
100 
105  const irep_idt &prefix, const typet &type)
106 {
107  return fresh_symbol(prefix, type);
108 }
109 
114  const irep_idt &prefix, const typet &type)
115 {
116  symbol_exprt s=fresh_symbol(prefix, type);
117  index_symbols.push_back(s);
118  return s;
119 }
120 
125  const irep_idt &prefix)
126 {
127  symbol_exprt b=fresh_symbol(prefix, bool_typet());
128  boolean_symbols.push_back(b);
129  return b;
130 }
131 
133 {
134  PRECONDITION(sum.operands().size() == 2);
135  const exprt zero = from_integer(0, sum.op0().type());
136  const binary_relation_exprt op0_negative(sum.op0(), ID_lt, zero);
137  const binary_relation_exprt op1_negative(sum.op1(), ID_lt, zero);
138  const binary_relation_exprt sum_negative(sum, ID_lt, zero);
139 
140  // overflow happens when we add two values of same sign but their sum has a
141  // different sign
142  return and_exprt(
143  equal_exprt(op0_negative, op1_negative),
144  notequal_exprt(op1_negative, sum_negative));
145 }
146 
151 {
152  if(s.length() == infinity_exprt(s.length().type()))
153  {
154  auto it = length_of_array.find(s);
155  if(it != length_of_array.end())
156  return it->second;
157  }
158  return s.length();
159 }
160 
165  const typet &index_type,
166  const typet &char_type)
167 {
168  symbol_exprt length = fresh_symbol("string_length", index_type);
169  array_typet array_type(char_type, length);
170  symbol_exprt content = fresh_symbol("string_content", array_type);
172  created_strings.insert(str);
173  return str;
174 }
175 
176 // Make a new char array for a char pointer. The size of the char array is a
177 // variable with no constraint.
179  const exprt &char_pointer,
180  const typet &char_array_type)
181 {
182  PRECONDITION(char_pointer.type().id() == ID_pointer);
183  PRECONDITION(char_array_type.id() == ID_array);
184  PRECONDITION(
185  char_array_type.subtype().id() == ID_unsignedbv ||
186  char_array_type.subtype().id() == ID_signedbv);
187 
188  if(char_pointer.id() == ID_if)
189  {
190  const if_exprt &if_expr = to_if_expr(char_pointer);
191  const array_string_exprt t =
192  make_char_array_for_char_pointer(if_expr.true_case(), char_array_type);
193  const array_string_exprt f =
194  make_char_array_for_char_pointer(if_expr.false_case(), char_array_type);
195  const array_typet array_type(
196  char_array_type.subtype(),
197  if_exprt(
198  if_expr.cond(),
199  to_array_type(t.type()).size(),
200  to_array_type(f.type()).size()));
201  return to_array_string_expr(if_exprt(if_expr.cond(), t, f, array_type));
202  }
203  const bool is_constant_array =
204  char_pointer.id() == ID_address_of &&
205  (to_address_of_expr(char_pointer).object().id() == ID_index) &&
206  char_pointer.op0().op0().id() == ID_array;
207  if(is_constant_array)
208  {
209  return to_array_string_expr(
210  to_index_expr(to_address_of_expr(char_pointer).object()).array());
211  }
212  const std::string symbol_name = "char_array_" + id2string(char_pointer.id());
213  const auto array_sym =
214  to_array_string_expr(fresh_symbol(symbol_name, char_array_type));
215  const auto insert_result =
216  arrays_of_pointers.insert({char_pointer, array_sym});
217  return to_array_string_expr(insert_result.first->second);
218 }
219 
221  const exprt &pointer_expr,
222  array_string_exprt &array_expr)
223 {
224  const exprt &length = array_expr.length();
225  if(length == infinity_exprt(length.type()))
226  {
227  auto pair = length_of_array.insert(
228  std::make_pair(array_expr, fresh_symbol("string_length", length.type())));
229  array_expr.length() = pair.first->second;
230  }
231 
232  const auto it_bool =
233  arrays_of_pointers.insert(std::make_pair(pointer_expr, array_expr));
234  INVARIANT(
235  it_bool.second, "should not associate two arrays to the same pointer");
236 }
237 
246 {
247  PRECONDITION(f.arguments().size() == 2);
248 
252  f.arguments()[0].id() == ID_index ? to_index_expr(f.arguments()[0]).array()
253  : f.arguments()[0]);
254 
255  const exprt &pointer_expr = f.arguments()[1];
256  array_pool.insert(pointer_expr, array_expr);
257  created_strings.emplace(to_array_string_expr(array_expr));
258  return from_integer(0, f.type());
259 }
260 
268 {
269  PRECONDITION(f.arguments().size() == 2);
271  const exprt &new_length = f.arguments()[1];
272 
273  const auto &length = array_pool.get_length(array_expr);
274  lemmas.push_back(equal_exprt(length, new_length));
275  return from_integer(0, f.type());
276 }
277 
284 {
286  const refined_string_exprt &str = to_string_expr(expr);
287  return char_array_of_pointer(str.content(), str.length());
288 }
289 
291 {
292  lemmas.clear();
293  constraints.clear();
294  not_contains_constraints.clear();
295 }
296 
310  const array_string_exprt &s,
311  const exprt &start,
312  const exprt &end,
313  const std::string &char_set)
314 {
315  // Parse char_set
316  PRECONDITION(char_set.length() == 3);
317  PRECONDITION(char_set[1] == '-');
318  const char &low_char = char_set[0];
319  const char &high_char = char_set[2];
320 
321  // Add constraint
322  const symbol_exprt qvar = fresh_univ_index("char_constr", s.length().type());
323  const exprt chr = s[qvar];
324  const and_exprt char_in_set(
325  binary_relation_exprt(chr, ID_ge, from_integer(low_char, chr.type())),
326  binary_relation_exprt(chr, ID_le, from_integer(high_char, chr.type())));
327  const string_constraintt sc(
328  qvar, zero_if_negative(start), zero_if_negative(end), char_in_set);
329  constraints.push_back(sc);
330 }
331 
344 {
345  const auto &args = f.arguments();
346  PRECONDITION(3 <= args.size() && args.size() <= 5);
347  PRECONDITION(args[2].type().id() == ID_string);
348  PRECONDITION(args[2].id() == ID_constant);
349  const array_string_exprt s = char_array_of_pointer(args[1], args[0]);
350  const irep_idt &char_set_string = to_constant_expr(args[2]).get_value();
351  const exprt &start =
352  args.size() >= 4 ? args[3] : from_integer(0, s.length().type());
353  const exprt &end = args.size() >= 5 ? args[4] : s.length();
354  add_constraint_on_characters(s, start, end, char_set_string.c_str());
355  return from_integer(0, get_return_code_type());
356 }
357 
360 array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length)
361 {
362  const array_typet array_type(pointer.type().subtype(), length);
363  return make_char_array_for_char_pointer(pointer, array_type);
364 }
365 
370  const exprt &pointer,
371  const exprt &length)
372 {
373  return *created_strings.insert(array_pool.find(pointer, length)).first;
374 }
375 
377 {
378  return find(str.content(), str.length());
379 }
380 
382 {
383  const auto string_argument = expr_checked_cast<struct_exprt>(arg);
384  return find(string_argument.op1(), string_argument.op0());
385 }
386 
388 {
389  const exprt &name = expr.function();
390  PRECONDITION(name.id() == ID_symbol);
391  return is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
392  : to_symbol_expr(name).get_identifier();
393 }
394 
396  const function_application_exprt &expr)
397 {
398  const irep_idt &id = get_function_name(expr);
399  if(id == ID_cprover_associate_array_to_pointer_func)
400  return associate_array_to_pointer(expr);
401  else if(id == ID_cprover_associate_length_to_array_func)
402  return associate_length_to_array(expr);
403  return {};
404 }
405 
412  const function_application_exprt &expr)
413 {
414  const irep_idt &id = get_function_name(expr);
415  exprt res;
416 
417  if(id==ID_cprover_char_literal_func)
418  res=add_axioms_for_char_literal(expr);
419  else if(id==ID_cprover_string_length_func)
420  res=add_axioms_for_length(expr);
421  else if(id==ID_cprover_string_equal_func)
422  res=add_axioms_for_equals(expr);
423  else if(id==ID_cprover_string_equals_ignore_case_func)
425  else if(id==ID_cprover_string_is_empty_func)
426  res=add_axioms_for_is_empty(expr);
427  else if(id==ID_cprover_string_char_at_func)
428  res=add_axioms_for_char_at(expr);
429  else if(id==ID_cprover_string_is_prefix_func)
430  res=add_axioms_for_is_prefix(expr);
431  else if(id==ID_cprover_string_is_suffix_func)
432  res=add_axioms_for_is_suffix(expr);
433  else if(id==ID_cprover_string_startswith_func)
434  res=add_axioms_for_is_prefix(expr, true);
435  else if(id==ID_cprover_string_endswith_func)
436  res=add_axioms_for_is_suffix(expr, true);
437  else if(id==ID_cprover_string_contains_func)
438  res=add_axioms_for_contains(expr);
439  else if(id==ID_cprover_string_hash_code_func)
440  res=add_axioms_for_hash_code(expr);
441  else if(id==ID_cprover_string_index_of_func)
442  res=add_axioms_for_index_of(expr);
443  else if(id==ID_cprover_string_last_index_of_func)
445  else if(id==ID_cprover_string_parse_int_func)
446  res=add_axioms_for_parse_int(expr);
447  else if(id==ID_cprover_string_code_point_at_func)
449  else if(id==ID_cprover_string_code_point_before_func)
451  else if(id==ID_cprover_string_code_point_count_func)
453  else if(id==ID_cprover_string_offset_by_code_point_func)
455  else if(id==ID_cprover_string_compare_to_func)
456  res=add_axioms_for_compare_to(expr);
457  else if(id==ID_cprover_string_literal_func)
458  res=add_axioms_from_literal(expr);
459  else if(id==ID_cprover_string_concat_code_point_func)
461  else if(id==ID_cprover_string_insert_func)
462  res=add_axioms_for_insert(expr);
463  else if(id==ID_cprover_string_insert_int_func)
464  res=add_axioms_for_insert_int(expr);
465  else if(id==ID_cprover_string_insert_long_func)
466  res = add_axioms_for_insert_int(expr);
467  else if(id==ID_cprover_string_insert_bool_func)
468  res=add_axioms_for_insert_bool(expr);
469  else if(id==ID_cprover_string_insert_char_func)
470  res=add_axioms_for_insert_char(expr);
471  else if(id==ID_cprover_string_insert_double_func)
473  else if(id==ID_cprover_string_insert_float_func)
474  res=add_axioms_for_insert_float(expr);
475  else if(id==ID_cprover_string_substring_func)
476  res=add_axioms_for_substring(expr);
477  else if(id==ID_cprover_string_trim_func)
478  res=add_axioms_for_trim(expr);
479  else if(id==ID_cprover_string_empty_string_func)
480  res=add_axioms_for_empty_string(expr);
481  else if(id==ID_cprover_string_copy_func)
482  res=add_axioms_for_copy(expr);
483  else if(id==ID_cprover_string_of_int_hex_func)
484  res=add_axioms_from_int_hex(expr);
485  else if(id==ID_cprover_string_of_float_func)
487  else if(id==ID_cprover_string_of_float_scientific_notation_func)
489  else if(id==ID_cprover_string_of_double_func)
490  res=add_axioms_from_double(expr);
491  else if(id==ID_cprover_string_of_long_func)
492  res=add_axioms_from_long(expr);
493  else if(id==ID_cprover_string_of_bool_func)
494  res=add_axioms_from_bool(expr);
495  else if(id==ID_cprover_string_of_char_func)
496  res=add_axioms_from_char(expr);
497  else if(id==ID_cprover_string_set_length_func)
498  res=add_axioms_for_set_length(expr);
499  else if(id==ID_cprover_string_delete_func)
500  res=add_axioms_for_delete(expr);
501  else if(id==ID_cprover_string_delete_char_at_func)
503  else if(id==ID_cprover_string_replace_func)
504  res=add_axioms_for_replace(expr);
505  else if(id==ID_cprover_string_intern_func)
506  res=add_axioms_for_intern(expr);
507  else if(id==ID_cprover_string_format_func)
508  res=add_axioms_for_format(expr);
509  else if(id == ID_cprover_string_constrain_characters_func)
511  else
512  {
513  std::string msg(
514  "string_constraint_generator::function_application: unknown symbol :");
515  msg+=id2string(id);
517  }
518  return res;
519 }
520 
527 DEPRECATED("should use substring instead")
528 exprt string_constraint_generatort::add_axioms_for_copy(
530 {
531  const auto &args=f.arguments();
532  PRECONDITION(args.size() == 3 || args.size() == 5);
533  const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
534  const array_string_exprt str = get_string_expr(args[2]);
535  const typet &index_type = str.length().type();
536  const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3];
537  const exprt count = args.size() == 3 ? str.length() : args[4];
538  return add_axioms_for_substring(res, str, offset, plus_exprt(offset, count));
539 }
540 
548 {
549  PRECONDITION(f.arguments().size() == 1);
550  const array_string_exprt str = get_string_expr(f.arguments()[0]);
551  return str.length();
552 }
553 
558 {
559  return binary_relation_exprt(x, ID_ge, from_integer(0, x.type()));
560 }
561 
567 {
569  PRECONDITION(args.size()==1); // there should be exactly 1 arg to char literal
570 
571  const exprt &arg=args[0];
572  // for C programs argument to char literal should be one string constant
573  // of size 1.
574  if(arg.operands().size()==1 &&
575  arg.op0().operands().size()==1 &&
576  arg.op0().op0().operands().size()==2 &&
577  arg.op0().op0().op0().id()==ID_string_constant)
578  {
579  const string_constantt s=to_string_constant(arg.op0().op0().op0());
580  irep_idt sval=s.get_value();
581  CHECK_RETURN(sval.size()==1);
582  return from_integer(unsigned(sval[0]), arg.type());
583  }
584  else
585  {
586  // convert_char_literal unimplemented
588  // For the compiler
589  throw 0;
590  }
591 }
592 
602 {
603  PRECONDITION(f.arguments().size() == 2);
605  symbol_exprt char_sym = fresh_symbol("char", str.type().subtype());
606  lemmas.push_back(equal_exprt(char_sym, str[f.arguments()[1]]));
607  return char_sym;
608 }
609 
610 exprt minimum(const exprt &a, const exprt &b)
611 {
612  return if_exprt(binary_relation_exprt(a, ID_le, b), a, b);
613 }
614 
615 exprt maximum(const exprt &a, const exprt &b)
616 {
617  return if_exprt(binary_relation_exprt(a, ID_le, b), b, a);
618 }
619 
624 {
625  return maximum(from_integer(0, expr.type()), expr);
626 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
exprt add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
The type of an expression.
Definition: type.h:22
exprt & true_case()
Definition: std_expr.h:3393
exprt add_axioms_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset...
Generates string constraints to link results from string functions with their arguments.
std::vector< string_not_contains_constraintt > not_contains_constraints
const std::set< array_string_exprt > & get_created_strings() const
Set of strings that have been created by the generator.
exprt sum_overflows(const plus_exprt &sum)
exprt add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
application of (mathematical) function
Definition: std_expr.h:4529
exprt & object()
Definition: std_expr.h:3178
const std::vector< string_constraintt > & get_constraints() const
static irep_idt get_function_name(const function_application_exprt &expr)
exprt add_axioms_from_literal(const function_application_exprt &f)
String corresponding to an internal cprover string.
exprt & op0()
Definition: expr.h:72
exprt add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
exprt add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
const exprt & content() const
Definition: string_expr.h:216
exprt add_axioms_for_length(const function_application_exprt &f)
Length of a string.
exprt add_axioms_for_insert_float(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.insert(F) java function.
const std::vector< exprt > & get_lemmas() const
Axioms are of three kinds: universally quantified string constraint, not contains string constraints ...
const irep_idt & get_identifier() const
Definition: std_expr.h:128
exprt minimum(const exprt &a, const exprt &b)
const irep_idt & get_value() const
Definition: std_expr.h:4439
argumentst & arguments()
Definition: std_expr.h:4562
std::unordered_map< exprt, array_string_exprt, irep_hash > arrays_of_pointers
exprt add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
exprt add_axioms_for_code_point_count(const function_application_exprt &f)
Add axioms corresponding the String.codePointCount java function.
exprt add_axioms_for_offset_by_code_point(const function_application_exprt &f)
Add axioms corresponding the String.offsetByCodePointCount java function.
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
exprt associate_array_to_pointer(const function_application_exprt &f)
Associate a char array to a char pointer.
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
std::vector< symbol_exprt > boolean_symbols
typet & type()
Definition: expr.h:56
exprt associate_length_to_array(const function_application_exprt &f)
Associate an integer length to a char array.
exprt add_axioms_from_long(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(J) java function.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3199
const std::vector< string_not_contains_constraintt > & get_not_contains_constraints() const
The proper Booleans.
Definition: std_types.h:34
A constant literal expression.
Definition: std_expr.h:4422
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
exprt 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...
exprt add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
exprt 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...
void clear_constraints()
Clear all constraints and lemmas.
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
const std::vector< symbol_exprt > & get_boolean_symbols() const
Boolean symbols for the results of some string functions.
equality
Definition: std_expr.h:1354
exprt 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...
exprt add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
exprt add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
const irep_idt & id() const
Definition: irep.h:259
exprt add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
An expression denoting infinity.
Definition: std_expr.h:4692
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
exprt add_axioms_for_hash_code(const function_application_exprt &f)
Value that is identical for strings with the same content.
exprt add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
exprt::operandst argumentst
Definition: std_expr.h:4560
std::vector< symbol_exprt > index_symbols
symbol_exprt add_axioms_for_intern(const function_application_exprt &f)
Add axioms corresponding to the String.intern java function.
exprt add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
exprt add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
nonstd::optional< T > optionalt
Definition: optional.h:35
boolean AND
Definition: std_expr.h:2255
exprt add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false)
Test if the target is a suffix of the string.
exprt & op1()
Definition: expr.h:75
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:230
inequality
Definition: std_expr.h:1406
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
exprt add_axioms_for_set_length(const function_application_exprt &f)
Reduce or extend a string to have the given length.
exprt add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
The plus expression.
Definition: std_expr.h:893
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
exprt add_axioms_for_char_literal(const function_application_exprt &f)
add axioms stating that the returned value is equal to the argument
symbol_exprt operator()(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
bitvector_typet index_type()
Definition: c_types.cpp:16
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:184
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
array_string_exprt of_argument(const exprt &arg)
Converts a struct containing a length and pointer to an array.
exprt add_axioms_for_insert_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(D) java function
exprt & false_case()
Definition: std_expr.h:3403
exprt add_axioms_for_insert_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(I) java function
Various predicates over pointers in programs.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
symbol_exprt & function()
Definition: std_expr.h:4550
#define DEPRECATED(msg)
Definition: deprecate.h:23
void insert(const exprt &pointer_expr, array_string_exprt &array)
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
#define UNIMPLEMENTED
Definition: invariant.h:287
exprt 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...
exprt add_axioms_for_char_at(const function_application_exprt &f)
Character at a given position.
const string_constantt & to_string_constant(const exprt &expr)
exprt 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...
exprt 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(st...
void 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.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
bool is_refined_string_type(const typet &type)
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
exprt 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...
exprt add_axioms_from_bool(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(Z) java function.
exprt add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
irep_idt get_object_name() const
Definition: ssa_expr.h:46
exprt add_axioms_for_format(const function_application_exprt &f)
Formatted string using a format string and list of arguments.
std::set< array_string_exprt > created_strings
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:173
const exprt & length() const
Definition: string_expr.h:206
#define string_refinement_invariantt(reason)
Universally quantified string constraint
exprt add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
arrays with given size
Definition: std_types.h:1013
exprt add_axioms_for_constrain_characters(const function_application_exprt &f)
Add axioms to ensure all characters of a string belong to a given set.
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const char * c_str() const
Definition: dstring.h:84
exprt add_axioms_for_insert_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(Z) java function
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
Definition: type.h:33
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
const irep_idt & get_value() const
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
std::vector< string_constraintt > constraints
std::unordered_map< array_string_exprt, symbol_exprt, irep_hash > length_of_array
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt add_axioms_from_char(const function_application_exprt &f)
Conversion from char to string.
const std::vector< symbol_exprt > & get_index_symbols() const
Symbols used in existential quantifications.
struct constructor from list of elements
Definition: std_expr.h:1815
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
bitvector_typet char_type()
Definition: c_types.cpp:114
exprt add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
exprt maximum(const exprt &a, const exprt &b)
exprt add_axioms_for_insert_char(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.insert(C) java function.
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:162
exprt 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 ...
symbol_generatort & fresh_symbol
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive