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 struct string_constraintst;
15 
16 #define CHARACTER_FOR_UNKNOWN '?'
17 
20 {
21 public:
23  virtual ~string_builtin_functiont() = default;
24 
26  {
27  return {};
28  }
29 
30  virtual std::vector<array_string_exprt> string_arguments() const
31  {
32  return {};
33  }
34 
39  virtual optionalt<exprt>
40  eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
41 
42  virtual std::string name() const = 0;
43 
46  virtual string_constraintst
47  constraints(string_constraint_generatort &constraint_generator) const = 0;
48 
51  virtual exprt length_constraint() const = 0;
52 
54 
58  virtual bool maybe_testing_function() const
59  {
60  return true;
61  }
62 
63 private:
64  string_builtin_functiont() = default;
65 
66 protected:
68  : return_code(std::move(return_code))
69  {
70  }
71 };
72 
75 {
76 public:
79 
85  result(std::move(result)),
86  input(std::move(input))
87  {
88  }
89 
96  const exprt &return_code,
97  const std::vector<exprt> &fun_args,
98  array_poolt &array_pool);
99 
101  {
102  return result;
103  }
104  std::vector<array_string_exprt> string_arguments() const override
105  {
106  return {input};
107  }
108  bool maybe_testing_function() const override
109  {
110  return false;
111  }
112 };
113 
117 {
118 public:
120 
126  const exprt &return_code,
127  const std::vector<exprt> &fun_args,
128  array_poolt &array_pool)
130  {
131  PRECONDITION(fun_args.size() == 4);
132  character = fun_args[3];
133  }
134 
136  eval(const std::function<exprt(const exprt &)> &get_value) const override;
137 
138  std::string name() const override
139  {
140  return "concat_char";
141  }
142 
144  constraints(string_constraint_generatort &generator) const override;
145 
146  exprt length_constraint() const override;
147 };
148 
152 {
153 public:
156 
162  const exprt &return_code,
163  const std::vector<exprt> &fun_args,
164  array_poolt &array_pool)
166  {
167  PRECONDITION(fun_args.size() == 5);
168  position = fun_args[3];
169  character = fun_args[4];
170  }
171 
173  eval(const std::function<exprt(const exprt &)> &get_value) const override;
174 
175  std::string name() const override
176  {
177  return "set_char";
178  }
179 
181  constraints(string_constraint_generatort &generator) const override;
182 
183  // \todo: length_constraint is not the best possible name because we also
184  // \todo: add constraint about the return code
185  exprt length_constraint() const override;
186 };
187 
192 {
193 public:
195  const exprt &return_code,
196  const std::vector<exprt> &fun_args,
197  array_poolt &array_pool)
199  {
200  }
201 
203  eval(const std::function<exprt(const exprt &)> &get_value) const override;
204 
205  std::string name() const override
206  {
207  return "to_lower_case";
208  }
209 
211  constraints(string_constraint_generatort &generator) const override;
212 
213  exprt length_constraint() const override
214  {
215  return and_exprt(
218  };
219 };
220 
225 {
226 public:
228  const exprt &return_code,
229  const std::vector<exprt> &fun_args,
230  array_poolt &array_pool)
232  {
233  }
234 
240  std::move(return_code),
241  std::move(result),
242  std::move(input))
243  {
244  }
245 
247  eval(const std::function<exprt(const exprt &)> &get_value) const override;
248 
249  std::string name() const override
250  {
251  return "to_upper_case";
252  }
253 
254  string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
255 
257  constraints(string_constraint_generatort &generator) const override
258  {
259  return constraints(generator.fresh_symbol);
260  };
261 
262  exprt length_constraint() const override
263  {
264  return and_exprt(
267  };
268 };
269 
272 {
273 public:
277  std::vector<exprt> args;
278 
286  const exprt &return_code,
287  const std::vector<exprt> &fun_args,
288  array_poolt &array_pool);
289 
291  {
292  return result;
293  }
294  std::vector<array_string_exprt> string_arguments() const override
295  {
296  return {input1, input2};
297  }
298 
300  virtual std::vector<mp_integer> eval(
301  const std::vector<mp_integer> &input1_value,
302  const std::vector<mp_integer> &input2_value,
303  const std::vector<mp_integer> &args_value) const;
304 
306  eval(const std::function<exprt(const exprt &)> &get_value) const override;
307 
308  std::string name() const override
309  {
310  return "insert";
311  }
312 
314  constraints(string_constraint_generatort &generator) const override;
315 
316  exprt length_constraint() const override;
317 
318  bool maybe_testing_function() const override
319  {
320  return false;
321  }
322 
323 protected:
326  {
327  }
328 };
329 
332 {
333 public:
341  const exprt &return_code,
342  const std::vector<exprt> &fun_args,
343  array_poolt &array_pool);
344 
345  std::vector<mp_integer> eval(
346  const std::vector<mp_integer> &input1_value,
347  const std::vector<mp_integer> &input2_value,
348  const std::vector<mp_integer> &args_value) const override;
349 
350  std::string name() const override
351  {
352  return "concat";
353  }
354 
356  constraints(string_constraint_generatort &generator) const override;
357 
358  exprt length_constraint() const override;
359 };
360 
363 {
364 public:
367 
369  const exprt &return_code,
370  const std::vector<exprt> &fun_args,
371  array_poolt &array_pool);
372 
374  {
375  return result;
376  }
377 
378  bool maybe_testing_function() const override
379  {
380  return false;
381  }
382 };
383 
386 {
387 public:
389  const exprt &return_code,
390  const std::vector<exprt> &fun_args,
391  array_poolt &array_pool)
392  : string_creation_builtin_functiont(return_code, fun_args, array_pool)
393  {
394  PRECONDITION(fun_args.size() <= 4);
395  if(fun_args.size() == 4)
396  radix = fun_args[3];
397  else
398  radix = from_integer(10, arg.type());
399  };
400 
402  eval(const std::function<exprt(const exprt &)> &get_value) const override;
403 
404  std::string name() const override
405  {
406  return "string_of_int";
407  }
408 
410  constraints(string_constraint_generatort &generator) const override;
411 
412  exprt length_constraint() const override;
413 
414 private:
416 };
417 
420 {
421 public:
423  std::vector<array_string_exprt> under_test;
424  std::vector<exprt> args;
425  std::vector<array_string_exprt> string_arguments() const override
426  {
427  return under_test;
428  }
429 };
430 
436 {
437 public:
440  std::vector<array_string_exprt> string_args;
441  std::vector<exprt> args;
442 
444  const exprt &return_code,
446  array_poolt &array_pool);
447 
448  std::string name() const override
449  {
451  }
452  std::vector<array_string_exprt> string_arguments() const override
453  {
454  return std::vector<array_string_exprt>(string_args);
455  }
457  {
458  return string_res;
459  }
460 
462  eval(const std::function<exprt(const exprt &)> &) const override
463  {
464  return {};
465  }
466 
468  constraints(string_constraint_generatort &generator) const override;
469 
470  exprt length_constraint() const override
471  {
472  // For now, there is no need for implementing that as `constraints`
473  // should always be called on these functions
475  }
476 };
477 
478 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
std::vector< array_string_exprt > string_arguments() const override
string_builtin_functiont()=default
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:4481
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
virtual string_constraintst constraints(string_constraint_generatort &constraint_generator) const =0
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
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:176
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 ...
Generation of fresh symbols of a given type.
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()
Return the type of the expression.
Definition: expr.h:68
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
String creation from integer types.
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
Collection of constraints of different types: existential formulas, universal formulas,...
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)
Equality.
Definition: std_expr.h:1484
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
string_to_upper_case_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
String creation from other types.
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
String builtin_function transforming one string into another.
optionalt< array_string_exprt > string_result() const override
optionalt< array_string_exprt > string_result() const override
string_insertion_builtin_functiont(const exprt &return_code)
nonstd::optional< T > optionalt
Definition: optional.h:35
Boolean AND.
Definition: std_expr.h:2409
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
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:438
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.
string_constraintst 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:4496
exprt & length()
Definition: string_expr.h:70
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:497
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
Base class for all expressions.
Definition: expr.h:54
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring that result is similar to input where the character at index position is ...
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.
string_constraintst 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() const override
Constraint ensuring that the length of the strings are coherent with the function call.
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_transformation_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input)
Setting a character at a particular position of a string.
optionalt< array_string_exprt > string_result() const override
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
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.
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
string_builtin_functiont(exprt return_code)