21 #include <unordered_set> 32 return type.
id() == ID_unsignedbv &&
39 if(type.
id() == ID_symbol)
62 auto ref = std::ref(static_cast<const exprt &>(expr));
66 const auto current_index = numeric_cast_v<std::size_t>(with_expr.where());
67 entries[current_index] = with_expr.new_value();
68 ref = with_expr.old();
78 return std::accumulate(
84 const std::pair<std::size_t, exprt> &entry) {
86 const exprt &then_expr = entry.second;
89 return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
95 const auto it =
entries.find(index);
101 return std::accumulate(
107 const std::pair<std::size_t, exprt> &entry) {
109 const exprt &then_expr = entry.second;
112 return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
118 const exprt &extra_value)
121 const auto &operands = expr.
operands();
122 exprt last_added = extra_value;
123 for(std::size_t i = 0; i < operands.size(); ++i)
125 const std::size_t index = operands.size() - 1 - i;
126 if(operands[index].
id() != ID_unknown && operands[index] != last_added)
128 entries[index] = operands[index];
129 last_added = operands[index];
136 const exprt &extra_value)
140 for(std::size_t i = 0; i < expr.
operands().size(); i += 2)
145 "all values in array should have the same type");
146 if(index.has_value() && expr.
operands()[i + 1].id() != ID_unknown)
154 if(
const auto &array_expr = expr_try_dynamic_cast<array_exprt>(expr))
156 if(
const auto &with_expr = expr_try_dynamic_cast<with_exprt>(expr))
158 if(
const auto &array_list = expr_try_dynamic_cast<array_list_exprt>(expr))
166 const auto it =
entries.lower_bound(index);
177 array.operands().reserve(size);
180 for(; it !=
entries.end() && it->first < size; ++it)
181 array.operands().resize(it->first + 1, it->second);
183 array.operands().resize(
200 std::vector<std::size_t>
210 const exprt &return_code,
215 : name.get_identifier();
217 if(
id == ID_cprover_string_insert_func)
218 return util_make_unique<string_insertion_builtin_functiont>(
219 return_code, fun_app.
arguments(), array_pool);
221 if(
id == ID_cprover_string_concat_func)
222 return util_make_unique<string_concatenation_builtin_functiont>(
223 return_code, fun_app.
arguments(), array_pool);
225 if(
id == ID_cprover_string_concat_char_func)
226 return util_make_unique<string_concat_char_builtin_functiont>(
227 return_code, fun_app.
arguments(), array_pool);
229 return util_make_unique<string_builtin_function_with_no_evalt>(
230 return_code, fun_app, array_pool);
237 if(!entry_inserted.second)
240 string_nodes.emplace_back(e, entry_inserted.first->second);
244 std::unique_ptr<const string_dependenciest::string_nodet>
249 return util_make_unique<const string_nodet>(
string_nodes.at(it->second));
254 std::unique_ptr<string_builtin_functiont> &builtin_function)
306 fun_app.
arguments()[1].type().id() == ID_pointer)
314 for(
const auto &expr : fun_app.
arguments())
319 [&](
const exprt &e) {
323 const auto string = array_pool.
of_argument(string_struct);
332 const std::function<
exprt(
const exprt &)> &get_value)
const 342 const auto &f = node.result_from;
343 if(f && node.dependencies.size() == 1)
369 auto builtin_function =
373 const auto &builtin_function_node = dependencies.
make_node(builtin_function);
377 const auto &string_result =
380 dependencies.
add_dependency(*string_result, builtin_function_node);
381 auto &node = dependencies.
get_node(*string_result);
385 for(
const auto arg : builtin_function_node.data->string_arguments())
389 (void)dependencies.
get_node(atomic);
395 dependencies, *fun_app, builtin_function_node, array_pool);
402 const std::function<
void(
const string_nodet &)> &f)
const 404 for(
const auto &s : node.
data->string_arguments())
406 std::vector<std::reference_wrapper<const exprt>>
stack({s});
407 while(!
stack.empty())
409 const auto current =
stack.back();
411 if(
const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
413 stack.emplace_back(if_expr->true_case());
414 stack.emplace_back(if_expr->false_case());
421 "dependencies of the node should have been added to the graph at node creation " 422 + current.get().pretty());
439 const std::function<
void(
const nodet &)> &f)
const 458 const std::function<
void(
const nodet &)> &f)
const 461 f(
nodet(string_node));
468 const auto for_each =
469 [&](
const std::function<void(const nodet &)> &f) {
472 const auto for_each_succ =
473 [&](
const nodet &n,
const std::function<void(const nodet &)> &f) {
476 const auto node_to_string = [&](
const nodet &n) {
477 std::stringstream ostream;
483 return ostream.str();
485 stream <<
"digraph dependencies {\n";
486 output_dot_generic<nodet>(stream, for_each, for_each_succ, node_to_string);
487 stream <<
'}' << std::endl;
493 std::unordered_set<nodet, node_hash> test_dependencies;
496 if(builtin.data->maybe_testing_function())
497 test_dependencies.insert(
nodet(builtin));
504 const std::function<
void(
const nodet &)> &f) {
510 if(test_dependencies.count(
nodet(node)))
513 const exprt return_value = builtin.
data->add_constraints(generator);
517 generator.
add_lemma(node.data->length_constraint());
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
const string_builtin_functiont & get_builtin_function(const builtin_function_nodet &node) const
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
A generic base class for relations, i.e., binary predicates.
virtual exprt to_if_expression(const exprt &index) const
Creates an if_expr corresponding to the result of accessing the array at the given index...
application of (mathematical) function
builtin_function_nodet & make_node(std::unique_ptr< string_builtin_functiont > &builtin_function)
builtin_function is reset to an empty pointer after the node is created
void clean_cache()
Clean the cache used by eval
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Deprecated expression utility functions.
bool can_cast_expr< with_exprt >(const exprt &base)
bool add_node(string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool)
When right hand side of equation is a builtin_function add a "string_builtin_function" node to the gr...
std::unique_ptr< string_builtin_functiont > data
string_nodet & get_node(const array_string_exprt &e)
enum string_dependenciest::nodet::@4 kind
virtual optionalt< array_string_exprt > string_result() const
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
interval_sparse_arrayt(const with_exprt &expr)
An expression of the form array_of(x) with {i:=a} with {j:=b} is converted to an array arr where for ...
The trinary if-then-else operator.
std::unique_ptr< const string_nodet > node_at(const array_string_exprt &e) const
exprt to_if_expression(const exprt &index) const override
Creates an if_expr corresponding to the result of accessing the array at the given index...
Magic numbers used throughout the codebase.
auto expr_dynamic_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
#define CHECK_RETURN(CONDITION)
std::vector< builtin_function_nodet > builtin_function_nodes
Set of nodes representing builtin_functions.
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
static void for_each_atomic_string(const array_string_exprt &e, const std::function< void(const array_string_exprt &)> f)
Applies f on all strings contained in e that are not if-expressions.
std::unordered_map< array_string_exprt, std::size_t, irep_hash > node_index_pool
Nodes describing dependencies of a string: values of the map correspond to indexes in the vector stri...
#define INVARIANT(CONDITION, REASON)
void for_each_successor(const nodet &i, const std::function< void(const nodet &)> &f) const
Applies f on all successors of the node n.
const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
static void add_dependency_to_string_subexprs(string_dependenciest &dependencies, const function_application_exprt &fun_app, const string_dependenciest::builtin_function_nodet &builtin_function_node, array_poolt &array_pool)
optionalt< exprt > eval(const array_string_exprt &s, const std::function< exprt(const exprt &)> &get_value) const
Attempt to evaluate the given string from the dependencies and valuation of strings on which it depen...
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
std::map< exprt, std::vector< std::size_t > > equations_containing
Record index of the equations that contain a given expression.
Represents arrays by the indexes up to which the value remains the same.
nonstd::optional< T > optionalt
std::vector< string_nodet > string_nodes
Set of nodes representing strings.
void clear()
Clear the content of the dependency graph.
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
API to expression classes.
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
std::map< std::size_t, exprt > entries
#define PRECONDITION(CONDITION)
optionalt< std::size_t > result_from
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
array constructor from single element
const typet & follow(const typet &) const
bitvector_typet index_type()
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
array_string_exprt of_argument(const exprt &arg)
Converts a struct containing a length and pointer to an array.
exprt at(std::size_t index) const override
Get the value at the specified index.
std::vector< optionalt< exprt > > eval_string_cache
std::unordered_map< std::size_t, std::vector< exprt > > strings_in_equation
Record expressions that are contained in the equation with the given index.
Keep track of dependencies between strings.
std::size_t get_width() const
A builtin function node contains a builtin function call.
symbol_exprt & function()
A string node points to builtin_function on which it depends.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
A Template Class for Graphs.
static std::unique_ptr< string_builtin_functiont > to_string_builtin_function(const function_application_exprt &fun_app, const exprt &return_code, array_poolt &array_pool)
Construct a string_builtin_functiont object from a function application.
std::vector< exprt > find_expressions(const std::size_t i)
Base class for all expressions.
bool is_refined_string_type(const typet &type)
Operator to update elements in structs and arrays.
irep_idt get_object_name() const
bool is_ssa_expr(const exprt &expr)
std::vector< std::size_t > dependencies
sparse_arrayt(const with_exprt &expr)
Initialize a sparse array from an expression of the form array_of(x) with {i:=a} with {j:=b} ...
void add_dependency(const array_string_exprt &e, const builtin_function_nodet &builtin_function)
Add edge from node for e to node for builtin_function if e is a simple array expression.
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor, otherwise returns empty optional.
Expression to hold a symbol (variable)
virtual exprt at(std::size_t index) const
Get the value at the specified index.
const typet & subtype() const
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character...
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
std::vector< std::size_t > find_equations(const exprt &expr)
struct constructor from list of elements
void for_each_node(const std::function< void(const nodet &)> &f) const
Applies f on all nodes.
array constructor from list of elements
void add_lemma(const exprt &)
void get_reachable(Container &set, const std::function< void(const typename Container::value_type &, const std::function< void(const typename Container::value_type &)> &)> &for_each_successor)
Add to set, nodes that are reachable from set.
void for_each_dependency(const string_nodet &node, const std::function< void(const builtin_function_nodet &)> &f) const
Applies f to each node on which node depends.
array_string_exprt & to_array_string_expr(exprt &expr)
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
void output_dot(std::ostream &stream) const