cprover
|
#include <algorithm>
#include <numeric>
#include <functional>
#include <iostream>
#include <util/arith_tools.h>
#include <util/expr_util.h>
#include <util/ssa_expr.h>
#include <util/std_expr.h>
#include <util/expr_iterator.h>
#include <util/graph.h>
#include <util/magic.h>
#include <util/make_unique.h>
#include <unordered_set>
#include "string_refinement_util.h"
Go to the source code of this file.
Functions | |
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. More... | |
bool | is_char_type (const typet &type) |
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character. More... | |
bool | is_char_array_type (const typet &type, const namespacet &ns) |
Distinguish char array from other types. More... | |
bool | is_char_pointer_type (const typet &type) |
For now, any unsigned bitvector type is considered a character. More... | |
bool | has_char_pointer_subtype (const typet &type, const namespacet &ns) |
bool | has_char_array_subexpr (const exprt &expr, const namespacet &ns) |
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. More... | |
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) |
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 graph and connect it to the strings on which it depends and which depends on it. More... | |
|
static |
Definition at line 297 of file string_refinement_util.cpp.
References string_dependenciest::add_dependency(), function_application_exprt::arguments(), expr_checked_cast(), array_poolt::find(), is_refined_string_type(), array_poolt::of_argument(), PRECONDITION, and exprt::type().
Referenced by add_node().
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 graph and connect it to the strings on which it depends and which depends on it.
If the string builtin_function is not a supported one, mark all the string arguments as depending on an unknown builtin_function.
dependencies | graph to which we add the node |
equation | an equation whose right hand side is possibly a call to a string builtin_function. |
array_pool | array pool containing arrays corresponding to the string exprt arguments of the builtin_function call |
Definition at line 359 of file string_refinement_util.cpp.
References string_dependenciest::add_dependency(), add_dependency_to_string_subexprs(), CHECK_RETURN, expr_try_dynamic_cast(), for_each_atomic_string(), string_dependenciest::get_builtin_function(), string_dependenciest::get_node(), binary_relation_exprt::lhs(), string_dependenciest::make_node(), string_dependenciest::string_nodet::result_from, binary_relation_exprt::rhs(), string_builtin_functiont::string_result(), and to_string_builtin_function().
Referenced by string_refinementt::dec_solve().
|
static |
Applies f
on all strings contained in e
that are not if-expressions.
For instance on input cond1?s1:cond2?s2:s3
we apply f
on s1, s2 and s3.
Definition at line 267 of file string_refinement_util.cpp.
References irept::id(), to_array_string_expr(), and to_if_expr().
Referenced by string_dependenciest::add_dependency(), and add_node().
bool has_char_array_subexpr | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
expr | an expression |
ns | namespace |
expr
is an array of characters Definition at line 54 of file string_refinement_util.cpp.
References has_subexpr(), is_char_array_type(), and exprt::type().
Referenced by string_refinementt::set_to().
bool has_char_pointer_subtype | ( | const typet & | type, |
const namespacet & | ns | ||
) |
type | a type |
ns | namespace |
type
is an pointer of characters. The meaning of "subtype" is in the algebraic datatype sense: for example, the subtypes of a struct are the types of its components, the subtype of a pointer is the type it points to, etc... Definition at line 49 of file string_refinement_util.cpp.
References has_subtype(), and is_char_pointer_type().
Referenced by generate_symbol_resolution_from_equations().
bool is_char_array_type | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Distinguish char array from other types.
For now, any unsigned bitvector type is considered a character.
type | a type |
ns | namespace |
Definition at line 37 of file string_refinement_util.cpp.
References namespace_baset::follow(), irept::id(), is_char_array_type(), is_char_type(), and typet::subtype().
Referenced by string_refinementt::get(), has_char_array_subexpr(), and is_char_array_type().
bool is_char_pointer_type | ( | const typet & | type | ) |
For now, any unsigned bitvector type is considered a character.
type | a type |
Definition at line 44 of file string_refinement_util.cpp.
References irept::id(), is_char_type(), and typet::subtype().
Referenced by generate_symbol_resolution_from_equations(), and has_char_pointer_subtype().
bool is_char_type | ( | const typet & | type | ) |
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
type | a type |
Definition at line 30 of file string_refinement_util.cpp.
References bitvector_typet::get_width(), irept::id(), STRING_REFINEMENT_MAX_CHAR_WIDTH, and to_unsignedbv_type().
Referenced by string_refinementt::get(), initial_index_set(), is_char_array_type(), is_char_pointer_type(), and update_index_set().
|
static |
Construct a string_builtin_functiont object from a function application.
Definition at line 208 of file string_refinement_util.cpp.
References function_application_exprt::arguments(), expr_checked_cast(), function_application_exprt::function(), ssa_exprt::get_object_name(), is_ssa_expr(), and to_ssa_expr().
Referenced by add_node().