CBMC
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 
8 
10 #include <util/string_expr.h>
11 
12 #include <vector>
13 
14 #define CHARACTER_FOR_UNKNOWN '?'
15 
72 {
73 public:
76  virtual ~string_builtin_functiont() = default;
77 
78  virtual std::optional<array_string_exprt> string_result() const
79  {
80  return {};
81  }
82 
83  virtual std::vector<array_string_exprt> string_arguments() const
84  {
85  return {};
86  }
87 
92  virtual std::optional<exprt>
93  eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
94 
95  virtual std::string name() const = 0;
96 
103  virtual string_constraintst
105 
108  virtual exprt length_constraint() const = 0;
109 
111 
115  virtual bool maybe_testing_function() const
116  {
117  return true;
118  }
119 
120 protected:
122 
125  {
126  }
127 };
128 
131 {
132 public:
135 
142  result(std::move(result)),
143  input(std::move(input))
144  {
145  }
146 
153  const exprt &return_code,
154  const std::vector<exprt> &fun_args,
156 
157  std::optional<array_string_exprt> string_result() const override
158  {
159  return result;
160  }
161  std::vector<array_string_exprt> string_arguments() const override
162  {
163  return {input};
164  }
165  bool maybe_testing_function() const override
166  {
167  return false;
168  }
169 };
170 
174 {
175 public:
177 
183  const exprt &return_code,
184  const std::vector<exprt> &fun_args,
187  {
188  PRECONDITION(fun_args.size() == 4);
189  character = fun_args[3];
190  }
191 
192  std::optional<exprt>
193  eval(const std::function<exprt(const exprt &)> &get_value) const override;
194 
195  std::string name() const override
196  {
197  return "concat_char";
198  }
199 
201  string_constraint_generatort &generator,
202  message_handlert &message_handlert) const override;
203 
204  exprt length_constraint() const override;
205 };
206 
210 {
211 public:
214 
220  const exprt &return_code,
221  const std::vector<exprt> &fun_args,
224  {
225  PRECONDITION(fun_args.size() == 5);
226  position = fun_args[3];
227  character = fun_args[4];
228  }
229 
230  std::optional<exprt>
231  eval(const std::function<exprt(const exprt &)> &get_value) const override;
232 
233  std::string name() const override
234  {
235  return "set_char";
236  }
237 
239  string_constraint_generatort &generator,
240  message_handlert &message_handler) const override;
241 
242  // \todo: length_constraint is not the best possible name because we also
243  // \todo: add constraint about the return code
244  exprt length_constraint() const override;
245 };
246 
251 {
252 public:
254  const exprt &return_code,
255  const std::vector<exprt> &fun_args,
258  {
259  }
260 
261  std::optional<exprt>
262  eval(const std::function<exprt(const exprt &)> &get_value) const override;
263 
264  std::string name() const override
265  {
266  return "to_lower_case";
267  }
268 
270  string_constraint_generatort &generator,
271  message_handlert &message_handler) const override;
272 
273  exprt length_constraint() const override
274  {
275  return and_exprt(
276  equal_exprt(
280  };
281 };
282 
287 {
288 public:
290  const exprt &return_code,
291  const std::vector<exprt> &fun_args,
294  {
295  }
296 
303  std::move(return_code),
304  std::move(result),
305  std::move(input),
306  array_pool)
307  {
308  }
309 
310  std::optional<exprt>
311  eval(const std::function<exprt(const exprt &)> &get_value) const override;
312 
313  std::string name() const override
314  {
315  return "to_upper_case";
316  }
317 
319  class symbol_generatort &fresh_symbol,
320  message_handlert &message_handler) const;
321 
323  string_constraint_generatort &generator,
324  message_handlert &message_handler) const override
325  {
326  return constraints(generator.fresh_symbol, message_handler);
327  };
328 
329  exprt length_constraint() const override
330  {
331  return and_exprt(
332  equal_exprt(
336  };
337 };
338 
341 {
342 public:
345 
347  const exprt &return_code,
348  const std::vector<exprt> &fun_args,
350 
351  std::optional<array_string_exprt> string_result() const override
352  {
353  return result;
354  }
355 
356  bool maybe_testing_function() const override
357  {
358  return false;
359  }
360 };
361 
364 {
365 public:
367  const exprt &return_code,
368  const std::vector<exprt> &fun_args,
371  {
372  PRECONDITION(fun_args.size() <= 4);
373  if(fun_args.size() == 4)
374  radix = fun_args[3];
375  else
376  radix = from_integer(10, arg.type());
377  };
378 
379  std::optional<exprt>
380  eval(const std::function<exprt(const exprt &)> &get_value) const override;
381 
382  std::string name() const override
383  {
384  return "string_of_int";
385  }
386 
388  string_constraint_generatort &generator,
389  message_handlert &message_handler) const override;
390 
391  exprt length_constraint() const override;
392 
393 private:
395 };
396 
399 {
400 public:
402  std::vector<array_string_exprt> under_test;
403  std::vector<exprt> args;
404  std::vector<array_string_exprt> string_arguments() const override
405  {
406  return under_test;
407  }
408 };
409 
415 {
416 public:
418  std::optional<array_string_exprt> string_res;
419  std::vector<array_string_exprt> string_args;
420  std::vector<exprt> args;
421 
423  const exprt &return_code,
426 
427  std::string name() const override
428  {
429  PRECONDITION(function_application.function().id() == ID_symbol);
430  return id2string(
432  }
433  std::vector<array_string_exprt> string_arguments() const override
434  {
435  return std::vector<array_string_exprt>(string_args);
436  }
437  std::optional<array_string_exprt> string_result() const override
438  {
439  return string_res;
440  }
441 
442  std::optional<exprt>
443  eval(const std::function<exprt(const exprt &)> &) const override
444  {
445  return {};
446  }
447 
449  string_constraint_generatort &generator,
450  message_handlert &message_handler) const override;
451 
452  exprt length_constraint() const override
453  {
454  // For now, there is no need for implementing that as `constraints`
455  // should always be called on these functions
457  }
458 };
459 
463 std::optional<std::vector<mp_integer>> eval_string(
464  const array_string_exprt &a,
465  const std::function<exprt(const exprt &)> &get_value);
466 
469  const std::vector<mp_integer> &array,
470  const array_typet &array_type);
471 
472 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Boolean AND.
Definition: std_expr.h:2120
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition: array_pool.cpp:26
Arrays with given size.
Definition: std_types.h:807
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
Application of (mathematical) function.
const irep_idt & id() const
Definition: irep.h:384
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
std::vector< array_string_exprt > string_args
std::optional< 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::optional< array_string_exprt > string_res
std::vector< array_string_exprt > string_arguments() const override
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
std::optional< 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.
function_application_exprt function_application
Base class for string functions that are built in the solver.
virtual std::vector< array_string_exprt > string_arguments() const
string_builtin_functiont(const string_builtin_functiont &)=delete
virtual std::optional< array_string_exprt > string_result() const
virtual string_constraintst constraints(string_constraint_generatort &, message_handlert &) const =0
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
string_builtin_functiont(exprt return_code, array_poolt &array_pool)
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
virtual ~string_builtin_functiont()=default
virtual exprt length_constraint() const =0
Constraint ensuring that the length of the strings are coherent with the function call.
virtual std::string name() const =0
virtual std::optional< 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 ...
Adding a character at the end of a string.
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::optional< 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_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handlert) const override
Set of constraints enforcing that result is the concatenation of input with character.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
String creation from other types.
std::optional< array_string_exprt > string_result() const override
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
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 creation from integer types.
string_of_int_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) 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.
std::string name() const override
std::optional< 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 ...
Setting a character at a particular position of a string.
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, message_handlert &message_handler) const override
Set of constraints ensuring that result is similar to input where the character at index position is ...
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.
std::optional< 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< array_string_exprt > string_arguments() const override
std::vector< array_string_exprt > under_test
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, message_handlert &message_handler) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
string_to_lower_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
std::optional< 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 ...
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
string_constraintst constraints(class symbol_generatort &fresh_symbol, message_handlert &message_handler) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
std::optional< 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 length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
string_to_upper_case_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)
string_to_upper_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
String builtin_function transforming one string into another.
std::optional< array_string_exprt > string_result() const override
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
string_transformation_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)
std::vector< array_string_exprt > string_arguments() const override
const irep_idt & get_identifier() const
Definition: std_expr.h:160
Generation of fresh symbols of a given type.
Definition: array_pool.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
API to expression classes for 'mathematical' expressions.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define UNIMPLEMENTED
Definition: invariant.h:558
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
std::optional< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Given a function get_value which gives a valuation to expressions, attempt to find the current value ...
Generates string constraints to link results from string functions with their arguments.
String expressions for the string solver.
Collection of constraints of different types: existential formulas, universal formulas,...