byte_operators.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_BYTE_OPERATORS_H
#define CPROVER_UTIL_BYTE_OPERATORS_H
 
#include "invariant.h"
#include "std_expr.h"
 
class byte_extract_exprt : public binary_exprt
{
public:
  byte_extract_exprt(
    irep_idt _id,
    const exprt &_op,
    const exprt &_offset,
    std::size_t bits_per_byte,
    const typet &_type)
    : binary_exprt(_op, _id, _offset, _type)
  {
    INVARIANT(
      _id == ID_byte_extract_little_endian || _id == ID_byte_extract_big_endian,
      "byte_extract_exprt: Invalid ID");
 
    set_bits_per_byte(bits_per_byte);
  }
 
  exprt &op() { return op0(); }
  exprt &offset() { return op1(); }
 
  const exprt &op() const { return op0(); }
  const exprt &offset() const { return op1(); }
 
  std::size_t get_bits_per_byte() const
  {
    return get_size_t(ID_bits_per_byte);
  }
 
  void set_bits_per_byte(std::size_t bits_per_byte)
  {
    set_size_t(ID_bits_per_byte, bits_per_byte);
  }
};
 
template <>
inline bool can_cast_expr<byte_extract_exprt>(const exprt &base)
{
  return base.id() == ID_byte_extract_little_endian ||
         base.id() == ID_byte_extract_big_endian;
}
 
inline const byte_extract_exprt &to_byte_extract_expr(const exprt &expr)
{
  PRECONDITION(expr.operands().size() == 2);
  return static_cast<const byte_extract_exprt &>(expr);
}
 
inline byte_extract_exprt &to_byte_extract_expr(exprt &expr)
{
  PRECONDITION(expr.operands().size() == 2);
  return static_cast<byte_extract_exprt &>(expr);
}
 
inline void validate_expr(const byte_extract_exprt &value)
{
  validate_operands(value, 2, "Byte extract must have two operands");
}
 
class byte_update_exprt : public ternary_exprt
{
public:
  byte_update_exprt(
    irep_idt _id,
    const exprt &_op,
    const exprt &_offset,
    const exprt &_value,
    std::size_t bits_per_byte)
    : ternary_exprt(_id, _op, _offset, _value, _op.type())
  {
    INVARIANT(
      _id == ID_byte_update_little_endian || _id == ID_byte_update_big_endian,
      "byte_update_exprt: Invalid ID");
 
    set_bits_per_byte(bits_per_byte);
  }
 
  void set_op(exprt e)
  {
    op0() = std::move(e);
  }
  void set_offset(exprt e)
  {
    op1() = std::move(e);
  }
  void set_value(exprt e)
  {
    op2() = std::move(e);
  }
 
  const exprt &op() const { return op0(); }
  const exprt &offset() const { return op1(); }
  const exprt &value() const { return op2(); }
 
  std::size_t get_bits_per_byte() const
  {
    return get_size_t(ID_bits_per_byte);
  }
 
  void set_bits_per_byte(std::size_t bits_per_byte)
  {
    set_size_t(ID_bits_per_byte, bits_per_byte);
  }
};
 
template <>
inline bool can_cast_expr<byte_update_exprt>(const exprt &base)
{
  return base.id() == ID_byte_update_little_endian ||
         base.id() == ID_byte_update_big_endian;
}
 
inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
{
  PRECONDITION(expr.operands().size() == 3);
  return static_cast<const byte_update_exprt &>(expr);
}
 
inline byte_update_exprt &to_byte_update_expr(exprt &expr)
{
  PRECONDITION(expr.operands().size() == 3);
  return static_cast<byte_update_exprt &>(expr);
}
 
byte_extract_exprt
make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type);
 
byte_update_exprt
make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
 
bool has_byte_operator(const exprt &src);
 
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns);
 
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns);
 
exprt lower_byte_operators(const exprt &src, const namespacet &ns);
 
#endif // CPROVER_UTIL_BYTE_OPERATORS_H