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 "invariant.h"
21 #include "std_expr.h"
22 
29 {
30 public:
32  irep_idt _id,
33  const exprt &_op,
34  const exprt &_offset,
35  const typet &_type)
36  : binary_exprt(_op, _id, _offset, _type)
37  {
38  INVARIANT(
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 
50 template <>
51 inline bool can_cast_expr<byte_extract_exprt>(const exprt &base)
52 {
53  return base.id() == ID_byte_extract_little_endian ||
54  base.id() == ID_byte_extract_big_endian;
55 }
56 
57 inline const byte_extract_exprt &to_byte_extract_expr(const exprt &expr)
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 
69 inline void validate_expr(const byte_extract_exprt &value)
70 {
71  validate_operands(value, 2, "Byte extract must have two operands");
72 }
73 
76 
81 {
82 public:
84  irep_idt _id,
85  const exprt &_op,
86  const exprt &_offset,
87  const exprt &_value)
88  : ternary_exprt(_id, _op, _offset, _value, _op.type())
89  {
90  INVARIANT(
91  _id == ID_byte_update_little_endian || _id == ID_byte_update_big_endian,
92  "byte_update_exprt: Invalid ID");
93  }
94 
95  DEPRECATED(SINCE(2019, 5, 21, "use set_op or as_const instead"))
96  exprt &op() { return op0(); }
97  DEPRECATED(SINCE(2019, 5, 21, "use set_offset or as_const instead"))
98  exprt &offset() { return op1(); }
99  DEPRECATED(SINCE(2019, 5, 21, "use set_value or as_const instead"))
100  exprt &value() { return op2(); }
101 
102  void set_op(exprt e)
103  {
104  op0() = std::move(e);
105  }
107  {
108  op1() = std::move(e);
109  }
110  void set_value(exprt e)
111  {
112  op2() = std::move(e);
113  }
114 
115  const exprt &op() const { return op0(); }
116  const exprt &offset() const { return op1(); }
117  const exprt &value() const { return op2(); }
118 };
119 
120 template <>
121 inline bool can_cast_expr<byte_update_exprt>(const exprt &base)
122 {
123  return base.id() == ID_byte_update_little_endian ||
124  base.id() == ID_byte_update_big_endian;
125 }
126 
127 inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
128 {
129  PRECONDITION(expr.operands().size() == 3);
130  return static_cast<const byte_update_exprt &>(expr);
131 }
132 
134 {
135  PRECONDITION(expr.operands().size() == 3);
136  return static_cast<byte_update_exprt &>(expr);
137 }
138 
139 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:81
byte_extract_exprt::op
const exprt & op() const
Definition: byte_operators.h:46
ternary_exprt::op2
exprt & op2()
Definition: expr.h:108
typet
The type of an expression, extends irept.
Definition: type.h:29
ternary_exprt
An expression with three operands.
Definition: std_expr.h:55
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
byte_update_exprt::offset
const exprt & offset() const
Definition: byte_operators.h:116
validate_operands
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
ternary_exprt::op1
exprt & op1()
Definition: expr.h:105
byte_update_exprt::set_value
void set_value(exprt e)
Definition: byte_operators.h:110
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
byte_update_exprt::set_op
void set_op(exprt e)
Definition: byte_operators.h:102
can_cast_expr< byte_update_exprt >
bool can_cast_expr< byte_update_exprt >(const exprt &base)
Definition: byte_operators.h:121
byte_extract_exprt::byte_extract_exprt
byte_extract_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const typet &_type)
Definition: byte_operators.h:31
can_cast_expr< byte_extract_exprt >
bool can_cast_expr< byte_extract_exprt >(const exprt &base)
Definition: byte_operators.h:51
validate_expr
void validate_expr(const byte_extract_exprt &value)
Definition: byte_operators.h:69
byte_extract_exprt::offset
const exprt & offset() const
Definition: byte_operators.h:47
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:127
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
ternary_exprt::op0
exprt & op0()
Definition: expr.h:102
irept::id
const irep_idt & id() const
Definition: irep.h:418
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
byte_update_id
irep_idt byte_update_id()
Definition: byte_operators.cpp:30
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
byte_update_exprt::value
const exprt & value() const
Definition: byte_operators.h:117
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
byte_update_exprt::value
exprt & value()
Definition: byte_operators.h:100
invariant.h
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
byte_update_exprt::offset
exprt & offset()
Definition: byte_operators.h:98
exprt::operands
operandst & operands()
Definition: expr.h:95
byte_update_exprt::op
exprt & op()
Definition: byte_operators.h:96
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
std_expr.h
API to expression classes.
byte_update_exprt::op
const exprt & op() const
Definition: byte_operators.h:115
byte_update_exprt::byte_update_exprt
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)
Definition: byte_operators.h:83
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
validation_modet::INVARIANT
@ INVARIANT
byte_update_exprt::set_offset
void set_offset(exprt e)
Definition: byte_operators.h:106