cprover
boolbv_bswap.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bit-blasting of bswap
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/invariant.h>
12 
14 {
15  const std::size_t width = boolbv_width(expr.type());
16 
17  // width must be multiple of bytes
18  const std::size_t byte_bits = expr.get_bits_per_byte();
19  if(width % byte_bits != 0)
20  return conversion_failed(expr);
21 
22  bvt result = convert_bv(expr.op(), width);
23 
24  std::size_t dest_base = width;
25 
26  for(std::size_t src = 0; src < width; ++src)
27  {
28  std::size_t bit_offset = src % byte_bits;
29  if(bit_offset == 0)
30  dest_base -= byte_bits;
31 
32  if(src >= dest_base)
33  break;
34 
35  result[src].swap(result[dest_base + bit_offset]);
36  }
37 
38  return result;
39 }
bvt
std::vector< literalt > bvt
Definition: literal.h:201
invariant.h
bswap_exprt::get_bits_per_byte
std::size_t get_bits_per_byte() const
Definition: std_expr.h:485
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:119
boolbvt::convert_bswap
virtual bvt convert_bswap(const bswap_exprt &expr)
Definition: boolbv_bswap.cpp:13
bswap_exprt
The byte swap expression.
Definition: std_expr.h:471
boolbv.h