cprover
boolbv_byte_extract.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 <cassert>
12 
13 #include <util/arith_tools.h>
14 #include <util/std_expr.h>
15 #include <util/byte_operators.h>
16 #include <util/endianness_map.h>
17 
18 #include "flatten_byte_operators.h"
19 
20 bvt map_bv(const endianness_mapt &map, const bvt &src)
21 {
22  assert(map.number_of_bits()==src.size());
23 
24  bvt result;
25  result.resize(src.size(), const_literal(false));
26 
27  for(std::size_t i=0; i<src.size(); i++)
28  {
29  size_t mapped_index=map.map_bit(i);
30  assert(mapped_index<src.size());
31  result[i]=src[mapped_index];
32  }
33 
34  return result;
35 }
36 
38 {
39  if(expr.operands().size()!=2)
40  throw "byte_extract takes two operands";
41 
42  // if we extract from an unbounded array, call the flattening code
43  if(is_unbounded_array(expr.op().type()))
44  {
45  exprt tmp=flatten_byte_extract(expr, ns);
46  return convert_bv(tmp);
47  }
48 
49  std::size_t width=boolbv_width(expr.type());
50 
51  // special treatment for bit-fields and big-endian:
52  // we need byte granularity
53  #if 0
54  if(expr.id()==ID_byte_extract_big_endian &&
55  expr.type().id()==ID_c_bit_field &&
56  (width%8)!=0)
57  {
58  byte_extract_exprt tmp=expr;
59  // round up
60  to_c_bit_field_type(tmp.type()).set_width(width+8-width%8);
61  convert_byte_extract(tmp, bv);
62  bv.resize(width); // chop down
63  return;
64  }
65  #endif
66 
67  if(width==0)
68  return conversion_failed(expr);
69 
70  const exprt &op=expr.op();
71  const exprt &offset=expr.offset();
72 
73  bool little_endian;
74 
75  if(expr.id()==ID_byte_extract_little_endian)
76  little_endian=true;
77  else if(expr.id()==ID_byte_extract_big_endian)
78  little_endian=false;
79  else
80  {
81  little_endian=false;
82  assert(false);
83  }
84 
85  // first do op0
86 
87  endianness_mapt op_map(op.type(), little_endian, ns);
88  const bvt op_bv=map_bv(op_map, convert_bv(op));
89 
90  // do result
91  endianness_mapt result_map(expr.type(), little_endian, ns);
92  bvt bv;
93  bv.resize(width);
94 
95  // see if the byte number is constant
96  unsigned byte_width=8;
97 
98  mp_integer index;
99  if(!to_integer(offset, index))
100  {
101  if(index<0)
102  throw "byte_extract flatting with negative offset: "+expr.pretty();
103 
104  mp_integer offset=index*byte_width;
105 
106  std::size_t offset_i=integer2unsigned(offset);
107 
108  for(std::size_t i=0; i<width; i++)
109  // out of bounds?
110  if(offset<0 || offset_i+i>=op_bv.size())
111  bv[i]=prop.new_variable();
112  else
113  bv[i]=op_bv[offset_i+i];
114  }
115  else
116  {
117  std::size_t bytes=op_bv.size()/byte_width;
118 
119  if(prop.has_set_to())
120  {
121  // free variables
122  for(std::size_t i=0; i<width; i++)
123  bv[i]=prop.new_variable();
124 
125  // add implications
126 
128  equality.lhs()=offset; // index operand
129 
130  typet constant_type=offset.type(); // type of index operand
131 
132  bvt equal_bv;
133  equal_bv.resize(width);
134 
135  for(std::size_t i=0; i<bytes; i++)
136  {
137  equality.rhs()=from_integer(i, constant_type);
138 
139  std::size_t offset=i*byte_width;
140 
141  for(std::size_t j=0; j<width; j++)
142  if(offset+j<op_bv.size())
143  equal_bv[j]=prop.lequal(bv[j], op_bv[offset+j]);
144  else
145  equal_bv[j]=const_literal(true);
146 
148  prop.limplies(convert(equality), prop.land(equal_bv)));
149  }
150  }
151  else
152  {
154  equality.lhs()=offset; // index operand
155 
156  typet constant_type(offset.type()); // type of index operand
157 
158  for(std::size_t i=0; i<bytes; i++)
159  {
160  equality.rhs()=from_integer(i, constant_type);
161 
162  literalt e=convert(equality);
163 
164  std::size_t offset=i*byte_width;
165 
166  for(std::size_t j=0; j<width; j++)
167  {
168  literalt l;
169 
170  if(offset+j<op_bv.size())
171  l=op_bv[offset+j];
172  else
173  l=const_literal(false);
174 
175  if(i==0)
176  bv[j]=l;
177  else
178  bv[j]=prop.lselect(e, l, bv[j]);
179  }
180  }
181  }
182  }
183 
184  // shuffle the result
185  bv=map_bv(result_map, bv);
186 
187  return bv;
188 }
The type of an expression.
Definition: type.h:20
BigInt mp_integer
Definition: mp_arith.h:19
Maps a big-endian offset to a little-endian offset.
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bvt map_bv(const endianness_mapt &map, const bvt &src)
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:673
exprt flatten_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
typet & type()
Definition: expr.h:60
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:47
equality
Definition: std_expr.h:1082
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:189
virtual literalt new_variable()=0
Expression classes for byte-level operators.
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const namespacet & ns
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1319
virtual literalt lequal(literalt a, literalt b)=0
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
literalt const_literal(bool value)
Definition: literal.h:187
size_t number_of_bits() const
Base class for all expressions.
Definition: expr.h:46
virtual bool has_set_to() const
Definition: prop.h:76
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
operandst & operands()
Definition: expr.h:70
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:197