cprover
string_expr.h
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: String expressions for the string solver
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_STRING_EXPR_H
13 #define CPROVER_UTIL_STRING_EXPR_H
14 
15 #include "arith_tools.h"
16 #include "refined_string_type.h"
17 #include "std_expr.h"
18 
19 // Given an representation of strings as exprt that implements `length` and
20 // `content` this provides additional useful methods.
21 template <typename child_t>
23 {
24 private:
26  {
27  return static_cast<child_t *>(this)->length();
28  }
29  const exprt &length() const
30  {
31  return static_cast<const child_t *>(this)->length();
32  }
34  {
35  return static_cast<child_t *>(this)->content();
36  }
37  const exprt &content() const
38  {
39  return static_cast<const child_t *>(this)->content();
40  }
41 
42 protected:
43  string_exprt() = default;
44 
45 public:
46  exprt operator[](const exprt &i) const
47  {
48  return index_exprt(content(), i);
49  }
50 
51  index_exprt operator[] (int i) const
52  {
53  return index_exprt(content(), from_integer(i, length().type()));
54  }
55 
56  // Comparison on the length of the strings
58  const string_exprt &rhs) const
59  {
60  return binary_relation_exprt(length(), ID_ge, rhs.length());
61  }
62 
64  const exprt &rhs) const
65  {
66  PRECONDITION(rhs.type() == length().type());
67  return binary_relation_exprt(length(), ID_ge, rhs);
68  }
69 
71  const exprt &rhs) const
72  {
73  PRECONDITION(rhs.type() == length().type());
74  return binary_relation_exprt(rhs, ID_lt, length());
75  }
76 
78  const string_exprt &rhs) const
79  {
80  return binary_relation_exprt(rhs.length(), ID_lt, length());
81  }
82 
84  {
85  return axiom_for_length_gt(from_integer(i, length().type()));
86  }
87 
89  const string_exprt &rhs) const
90  {
91  return binary_relation_exprt(length(), ID_le, rhs.length());
92  }
93 
95  const exprt &rhs) const
96  {
97  PRECONDITION(rhs.type() == length().type());
98  return binary_relation_exprt(length(), ID_le, rhs);
99  }
100 
102  {
103  return axiom_for_length_le(from_integer(i, length().type()));
104  }
105 
107  const string_exprt &rhs) const
108  {
109  return binary_relation_exprt(length(), ID_lt, rhs.length());
110  }
111 
113  const exprt &rhs) const
114  {
115  PRECONDITION(rhs.type() == length().type());
116  return binary_relation_exprt(length(), ID_lt, rhs);
117  }
118 
120  const string_exprt &rhs) const
121  {
122  return equal_exprt(length(), rhs.length());
123  }
124 
126  {
127  PRECONDITION(rhs.type() == length().type());
128  return equal_exprt(length(), rhs);
129  }
130 
132  {
133  return axiom_for_has_length(from_integer(i, length().type()));
134  }
135 };
136 
137 // Representation of strings as arrays
138 class array_string_exprt : public string_exprt<array_string_exprt>, public exprt
139 {
140 public:
142  {
143  return to_array_type(type()).size();
144  }
145 
146  const exprt &length() const
147  {
148  return to_array_type(type()).size();
149  }
150 
152  {
153  return *this;
154  }
155 
156  const exprt &content() const
157  {
158  return *this;
159  }
160 };
161 
163 {
164  PRECONDITION(expr.type().id() == ID_array);
165  return static_cast<array_string_exprt &>(expr);
166 }
167 
169 {
170  PRECONDITION(expr.type().id() == ID_array);
171  return static_cast<const array_string_exprt &>(expr);
172 }
173 
174 // Represent strings as a struct with a length field and a content field
176  public string_exprt<refined_string_exprt>
177 {
178 public:
180  {
181  }
182 
184  {
185  operands().resize(2);
186  }
187 
189  const exprt &_length,
190  const exprt &_content,
191  const typet &type)
192  : struct_exprt(type)
193  {
194  copy_to_operands(_length, _content);
195  }
196 
197  refined_string_exprt(const exprt &_length, const exprt &_content)
199  _length,
200  _content,
201  refined_string_typet(_length.type(), _content.type()))
202  {
203  }
204 
205  // Expression corresponding to the length of the string
206  const exprt &length() const
207  {
208  return op0();
209  }
211  {
212  return op0();
213  }
214 
215  // Expression corresponding to the content (array of characters) of the string
216  const exprt &content() const
217  {
218  return op1();
219  }
221  {
222  return op1();
223  }
224 
225  static exprt within_bounds(const exprt &idx, const exprt &bound);
226 
227  friend inline refined_string_exprt &to_string_expr(exprt &expr);
228 };
229 
231 {
232  PRECONDITION(expr.id()==ID_struct);
233  PRECONDITION(expr.operands().size()==2);
234  return static_cast<refined_string_exprt &>(expr);
235 }
236 
237 inline const refined_string_exprt &to_string_expr(const exprt &expr)
238 {
239  PRECONDITION(expr.id()==ID_struct);
240  PRECONDITION(expr.operands().size()==2);
241  return static_cast<const refined_string_exprt &>(expr);
242 }
243 
244 template <>
246 {
247  return base.id() == ID_struct && base.operands().size() == 2;
248 }
249 
250 inline void validate_expr(const refined_string_exprt &x)
251 {
252  INVARIANT(x.id() == ID_struct, "refined string exprs are struct");
253  validate_operands(x, 2, "refined string expr has length and content fields");
254  INVARIANT(x.length().type().id() == ID_signedbv, "length is an unsigned int");
255  INVARIANT(x.content().type().id() == ID_array, "content is an array");
256 }
257 
258 #endif
The type of an expression.
Definition: type.h:22
static exprt within_bounds(const exprt &idx, const exprt &bound)
BigInt mp_integer
Definition: mp_arith.h:22
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
binary_relation_exprt axiom_for_length_ge(const string_exprt &rhs) const
Definition: string_expr.h:57
binary_relation_exprt axiom_for_length_gt(const string_exprt &rhs) const
Definition: string_expr.h:77
exprt & op0()
Definition: expr.h:72
string_exprt()=default
const exprt & content() const
Definition: string_expr.h:37
const exprt & length() const
Definition: string_expr.h:146
const exprt & content() const
Definition: string_expr.h:216
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
Type for string expressions used by the string solver.
equal_exprt axiom_for_has_length(const exprt &rhs) const
Definition: string_expr.h:125
const exprt & content() const
Definition: string_expr.h:156
const exprt & length() const
Definition: string_expr.h:29
typet & type()
Definition: expr.h:56
bool can_cast_expr< refined_string_exprt >(const exprt &base)
Definition: string_expr.h:245
friend refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:230
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:206
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
equality
Definition: std_expr.h:1354
binary_relation_exprt axiom_for_length_ge(const exprt &rhs) const
Definition: string_expr.h:63
exprt & length()
Definition: string_expr.h:25
const irep_idt & id() const
Definition: irep.h:189
equal_exprt axiom_for_has_length(mp_integer i) const
Definition: string_expr.h:131
binary_relation_exprt axiom_for_length_le(mp_integer i) const
Definition: string_expr.h:101
void validate_expr(const refined_string_exprt &x)
Definition: string_expr.h:250
binary_relation_exprt axiom_for_length_le(const string_exprt &rhs) const
Definition: string_expr.h:88
API to expression classes.
equal_exprt axiom_for_has_same_length_as(const string_exprt &rhs) const
Definition: string_expr.h:119
exprt & op1()
Definition: expr.h:75
binary_relation_exprt axiom_for_length_lt(const exprt &rhs) const
Definition: string_expr.h:112
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:230
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
const exprt & size() const
Definition: std_types.h:1014
binary_relation_exprt axiom_for_length_lt(const string_exprt &rhs) const
Definition: string_expr.h:106
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
refined_string_exprt(const exprt &_length, const exprt &_content, const typet &type)
Definition: string_expr.h:188
binary_relation_exprt axiom_for_length_gt(const exprt &rhs) const
Definition: string_expr.h:70
const exprt & length() const
Definition: string_expr.h:206
binary_relation_exprt axiom_for_length_le(const exprt &rhs) const
Definition: string_expr.h:94
refined_string_exprt(const typet &type)
Definition: string_expr.h:183
binary_relation_exprt axiom_for_length_gt(mp_integer i) const
Definition: string_expr.h:83
refined_string_exprt(const exprt &_length, const exprt &_content)
Definition: string_expr.h:197
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt & content()
Definition: string_expr.h:33
struct constructor from list of elements
Definition: std_expr.h:1815
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:162
exprt operator[](const exprt &i) const
Definition: string_expr.h:46
array index operator
Definition: std_expr.h:1462