CBMC
Loading...
Searching...
No Matches
byte_operators.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 "invariant.h"
21#include "std_expr.h"
22
29{
30public:
33 const exprt &_op,
34 const exprt &_offset,
35 std::size_t bits_per_byte,
36 const typet &_type)
37 : binary_exprt(_op, _id, _offset, _type)
38 {
41 "byte_extract_exprt: Invalid ID");
42
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 std::size_t get_bits_per_byte() const
53 {
55 }
56
61};
62
63template <>
65{
66 return base.id() == ID_byte_extract_little_endian ||
68}
69
71{
72 PRECONDITION(expr.operands().size() == 2);
73 return static_cast<const byte_extract_exprt &>(expr);
74}
75
77{
78 PRECONDITION(expr.operands().size() == 2);
79 return static_cast<byte_extract_exprt &>(expr);
80}
81
82inline void validate_expr(const byte_extract_exprt &value)
83{
84 validate_operands(value, 2, "Byte extract must have two operands");
85}
86
91{
92public:
95 const exprt &_op,
96 const exprt &_offset,
97 const exprt &_value,
98 std::size_t bits_per_byte)
99 : ternary_exprt(_id, _op, _offset, _value, _op.type())
100 {
101 INVARIANT(
103 "byte_update_exprt: Invalid ID");
104
106 }
107
108 void set_op(exprt e)
109 {
110 op0() = std::move(e);
111 }
113 {
114 op1() = std::move(e);
115 }
117 {
118 op2() = std::move(e);
119 }
120
121 const exprt &op() const { return op0(); }
122 const exprt &offset() const { return op1(); }
123 const exprt &value() const { return op2(); }
124
125 std::size_t get_bits_per_byte() const
126 {
128 }
129
134};
135
136template <>
138{
139 return base.id() == ID_byte_update_little_endian ||
141}
142
144{
145 PRECONDITION(expr.operands().size() == 3);
146 return static_cast<const byte_update_exprt &>(expr);
147}
148
150{
151 PRECONDITION(expr.operands().size() == 3);
152 return static_cast<byte_update_exprt &>(expr);
153}
154
158make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type);
159
163make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
164
167bool has_byte_operator(const exprt &src);
168
177
186
193exprt lower_byte_operators(const exprt &src, const namespacet &ns);
194
195#endif // CPROVER_UTIL_BYTE_OPERATORS_H
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
byte_update_exprt make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
Construct a byte_update_exprt with endianness and byte width matching the current configuration.
void validate_expr(const byte_extract_exprt &value)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bool has_byte_operator(const exprt &src)
Return true iff src or one of its operands contain a byte extract or byte update expression.
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
Rewrite a byte update expression to more fundamental operations.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
bool can_cast_expr< byte_update_exprt >(const exprt &base)
bool can_cast_expr< byte_extract_exprt >(const exprt &base)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A base class for binary expressions.
Definition std_expr.h:638
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
Expression of type type extracted from some object op starting at position offset (given in number of...
byte_extract_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, std::size_t bits_per_byte, const typet &_type)
const exprt & offset() const
const exprt & op() const
void set_bits_per_byte(std::size_t bits_per_byte)
std::size_t get_bits_per_byte() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value, std::size_t bits_per_byte)
const exprt & offset() const
void set_offset(exprt e)
void set_bits_per_byte(std::size_t bits_per_byte)
void set_value(exprt e)
const exprt & op() const
void set_op(exprt e)
std::size_t get_bits_per_byte() const
const exprt & value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:67
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:82
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
An expression with three operands.
Definition std_expr.h:67
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
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
#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.