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 
18 #include "bv_endianness_map.h"
19 
21 {
22  // if we update (from) an unbounded array, lower the expression as the array
23  // logic does not handle byte operators
24  if(
25  is_unbounded_array(expr.op().type()) ||
26  is_unbounded_array(expr.value().type()))
27  {
28  return convert_bv(lower_byte_update(expr, ns));
29  }
30 
31  const exprt &op = expr.op();
32  const exprt &offset_expr=expr.offset();
33  const exprt &value=expr.value();
34 
36  expr.id() == ID_byte_update_little_endian ||
37  expr.id() == ID_byte_update_big_endian);
38  const bool little_endian = expr.id() == ID_byte_update_little_endian;
39 
40  bvt bv=convert_bv(op);
41 
42  const bvt &value_bv=convert_bv(value);
43  std::size_t update_width=value_bv.size();
44  std::size_t byte_width=8;
45 
46  if(update_width>bv.size())
47  update_width=bv.size();
48 
49  // see if the byte number is constant
50 
51  const auto index = numeric_cast<mp_integer>(offset_expr);
52  if(index.has_value())
53  {
54  // yes!
55  const mp_integer offset = *index * 8;
56 
57  if(offset+update_width>mp_integer(bv.size()) || offset<0)
58  {
59  // out of bounds
60  }
61  else
62  {
63  if(little_endian)
64  {
65  for(std::size_t i=0; i<update_width; i++)
66  bv[numeric_cast_v<std::size_t>(offset + i)] = value_bv[i];
67  }
68  else
69  {
70  bv_endianness_mapt map_op(op.type(), false, ns, boolbv_width);
71  bv_endianness_mapt map_value(value.type(), false, ns, boolbv_width);
72 
73  const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);
74 
75  for(std::size_t i=0; i<update_width; i++)
76  {
77  size_t index_op=map_op.map_bit(offset_i+i);
78  size_t index_value=map_value.map_bit(i);
79 
80  INVARIANT(
81  index_op < bv.size(), "bit vector index shall be within bounds");
82  INVARIANT(
83  index_value < value_bv.size(),
84  "bit vector index shall be within bounds");
85 
86  bv[index_op]=value_bv[index_value];
87  }
88  }
89  }
90 
91  return bv;
92  }
93 
94  // byte_update with variable index
95  for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
96  {
97  // index condition
99  offset_expr, from_integer(offset / byte_width, offset_expr.type()));
100  literalt equal=convert(equality);
101 
102  bv_endianness_mapt map_op(op.type(), little_endian, ns, boolbv_width);
103  bv_endianness_mapt map_value(value.type(), little_endian, ns, boolbv_width);
104 
105  for(std::size_t bit=0; bit<update_width; bit++)
106  if(offset+bit<bv.size())
107  {
108  std::size_t bv_o=map_op.map_bit(offset+bit);
109  std::size_t value_bv_o=map_value.map_bit(bit);
110 
111  bv[bv_o]=prop.lselect(equal, value_bv[value_bv_o], bv[bv_o]);
112  }
113  }
114 
115  return bv;
116 }
boolbvt::convert_byte_update
virtual bvt convert_byte_update(const byte_update_exprt &expr)
Definition: boolbv_byte_update.cpp:20
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
bv_endianness_map.h
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bv_endianness_mapt
Map bytes according to the configured endianness.
Definition: bv_endianness_map.h:21
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
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:2057
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
equal_exprt
Equality.
Definition: std_expr.h:1190
expr_lowering.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
byte_operators.h
Expression classes for byte-level operators.
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:48
irept::id
const irep_idt & id() const
Definition: irep.h:418
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
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
expr_util.h
Deprecated expression utility functions.
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
byte_update_exprt::value
exprt & value()
Definition: byte_operators.h:100
literalt
Definition: literal.h:26
byte_update_exprt::offset
exprt & offset()
Definition: byte_operators.h:98
boolbv.h
byte_update_exprt::op
exprt & op()
Definition: byte_operators.h:96
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
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131