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 #include <cassert>
13 
14 #include <util/arith_tools.h>
15 #include <util/byte_operators.h>
16 
17 #include "bv_endianness_map.h"
18 
20 {
21  if(expr.operands().size()!=3)
22  throw "byte_update takes three operands";
23 
24  const exprt &op=expr.op0();
25  const exprt &offset_expr=expr.offset();
26  const exprt &value=expr.value();
27 
28  bool little_endian;
29 
30  if(expr.id()==ID_byte_update_little_endian)
31  little_endian=true;
32  else if(expr.id()==ID_byte_update_big_endian)
33  little_endian=false;
34  else
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  mp_integer index;
49  if(!to_integer(offset_expr, index))
50  {
51  // yes!
52  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  if(little_endian)
61  {
62  for(std::size_t i=0; i<update_width; i++)
63  bv[integer2size_t(offset+i)]=value_bv[i];
64  }
65  else
66  {
67  bv_endianness_mapt map_op(op.type(), false, ns, boolbv_width);
68  bv_endianness_mapt map_value(value.type(), false, ns, boolbv_width);
69 
70  std::size_t offset_i=integer2unsigned(offset);
71 
72  for(std::size_t i=0; i<update_width; i++)
73  {
74  size_t index_op=map_op.map_bit(offset_i+i);
75  size_t index_value=map_value.map_bit(i);
76 
77  assert(index_op<bv.size());
78  assert(index_value<value_bv.size());
79 
80  bv[index_op]=value_bv[index_value];
81  }
82  }
83  }
84 
85  return bv;
86  }
87 
88  // byte_update with variable index
89  for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
90  {
91  // index condition
93  equality.lhs()=offset_expr;
94  equality.rhs()=from_integer(offset/byte_width, offset_expr.type());
95  literalt equal=convert(equality);
96 
97  bv_endianness_mapt map_op(op.type(), little_endian, ns, boolbv_width);
98  bv_endianness_mapt map_value(value.type(), little_endian, ns, boolbv_width);
99 
100  for(std::size_t bit=0; bit<update_width; bit++)
101  if(offset+bit<bv.size())
102  {
103  std::size_t bv_o=map_op.map_bit(offset+bit);
104  std::size_t value_bv_o=map_value.map_bit(bit);
105 
106  bv[bv_o]=prop.lselect(equal, value_bv[value_bv_o], bv[bv_o]);
107  }
108  }
109 
110  return bv;
111 }
BigInt mp_integer
Definition: mp_arith.h:22
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
exprt & op0()
Definition: expr.h:72
boolbv_widtht boolbv_width
Definition: boolbv.h:90
typet & type()
Definition: expr.h:56
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:189
Expression classes for byte-level operators.
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
const namespacet & ns
Map bytes according to the configured endianness.
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:202
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
Base class for all expressions.
Definition: expr.h:42
#define UNREACHABLE
Definition: invariant.h:250
TO_BE_DOCUMENTED.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:200