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 <iterator>
23 #include <limits>
25 
26 #include <util/arith_tools.h>
28 #include <util/ssa_expr.h>
29 #include <util/string_constant.h>
30 #include <util/deprecate.h>
31 
33  : array_pool(fresh_symbol), ns(ns)
34 {
35 }
36 
42 operator()(const irep_idt &prefix, const typet &type)
43 {
44  std::ostringstream buf;
45  buf << "string_refinement#" << prefix << "#" << ++symbol_count;
46  irep_idt name(buf.str());
47  symbol_exprt result(name, type);
48 #ifdef DEBUG
49  created_symbols.push_back(result);
50 #endif
51  return result;
52 }
53 
55 {
56  PRECONDITION(sum.operands().size() == 2);
57  const exprt zero = from_integer(0, sum.op0().type());
58  const binary_relation_exprt op0_negative(sum.op0(), ID_lt, zero);
59  const binary_relation_exprt op1_negative(sum.op1(), ID_lt, zero);
60  const binary_relation_exprt sum_negative(sum, ID_lt, zero);
61 
62  // overflow happens when we add two values of same sign but their sum has a
63  // different sign
64  return and_exprt(
65  equal_exprt(op0_negative, op1_negative),
66  notequal_exprt(op1_negative, sum_negative));
67 }
68 
73 {
74  if(s.length() == infinity_exprt(s.length().type()))
75  {
76  auto it = length_of_array.find(s);
77  if(it != length_of_array.end())
78  return it->second;
79  }
80  return s.length();
81 }
82 
88 {
89  symbol_exprt length = fresh_symbol("string_length", index_type);
90  array_typet array_type(char_type, length);
91  symbol_exprt content = fresh_symbol("string_content", array_type);
93  created_strings_value.insert(str);
94  return str;
95 }
96 
97 // Make a new char array for a char pointer. The size of the char array is a
98 // variable with no constraint.
100  const exprt &char_pointer,
101  const typet &char_array_type)
102 {
103  PRECONDITION(char_pointer.type().id() == ID_pointer);
104  PRECONDITION(char_array_type.id() == ID_array);
105  PRECONDITION(
106  char_array_type.subtype().id() == ID_unsignedbv ||
107  char_array_type.subtype().id() == ID_signedbv);
108 
109  if(char_pointer.id() == ID_if)
110  {
111  const if_exprt &if_expr = to_if_expr(char_pointer);
112  const array_string_exprt t =
113  make_char_array_for_char_pointer(if_expr.true_case(), char_array_type);
114  const array_string_exprt f =
115  make_char_array_for_char_pointer(if_expr.false_case(), char_array_type);
116  const array_typet array_type(
117  char_array_type.subtype(),
118  if_exprt(
119  if_expr.cond(),
120  to_array_type(t.type()).size(),
121  to_array_type(f.type()).size()));
122  return to_array_string_expr(if_exprt(if_expr.cond(), t, f, array_type));
123  }
124  const bool is_constant_array =
125  char_pointer.id() == ID_address_of &&
126  (to_address_of_expr(char_pointer).object().id() == ID_index) &&
127  char_pointer.op0().op0().id() == ID_array;
128  if(is_constant_array)
129  {
130  return to_array_string_expr(
131  to_index_expr(to_address_of_expr(char_pointer).object()).array());
132  }
133  const std::string symbol_name = "char_array_" + id2string(char_pointer.id());
134  const auto array_sym =
135  to_array_string_expr(fresh_symbol(symbol_name, char_array_type));
136  const auto insert_result =
137  arrays_of_pointers.insert({char_pointer, array_sym});
138  return to_array_string_expr(insert_result.first->second);
139 }
140 
142  const exprt &pointer_expr,
143  array_string_exprt &array_expr)
144 {
145  const exprt &length = array_expr.length();
146  if(length == infinity_exprt(length.type()))
147  {
148  auto pair = length_of_array.insert(
149  std::make_pair(array_expr, fresh_symbol("string_length", length.type())));
150  array_expr.length() = pair.first->second;
151  }
152 
153  const auto it_bool =
154  arrays_of_pointers.insert(std::make_pair(pointer_expr, array_expr));
155  created_strings_value.insert(array_expr);
156  INVARIANT(
157  it_bool.second, "should not associate two arrays to the same pointer");
158 }
159 
160 const std::set<array_string_exprt> &array_poolt::created_strings() const
161 {
162  return created_strings_value;
163 }
164 
173 {
174  PRECONDITION(f.arguments().size() == 2);
175 
179  f.arguments()[0].id() == ID_index ? to_index_expr(f.arguments()[0]).array()
180  : f.arguments()[0]);
181 
182  const exprt &pointer_expr = f.arguments()[1];
183  array_pool.insert(pointer_expr, array_expr);
184  // created_strings.emplace(to_array_string_expr(array_expr));
185  return from_integer(0, f.type());
186 }
187 
195 {
196  PRECONDITION(f.arguments().size() == 2);
198  const exprt &new_length = f.arguments()[1];
199 
200  const auto &length = array_pool.get_length(array_expr);
201  constraints.existential.push_back(equal_exprt(length, new_length));
202  return from_integer(0, f.type());
203 }
204 
211 {
213  const refined_string_exprt &str = to_string_expr(expr);
214  return char_array_of_pointer(pool, str.content(), str.length());
215 }
216 
218 {
219  existential.clear();
220  universal.clear();
221  not_contains.clear();
222 }
223 
226 {
227  std::move(
228  other.existential.begin(),
229  other.existential.end(),
230  std::back_inserter(result.existential));
231  std::move(
232  other.universal.begin(),
233  other.universal.end(),
234  std::back_inserter(result.universal));
235  std::move(
236  other.not_contains.begin(),
237  other.not_contains.end(),
238  std::back_inserter(result.not_contains));
239 }
240 
255  symbol_generatort &fresh_symbol,
256  const array_string_exprt &s,
257  const exprt &start,
258  const exprt &end,
259  const std::string &char_set)
260 {
261  // Parse char_set
262  PRECONDITION(char_set.length() == 3);
263  PRECONDITION(char_set[1] == '-');
264  const char &low_char = char_set[0];
265  const char &high_char = char_set[2];
266 
267  // Add constraint
268  const symbol_exprt qvar = fresh_symbol("char_constr", s.length().type());
269  const exprt chr = s[qvar];
270  const and_exprt char_in_set(
271  binary_relation_exprt(chr, ID_ge, from_integer(low_char, chr.type())),
272  binary_relation_exprt(chr, ID_le, from_integer(high_char, chr.type())));
273  const string_constraintt sc(
274  qvar, zero_if_negative(start), zero_if_negative(end), char_in_set);
275  return {{}, {sc}, {}};
276 }
277 
290 std::pair<exprt, string_constraintst> add_axioms_for_constrain_characters(
291  symbol_generatort &fresh_symbol,
293  array_poolt &array_pool)
294 {
295  const auto &args = f.arguments();
296  PRECONDITION(3 <= args.size() && args.size() <= 5);
297  PRECONDITION(args[2].type().id() == ID_string);
298  PRECONDITION(args[2].id() == ID_constant);
299 
300  const array_string_exprt s =
301  char_array_of_pointer(array_pool, args[1], args[0]);
302  const irep_idt &char_set_string = to_constant_expr(args[2]).get_value();
303  const exprt &start =
304  args.size() >= 4 ? args[3] : from_integer(0, s.length().type());
305  const exprt &end = args.size() >= 5 ? args[4] : s.length();
306  auto constraints = add_constraint_on_characters(
307  fresh_symbol, s, start, end, char_set_string.c_str());
308  return {from_integer(0, get_return_code_type()), std::move(constraints)};
309 }
310 
313 const array_string_exprt &
314 array_poolt::find(const exprt &pointer, const exprt &length)
315 {
316  const array_typet array_type(pointer.type().subtype(), length);
317  const array_string_exprt array =
318  make_char_array_for_char_pointer(pointer, array_type);
319  return *created_strings_value.insert(array).first;
320 }
321 
326  array_poolt &pool,
327  const exprt &pointer,
328  const exprt &length)
329 {
330  return pool.find(pointer, length);
331 }
332 
334 {
335  const auto string_argument = expr_checked_cast<struct_exprt>(arg);
336  return array_pool.find(string_argument.op1(), string_argument.op0());
337 }
338 
340 {
341  return signedbv_typet(32);
342 }
343 
345 {
346  const exprt &name = expr.function();
347  PRECONDITION(name.id() == ID_symbol);
348  return is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
349  : to_symbol_expr(name).get_identifier();
350 }
351 
353  const function_application_exprt &expr)
354 {
355  const irep_idt &id = get_function_name(expr);
356  if(id == ID_cprover_associate_array_to_pointer_func)
357  return associate_array_to_pointer(expr);
358  else if(id == ID_cprover_associate_length_to_array_func)
359  return associate_length_to_array(expr);
360  return {};
361 }
362 
369 std::pair<exprt, string_constraintst>
371  symbol_generatort &fresh_symbol,
372  const function_application_exprt &expr)
373 {
374  const irep_idt &id = get_function_name(expr);
375 
376  if(id==ID_cprover_char_literal_func)
377  return add_axioms_for_char_literal(expr);
378  else if(id==ID_cprover_string_length_func)
379  return add_axioms_for_length(expr, array_pool);
380  else if(id==ID_cprover_string_equal_func)
382  else if(id==ID_cprover_string_equals_ignore_case_func)
384  else if(id==ID_cprover_string_is_empty_func)
386  else if(id==ID_cprover_string_char_at_func)
388  else if(id==ID_cprover_string_is_prefix_func)
389  return add_axioms_for_is_prefix(fresh_symbol, expr, false, array_pool);
390  else if(id==ID_cprover_string_is_suffix_func)
391  return add_axioms_for_is_suffix(fresh_symbol, expr, false, array_pool);
392  else if(id==ID_cprover_string_startswith_func)
393  return add_axioms_for_is_prefix(fresh_symbol, expr, true, array_pool);
394  else if(id==ID_cprover_string_endswith_func)
395  return add_axioms_for_is_suffix(fresh_symbol, expr, true, array_pool);
396  else if(id==ID_cprover_string_contains_func)
398  else if(id==ID_cprover_string_hash_code_func)
400  else if(id==ID_cprover_string_index_of_func)
402  else if(id==ID_cprover_string_last_index_of_func)
404  else if(id==ID_cprover_string_parse_int_func)
406  else if(id==ID_cprover_string_code_point_at_func)
408  else if(id==ID_cprover_string_code_point_before_func)
410  else if(id==ID_cprover_string_code_point_count_func)
412  else if(id==ID_cprover_string_offset_by_code_point_func)
414  else if(id==ID_cprover_string_compare_to_func)
416  else if(id==ID_cprover_string_literal_func)
418  else if(id==ID_cprover_string_concat_code_point_func)
420  else if(id==ID_cprover_string_insert_func)
422  else if(id==ID_cprover_string_insert_int_func)
424  else if(id==ID_cprover_string_insert_long_func)
426  else if(id==ID_cprover_string_insert_bool_func)
428  else if(id==ID_cprover_string_insert_char_func)
430  else if(id==ID_cprover_string_insert_double_func)
432  else if(id==ID_cprover_string_insert_float_func)
434  else if(id==ID_cprover_string_substring_func)
436  else if(id==ID_cprover_string_trim_func)
438  else if(id==ID_cprover_string_empty_string_func)
439  return add_axioms_for_empty_string(expr);
440  else if(id==ID_cprover_string_copy_func)
442  else if(id==ID_cprover_string_of_int_hex_func)
443  return add_axioms_from_int_hex(expr, array_pool);
444  else if(id==ID_cprover_string_of_float_func)
446  else if(id==ID_cprover_string_of_float_scientific_notation_func)
448  fresh_symbol, expr, array_pool, ns);
449  else if(id==ID_cprover_string_of_double_func)
451  else if(id==ID_cprover_string_of_long_func)
452  return add_axioms_from_long(expr, array_pool, ns);
453  else if(id==ID_cprover_string_of_bool_func)
454  return add_axioms_from_bool(expr, array_pool);
455  else if(id==ID_cprover_string_of_char_func)
456  return add_axioms_from_char(expr, array_pool);
457  else if(id==ID_cprover_string_set_length_func)
459  else if(id==ID_cprover_string_delete_func)
461  else if(id==ID_cprover_string_delete_char_at_func)
463  else if(id==ID_cprover_string_replace_func)
465  else if(id==ID_cprover_string_intern_func)
466  return add_axioms_for_intern(fresh_symbol, expr);
467  else if(id==ID_cprover_string_format_func)
469  else if(id == ID_cprover_string_constrain_characters_func)
471  else
472  {
473  std::string msg(
474  "string_constraint_generator::function_application: unknown symbol :");
475  msg+=id2string(id);
477  }
478  UNREACHABLE;
479 }
480 
489 DEPRECATED("should use substring instead")
491  symbol_generatort &fresh_symbol,
493  array_poolt &array_pool)
494 {
495  const auto &args=f.arguments();
496  PRECONDITION(args.size() == 3 || args.size() == 5);
497  const array_string_exprt res =
498  char_array_of_pointer(array_pool, args[1], args[0]);
499  const array_string_exprt str = get_string_expr(array_pool, args[2]);
500  const typet &index_type = str.length().type();
501  const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3];
502  const exprt count = args.size() == 3 ? str.length() : args[4];
504  fresh_symbol, res, str, offset, plus_exprt(offset, count));
505 }
506 
513 std::pair<exprt, string_constraintst> add_axioms_for_length(
515  array_poolt &array_pool)
516 {
517  PRECONDITION(f.arguments().size() == 1);
518  const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
519  return {str.length(), {}};
520 }
521 
525 {
526  return binary_relation_exprt(x, ID_ge, from_integer(0, x.type()));
527 }
528 
532 std::pair<exprt, string_constraintst> add_axioms_for_char_literal(
534 {
536  PRECONDITION(args.size()==1); // there should be exactly 1 arg to char literal
537 
538  const exprt &arg=args[0];
539  // for C programs argument to char literal should be one string constant
540  // of size 1.
541  if(arg.operands().size()==1 &&
542  arg.op0().operands().size()==1 &&
543  arg.op0().op0().operands().size()==2 &&
544  arg.op0().op0().op0().id()==ID_string_constant)
545  {
546  const string_constantt s=to_string_constant(arg.op0().op0().op0());
547  irep_idt sval=s.get_value();
548  CHECK_RETURN(sval.size()==1);
549  return {from_integer(unsigned(sval[0]), arg.type()), {}};
550  }
551  else
552  {
554  }
555 }
556 
566 std::pair<exprt, string_constraintst> add_axioms_for_char_at(
567  symbol_generatort &fresh_symbol,
569  array_poolt &array_pool)
570 {
571  PRECONDITION(f.arguments().size() == 2);
572  array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
573  symbol_exprt char_sym = fresh_symbol("char", str.type().subtype());
574  const exprt constraint = equal_exprt(char_sym, str[f.arguments()[1]]);
575  return {char_sym, {{constraint}}};
576 }
577 
578 exprt minimum(const exprt &a, const exprt &b)
579 {
580  return if_exprt(binary_relation_exprt(a, ID_le, b), a, b);
581 }
582 
583 exprt maximum(const exprt &a, const exprt &b)
584 {
585  return if_exprt(binary_relation_exprt(a, ID_le, b), b, a);
586 }
587 
592 {
593  return maximum(from_integer(0, expr.type()), expr);
594 }
595 
598 std::pair<exprt, string_constraintst> combine_results(
599  std::pair<exprt, string_constraintst> result1,
600  std::pair<exprt, string_constraintst> result2)
601 {
602  const exprt return_code = maximum(result1.first, result2.first);
603  merge(result2.second, std::move(result1.second));
604  return {return_code, std::move(result2.second)};
605 }
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:532
get_function_name
static irep_idt get_function_name(const function_application_exprt &expr)
Definition: string_constraint_generator_main.cpp:344
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
string_constraint_generatort::add_axioms_for_intern
std::pair< symbol_exprt, string_constraintst > add_axioms_for_intern(symbol_generatort &fresh_symbol, const function_application_exprt &f)
Add axioms corresponding to the String.intern java function.
Definition: string_constraint_generator_comparison.cpp:310
function_application_exprt::arguments
argumentst & arguments()
Definition: std_expr.h:4506
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
dstringt::c_str
const char * c_str() const
Definition: dstring.h:86
string_constraint_generatort::associate_length_to_array
exprt associate_length_to_array(const function_application_exprt &f)
Associate an integer length to a char array.
Definition: string_constraint_generator_main.cpp:193
symbol_generatort::operator()
symbol_exprt operator()(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
Definition: string_constraint_generator_main.cpp:42
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:63
typet::subtype
const typet & subtype() const
Definition: type.h:38
array_poolt::length_of_array
std::unordered_map< array_string_exprt, symbol_exprt, irep_hash > length_of_array
Definition: string_constraint_generator.h:80
is_positive
exprt is_positive(const exprt &x)
Definition: string_constraint_generator_main.cpp:524
add_axioms_for_delete
std::pair< exprt, string_constraintst > add_axioms_for_delete(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &array_pool)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
Definition: string_constraint_generator_transformation.cpp:374
add_axioms_for_concat_code_point
std::pair< exprt, string_constraintst > add_axioms_for_concat_code_point(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
Definition: string_constraint_generator_concat.cpp:143
arith_tools.h
add_axioms_for_substring
std::pair< exprt, string_constraintst > add_axioms_for_substring(symbol_generatort &fresh_symbol, 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...
Definition: string_constraint_generator_transformation.cpp:124
add_axioms_for_is_suffix
std::pair< exprt, string_constraintst > add_axioms_for_is_suffix(symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool)
Test if the target is a suffix of the string.
Definition: string_constraint_generator_testing.cpp:168
address_of_exprt::object
exprt & object()
Definition: std_expr.h:3265
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:485
to_string_expr
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:161
typet
The type of an expression, extends irept.
Definition: type.h:27
add_axioms_from_char
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
Conversion from char to string.
Definition: string_constraint_generator_valueof.cpp:294
add_axioms_for_string_of_float
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
String representation of a float value.
Definition: string_constraint_generator_float.cpp:158
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
array_poolt::get_length
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
Definition: string_constraint_generator_main.cpp:72
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:598
add_axioms_for_insert_float
std::pair< exprt, string_constraintst > add_axioms_for_insert_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the StringBuilder.insert(F) java function.
Definition: string_constraint_generator_insert.cpp:252
string_constraintt
Definition: string_constraint.h:58
char_array_of_pointer
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Definition: string_constraint_generator_main.cpp:325
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
add_axioms_for_insert_int
std::pair< exprt, string_constraintst > add_axioms_for_insert_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
add axioms corresponding to the StringBuilder.insert(I) java function
Definition: string_constraint_generator_insert.cpp:144
pointer_predicates.h
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:216
add_axioms_for_format
std::pair< exprt, string_constraintst > add_axioms_for_format(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const messaget &message, const namespacet &ns)
Formatted string using a format string and list of arguments.
Definition: string_constraint_generator_format.cpp:510
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:133
and_exprt
Boolean AND.
Definition: std_expr.h:2409
add_axioms_from_literal
std::pair< exprt, string_constraintst > add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
String corresponding to an internal cprover string.
Definition: string_constraint_generator_constants.cpp:114
string_refinement_invariant.h
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:34
add_axioms_from_double
std::pair< exprt, string_constraintst > add_axioms_from_double(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the String.valueOf(D) java function.
Definition: string_constraint_generator_float.cpp:177
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
ssa_exprt::get_object_name
irep_idt get_object_name() const
Definition: ssa_expr.h:46
add_axioms_for_insert_char
std::pair< exprt, string_constraintst > add_axioms_for_insert_char(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the StringBuilder.insert(C) java function.
Definition: string_constraint_generator_insert.cpp:196
string_constraint_generatort::add_axioms_for_function_application
std::pair< exprt, string_constraintst > add_axioms_for_function_application(symbol_generatort &fresh_symbol, 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:370
exprt::op0
exprt & op0()
Definition: expr.h:84
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
string_constraint_generatort::make_array_pointer_association
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
Definition: string_constraint_generator_main.cpp:352
string_constraint_generatort::string_constraint_generatort
string_constraint_generatort(const namespacet &ns)
Definition: string_constraint_generator_main.cpp:32
minimum
exprt minimum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:578
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
string_constantt
Definition: string_constant.h:15
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: std_expr.h:4484
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:135
add_axioms_for_insert_bool
std::pair< exprt, string_constraintst > add_axioms_for_insert_bool(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
add axioms corresponding to the StringBuilder.insert(Z) java function
Definition: string_constraint_generator_insert.cpp:171
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4625
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
notequal_exprt
Disequality.
Definition: std_expr.h:1545
refined_string_exprt
Definition: string_expr.h:114
refined_string_exprt::length
const exprt & length() const
Definition: string_expr.h:139
add_axioms_for_copy
std::pair< exprt, string_constraintst > add_axioms_for_copy(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
add axioms to say that the returned string expression is equal to the argument of the function applic...
Definition: string_constraint_generator_main.cpp:490
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
add_axioms_for_is_empty
std::pair< exprt, string_constraintst > add_axioms_for_is_empty(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms stating that the returned value is true exactly when the argument string is empty.
Definition: string_constraint_generator_testing.cpp:126
symbol_generatort
Generation of fresh symbols of a given type.
Definition: string_constraint_generator.h:32
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:179
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:225
add_axioms_from_float_scientific_notation
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms to write the float in scientific notation.
Definition: string_constraint_generator_float.cpp:344
add_axioms_for_constrain_characters
std::pair< exprt, string_constraintst > add_axioms_for_constrain_characters(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms to ensure all characters of a string belong to a given set.
Definition: string_constraint_generator_main.cpp:290
add_axioms_from_long
std::pair< exprt, string_constraintst > add_axioms_from_long(const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the String.valueOf(J) java function.
Definition: string_constraint_generator_valueof.cpp:45
string_constraint_generatort::ns
const namespacet ns
Definition: string_constraint_generator.h:139
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
deprecate.h
add_constraint_on_characters
string_constraintst add_constraint_on_characters(symbol_generatort &fresh_symbol, 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:254
array_poolt::created_strings_value
std::set< array_string_exprt > created_strings_value
Definition: string_constraint_generator.h:86
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
string_constraint_generatort::constraints
string_constraintst constraints
Definition: string_constraint_generator.h:137
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1278
exprt::op1
exprt & op1()
Definition: expr.h:87
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
of_argument
array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)
Converts a struct containing a length and pointer to an array.
Definition: string_constraint_generator_main.cpp:333
get_string_expr
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
Definition: string_constraint_generator_main.cpp:210
add_axioms_for_trim
std::pair< exprt, string_constraintst > add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Remove leading and trailing whitespaces.
Definition: string_constraint_generator_transformation.cpp:183
string_constraintst::clear
void clear()
Clear all constraints.
Definition: string_constraint_generator_main.cpp:217
add_axioms_for_equals_ignore_case
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Equality of the content ignoring case of characters.
Definition: string_constraint_generator_comparison.cpp:132
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
add_axioms_for_code_point_count
std::pair< exprt, string_constraintst > add_axioms_for_code_point_count(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Add axioms corresponding the String.codePointCount java function.
Definition: string_constraint_generator_code_points.cpp:193
add_axioms_for_char_at
std::pair< exprt, string_constraintst > add_axioms_for_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Character at a given position.
Definition: string_constraint_generator_main.cpp:566
add_axioms_for_equals
std::pair< exprt, string_constraintst > add_axioms_for_equals(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Equality of the content of two strings.
Definition: string_constraint_generator_comparison.cpp:31
add_axioms_for_last_index_of
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, 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:346
to_array_string_expr
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:101
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
symbol_generatort::symbol_count
unsigned symbol_count
Definition: string_constraint_generator.h:39
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
add_axioms_for_insert_double
std::pair< exprt, string_constraintst > add_axioms_for_insert_double(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
add axioms corresponding to the StringBuilder.insert(D) java function
Definition: string_constraint_generator_insert.cpp:223
ssa_expr.h
add_axioms_for_code_point_at
std::pair< exprt, string_constraintst > add_axioms_for_code_point_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
add axioms corresponding to the String.codePointAt java function
Definition: string_constraint_generator_code_points.cpp:122
refined_string_exprt::content
const exprt & content() const
Definition: string_expr.h:149
array_typet
Arrays with given size.
Definition: std_types.h:1000
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
array_poolt::find
const array_string_exprt & find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: string_constraint_generator_main.cpp:314
array_poolt::insert
void insert(const exprt &pointer_expr, array_string_exprt &array)
Definition: string_constraint_generator_main.cpp:141
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:497
string_constraint_generatort::add_axioms_for_hash_code
std::pair< exprt, string_constraintst > add_axioms_for_hash_code(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
Value that is identical for strings with the same content.
Definition: string_constraint_generator_comparison.cpp:190
string_constraint_generatort::associate_array_to_pointer
exprt associate_array_to_pointer(const function_application_exprt &f)
Associate a char array to a char pointer.
Definition: string_constraint_generator_main.cpp:171
add_axioms_for_replace
std::pair< exprt, string_constraintst > add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Replace a character by another in a string.
Definition: string_constraint_generator_transformation.cpp:297
string_constraint_generatort::message
const messaget message
Definition: string_constraint_generator.h:169
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
string_refinement_invariantt
#define string_refinement_invariantt(reason)
Definition: string_refinement_invariant.h:12
add_axioms_for_insert
std::pair< exprt, string_constraintst > add_axioms_for_insert(symbol_generatort &fresh_symbol, 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.
Definition: string_constraint_generator_insert.cpp:33
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
array_poolt::fresh_symbol
symbol_generatort & fresh_symbol
Definition: string_constraint_generator.h:83
array_string_exprt::length
exprt & length()
Definition: string_expr.h:70
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:591
function_application_exprt::function
symbol_exprt & function()
Definition: std_expr.h:4496
add_axioms_from_bool
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the String.valueOf(Z) java function.
Definition: string_constraint_generator_valueof.cpp:66
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
is_refined_string_type
bool is_refined_string_type(const typet &type)
Definition: refined_string_type.h:52
add_axioms_for_set_length
std::pair< exprt, string_constraintst > add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Reduce or extend a string to have the given length.
Definition: string_constraint_generator_transformation.cpp:37
get_return_code_type
signedbv_typet get_return_code_type()
Definition: string_constraint_generator_main.cpp:339
add_axioms_for_code_point_before
std::pair< exprt, string_constraintst > add_axioms_for_code_point_before(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
add axioms corresponding to the String.codePointBefore java function
Definition: string_constraint_generator_code_points.cpp:155
array_poolt::created_strings
const std::set< array_string_exprt > & created_strings() const
Definition: string_constraint_generator_main.cpp:160
string_constraintst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_constraint_generator.h:112
add_axioms_for_compare_to
std::pair< exprt, string_constraintst > add_axioms_for_compare_to(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Lexicographic comparison of two strings.
Definition: string_constraint_generator_comparison.cpp:241
exprt::operands
operandst & operands()
Definition: expr.h:78
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:583
array_poolt::make_char_array_for_char_pointer
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
Definition: string_constraint_generator_main.cpp:99
add_axioms_for_offset_by_code_point
std::pair< exprt, string_constraintst > add_axioms_for_offset_by_code_point(symbol_generatort &fresh_symbol, const function_application_exprt &f)
Add axioms corresponding the String.offsetByCodePointCount java function.
Definition: string_constraint_generator_code_points.cpp:222
string_constraint_generator.h
add_axioms_for_length
std::pair< exprt, string_constraintst > add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool)
Length of a string.
Definition: string_constraint_generator_main.cpp:513
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4403
add_axioms_for_parse_int
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Integer value represented by a string.
Definition: string_constraint_generator_valueof.cpp:507
add_axioms_for_is_prefix
std::pair< exprt, string_constraintst > add_axioms_for_is_prefix(symbol_generatort &fresh_symbol, 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:37
array_string_exprt
Definition: string_expr.h:67
string_constantt::get_value
const irep_idt & get_value() const
Definition: string_constant.h:25
array_poolt::arrays_of_pointers
std::unordered_map< exprt, array_string_exprt, irep_hash > arrays_of_pointers
Definition: string_constraint_generator.h:76
sum_overflows
exprt sum_overflows(const plus_exprt &sum)
Definition: string_constraint_generator_main.cpp:54
add_axioms_for_delete_char_at
std::pair< exprt, string_constraintst > add_axioms_for_delete_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &expr, array_poolt &array_pool)
add axioms corresponding to the StringBuilder.deleteCharAt java function
Definition: string_constraint_generator_transformation.cpp:339
validation_modet::INVARIANT
array_poolt::fresh_string
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
Definition: string_constraint_generator_main.cpp:87
add_axioms_for_contains
std::pair< exprt, string_constraintst > add_axioms_for_contains(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Test whether a string contains another.
Definition: string_constraint_generator_testing.cpp:233
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:111
add_axioms_for_index_of
std::pair< exprt, string_constraintst > add_axioms_for_index_of(symbol_generatort &fresh_symbol, 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
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470