cprover
string_refinement_util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String solver
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
10 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
11 
12 #include <memory>
13 
15 #include "string_constraint.h"
17 
25 bool is_char_type(const typet &type);
26 
32 bool is_char_array_type(const typet &type, const namespacet &ns);
33 
37 bool is_char_pointer_type(const typet &type);
38 
45 bool has_char_pointer_subtype(const typet &type, const namespacet &ns);
46 
50 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);
51 
57 std::string
58 utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);
59 
61 {
62  std::map<exprt, std::set<exprt>> cumulative;
63  std::map<exprt, std::set<exprt>> current;
64 };
65 
67 {
68  std::vector<string_constraintt> universal;
69  std::vector<string_not_contains_constraintt> not_contains;
70 };
71 
75 {
76 public:
81  explicit sparse_arrayt(const with_exprt &expr);
82 
85  static exprt to_if_expression(const with_exprt &expr, const exprt &index);
86 
87 protected:
89  std::map<std::size_t, exprt> entries;
91  {
92  }
93 };
94 
100 {
101 public:
106  explicit interval_sparse_arrayt(const with_exprt &expr) : sparse_arrayt(expr)
107  {
108  }
109 
113  interval_sparse_arrayt(const array_exprt &expr, const exprt &extra_value);
114 
119  const array_list_exprt &expr,
120  const exprt &extra_value);
121 
122  exprt to_if_expression(const exprt &index) const;
123 
127  of_expr(const exprt &expr, const exprt &extra_value);
128 
130  array_exprt concretize(std::size_t size, const typet &index_type) const;
131 
134  exprt at(std::size_t index) const;
135 
139  {
140  }
141 };
142 
143 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
string_axiomst::universal
std::vector< string_constraintt > universal
Definition: string_refinement_util.h:68
string_builtin_function.h
typet
The type of an expression, extends irept.
Definition: type.h:29
sparse_arrayt
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
Definition: string_refinement_util.h:75
index_set_pairt
Definition: string_refinement_util.h:61
interval_sparse_arrayt
Represents arrays by the indexes up to which the value remains the same.
Definition: string_refinement_util.h:100
interval_sparse_arrayt::to_if_expression
exprt to_if_expression(const exprt &index) const
Definition: string_refinement_util.cpp:107
sparse_arrayt::sparse_arrayt
sparse_arrayt(exprt default_value)
Definition: string_refinement_util.h:90
exprt
Base class for all expressions.
Definition: expr.h:53
interval_sparse_arrayt::of_expr
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,...
Definition: string_refinement_util.cpp:160
string_axiomst
Definition: string_refinement_util.h:67
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
sparse_arrayt::sparse_arrayt
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} ....
Definition: string_refinement_util.cpp:69
interval_sparse_arrayt::interval_sparse_arrayt
interval_sparse_arrayt(exprt default_value)
Array containing the same value at each index.
Definition: string_refinement_util.h:137
sparse_arrayt::to_if_expression
static exprt to_if_expression(const with_exprt &expr, const exprt &index)
Creates an if_expr corresponding to the result of accessing the array at the given index.
Definition: string_refinement_util.cpp:86
sparse_arrayt::default_value
exprt default_value
Definition: string_refinement_util.h:88
interval_sparse_arrayt::interval_sparse_arrayt
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 ...
Definition: string_refinement_util.h:106
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
interval_sparse_arrayt::at
exprt at(std::size_t index) const
Get the value at the specified index.
Definition: string_refinement_util.cpp:171
has_char_array_subexpr
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
Definition: string_refinement_util.cpp:49
is_char_pointer_type
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
Definition: string_refinement_util.cpp:39
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
interval_sparse_arrayt::concretize
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
Definition: string_refinement_util.cpp:178
string_constraint.h
Defines string constraints.
utf16_constant_array_to_java
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
Definition: string_refinement_util.cpp:56
sparse_arrayt::entries
std::map< std::size_t, exprt > entries
Definition: string_refinement_util.h:89
index_set_pairt::current
std::map< exprt, std::set< exprt > > current
Definition: string_refinement_util.h:63
has_char_pointer_subtype
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
Definition: string_refinement_util.cpp:44
index_set_pairt::cumulative
std::map< exprt, std::set< exprt > > cumulative
Definition: string_refinement_util.h:62
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1478
is_char_array_type
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
Definition: string_refinement_util.cpp:32
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.
Definition: string_refinement_util.cpp:26
string_constraint_generator.h
Generates string constraints to link results from string functions with their arguments.
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
string_axiomst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_refinement_util.h:69