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 
8 
10 #include <util/optional.h>
11 #include <util/string_expr.h>
12 
13 #include <vector>
14 
15 #define CHARACTER_FOR_UNKNOWN '?'
16 
73 {
74 public:
77  virtual ~string_builtin_functiont() = default;
78 
80  {
81  return {};
82  }
83 
84  virtual std::vector<array_string_exprt> string_arguments() const
85  {
86  return {};
87  }
88 
93  virtual optionalt<exprt>
94  eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
95 
96  virtual std::string name() const = 0;
97 
104  virtual string_constraintst
105  constraints(string_constraint_generatort &constraint_generator) const = 0;
106 
109  virtual exprt length_constraint() const = 0;
110 
112 
116  virtual bool maybe_testing_function() const
117  {
118  return true;
119  }
120 
121 protected:
123 
126  {
127  }
128 };
129 
132 {
133 public:
136 
143  result(std::move(result)),
144  input(std::move(input))
145  {
146  }
147 
154  const exprt &return_code,
155  const std::vector<exprt> &fun_args,
157 
159  {
160  return result;
161  }
162  std::vector<array_string_exprt> string_arguments() const override
163  {
164  return {input};
165  }
166  bool maybe_testing_function() const override
167  {
168  return false;
169  }
170 };
171 
175 {
176 public:
178 
184  const exprt &return_code,
185  const std::vector<exprt> &fun_args,
188  {
189  PRECONDITION(fun_args.size() == 4);
190  character = fun_args[3];
191  }
192 
194  eval(const std::function<exprt(const exprt &)> &get_value) const override;
195 
196  std::string name() const override
197  {
198  return "concat_char";
199  }
200 
202  constraints(string_constraint_generatort &generator) 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 
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  constraints(string_constraint_generatort &generator) const override;
240 
241  // \todo: length_constraint is not the best possible name because we also
242  // \todo: add constraint about the return code
243  exprt length_constraint() const override;
244 };
245 
250 {
251 public:
253  const exprt &return_code,
254  const std::vector<exprt> &fun_args,
257  {
258  }
259 
261  eval(const std::function<exprt(const exprt &)> &get_value) const override;
262 
263  std::string name() const override
264  {
265  return "to_lower_case";
266  }
267 
269  constraints(string_constraint_generatort &generator) const override;
270 
271  exprt length_constraint() const override
272  {
273  return and_exprt(
274  equal_exprt(
278  };
279 };
280 
285 {
286 public:
288  const exprt &return_code,
289  const std::vector<exprt> &fun_args,
292  {
293  }
294 
301  std::move(return_code),
302  std::move(result),
303  std::move(input),
304  array_pool)
305  {
306  }
307 
309  eval(const std::function<exprt(const exprt &)> &get_value) const override;
310 
311  std::string name() const override
312  {
313  return "to_upper_case";
314  }
315 
316  string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
317 
319  constraints(string_constraint_generatort &generator) const override
320  {
321  return constraints(generator.fresh_symbol);
322  };
323 
324  exprt length_constraint() const override
325  {
326  return and_exprt(
327  equal_exprt(
331  };
332 };
333 
336 {
337 public:
340 
342  const exprt &return_code,
343  const std::vector<exprt> &fun_args,
345 
347  {
348  return result;
349  }
350 
351  bool maybe_testing_function() const override
352  {
353  return false;
354  }
355 };
356 
359 {
360 public:
362  const exprt &return_code,
363  const std::vector<exprt> &fun_args,
366  {
367  PRECONDITION(fun_args.size() <= 4);
368  if(fun_args.size() == 4)
369  radix = fun_args[3];
370  else
371  radix = from_integer(10, arg.type());
372  };
373 
375  eval(const std::function<exprt(const exprt &)> &get_value) const override;
376 
377  std::string name() const override
378  {
379  return "string_of_int";
380  }
381 
383  constraints(string_constraint_generatort &generator) const override;
384 
385  exprt length_constraint() const override;
386 
387 private:
389 };
390 
393 {
394 public:
396  std::vector<array_string_exprt> under_test;
397  std::vector<exprt> args;
398  std::vector<array_string_exprt> string_arguments() const override
399  {
400  return under_test;
401  }
402 };
403 
409 {
410 public:
413  std::vector<array_string_exprt> string_args;
414  std::vector<exprt> args;
415 
417  const exprt &return_code,
420 
421  std::string name() const override
422  {
423  PRECONDITION(function_application.function().id() == ID_symbol);
424  return id2string(
426  }
427  std::vector<array_string_exprt> string_arguments() const override
428  {
429  return std::vector<array_string_exprt>(string_args);
430  }
432  {
433  return string_res;
434  }
435 
437  eval(const std::function<exprt(const exprt &)> &) const override
438  {
439  return {};
440  }
441 
443  constraints(string_constraint_generatort &generator) const override;
444 
445  exprt length_constraint() const override
446  {
447  // For now, there is no need for implementing that as `constraints`
448  // should always be called on these functions
450  }
451 };
452 
457  const array_string_exprt &a,
458  const std::function<exprt(const exprt &)> &get_value);
459 
462  const std::vector<mp_integer> &array,
463  const array_typet &array_type);
464 
465 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
string_builtin_functiont::maybe_testing_function
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
Definition: string_builtin_function.h:116
string_concat_char_builtin_functiont::constraints
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
Definition: string_builtin_function.cpp:103
make_string
array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
Definition: string_builtin_function.cpp:71
string_creation_builtin_functiont::maybe_testing_function
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
Definition: string_builtin_function.h:351
string_of_int_builtin_functiont::radix
exprt radix
Definition: string_builtin_function.h:388
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:525
string_test_builtin_functiont::result
exprt result
Definition: string_builtin_function.h:395
string_builtin_functiont::~string_builtin_functiont
virtual ~string_builtin_functiont()=default
string_to_lower_case_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:263
string_to_lower_case_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.h:271
string_builtin_function_with_no_evalt::name
std::string name() const override
Definition: string_builtin_function.h:421
string_to_upper_case_builtin_functiont::constraints
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
Definition: string_builtin_function.cpp:336
array_poolt
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
optional.h
string_builtin_functiont::return_code
exprt return_code
Definition: string_builtin_function.h:111
string_builtin_functiont::string_builtin_functiont
string_builtin_functiont(const string_builtin_functiont &)=delete
string_transformation_builtin_functiont
String builtin_function transforming one string into another.
Definition: string_builtin_function.h:132
string_of_int_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.cpp:415
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:59
and_exprt
Boolean AND.
Definition: std_expr.h:1920
string_set_char_builtin_functiont::position
exprt position
Definition: string_builtin_function.h:212
array_poolt::get_or_create_length
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
string_to_lower_case_builtin_functiont::string_to_lower_case_builtin_functiont
string_to_lower_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Definition: string_builtin_function.h:252
string_builtin_function_with_no_evalt::function_application
function_application_exprt function_application
Definition: string_builtin_function.h:411
string_creation_builtin_functiont
String creation from other types.
Definition: string_builtin_function.h:336
exprt
Base class for all expressions.
Definition: expr.h:54
string_builtin_function_with_no_evalt::string_args
std::vector< array_string_exprt > string_args
Definition: string_builtin_function.h:413
string_to_upper_case_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:310
string_concat_char_builtin_functiont::string_concat_char_builtin_functiont
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.
Definition: string_builtin_function.h:183
string_of_int_builtin_functiont::string_of_int_builtin_functiont
string_of_int_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Definition: string_builtin_function.h:361
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:39
string_builtin_function_with_no_evalt::args
std::vector< exprt > args
Definition: string_builtin_function.h:414
string_to_lower_case_builtin_functiont
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowerc...
Definition: string_builtin_function.h:250
string_builtin_functiont::string_result
virtual optionalt< array_string_exprt > string_result() const
Definition: string_builtin_function.h:79
string_to_lower_case_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:216
equal_exprt
Equality.
Definition: std_expr.h:1225
string_builtin_functiont::constraints
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_builtin_functiont::string_arguments
virtual std::vector< array_string_exprt > string_arguments() const
Definition: string_builtin_function.h:84
string_constraint_generatort
Definition: string_constraint_generator.h:48
string_set_char_builtin_functiont::string_set_char_builtin_functiont
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.
Definition: string_builtin_function.h:219
string_builtin_functiont::array_pool
array_poolt & array_pool
Definition: string_builtin_function.h:122
string_concat_char_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:196
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
string_concat_char_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.cpp:123
string_transformation_builtin_functiont::input
array_string_exprt input
Definition: string_builtin_function.h:135
symbol_generatort
Generation of fresh symbols of a given type.
Definition: array_pool.h:22
string_builtin_function_with_no_evalt
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
Definition: string_builtin_function.h:409
string_to_upper_case_builtin_functiont
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
Definition: string_builtin_function.h:285
string_set_char_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:233
string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
Definition: string_builtin_function.cpp:445
string_set_char_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.cpp:187
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
string_test_builtin_functiont::args
std::vector< exprt > args
Definition: string_builtin_function.h:397
string_builtin_function_with_no_evalt::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.h:445
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
string_test_builtin_functiont::string_arguments
std::vector< array_string_exprt > string_arguments() const override
Definition: string_builtin_function.h:398
string_test_builtin_functiont::under_test
std::vector< array_string_exprt > under_test
Definition: string_builtin_function.h:396
string_builtin_functiont::string_builtin_functiont
string_builtin_functiont(exprt return_code, array_poolt &array_pool)
Definition: string_builtin_function.h:124
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:192
string_concat_char_builtin_functiont::character
exprt character
Definition: string_builtin_function.h:177
string_of_int_builtin_functiont
String creation from integer types.
Definition: string_builtin_function.h:359
string_to_upper_case_builtin_functiont::string_to_upper_case_builtin_functiont
string_to_upper_case_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)
Definition: string_builtin_function.h:295
string_builtin_function_with_no_evalt::constraints
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...
Definition: string_builtin_function.cpp:475
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
string_to_upper_case_builtin_functiont::constraints
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...
Definition: string_builtin_function.h:319
irept::id
const irep_idt & id() const
Definition: irep.h:407
string_concat_char_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:76
eval_string
optionalt< 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 ...
Definition: string_builtin_function.cpp:24
string_builtin_function_with_no_evalt::string_result
optionalt< array_string_exprt > string_result() const override
Definition: string_builtin_function.h:431
string_builtin_functiont::string_builtin_functiont
string_builtin_functiont()=delete
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
string_builtin_functiont
Base class for string functions that are built in the solver.
Definition: string_builtin_function.h:73
string_transformation_builtin_functiont::string_arguments
std::vector< array_string_exprt > string_arguments() const override
Definition: string_builtin_function.h:162
string_transformation_builtin_functiont::string_result
optionalt< array_string_exprt > string_result() const override
Definition: string_builtin_function.h:158
string_builtin_functiont::eval
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 ...
string_of_int_builtin_functiont::constraints
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...
Definition: string_builtin_function.cpp:406
string_to_upper_case_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:311
string_of_int_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:377
string_set_char_builtin_functiont
Setting a character at a particular position of a string.
Definition: string_builtin_function.h:210
string_builtin_function_with_no_evalt::string_res
optionalt< array_string_exprt > string_res
Definition: string_builtin_function.h:412
array_typet
Arrays with given size.
Definition: std_types.h:763
function_application_exprt::function
exprt & function()
Definition: mathematical_expr.h:200
string_creation_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:338
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
string_concat_char_builtin_functiont
Adding a character at the end of a string.
Definition: string_builtin_function.h:175
string_transformation_builtin_functiont::string_transformation_builtin_functiont
string_transformation_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)
Definition: string_builtin_function.h:137
string_creation_builtin_functiont::arg
exprt arg
Definition: string_builtin_function.h:339
string_builtin_functiont::length_constraint
virtual exprt length_constraint() const =0
Constraint ensuring that the length of the strings are coherent with the function call.
string_transformation_builtin_functiont::maybe_testing_function
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
Definition: string_builtin_function.h:166
string_set_char_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:128
string_builtin_functiont::name
virtual std::string name() const =0
string_test_builtin_functiont
String test.
Definition: string_builtin_function.h:393
string_set_char_builtin_functiont::character
exprt character
Definition: string_builtin_function.h:213
string_to_upper_case_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_builtin_function.h:324
string_to_upper_case_builtin_functiont::string_to_upper_case_builtin_functiont
string_to_upper_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Definition: string_builtin_function.h:287
string_constraint_generator.h
Generates string constraints to link results from string functions with their arguments.
string_expr.h
String expressions for the string solver.
string_creation_builtin_functiont::string_result
optionalt< array_string_exprt > string_result() const override
Definition: string_builtin_function.h:346
string_transformation_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:134
array_string_exprt
Definition: string_expr.h:67
string_builtin_function_with_no_evalt::eval
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 ...
Definition: string_builtin_function.h:437
string_to_lower_case_builtin_functiont::constraints
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
Definition: string_builtin_function.cpp:281
string_builtin_function_with_no_evalt::string_arguments
std::vector< array_string_exprt > string_arguments() const override
Definition: string_builtin_function.h:427
string_creation_builtin_functiont::string_creation_builtin_functiont
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.
Definition: string_builtin_function.cpp:362
string_set_char_builtin_functiont::constraints
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 ...
Definition: string_builtin_function.cpp:153
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
string_of_int_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:373