CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 "pointer_expr.h"
17#include "refined_string_type.h"
18#include "std_expr.h"
19
21{
22 PRECONDITION(rhs.type() == lhs.type());
23 return binary_relation_exprt(std::move(lhs), ID_ge, std::move(rhs));
24}
25
27{
28 PRECONDITION(rhs.type() == lhs.type());
29 return binary_relation_exprt(std::move(rhs), ID_lt, std::move(lhs));
30}
31
33{
34 return binary_relation_exprt(from_integer(i, lhs.type()), ID_lt, lhs);
35}
36
38{
39 PRECONDITION(rhs.type() == lhs.type());
40 return binary_relation_exprt(std::move(lhs), ID_le, std::move(rhs));
41}
42
45{
46 return binary_relation_exprt(lhs, ID_le, from_integer(i, lhs.type()));
47}
48
50{
51 PRECONDITION(rhs.type() == lhs.type());
52 return binary_relation_exprt(std::move(lhs), ID_lt, std::move(rhs));
53}
54
56{
57 PRECONDITION(rhs.type() == lhs.type());
58 return equal_exprt(std::move(lhs), std::move(rhs));
59}
60
61inline equal_exprt equal_to(const exprt &lhs, mp_integer i)
62{
63 return equal_exprt(lhs, from_integer(i, lhs.type()));
64}
65
66// Representation of strings as arrays
68{
69public:
70 const typet &length_type() const
71 {
72 return to_array_type(type()).size().type();
73 }
74
76 {
77 return *this;
78 }
79
80 const exprt &content() const
81 {
82 return *this;
83 }
84
85 exprt operator[](const exprt &i) const
86 {
87 return index_exprt(content(), i);
88 }
89
91 {
93 }
94};
95
97{
98 PRECONDITION(expr.type().id() == ID_array);
99 return static_cast<array_string_exprt &>(expr);
100}
101
103{
104 PRECONDITION(expr.type().id() == ID_array);
105 return static_cast<const array_string_exprt &>(expr);
106}
107
108// Represent strings as a struct with a length field and a content field
110{
111public:
113 const exprt &_length,
114 const exprt &_content,
115 const typet &type)
117 {
118 }
119
127
128 // Expression corresponding to the length of the string
129 const exprt &length() const
130 {
131 return op0();
132 }
134 {
135 return op0();
136 }
137
138 // Expression corresponding to the content (array of characters) of the string
139 const exprt &content() const
140 {
141 return op1();
142 }
144 {
145 return op1();
146 }
147
148 friend inline refined_string_exprt &to_string_expr(exprt &expr);
149};
150
152{
153 PRECONDITION(expr.id()==ID_struct);
154 PRECONDITION(expr.operands().size()==2);
155 return static_cast<refined_string_exprt &>(expr);
156}
157
158inline const refined_string_exprt &to_string_expr(const exprt &expr)
159{
160 PRECONDITION(expr.id()==ID_struct);
161 PRECONDITION(expr.operands().size()==2);
162 return static_cast<const refined_string_exprt &>(expr);
163}
164
165template <>
167{
168 return base.id() == ID_struct && base.operands().size() == 2 &&
170}
171
173{
174 INVARIANT(x.id() == ID_struct, "refined string exprs are struct");
175 validate_operands(x, 2, "refined string expr has length and content fields");
176 INVARIANT(
177 x.length().type().id() == ID_signedbv, "length should be a signed int");
178 INVARIANT(x.content().type().id() == ID_array, "content should be an array");
179}
180
181#endif
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
exprt operator[](const exprt &i) const
Definition string_expr.h:85
const exprt & content() const
Definition string_expr.h:80
const typet & length_type() const
Definition string_expr.h:70
index_exprt operator[](int i) const
Definition string_expr.h:90
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
Array index operator.
Definition std_expr.h:1470
const irep_idt & id() const
Definition irep.h:388
exprt & op1()
Definition std_expr.h:938
exprt & op0()
Definition std_expr.h:932
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:1877
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
API to expression classes for Pointers.
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:17
#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:888
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition string_expr.h:49
void validate_expr(const refined_string_exprt &x)
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:37
array_string_exprt & to_array_string_expr(exprt &expr)
Definition string_expr.h:96
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:20
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition string_expr.h:26
refined_string_exprt & to_string_expr(exprt &expr)
equal_exprt equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:55
bool can_cast_expr< refined_string_exprt >(const exprt &base)