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
13
bvt
boolbvt::convert_bswap
(
const
bswap_exprt
&expr)
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:200
bswap_exprt::get_bits_per_byte
std::size_t get_bits_per_byte() const
Definition:
std_expr.h:583
invariant.h
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:68
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition:
boolbv.h:92
messaget::result
mstreamt & result() const
Definition:
message.h:396
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition:
boolbv.h:110
unary_exprt::op
const exprt & op() const
Definition:
std_expr.h:371
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition:
boolbv.cpp:112
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:568
boolbv.h
solvers
flattening
boolbv_bswap.cpp
Generated by
1.8.16