cprover
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:
32 irep_idt _id,
33 const exprt &_op,
34 const exprt &_offset,
35 const typet &_type)
36 : binary_exprt(_op, _id, _offset, _type)
37 {
39 _id == ID_byte_extract_little_endian || _id == ID_byte_extract_big_endian,
40 "byte_extract_exprt: Invalid ID");
41 }
42
43 exprt &op() { return op0(); }
44 exprt &offset() { return op1(); }
45
46 const exprt &op() const { return op0(); }
47 const exprt &offset() const { return op1(); }
48};
49
50template <>
52{
53 return base.id() == ID_byte_extract_little_endian ||
54 base.id() == ID_byte_extract_big_endian;
55}
56
58{
59 PRECONDITION(expr.operands().size() == 2);
60 return static_cast<const byte_extract_exprt &>(expr);
61}
62
64{
65 PRECONDITION(expr.operands().size() == 2);
66 return static_cast<byte_extract_exprt &>(expr);
67}
68
69inline void validate_expr(const byte_extract_exprt &value)
70{
71 validate_operands(value, 2, "Byte extract must have two operands");
72}
73
78{
79public:
81 irep_idt _id,
82 const exprt &_op,
83 const exprt &_offset,
84 const exprt &_value)
85 : ternary_exprt(_id, _op, _offset, _value, _op.type())
86 {
88 _id == ID_byte_update_little_endian || _id == ID_byte_update_big_endian,
89 "byte_update_exprt: Invalid ID");
90 }
91
92 void set_op(exprt e)
93 {
94 op0() = std::move(e);
95 }
97 {
98 op1() = std::move(e);
99 }
101 {
102 op2() = std::move(e);
103 }
104
105 const exprt &op() const { return op0(); }
106 const exprt &offset() const { return op1(); }
107 const exprt &value() const { return op2(); }
108};
109
110template <>
112{
113 return base.id() == ID_byte_update_little_endian ||
114 base.id() == ID_byte_update_big_endian;
115}
116
118{
119 PRECONDITION(expr.operands().size() == 3);
120 return static_cast<const byte_update_exprt &>(expr);
121}
122
124{
125 PRECONDITION(expr.operands().size() == 3);
126 return static_cast<byte_update_exprt &>(expr);
127}
128
132make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type);
133
137make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
138
139#endif // CPROVER_UTIL_BYTE_OPERATORS_H
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
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)
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)
A base class for binary expressions.
Definition std_expr.h:550
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
Expression of type type extracted from some object op starting at position offset (given in number of...
const exprt & offset() const
const exprt & op() const
byte_extract_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const typet &_type)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
void set_offset(exprt e)
void set_value(exprt e)
const exprt & op() const
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)
void set_op(exprt e)
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:37
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
const irep_idt & id() const
Definition irep.h:396
An expression with three operands.
Definition std_expr.h:53
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
exprt & op2()
Definition expr.h:105
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.