cprover
Loading...
Searching...
No Matches
boolbv_byte_update.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <util/arith_tools.h>
12#include <util/byte_operators.h>
13#include <util/invariant.h>
14
16
18{
19 // if we update (from) an unbounded array, lower the expression as the array
20 // logic does not handle byte operators
21 if(
22 is_unbounded_array(expr.op().type()) ||
24 {
25 return convert_bv(lower_byte_update(expr, ns));
26 }
27
28 const exprt &op = expr.op();
29 const exprt &offset_expr=expr.offset();
30 const exprt &value=expr.value();
31
33 expr.id() == ID_byte_update_little_endian ||
34 expr.id() == ID_byte_update_big_endian);
35 const bool little_endian = expr.id() == ID_byte_update_little_endian;
36
37 bvt bv=convert_bv(op);
38
39 const bvt &value_bv=convert_bv(value);
40 std::size_t update_width=value_bv.size();
41 std::size_t byte_width=8;
42
43 if(update_width>bv.size())
44 update_width=bv.size();
45
46 // see if the byte number is constant
47
48 const auto index = numeric_cast<mp_integer>(offset_expr);
49 if(index.has_value())
50 {
51 // yes!
52 const mp_integer offset = *index * 8;
53
54 if(offset+update_width>mp_integer(bv.size()) || offset<0)
55 {
56 // out of bounds
57 }
58 else
59 {
60 endianness_mapt map_op = endianness_map(op.type(), little_endian);
61 endianness_mapt map_value = endianness_map(value.type(), little_endian);
62
63 const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);
64
65 for(std::size_t i = 0; i < update_width; i++)
66 {
67 size_t index_op = map_op.map_bit(offset_i + i);
68 size_t index_value = map_value.map_bit(i);
69
71 index_op < bv.size(), "bit vector index shall be within bounds");
73 index_value < value_bv.size(),
74 "bit vector index shall be within bounds");
75
76 bv[index_op] = value_bv[index_value];
77 }
78 }
79
80 return bv;
81 }
82
83 // byte_update with variable index
84 for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
85 {
86 // index condition
88 offset_expr, from_integer(offset / byte_width, offset_expr.type()));
90
91 endianness_mapt map_op = endianness_map(op.type(), little_endian);
92 endianness_mapt map_value = endianness_map(value.type(), little_endian);
93
94 for(std::size_t bit=0; bit<update_width; bit++)
95 if(offset+bit<bv.size())
96 {
97 std::size_t bv_o=map_op.map_bit(offset+bit);
98 std::size_t value_bv_o=map_value.map_bit(bit);
99
100 bv[bv_o]=prop.lselect(equal, value_bv[value_bv_o], bv[bv_o]);
101 }
102 }
103
104 return bv;
105}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Expression classes for byte-level operators.
const namespacet & ns
Definition: arrays.h:56
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:547
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:40
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition: boolbv.h:105
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
const exprt & op() const
const exprt & value() const
Maps a big-endian offset to a little-endian offset.
size_t map_bit(size_t bit) const
Equality.
Definition: std_expr.h:1225
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
const irep_idt & id() const
Definition: irep.h:396
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::vector< literalt > bvt
Definition: literal.h:201
BigInt mp_integer
Definition: smt_terms.h:12
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423