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