cprover
byte_operators.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_BYTE_OPERATORS_H
11 #define CPROVER_UTIL_BYTE_OPERATORS_H
12 
20 #include "expr.h"
21 
25 {
26 public:
27  explicit byte_extract_exprt(irep_idt _id):exprt(_id)
28  {
29  operands().resize(2);
30  }
31 
32  explicit byte_extract_exprt(irep_idt _id, const typet &_type):
33  exprt(_id, _type)
34  {
35  operands().resize(2);
36  }
37 
39  irep_idt _id,
40  const exprt &_op, const exprt &_offset, const typet &_type):
41  exprt(_id, _type)
42  {
43  copy_to_operands(_op, _offset);
44  }
45 
46  exprt &op() { return op0(); }
47  exprt &offset() { return op1(); }
48 
49  const exprt &op() const { return op0(); }
50  const exprt &offset() const { return op1(); }
51 };
52 
53 inline const byte_extract_exprt &to_byte_extract_expr(const exprt &expr)
54 {
55  assert(expr.operands().size()==2);
56  return static_cast<const byte_extract_exprt &>(expr);
57 }
58 
60 {
61  assert(expr.operands().size()==2);
62  return static_cast<byte_extract_exprt &>(expr);
63 }
64 
67 
71 {
72 public:
74  byte_extract_exprt(ID_byte_extract_little_endian)
75  {
76  }
77 };
78 
81 {
82  assert(expr.id()==ID_byte_extract_little_endian && expr.operands().size()==2);
83  return static_cast<const byte_extract_little_endian_exprt &>(expr);
84 }
85 
88 {
89  assert(expr.id()==ID_byte_extract_little_endian && expr.operands().size()==2);
90  return static_cast<byte_extract_little_endian_exprt &>(expr);
91 }
92 
96 {
97 public:
99  byte_extract_exprt(ID_byte_extract_big_endian)
100  {
101  }
102 
104  const exprt &_op, const exprt &_offset, const typet &_type):
105  byte_extract_exprt(ID_byte_extract_big_endian, _op, _offset, _type)
106  {
107  }
108 };
109 
112 {
113  assert(expr.id()==ID_byte_extract_big_endian && expr.operands().size()==2);
114  return static_cast<const byte_extract_big_endian_exprt &>(expr);
115 }
116 
119 {
120  assert(expr.id()==ID_byte_extract_big_endian && expr.operands().size()==2);
121  return static_cast<byte_extract_big_endian_exprt &>(expr);
122 }
123 
127 {
128 public:
129  explicit byte_update_exprt(irep_idt _id):exprt(_id)
130  {
131  operands().resize(3);
132  }
133 
134  byte_update_exprt(irep_idt _id, const typet &_type):
135  exprt(_id, _type)
136  {
137  operands().resize(3);
138  }
139 
141  irep_idt _id,
142  const exprt &_op, const exprt &_offset, const exprt &_value):
143  exprt(_id, _op.type())
144  {
145  copy_to_operands(_op, _offset, _value);
146  }
147 
148  exprt &op() { return op0(); }
149  exprt &offset() { return op1(); }
150  exprt &value() { return op2(); }
151 
152  const exprt &op() const { return op0(); }
153  const exprt &offset() const { return op1(); }
154  const exprt &value() const { return op2(); }
155 };
156 
157 inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
158 {
159  assert(expr.operands().size()==3);
160  return static_cast<const byte_update_exprt &>(expr);
161 }
162 
164 {
165  assert(expr.operands().size()==3);
166  return static_cast<byte_update_exprt &>(expr);
167 }
168 
172 {
173 public:
175  byte_update_exprt(ID_byte_update_little_endian)
176  {
177  }
178 
180  const exprt &_op, const exprt &_offset, const exprt &_value):
181  byte_update_exprt(ID_byte_update_little_endian, _op, _offset, _value)
182  {
183  }
184 };
185 
188 {
189  assert(expr.id()==ID_byte_update_little_endian && expr.operands().size()==3);
190  return static_cast<const byte_update_little_endian_exprt &>(expr);
191 }
192 
195 {
196  assert(expr.id()==ID_byte_update_little_endian && expr.operands().size()==3);
197  return static_cast<byte_update_little_endian_exprt &>(expr);
198 }
199 
203 {
204 public:
206  byte_update_exprt(ID_byte_update_big_endian)
207  {
208  }
209 
211  const exprt &_op, const exprt &_offset, const exprt &_value):
212  byte_update_exprt(ID_byte_update_big_endian, _op, _offset, _value)
213  {
214  }
215 };
216 
217 inline const byte_update_big_endian_exprt
219 {
220  assert(expr.id()==ID_byte_update_big_endian && expr.operands().size()==3);
221  return static_cast<const byte_update_big_endian_exprt &>(expr);
222 }
223 
226 {
227  assert(expr.id()==ID_byte_update_big_endian && expr.operands().size()==3);
228  return static_cast<byte_update_big_endian_exprt &>(expr);
229 }
230 
231 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
byte_extract_exprt(irep_idt _id, const typet &_type)
The type of an expression.
Definition: type.h:20
byte_extract_exprt(irep_idt _id)
const byte_update_big_endian_exprt & to_byte_update_big_endian_expr(const exprt &expr)
const exprt & offset() const
const byte_update_little_endian_exprt & to_byte_update_little_endian_expr(const exprt &expr)
irep_idt byte_update_id()
const exprt & op() const
exprt & op0()
Definition: expr.h:84
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
const exprt & value() const
typet & type()
Definition: expr.h:60
const exprt & op() const
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
byte_extract_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const typet &_type)
const irep_idt & id() const
Definition: irep.h:189
byte_extract_big_endian_exprt(const exprt &_op, const exprt &_offset, const typet &_type)
const exprt & offset() const
exprt & op1()
Definition: expr.h:87
irep_idt byte_extract_id()
byte_update_big_endian_exprt(const exprt &_op, const exprt &_offset, const exprt &_value)
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)
const byte_extract_little_endian_exprt & to_byte_extract_little_endian_expr(const exprt &expr)
byte_update_exprt(irep_idt _id, const typet &_type)
const byte_extract_big_endian_exprt & to_byte_extract_big_endian_expr(const exprt &expr)
Base class for all expressions.
Definition: expr.h:46
TO_BE_DOCUMENTED.
exprt & op2()
Definition: expr.h:90
byte_update_exprt(irep_idt _id)
byte_update_little_endian_exprt(const exprt &_op, const exprt &_offset, const exprt &_value)
operandst & operands()
Definition: expr.h:70
TO_BE_DOCUMENTED.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)