Skip to content

Commit 8ab6023

Browse files
author
Natasha Yogananda Jeppu
committed
Add utility modules for byte extract and update metric reporting
Provides the utility modules required to report byte extract and byte update metrics. This includes helper functions to check if given expr is a byte extract or update and an SSA_stept class member function that returns the relevant ssa expression from a given SSA step. If the SSA step is a shared_read or shared_write, return ssa_lhs, else return cond_expr. Also, added an invariant in the constructor for byte_extract_exprt and byte_update_exprt to confirm _id is valid for additional correctness checks.
1 parent daa4178 commit 8ab6023

File tree

2 files changed

+19
-1
lines changed

2 files changed

+19
-1
lines changed

src/goto-symex/ssa_step.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,11 @@ class SSA_stept
148148
exprt cond_handle;
149149
std::string comment;
150150

151+
exprt get_ssa_expr() const
152+
{
153+
return ((is_shared_read() || is_shared_write()) ? ssa_lhs : cond_expr);
154+
}
155+
151156
// for INPUT/OUTPUT
152157
irep_idt format_string, io_id;
153158
bool formatted = false;

src/util/byte_operators.h

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
2525
/// The object can either be interpreted in big endian or little endian, which
2626
/// is reflected by the \c id of the expression which is either
2727
/// \c ID_byte_extract_big_endian or \c ID_byte_extract_little_endian
28-
class byte_extract_exprt:public binary_exprt
28+
class byte_extract_exprt : public binary_exprt
2929
{
3030
public:
3131
byte_extract_exprt(
@@ -35,6 +35,9 @@ class byte_extract_exprt:public binary_exprt
3535
const typet &_type)
3636
: binary_exprt(_op, _id, _offset, _type)
3737
{
38+
INVARIANT(
39+
_id == ID_byte_extract_little_endian || _id == ID_byte_extract_big_endian,
40+
"byte_extract_exprt: Invalid ID");
3841
}
3942

4043
exprt &op() { return op0(); }
@@ -84,6 +87,9 @@ class byte_update_exprt : public ternary_exprt
8487
const exprt &_value)
8588
: ternary_exprt(_id, _op, _offset, _value, _op.type())
8689
{
90+
INVARIANT(
91+
_id == ID_byte_update_little_endian || _id == ID_byte_update_big_endian,
92+
"byte_update_exprt: Invalid ID");
8793
}
8894

8995
DEPRECATED(SINCE(2019, 5, 21, "use set_op or as_const instead"))
@@ -111,6 +117,13 @@ class byte_update_exprt : public ternary_exprt
111117
const exprt &value() const { return op2(); }
112118
};
113119

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+
114127
inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
115128
{
116129
PRECONDITION(expr.operands().size() == 3);

0 commit comments

Comments
 (0)