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(qvar, start, end, char_in_set);
328  constraints.push_back(sc);
329 }
330 
343 {
344  const auto &args = f.arguments();
345  PRECONDITION(3 <= args.size() && args.size() <= 5);
346  PRECONDITION(args[2].type().id() == ID_string);
347  PRECONDITION(args[2].id() == ID_constant);
348  const array_string_exprt s = char_array_of_pointer(args[1], args[0]);
349  const irep_idt &char_set_string = to_constant_expr(args[2]).get_value();
350  const exprt &start =
351  args.size() >= 4 ? args[3] : from_integer(0, s.length().type());
352  const exprt &end = args.size() >= 5 ? args[4] : s.length();
353  add_constraint_on_characters(s, start, end, char_set_string.c_str());
354  return from_integer(0, get_return_code_type());
355 }
356 
359 array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length)
360 {
361  const array_typet array_type(pointer.type().subtype(), length);
362  return make_char_array_for_char_pointer(pointer, array_type);
363 }
364 
369  const exprt &pointer,
370  const exprt &length)
371 {
372  return *created_strings.insert(array_pool.find(pointer, length)).first;
373 }
374 
376 {
377  return find(str.content(), str.length());
378 }
379 
381 {
382  const auto string_argument = expr_checked_cast<struct_exprt>(arg);
383  return find(string_argument.op1(), string_argument.op0());
384 }
385 
387 {
388  const exprt &name = expr.function();
389  PRECONDITION(name.id() == ID_symbol);
390  return is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
391  : to_symbol_expr(name).get_identifier();
392 }
393 
395  const function_application_exprt &expr)
396 {
397  const irep_idt &id = get_function_name(expr);
398  if(id == ID_cprover_associate_array_to_pointer_func)
399  return associate_array_to_pointer(expr);
400  else if(id == ID_cprover_associate_length_to_array_func)
401  return associate_length_to_array(expr);
402  return {};
403 }
404 
411  const function_application_exprt &expr)
412 {
413  const irep_idt &id = get_function_name(expr);
414  exprt res;
415 
416  if(id==ID_cprover_char_literal_func)
417  res=add_axioms_for_char_literal(expr);
418  else if(id==ID_cprover_string_length_func)
419  res=add_axioms_for_length(expr);
420  else if(id==ID_cprover_string_equal_func)
421  res=add_axioms_for_equals(expr);
422  else if(id==ID_cprover_string_equals_ignore_case_func)
424  else if(id==ID_cprover_string_is_empty_func)
425  res=add_axioms_for_is_empty(expr);
426  else if(id==ID_cprover_string_char_at_func)
427  res=add_axioms_for_char_at(expr);
428  else if(id==ID_cprover_string_is_prefix_func)
429  res=add_axioms_for_is_prefix(expr);
430  else if(id==ID_cprover_string_is_suffix_func)
431  res=add_axioms_for_is_suffix(expr);
432  else if(id==ID_cprover_string_startswith_func)
433  res=add_axioms_for_is_prefix(expr, true);
434  else if(id==ID_cprover_string_endswith_func)
435  res=add_axioms_for_is_suffix(expr, true);
436  else if(id==ID_cprover_string_contains_func)
437  res=add_axioms_for_contains(expr);
438  else if(id==ID_cprover_string_hash_code_func)
439  res=add_axioms_for_hash_code(expr);
440  else if(id==ID_cprover_string_index_of_func)
441  res=add_axioms_for_index_of(expr);
442  else if(id==ID_cprover_string_last_index_of_func)
444  else if(id==ID_cprover_string_parse_int_func)
445  res=add_axioms_for_parse_int(expr);
446  else if(id==ID_cprover_string_code_point_at_func)
448  else if(id==ID_cprover_string_code_point_before_func)
450  else if(id==ID_cprover_string_code_point_count_func)
452  else if(id==ID_cprover_string_offset_by_code_point_func)
454  else if(id==ID_cprover_string_compare_to_func)
455  res=add_axioms_for_compare_to(expr);
456  else if(id==ID_cprover_string_literal_func)
457  res=add_axioms_from_literal(expr);
458  else if(id==ID_cprover_string_concat_func)
459  res=add_axioms_for_concat(expr);
460  else if(id==ID_cprover_string_concat_char_func)
461  res=add_axioms_for_concat_char(expr);
462  else if(id==ID_cprover_string_concat_code_point_func)
464  else if(id==ID_cprover_string_insert_func)
465  res=add_axioms_for_insert(expr);
466  else if(id==ID_cprover_string_insert_int_func)
467  res=add_axioms_for_insert_int(expr);
468  else if(id==ID_cprover_string_insert_long_func)
469  res = add_axioms_for_insert_int(expr);
470  else if(id==ID_cprover_string_insert_bool_func)
471  res=add_axioms_for_insert_bool(expr);
472  else if(id==ID_cprover_string_insert_char_func)
473  res=add_axioms_for_insert_char(expr);
474  else if(id==ID_cprover_string_insert_double_func)
476  else if(id==ID_cprover_string_insert_float_func)
477  res=add_axioms_for_insert_float(expr);
478  else if(id==ID_cprover_string_substring_func)
479  res=add_axioms_for_substring(expr);
480  else if(id==ID_cprover_string_trim_func)
481  res=add_axioms_for_trim(expr);
482  else if(id==ID_cprover_string_to_lower_case_func)
484  else if(id==ID_cprover_string_to_upper_case_func)
486  else if(id==ID_cprover_string_char_set_func)
487  res=add_axioms_for_char_set(expr);
488  else if(id==ID_cprover_string_empty_string_func)
489  res=add_axioms_for_empty_string(expr);
490  else if(id==ID_cprover_string_copy_func)
491  res=add_axioms_for_copy(expr);
492  else if(id==ID_cprover_string_of_int_func)
493  res=add_axioms_from_int(expr);
494  else if(id==ID_cprover_string_of_int_hex_func)
495  res=add_axioms_from_int_hex(expr);
496  else if(id==ID_cprover_string_of_float_func)
498  else if(id==ID_cprover_string_of_float_scientific_notation_func)
500  else if(id==ID_cprover_string_of_double_func)
501  res=add_axioms_from_double(expr);
502  else if(id==ID_cprover_string_of_long_func)
503  res=add_axioms_from_long(expr);
504  else if(id==ID_cprover_string_of_bool_func)
505  res=add_axioms_from_bool(expr);
506  else if(id==ID_cprover_string_of_char_func)
507  res=add_axioms_from_char(expr);
508  else if(id==ID_cprover_string_set_length_func)
509  res=add_axioms_for_set_length(expr);
510  else if(id==ID_cprover_string_delete_func)
511  res=add_axioms_for_delete(expr);
512  else if(id==ID_cprover_string_delete_char_at_func)
514  else if(id==ID_cprover_string_replace_func)
515  res=add_axioms_for_replace(expr);
516  else if(id==ID_cprover_string_intern_func)
517  res=add_axioms_for_intern(expr);
518  else if(id==ID_cprover_string_format_func)
519  res=add_axioms_for_format(expr);
520  else if(id == ID_cprover_string_constrain_characters_func)
522  else
523  {
524  std::string msg(
525  "string_constraint_generator::function_application: unknown symbol :");
526  msg+=id2string(id);
528  }
529  return res;
530 }
531 
538 DEPRECATED("should use substring instead")
539 exprt string_constraint_generatort::add_axioms_for_copy(
541 {
542  const auto &args=f.arguments();
543  PRECONDITION(args.size() == 3 || args.size() == 5);
544  const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
545  const array_string_exprt str = get_string_expr(args[2]);
546  const typet &index_type = str.length().type();
547  const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3];
548  const exprt count = args.size() == 3 ? str.length() : args[4];
549  return add_axioms_for_substring(res, str, offset, plus_exprt(offset, count));
550 }
551 
559 {
560  PRECONDITION(f.arguments().size() == 1);
561  const array_string_exprt str = get_string_expr(f.arguments()[0]);
562  return str.length();
563 }
564 
569 {
570  return binary_relation_exprt(x, ID_ge, from_integer(0, x.type()));
571 }
572 
578 {
580  PRECONDITION(args.size()==1); // there should be exactly 1 arg to char literal
581 
582  const exprt &arg=args[0];
583  // for C programs argument to char literal should be one string constant
584  // of size 1.
585  if(arg.operands().size()==1 &&
586  arg.op0().operands().size()==1 &&
587  arg.op0().op0().operands().size()==2 &&
588  arg.op0().op0().op0().id()==ID_string_constant)
589  {
590  const string_constantt s=to_string_constant(arg.op0().op0().op0());
591  irep_idt sval=s.get_value();
592  CHECK_RETURN(sval.size()==1);
593  return from_integer(unsigned(sval[0]), arg.type());
594  }
595  else
596  {
597  // convert_char_literal unimplemented
599  // For the compiler
600  throw 0;
601  }
602 }
603 
613 {
614  PRECONDITION(f.arguments().size() == 2);
616  symbol_exprt char_sym = fresh_symbol("char", str.type().subtype());
617  lemmas.push_back(equal_exprt(char_sym, str[f.arguments()[1]]));
618  return char_sym;
619 }
620 
621 exprt minimum(const exprt &a, const exprt &b)
622 {
623  return if_exprt(binary_relation_exprt(a, ID_le, b), a, b);
624 }
625 
626 exprt maximum(const exprt &a, const exprt &b)
627 {
628  return if_exprt(binary_relation_exprt(a, ID_le, b), b, a);
629 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
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:3395
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:43
application of (mathematical) function
Definition: std_expr.h:4531
exprt & object()
Definition: std_expr.h:3180
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_from_int(const function_application_exprt &f)
Convert an integer to a string.
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:4441
argumentst & arguments()
Definition: std_expr.h:4564
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:3361
exprt & cond()
Definition: std_expr.h:3385
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:3201
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:4424
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
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:205
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)
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal...
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:189
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:4694
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
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:4562
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:230
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
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
exprt add_axioms_for_char_set(const function_application_exprt &f)
Set a character to a specific value at an index of the string.
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:3405
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:4465
symbol_exprt & function()
Definition: std_expr.h:4552
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:266
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:1045
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_to_lower_case(const function_application_exprt &f)
Conversion of a string to lower case.
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:1004
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:72
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
const irep_idt & get_value() const
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
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
exprt add_axioms_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, const exprt &c)
Add axioms enforcing that res is the concatenation of s1 with character c.
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(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.
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 add_axioms_for_to_upper_case(const function_application_exprt &f)
Conversion of a string to upper case.
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive