CBMC
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 "string_constraint.h"
13 
14 #include <map>
15 #include <set>
16 
24 bool is_char_type(const typet &type);
25 
31 bool is_char_array_type(const typet &type, const namespacet &ns);
32 
36 bool is_char_pointer_type(const typet &type);
37 
44 bool has_char_pointer_subtype(const typet &type, const namespacet &ns);
45 
49 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);
50 
56 std::string
57 utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);
58 
60 {
61  std::map<exprt, std::set<exprt>> cumulative;
62  std::map<exprt, std::set<exprt>> current;
63 };
64 
66 {
67  std::vector<string_constraintt> universal;
68  std::vector<string_not_contains_constraintt> not_contains;
69 };
70 
74 {
75 public:
80  explicit sparse_arrayt(const with_exprt &expr);
81 
84  static exprt to_if_expression(const with_exprt &expr, const exprt &index);
85 
86 protected:
88  std::map<std::size_t, exprt> entries;
90  {
91  }
92 };
93 
99 {
100 public:
105  explicit interval_sparse_arrayt(const with_exprt &expr) : sparse_arrayt(expr)
106  {
107  }
108 
112  interval_sparse_arrayt(const array_exprt &expr, const exprt &extra_value);
113 
118  const array_list_exprt &expr,
119  const exprt &extra_value);
120 
121  exprt to_if_expression(const exprt &index) const;
122 
125  static std::optional<interval_sparse_arrayt>
126  of_expr(const exprt &expr, const exprt &extra_value);
127 
129  array_exprt concretize(std::size_t size, const typet &index_type) const;
130 
133  exprt at(std::size_t index) const;
134 
138  {
139  }
140 };
141 
142 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
Array constructor from list of elements.
Definition: std_expr.h:1621
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1681
Base class for all expressions.
Definition: expr.h:56
Represents arrays by the indexes up to which the value remains the same.
exprt to_if_expression(const exprt &index) const
static std::optional< 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,...
interval_sparse_arrayt(exprt default_value)
Array containing the same value at each index.
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
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 ...
exprt at(std::size_t index) const
Get the value at the specified index.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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
sparse_arrayt(exprt default_value)
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.
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} ....
The type of an expression, extends irept.
Definition: type.h:29
Operator to update elements in structs and arrays.
Definition: std_expr.h:2481
Defines string constraints.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
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 has_char_pointer_subtype(const typet &type, const namespacet &ns)
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
std::map< exprt, std::set< exprt > > current
std::map< exprt, std::set< exprt > > cumulative
std::vector< string_constraintt > universal
std::vector< string_not_contains_constraintt > not_contains