Base class for string functions that are built in the solver. More...
#include <string_builtin_function.h>
Inheritance diagram for string_builtin_functiont: Collaboration diagram for string_builtin_functiont:Public Member Functions | |
| string_builtin_functiont ()=delete | |
| string_builtin_functiont (const string_builtin_functiont &)=delete | |
| virtual | ~string_builtin_functiont ()=default |
| virtual std::optional< array_string_exprt > | string_result () const |
| virtual std::vector< array_string_exprt > | string_arguments () const |
| 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 builtin function. More... | |
| virtual std::string | name () const =0 |
| 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 the value of the function call. More... | |
| virtual exprt | length_constraint () const =0 |
| Constraint ensuring that the length of the strings are coherent with the function call. More... | |
| virtual bool | maybe_testing_function () const |
Tells whether the builtin function can be a testing function, that is a function that does not return a string, for instance like equals, indexOf or compare. More... | |
Public Attributes | |
| exprt | return_code |
Protected Member Functions | |
| string_builtin_functiont (exprt return_code, array_poolt &array_pool) | |
Protected Attributes | |
| array_poolt & | array_pool |
Detailed Description
Base class for string functions that are built in the solver.
The string_dependenciest framework handles string operations by either:
- generating constraints for the solver, which is done by the
constraints()function, - evaluating constant operations from the solver model, which is done by the
eval()function.
Only the content of the strings are managed in that way. The constraints for the lengths are always added, see length_constraint().
Concretely, if a built-in function supports constraint generation, it means that the result of the operation can be tested. For instance in this Java example:
if the built-in function for concatenation supports constraint generation, then the first assertion is reachable, but the second is not.
If a built-in function supports evaluation, then adding the constraints can be avoided if the string operation is not relevant to the control flow, e.g. in:
In this case, if concatenation supports evaluation, then the constraints for the concatenation operations are not added, but the concatenation is evaluated after solving, from the model, to render the concatenated string which is needed for generating the trace.
If the built-in function supports constraint generation for the string length, it means that the length of the string can be tested, as in:
As computing lengths is often much simpler than computing string constraints, there is no option to only evaluate string lengths from the solver model. String length constraints are generated by length_constraint().
The decision about whether to add constraints or not is implemented in in string_dependenciest.
Specific string operations are implemented by inheriting from string_builtin_functiont and implementing the virtual methods.
Definition at line 71 of file string_builtin_function.h.
Constructor & Destructor Documentation
◆ string_builtin_functiont() [1/3]
|
delete |
◆ string_builtin_functiont() [2/3]
|
delete |
◆ ~string_builtin_functiont()
|
virtualdefault |
◆ string_builtin_functiont() [3/3]
|
inlineprotected |
Definition at line 123 of file string_builtin_function.h.
Member Function Documentation
◆ constraints()
|
pure virtual |
Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call.
The constraints are only added when deemed necessary, i.e. when maybe_testing_function() returns true, or when testing function depends on the result of this function. This logic is implemented in add_constraints().
Implemented in string_concat_char_builtin_functiont, string_insertion_builtin_functiont, string_format_builtin_functiont, string_concatenation_builtin_functiont, string_builtin_function_with_no_evalt, string_of_int_builtin_functiont, string_to_upper_case_builtin_functiont, string_to_lower_case_builtin_functiont, and string_set_char_builtin_functiont.
◆ eval()
|
pure virtual |
Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function.
If not enough information can be gathered from get_value, return an empty optional.
Implemented in string_insertion_builtin_functiont, string_format_builtin_functiont, string_of_int_builtin_functiont, string_to_upper_case_builtin_functiont, string_to_lower_case_builtin_functiont, string_set_char_builtin_functiont, string_concat_char_builtin_functiont, and string_builtin_function_with_no_evalt.
◆ length_constraint()
|
pure virtual |
Constraint ensuring that the length of the strings are coherent with the function call.
Implemented in string_insertion_builtin_functiont, string_format_builtin_functiont, string_concatenation_builtin_functiont, string_builtin_function_with_no_evalt, string_of_int_builtin_functiont, string_to_upper_case_builtin_functiont, string_to_lower_case_builtin_functiont, string_set_char_builtin_functiont, and string_concat_char_builtin_functiont.
◆ maybe_testing_function()
|
inlinevirtual |
Tells whether the builtin function can be a testing function, that is a function that does not return a string, for instance like equals, indexOf or compare.
Reimplemented in string_insertion_builtin_functiont, string_format_builtin_functiont, string_creation_builtin_functiont, and string_transformation_builtin_functiont.
Definition at line 115 of file string_builtin_function.h.
◆ name()
|
pure virtual |
Implemented in string_insertion_builtin_functiont, string_format_builtin_functiont, string_concatenation_builtin_functiont, string_builtin_function_with_no_evalt, string_of_int_builtin_functiont, string_to_upper_case_builtin_functiont, string_to_lower_case_builtin_functiont, string_set_char_builtin_functiont, and string_concat_char_builtin_functiont.
◆ string_arguments()
|
inlinevirtual |
Reimplemented in string_insertion_builtin_functiont, string_format_builtin_functiont, string_builtin_function_with_no_evalt, string_test_builtin_functiont, and string_transformation_builtin_functiont.
Definition at line 83 of file string_builtin_function.h.
◆ string_result()
|
inlinevirtual |
Reimplemented in string_insertion_builtin_functiont, string_format_builtin_functiont, string_builtin_function_with_no_evalt, string_creation_builtin_functiont, and string_transformation_builtin_functiont.
Definition at line 78 of file string_builtin_function.h.
Member Data Documentation
◆ array_pool
|
protected |
Definition at line 121 of file string_builtin_function.h.
◆ return_code
| exprt string_builtin_functiont::return_code |
Definition at line 110 of file string_builtin_function.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/solvers/strings/string_builtin_function.h
