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
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Boolean AND.
Definition: std_expr.h:1835
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:43
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:968
Equality.
Definition: std_expr.h:1140
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
Application of (mathematical) function.
const irep_idt & id() const
Definition: irep.h:407
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
std::vector< array_string_exprt > string_args
optionalt< array_string_exprt > string_res
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 ...
optionalt< array_string_exprt > string_result() const override
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)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
function_application_exprt 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...
Base class for string functions that are built in the solver.
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 ...
virtual std::vector< array_string_exprt > string_arguments() const
string_builtin_functiont(const string_builtin_functiont &)=delete
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 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...
virtual optionalt< array_string_exprt > string_result() const
virtual std::string name() const =0
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.
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_constraintst constraints(string_constraint_generatort &generator) 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.
optionalt< 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)
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...
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::string name() const override
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.
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_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 ...
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::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...
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_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.
string_to_lower_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
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 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_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 builtin_function transforming one string into another.
optionalt< 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:110
Generation of fresh symbols of a given type.
Definition: array_pool.h:23
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
nonstd::optional< T > optionalt
Definition: optional.h:35
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define UNIMPLEMENTED
Definition: invariant.h:523
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
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 ...
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,...