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 
78 {
79 public:
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  {
87  INVARIANT(
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  }
96  void set_offset(exprt e)
97  {
98  op1() = std::move(e);
99  }
100  void set_value(exprt e)
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 
110 template <>
111 inline bool can_cast_expr<byte_update_exprt>(const exprt &base)
112 {
113  return base.id() == ID_byte_update_little_endian ||
114  base.id() == ID_byte_update_big_endian;
115 }
116 
117 inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
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 
132 make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type);
133 
137 make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
138 
139 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
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)
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)
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bool can_cast_expr< byte_extract_exprt >(const exprt &base)
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
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 & value() const
void set_offset(exprt e)
void set_value(exprt e)
const exprt & op() const
const exprt & offset() const
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)
void set_op(exprt e)
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:407
An expression with three operands.
Definition: std_expr.h:53
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
The type of an expression, extends irept.
Definition: type.h:28
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
API to expression classes.