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 // Comparison on the length of the strings
20 template <typename T>
21 binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
22 {
23  PRECONDITION(rhs.type() == lhs.length().type());
24  return binary_relation_exprt(lhs.length(), ID_ge, rhs);
25 }
26 
27 template <typename T>
28 binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
29 {
30  PRECONDITION(rhs.type() == lhs.length().type());
31  return binary_relation_exprt(rhs, ID_lt, lhs.length());
32 }
33 
34 template <typename T>
36 {
37  return length_gt(lhs, from_integer(i, lhs.length().type()));
38 }
39 
40 template <typename T>
41 binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
42 {
43  PRECONDITION(rhs.type() == lhs.length().type());
44  return binary_relation_exprt(lhs.length(), ID_le, rhs);
45 }
46 
47 template <typename T>
49 {
50  return length_le(lhs, from_integer(i, lhs.length().type()));
51 }
52 
53 template <typename T>
54 equal_exprt length_eq(const T &lhs, const exprt &rhs)
55 {
56  PRECONDITION(rhs.type() == lhs.length().type());
57  return equal_exprt(lhs.length(), rhs);
58 }
59 
60 template <typename T>
62 {
63  return length_eq(lhs, from_integer(i, lhs.length().type()));
64 }
65 
66 // Representation of strings as arrays
67 class array_string_exprt : public exprt
68 {
69 public:
71  {
72  return to_array_type(type()).size();
73  }
74 
75  const exprt &length() const
76  {
77  return to_array_type(type()).size();
78  }
79 
81  {
82  return *this;
83  }
84 
85  const exprt &content() const
86  {
87  return *this;
88  }
89 
90  exprt operator[](const exprt &i) const
91  {
92  return index_exprt(content(), i);
93  }
94 
95  index_exprt operator[](int i) const
96  {
97  return index_exprt(content(), from_integer(i, length().type()));
98  }
99 };
100 
102 {
103  PRECONDITION(expr.type().id() == ID_array);
104  return static_cast<array_string_exprt &>(expr);
105 }
106 
108 {
109  PRECONDITION(expr.type().id() == ID_array);
110  return static_cast<const array_string_exprt &>(expr);
111 }
112 
113 // Represent strings as a struct with a length field and a content field
115 {
116 public:
118  {
119  }
120 
122  const exprt &_length,
123  const exprt &_content,
124  const typet &type)
125  : struct_exprt(type)
126  {
127  add_to_operands(_length, _content);
128  }
129 
130  refined_string_exprt(const exprt &_length, const exprt &_content)
132  _length,
133  _content,
134  refined_string_typet(_length.type(), to_pointer_type(_content.type())))
135  {
136  }
137 
138  // Expression corresponding to the length of the string
139  const exprt &length() const
140  {
141  return op0();
142  }
144  {
145  return op0();
146  }
147 
148  // Expression corresponding to the content (array of characters) of the string
149  const exprt &content() const
150  {
151  return op1();
152  }
154  {
155  return op1();
156  }
157 
158  friend inline refined_string_exprt &to_string_expr(exprt &expr);
159 };
160 
162 {
163  PRECONDITION(expr.id()==ID_struct);
164  PRECONDITION(expr.operands().size()==2);
165  return static_cast<refined_string_exprt &>(expr);
166 }
167 
168 inline const refined_string_exprt &to_string_expr(const exprt &expr)
169 {
170  PRECONDITION(expr.id()==ID_struct);
171  PRECONDITION(expr.operands().size()==2);
172  return static_cast<const refined_string_exprt &>(expr);
173 }
174 
175 template <>
177 {
178  return base.id() == ID_struct && base.operands().size() == 2;
179 }
180 
181 inline void validate_expr(const refined_string_exprt &x)
182 {
183  INVARIANT(x.id() == ID_struct, "refined string exprs are struct");
184  validate_operands(x, 2, "refined string expr has length and content fields");
185  INVARIANT(
186  x.length().type().id() == ID_signedbv, "length should be a signed int");
187  INVARIANT(x.content().type().id() == ID_array, "content should be an array");
188 }
189 
190 #endif
The type of an expression, extends irept.
Definition: type.h:27
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
Definition: string_expr.h:21
BigInt mp_integer
Definition: mp_arith.h:22
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
exprt & op0()
Definition: expr.h:84
const exprt & length() const
Definition: string_expr.h:75
const exprt & content() const
Definition: string_expr.h:149
exprt operator[](const exprt &i) const
Definition: string_expr.h:90
Type for string expressions used by the string solver.
const exprt & content() const
Definition: string_expr.h:85
typet & type()
Return the type of the expression.
Definition: expr.h:68
bool can_cast_expr< refined_string_exprt >(const exprt &base)
Definition: string_expr.h:176
friend refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:161
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)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
Equality.
Definition: std_expr.h:1484
const irep_idt & id() const
Definition: irep.h:259
exprt & content()
Definition: string_expr.h:80
void validate_expr(const refined_string_exprt &x)
Definition: string_expr.h:181
API to expression classes.
exprt & op1()
Definition: expr.h:87
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:161
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const exprt & size() const
Definition: std_types.h:1010
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
Definition: string_expr.h:28
exprt & length()
Definition: string_expr.h:70
equal_exprt length_eq(const T &lhs, const exprt &rhs)
Definition: string_expr.h:54
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
refined_string_exprt(const exprt &_length, const exprt &_content, const typet &type)
Definition: string_expr.h:121
const exprt & length() const
Definition: string_expr.h:139
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
refined_string_exprt(const exprt &_length, const exprt &_content)
Definition: string_expr.h:130
operandst & operands()
Definition: expr.h:78
index_exprt operator[](int i) const
Definition: string_expr.h:95
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Struct constructor from list of elements.
Definition: std_expr.h:1920
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
Definition: string_expr.h:41
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:130
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:101
Array index operator.
Definition: std_expr.h:1595