cprover
string_refinement_util.cpp File Reference
#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"
Include dependency graph for string_refinement_util.cpp:

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_functiontto_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...
 

Function Documentation

◆ add_dependency_to_string_subexprs()

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 
)
static

◆ 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.

Parameters
dependenciesgraph to which we add the node
equationan equation whose right hand side is possibly a call to a string builtin_function.
array_poolarray pool containing arrays corresponding to the string exprt arguments of the builtin_function call
Returns
true if a node was added, if false is returned it either means that the right hand side is not a function application

Definition at line 373 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().

◆ for_each_atomic_string()

static void for_each_atomic_string ( const array_string_exprt e,
const std::function< void(const array_string_exprt &)>  f 
)
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 281 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().

◆ has_char_array_subexpr()

bool has_char_array_subexpr ( const exprt expr,
const namespacet ns 
)
Parameters
expran expression
nsnamespace
Returns
true if a subexpression of 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().

◆ has_char_pointer_subtype()

bool has_char_pointer_subtype ( const typet type,
const namespacet ns 
)
Parameters
typea type
nsnamespace
Returns
true if a subtype of 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().

◆ is_char_array_type()

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.

Parameters
typea type
nsnamespace
Returns
true if the given type is an array of characters

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().

◆ is_char_pointer_type()

bool is_char_pointer_type ( const typet type)

For now, any unsigned bitvector type is considered a character.

Parameters
typea type
Returns
true if the given type represents a pointer to characters

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().

◆ is_char_type()

bool is_char_type ( const typet type)

For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.

Note
type that are not characters maybe detected as characters (for instance unsigned char in C), this will make dec_solve do unnecessary steps for these, but should not affect correctness.
Parameters
typea type
Returns
true if the given type represents characters

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().

◆ to_string_builtin_function()

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 
)
static

Construct a string_builtin_functiont object from a function application.

Returns
a unique pointer to the created object

Definition at line 206 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().