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 <iostream>
12 
13 #include <util/arith_tools.h>
14 #include <util/byte_operators.h>
15 #include <util/invariant.h>
16 
17 #include "bv_endianness_map.h"
18 
20 {
21  const exprt &op = expr.op();
22  const exprt &offset_expr=expr.offset();
23  const exprt &value=expr.value();
24 
26  expr.id() == ID_byte_update_little_endian ||
27  expr.id() == ID_byte_update_big_endian);
28  const bool little_endian = expr.id() == ID_byte_update_little_endian;
29 
30  bvt bv=convert_bv(op);
31 
32  const bvt &value_bv=convert_bv(value);
33  std::size_t update_width=value_bv.size();
34  std::size_t byte_width=8;
35 
36  if(update_width>bv.size())
37  update_width=bv.size();
38 
39  // see if the byte number is constant
40 
41  const auto index = numeric_cast<mp_integer>(offset_expr);
42  if(index.has_value())
43  {
44  // yes!
45  const mp_integer offset = *index * 8;
46 
47  if(offset+update_width>mp_integer(bv.size()) || offset<0)
48  {
49  // out of bounds
50  }
51  else
52  {
53  if(little_endian)
54  {
55  for(std::size_t i=0; i<update_width; i++)
56  bv[numeric_cast_v<std::size_t>(offset + i)] = value_bv[i];
57  }
58  else
59  {
60  bv_endianness_mapt map_op(op.type(), false, ns, boolbv_width);
61  bv_endianness_mapt map_value(value.type(), false, ns, boolbv_width);
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 
70  INVARIANT(
71  index_op < bv.size(), "bit vector index shall be within bounds");
72  INVARIANT(
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 
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  equality.lhs()=offset_expr;
90  equality.rhs()=from_integer(offset/byte_width, offset_expr.type());
91  literalt equal=convert(equality);
92 
93  bv_endianness_mapt map_op(op.type(), little_endian, ns, boolbv_width);
94  bv_endianness_mapt map_value(value.type(), little_endian, ns, boolbv_width);
95 
96  for(std::size_t bit=0; bit<update_width; bit++)
97  if(offset+bit<bv.size())
98  {
99  std::size_t bv_o=map_op.map_bit(offset+bit);
100  std::size_t value_bv_o=map_value.map_bit(bit);
101 
102  bv[bv_o]=prop.lselect(equal, value_bv[value_bv_o], bv[bv_o]);
103  }
104  }
105 
106  return bv;
107 }
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
boolbvt::convert_byte_update
virtual bvt convert_byte_update(const byte_update_exprt &expr)
Definition: boolbv_byte_update.cpp:19
byte_update_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:70
arith_tools.h
bv_endianness_map.h
bvt
std::vector< literalt > bvt
Definition: literal.h:200
bv_endianness_mapt
Map bytes according to the configured endianness.
Definition: bv_endianness_map.h:20
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
exprt
Base class for all expressions.
Definition: expr.h:54
invariant.h
equal_exprt
Equality.
Definition: std_expr.h:1484
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
byte_operators.h
Expression classes for byte-level operators.
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:92
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:48
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
irept::id
const irep_idt & id() const
Definition: irep.h:259
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
byte_update_exprt::value
exprt & value()
Definition: byte_operators.h:84
literalt
Definition: literal.h:24
byte_update_exprt::offset
exprt & offset()
Definition: byte_operators.h:83
boolbv.h
byte_update_exprt::op
exprt & op()
Definition: byte_operators.h:82
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.h:152