cprover
Loading...
Searching...
No Matches
string_expr.h
Go to the documentation of this file.
1/******************************************************************\
2
3Module: String expressions for the string solver
4
5Author: 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
20{
21 PRECONDITION(rhs.type() == lhs.type());
22 return binary_relation_exprt(std::move(lhs), ID_ge, std::move(rhs));
23}
24
26{
27 PRECONDITION(rhs.type() == lhs.type());
28 return binary_relation_exprt(std::move(rhs), ID_lt, std::move(lhs));
29}
30
32{
33 return binary_relation_exprt(from_integer(i, lhs.type()), ID_lt, lhs);
34}
35
37{
38 PRECONDITION(rhs.type() == lhs.type());
39 return binary_relation_exprt(std::move(lhs), ID_le, std::move(rhs));
40}
41
44{
45 return binary_relation_exprt(lhs, ID_le, from_integer(i, lhs.type()));
46}
47
49{
50 PRECONDITION(rhs.type() == lhs.type());
51 return binary_relation_exprt(std::move(lhs), ID_lt, std::move(rhs));
52}
53
55{
56 PRECONDITION(rhs.type() == lhs.type());
57 return equal_exprt(std::move(lhs), std::move(rhs));
58}
59
60inline equal_exprt equal_to(const exprt &lhs, mp_integer i)
61{
62 return equal_exprt(lhs, from_integer(i, lhs.type()));
63}
64
65// Representation of strings as arrays
67{
68public:
69 const typet &length_type() const
70 {
71 return to_array_type(type()).size().type();
72 }
73
75 {
76 return *this;
77 }
78
79 const exprt &content() const
80 {
81 return *this;
82 }
83
84 exprt operator[](const exprt &i) const
85 {
86 return index_exprt(content(), i);
87 }
88
90 {
92 }
93};
94
96{
97 PRECONDITION(expr.type().id() == ID_array);
98 return static_cast<array_string_exprt &>(expr);
99}
100
102{
103 PRECONDITION(expr.type().id() == ID_array);
104 return static_cast<const array_string_exprt &>(expr);
105}
106
107// Represent strings as a struct with a length field and a content field
109{
110public:
112 const exprt &_length,
113 const exprt &_content,
114 const typet &type)
115 : struct_exprt({_length, _content}, type)
116 {
117 }
118
119 refined_string_exprt(const exprt &_length, const exprt &_content)
121 _length,
122 _content,
123 refined_string_typet(_length.type(), to_pointer_type(_content.type())))
124 {
125 }
126
127 // Expression corresponding to the length of the string
128 const exprt &length() const
129 {
130 return op0();
131 }
133 {
134 return op0();
135 }
136
137 // Expression corresponding to the content (array of characters) of the string
138 const exprt &content() const
139 {
140 return op1();
141 }
143 {
144 return op1();
145 }
146
147 friend inline refined_string_exprt &to_string_expr(exprt &expr);
148};
149
151{
152 PRECONDITION(expr.id()==ID_struct);
153 PRECONDITION(expr.operands().size()==2);
154 return static_cast<refined_string_exprt &>(expr);
155}
156
157inline const refined_string_exprt &to_string_expr(const exprt &expr)
158{
159 PRECONDITION(expr.id()==ID_struct);
160 PRECONDITION(expr.operands().size()==2);
161 return static_cast<const refined_string_exprt &>(expr);
162}
163
164template <>
166{
167 return base.id() == ID_struct && base.operands().size() == 2 &&
169}
170
172{
173 INVARIANT(x.id() == ID_struct, "refined string exprs are struct");
174 validate_operands(x, 2, "refined string expr has length and content fields");
175 INVARIANT(
176 x.length().type().id() == ID_signedbv, "length should be a signed int");
177 INVARIANT(x.content().type().id() == ID_array, "content should be an array");
178}
179
180#endif
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt operator[](const exprt &i) const
Definition string_expr.h:84
const exprt & content() const
Definition string_expr.h:79
const typet & length_type() const
Definition string_expr.h:69
index_exprt operator[](int i) const
Definition string_expr.h:89
const exprt & size() const
Definition std_types.h:790
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
Array index operator.
Definition std_expr.h:1328
const irep_idt & id() const
Definition irep.h:396
exprt & op1()
Definition std_expr.h:850
exprt & op0()
Definition std_expr.h:844
const exprt & length() const
refined_string_exprt(const exprt &_length, const exprt &_content, const typet &type)
refined_string_exprt(const exprt &_length, const exprt &_content)
const exprt & content() const
friend refined_string_exprt & to_string_expr(exprt &expr)
Struct constructor from list of elements.
Definition std_expr.h:1722
The type of an expression, extends irept.
Definition type.h:29
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Type for string expressions used by the string solver.
bool is_refined_string_type(const typet &type)
BigInt mp_integer
Definition smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition string_expr.h:48
void validate_expr(const refined_string_exprt &x)
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:36
array_string_exprt & to_array_string_expr(exprt &expr)
Definition string_expr.h:95
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:19
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition string_expr.h:25
refined_string_exprt & to_string_expr(exprt &expr)
equal_exprt equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:54
bool can_cast_expr< refined_string_exprt >(const exprt &base)