cprover
string_builtin_function.h
Go to the documentation of this file.
1 
4 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
5 #define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
6 
7 #include <vector>
8 #include <util/optional.h>
9 #include <util/string_expr.h>
11 
12 class array_poolt;
13 
14 #define CHARACTER_FOR_UNKNOWN '?'
15 
18 {
19 public:
21  virtual ~string_builtin_functiont() = default;
22 
24  {
25  return {};
26  }
27 
28  virtual std::vector<array_string_exprt> string_arguments() const
29  {
30  return {};
31  }
32 
37  virtual optionalt<exprt>
38  eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
39 
40  virtual std::string name() const = 0;
41 
44  virtual exprt
45  add_constraints(string_constraint_generatort &constraint_generator) const = 0;
46 
49  virtual exprt length_constraint() const = 0;
50 
52 
56  virtual bool maybe_testing_function() const
57  {
58  return true;
59  }
60 
61 private:
62  string_builtin_functiont() = default;
63 
64 protected:
67  {
68  }
69 };
70 
73 {
74 public:
77 
84  const exprt &return_code,
85  const std::vector<exprt> &fun_args,
86  array_poolt &array_pool);
87 
89  {
90  return result;
91  }
92  std::vector<array_string_exprt> string_arguments() const override
93  {
94  return {input};
95  }
96  bool maybe_testing_function() const override
97  {
98  return false;
99  }
100 };
101 
105 {
106 public:
108 
114  const exprt &return_code,
115  const std::vector<exprt> &fun_args,
116  array_poolt &array_pool)
118  {
119  PRECONDITION(fun_args.size() == 4);
120  character = fun_args[3];
121  }
122 
124  eval(const std::function<exprt(const exprt &)> &get_value) const override;
125 
126  std::string name() const override
127  {
128  return "concat_char";
129  }
130 
132  {
133  return generator.add_axioms_for_concat_char(result, input, character);
134  }
135 
136  exprt length_constraint() const override
137  {
139  }
140 };
141 
145 {
146 public:
149 
155  const exprt &return_code,
156  const std::vector<exprt> &fun_args,
157  array_poolt &array_pool)
159  {
160  PRECONDITION(fun_args.size() == 5);
161  position = fun_args[3];
162  character = fun_args[4];
163  }
164 
166  eval(const std::function<exprt(const exprt &)> &get_value) const override;
167 
168  std::string name() const override
169  {
170  return "set_char";
171  }
172 
174  {
175  return generator.add_axioms_for_set_char(
177  }
178 
179  // \todo: length_constraint is not the best possible name because we also
180  // \todo: add constraint about the return code
181  exprt length_constraint() const override;
182 };
183 
188 {
189 public:
191  const exprt &return_code,
192  const std::vector<exprt> &fun_args,
193  array_poolt &array_pool)
195  {
196  }
197 
199  eval(const std::function<exprt(const exprt &)> &get_value) const override;
200 
201  std::string name() const override
202  {
203  return "to_lower_case";
204  }
205 
207  {
208  return generator.add_axioms_for_to_lower_case(result, input);
209  };
210 
211  exprt length_constraint() const override
212  {
213  return equal_exprt(result.length(), input.length());
214  };
215 };
216 
221 {
222 public:
224  const exprt &return_code,
225  const std::vector<exprt> &fun_args,
226  array_poolt &array_pool)
228  {
229  }
230 
232  eval(const std::function<exprt(const exprt &)> &get_value) const override;
233 
234  std::string name() const override
235  {
236  return "to_upper_case";
237  }
238 
240  {
241  return generator.add_axioms_for_to_upper_case(result, input);
242  };
243 
244  exprt length_constraint() const override
245  {
246  return equal_exprt(result.length(), input.length());
247  };
248 };
249 
252 {
253 public:
257  std::vector<exprt> args;
258 
266  const exprt &return_code,
267  const std::vector<exprt> &fun_args,
268  array_poolt &array_pool);
269 
271  {
272  return result;
273  }
274  std::vector<array_string_exprt> string_arguments() const override
275  {
276  return {input1, input2};
277  }
278 
280  virtual std::vector<mp_integer> eval(
281  const std::vector<mp_integer> &input1_value,
282  const std::vector<mp_integer> &input2_value,
283  const std::vector<mp_integer> &args_value) const;
284 
286  eval(const std::function<exprt(const exprt &)> &get_value) const override;
287 
288  std::string name() const override
289  {
290  return "insert";
291  }
292 
294  {
295  if(args.size() == 1)
296  return generator.add_axioms_for_insert(result, input1, input2, args[0]);
297  if(args.size() == 3)
299  UNREACHABLE;
300  };
301 
302  exprt length_constraint() const override
303  {
304  if(args.size() == 1)
306  if(args.size() == 3)
308  UNREACHABLE;
309  };
310 
311  bool maybe_testing_function() const override
312  {
313  return false;
314  }
315 
316 protected:
319  {
320  }
321 };
322 
325 {
326 public:
334  const exprt &return_code,
335  const std::vector<exprt> &fun_args,
336  array_poolt &array_pool);
337 
338  std::vector<mp_integer> eval(
339  const std::vector<mp_integer> &input1_value,
340  const std::vector<mp_integer> &input2_value,
341  const std::vector<mp_integer> &args_value) const override;
342 
343  std::string name() const override
344  {
345  return "concat";
346  }
347 
349  {
350  if(args.size() == 0)
351  return generator.add_axioms_for_concat(result, input1, input2);
352  if(args.size() == 2)
353  return generator.add_axioms_for_concat_substr(
354  result, input1, input2, args[0], args[1]);
355  UNREACHABLE;
356  };
357 
358  exprt length_constraint() const override
359  {
360  if(args.size() == 0)
362  if(args.size() == 2)
364  result, input1, input2, args[0], args[1]);
365  UNREACHABLE;
366  }
367 };
368 
371 {
372 public:
375 
377  const exprt &return_code,
378  const std::vector<exprt> &fun_args,
379  array_poolt &array_pool);
380 
382  {
383  return result;
384  }
385 
386  bool maybe_testing_function() const override
387  {
388  return false;
389  }
390 };
391 
394 {
395 public:
397  const exprt &return_code,
398  const std::vector<exprt> &fun_args,
399  array_poolt &array_pool)
400  : string_creation_builtin_functiont(return_code, fun_args, array_pool)
401  {
402  PRECONDITION(fun_args.size() <= 4);
403  if(fun_args.size() == 4)
404  radix = fun_args[3];
405  else
406  radix = from_integer(10, arg.type());
407  };
408 
410  eval(const std::function<exprt(const exprt &)> &get_value) const override;
411 
412  std::string name() const override
413  {
414  return "string_of_int";
415  }
416 
418  {
420  result, arg, radix);
421  }
422 
423  exprt length_constraint() const override;
424 
425 private:
427 };
428 
431 {
432 public:
434  std::vector<array_string_exprt> under_test;
435  std::vector<exprt> args;
436  std::vector<array_string_exprt> string_arguments() const override
437  {
438  return under_test;
439  }
440 };
441 
447 {
448 public:
451  std::vector<array_string_exprt> string_args;
452  std::vector<exprt> args;
453 
455  const exprt &return_code,
457  array_poolt &array_pool);
458 
459  std::string name() const override
460  {
462  }
463  std::vector<array_string_exprt> string_arguments() const override
464  {
465  return std::vector<array_string_exprt>(string_args);
466  }
468  {
469  return string_res;
470  }
471 
473  eval(const std::function<exprt(const exprt &)> &) const override
474  {
475  return {};
476  }
477 
479  {
481  };
482 
483  exprt length_constraint() const override
484  {
485  // For now, there is no need for implementing that as `add_constraints`
486  // should always be called on these functions
488  }
489 };
490 
491 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
std::vector< array_string_exprt > string_arguments() const override
string_builtin_functiont()=default
exprt length_constraint_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2...
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...
Adding a character at the end of a string.
Generates string constraints to link results from string functions with their arguments.
virtual std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const
Evaluate the result from a concrete valuation of the arguments.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
application of (mathematical) function
Definition: std_expr.h:4529
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
string_concatenation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
function_application_exprt function_application
std::vector< array_string_exprt > under_test
string_concat_char_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
std::vector< array_string_exprt > string_arguments() const override
string_to_lower_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
virtual ~string_builtin_functiont()=default
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
std::vector< array_string_exprt > string_arguments() const override
const irep_idt & get_identifier() const
Definition: std_expr.h:128
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
virtual optionalt< array_string_exprt > string_result() const
String inserting a string into another one.
std::vector< array_string_exprt > string_args
string_insertion_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
typet & type()
Definition: expr.h:56
exprt add_axioms_for_to_upper_case(const array_string_exprt &res, const array_string_exprt &expr)
Add axioms ensuring res corresponds to str in which lowercase characters of Basic Latin and Latin-1 s...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
String creation from integer types.
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
string_of_int_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
string_builtin_functiont(const exprt &return_code)
equality
Definition: std_expr.h:1354
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
String creation from other types.
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_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String...
string_to_upper_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
virtual exprt length_constraint() const =0
Constraint ensuring that the length of the strings are coherent with the function call...
virtual std::vector< array_string_exprt > string_arguments() const
exprt add_axioms_for_to_lower_case(const array_string_exprt &res, const array_string_exprt &str)
Add axioms ensuring res corresponds to str in which uppercase characters have been converted to lower...
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
String builtin_function transforming one string into another.
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
optionalt< array_string_exprt > string_result() const override
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
optionalt< array_string_exprt > string_result() const override
string_insertion_builtin_functiont(const exprt &return_code)
nonstd::optional< T > optionalt
Definition: optional.h:35
virtual exprt add_constraints(string_constraint_generatort &constraint_generator) const =0
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt length_constraint_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 ...
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
virtual optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const =0
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
std::vector< array_string_exprt > string_arguments() const override
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
optionalt< array_string_exprt > string_result() const override
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
string_creation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
exprt add_axioms_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index â...
exprt length_constraint_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
std::string name() const override
symbol_exprt & function()
Definition: std_expr.h:4550
string_transformation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
String expressions for the string solver.
string_set_char_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
#define UNIMPLEMENTED
Definition: invariant.h:287
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
Base class for all expressions.
Definition: expr.h:42
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
exprt add_axioms_for_set_char(const array_string_exprt &res, const array_string_exprt &str, const exprt &position, const exprt &character)
Add axioms ensuring that the result res is similar to input string str where the character at index p...
optionalt< array_string_exprt > string_res
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowerc...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
#define UNREACHABLE
Definition: invariant.h:271
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
Setting a character at a particular position of a string.
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
optionalt< array_string_exprt > string_result() const override
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
Functions that are not yet supported in this class but are supported by string_constraint_generatort...
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)
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const override
Evaluate the result from a concrete valuation of the arguments.
virtual std::string name() const =0
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.