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

Definition at line 311 of file string_refinement_util.cpp.

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

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

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

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

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

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

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

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