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 #include <util/optional.h>
9 #include <util/string_expr.h>
10 #include <vector>
11 
12 class array_poolt;
13 struct string_constraintst;
15 
16 #define CHARACTER_FOR_UNKNOWN '?'
17 
74 {
75 public:
78  virtual ~string_builtin_functiont() = default;
79 
81  {
82  return {};
83  }
84 
85  virtual std::vector<array_string_exprt> string_arguments() const
86  {
87  return {};
88  }
89 
94  virtual optionalt<exprt>
95  eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
96 
97  virtual std::string name() const = 0;
98 
105  virtual string_constraintst
106  constraints(string_constraint_generatort &constraint_generator) const = 0;
107 
110  virtual exprt length_constraint() const = 0;
111 
113 
117  virtual bool maybe_testing_function() const
118  {
119  return true;
120  }
121 
122 protected:
124 
127  {
128  }
129 };
130 
133 {
134 public:
137 
144  result(std::move(result)),
145  input(std::move(input))
146  {
147  }
148 
155  const exprt &return_code,
156  const std::vector<exprt> &fun_args,
158 
160  {
161  return result;
162  }
163  std::vector<array_string_exprt> string_arguments() const override
164  {
165  return {input};
166  }
167  bool maybe_testing_function() const override
168  {
169  return false;
170  }
171 };
172 
176 {
177 public:
179 
185  const exprt &return_code,
186  const std::vector<exprt> &fun_args,
189  {
190  PRECONDITION(fun_args.size() == 4);
191  character = fun_args[3];
192  }
193 
195  eval(const std::function<exprt(const exprt &)> &get_value) const override;
196 
197  std::string name() const override
198  {
199  return "concat_char";
200  }
201 
203  constraints(string_constraint_generatort &generator) const override;
204 
205  exprt length_constraint() const override;
206 };
207 
211 {
212 public:
215 
221  const exprt &return_code,
222  const std::vector<exprt> &fun_args,
225  {
226  PRECONDITION(fun_args.size() == 5);
227  position = fun_args[3];
228  character = fun_args[4];
229  }
230 
232  eval(const std::function<exprt(const exprt &)> &get_value) const override;
233 
234  std::string name() const override
235  {
236  return "set_char";
237  }
238 
240  constraints(string_constraint_generatort &generator) 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 
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  constraints(string_constraint_generatort &generator) const override;
271 
272  exprt length_constraint() const override
273  {
274  return and_exprt(
275  equal_exprt(
279  };
280 };
281 
286 {
287 public:
289  const exprt &return_code,
290  const std::vector<exprt> &fun_args,
293  {
294  }
295 
302  std::move(return_code),
303  std::move(result),
304  std::move(input),
305  array_pool)
306  {
307  }
308 
310  eval(const std::function<exprt(const exprt &)> &get_value) const override;
311 
312  std::string name() const override
313  {
314  return "to_upper_case";
315  }
316 
317  string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
318 
320  constraints(string_constraint_generatort &generator) const override
321  {
322  return constraints(generator.fresh_symbol);
323  };
324 
325  exprt length_constraint() const override
326  {
327  return and_exprt(
328  equal_exprt(
332  };
333 };
334 
337 {
338 public:
341 
343  const exprt &return_code,
344  const std::vector<exprt> &fun_args,
346 
348  {
349  return result;
350  }
351 
352  bool maybe_testing_function() const override
353  {
354  return false;
355  }
356 };
357 
360 {
361 public:
363  const exprt &return_code,
364  const std::vector<exprt> &fun_args,
367  {
368  PRECONDITION(fun_args.size() <= 4);
369  if(fun_args.size() == 4)
370  radix = fun_args[3];
371  else
372  radix = from_integer(10, arg.type());
373  };
374 
376  eval(const std::function<exprt(const exprt &)> &get_value) const override;
377 
378  std::string name() const override
379  {
380  return "string_of_int";
381  }
382 
384  constraints(string_constraint_generatort &generator) const override;
385 
386  exprt length_constraint() const override;
387 
388 private:
390 };
391 
394 {
395 public:
397  std::vector<array_string_exprt> under_test;
398  std::vector<exprt> args;
399  std::vector<array_string_exprt> string_arguments() const override
400  {
401  return under_test;
402  }
403 };
404 
410 {
411 public:
414  std::vector<array_string_exprt> string_args;
415  std::vector<exprt> args;
416 
418  const exprt &return_code,
421 
422  std::string name() const override
423  {
424  PRECONDITION(function_application.function().id() == ID_symbol);
425  return id2string(
427  }
428  std::vector<array_string_exprt> string_arguments() const override
429  {
430  return std::vector<array_string_exprt>(string_args);
431  }
433  {
434  return string_res;
435  }
436 
438  eval(const std::function<exprt(const exprt &)> &) const override
439  {
440  return {};
441  }
442 
444  constraints(string_constraint_generatort &generator) const override;
445 
446  exprt length_constraint() const override
447  {
448  // For now, there is no need for implementing that as `constraints`
449  // should always be called on these functions
451  }
452 };
453 
458  const array_string_exprt &a,
459  const std::function<exprt(const exprt &)> &get_value);
460 
463  const std::vector<mp_integer> &array,
464  const array_typet &array_type);
465 
466 #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:117
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:352
string_of_int_builtin_functiont::radix
exprt radix
Definition: string_builtin_function.h:389
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:523
string_test_builtin_functiont::result
exprt result
Definition: string_builtin_function.h:396
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:264
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:272
string_builtin_function_with_no_evalt::name
std::string name() const override
Definition: string_builtin_function.h:422
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:43
optional.h
string_builtin_functiont::return_code
exprt return_code
Definition: string_builtin_function.h:112
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:133
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:56
and_exprt
Boolean AND.
Definition: std_expr.h:2137
string_set_char_builtin_functiont::position
exprt position
Definition: string_builtin_function.h:213
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:24
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:253
string_builtin_function_with_no_evalt::function_application
function_application_exprt function_application
Definition: string_builtin_function.h:412
string_creation_builtin_functiont
String creation from other types.
Definition: string_builtin_function.h:337
exprt
Base class for all expressions.
Definition: expr.h:53
string_builtin_function_with_no_evalt::string_args
std::vector< array_string_exprt > string_args
Definition: string_builtin_function.h:414
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:184
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:362
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:36
string_builtin_function_with_no_evalt::args
std::vector< exprt > args
Definition: string_builtin_function.h:415
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:251
string_builtin_functiont::string_result
virtual optionalt< array_string_exprt > string_result() const
Definition: string_builtin_function.h:80
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:1190
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:85
string_constraint_generatort
Definition: string_constraint_generator.h:45
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:220
string_builtin_functiont::array_pool
array_poolt & array_pool
Definition: string_builtin_function.h:123
string_concat_char_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:197
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:136
symbol_generatort
Generation of fresh symbols of a given type.
Definition: array_pool.h:23
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:410
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:286
string_set_char_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:234
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:44
string_test_builtin_functiont::args
std::vector< exprt > args
Definition: string_builtin_function.h:398
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:446
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
string_test_builtin_functiont::string_arguments
std::vector< array_string_exprt > string_arguments() const override
Definition: string_builtin_function.h:399
string_test_builtin_functiont::under_test
std::vector< array_string_exprt > under_test
Definition: string_builtin_function.h:397
string_builtin_functiont::string_builtin_functiont
string_builtin_functiont(exprt return_code, array_poolt &array_pool)
Definition: string_builtin_function.h:125
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
string_concat_char_builtin_functiont::character
exprt character
Definition: string_builtin_function.h:178
string_of_int_builtin_functiont
String creation from integer types.
Definition: string_builtin_function.h:360
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:296
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:177
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:320
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:432
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:74
string_transformation_builtin_functiont::string_arguments
std::vector< array_string_exprt > string_arguments() const override
Definition: string_builtin_function.h:163
string_transformation_builtin_functiont::string_result
optionalt< array_string_exprt > string_result() const override
Definition: string_builtin_function.h:159
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:312
string_of_int_builtin_functiont::name
std::string name() const override
Definition: string_builtin_function.h:378
string_set_char_builtin_functiont
Setting a character at a particular position of a string.
Definition: string_builtin_function.h:211
string_builtin_function_with_no_evalt::string_res
optionalt< array_string_exprt > string_res
Definition: string_builtin_function.h:413
array_typet
Arrays with given size.
Definition: std_types.h:965
function_application_exprt::function
exprt & function()
Definition: mathematical_expr.h:211
string_creation_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:339
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:176
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:138
string_creation_builtin_functiont::arg
exprt arg
Definition: string_builtin_function.h:340
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:167
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:394
string_set_char_builtin_functiont::character
exprt character
Definition: string_builtin_function.h:214
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:325
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:288
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:347
string_transformation_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:135
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:438
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:428
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
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