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/byte_operators.h>
16 #include <util/std_expr.h>
17 #include <util/throw_with_nested.h>
18 
21 
23 #include "bv_endianness_map.h"
24 
25 bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
26 {
27  PRECONDITION(map.number_of_bits() == src.size());
28  bvt result;
29  result.reserve(src.size());
30 
31  for(std::size_t i=0; i<src.size(); i++)
32  {
33  const size_t mapped_index = map.map_bit(i);
34  CHECK_RETURN(mapped_index < src.size());
35  result.push_back(src[mapped_index]);
36  }
37 
38  return result;
39 }
40 
42 {
43  // if we extract from an unbounded array, call the flattening code
44  if(is_unbounded_array(expr.op().type()))
45  {
46  try
47  {
48  return convert_bv(lower_byte_extract(expr, ns));
49  }
50  catch(const flatten_byte_extract_exceptiont &)
51  {
53  bitvector_conversion_exceptiont("Can't convert byte_extraction", expr));
54  }
55  }
56 
57  const std::size_t width = boolbv_width(expr.type());
58 
59  // special treatment for bit-fields and big-endian:
60  // we need byte granularity
61  #if 0
62  if(expr.id()==ID_byte_extract_big_endian &&
63  expr.type().id()==ID_c_bit_field &&
64  (width%8)!=0)
65  {
66  byte_extract_exprt tmp=expr;
67  // round up
68  to_c_bit_field_type(tmp.type()).set_width(width+8-width%8);
69  convert_byte_extract(tmp, bv);
70  bv.resize(width); // chop down
71  return;
72  }
73  #endif
74 
75  if(width==0)
76  return conversion_failed(expr);
77 
78  // see if the byte number is constant and within bounds, else work from the
79  // root object
80  const auto op_bytes_opt = pointer_offset_size(expr.op().type(), ns);
81  auto index = numeric_cast<mp_integer>(expr.offset());
82 
83  if(
84  (!index.has_value() || !op_bytes_opt.has_value() ||
85  *index < 0 || *index >= *op_bytes_opt) &&
86  (expr.op().id() == ID_member ||
87  expr.op().id() == ID_index ||
88  expr.op().id() == ID_byte_extract_big_endian ||
89  expr.op().id() == ID_byte_extract_little_endian))
90  {
92  o.build(expr.op(), ns);
93  CHECK_RETURN(o.offset().id() != ID_unknown);
94  if(o.offset().type() != expr.offset().type())
95  o.offset().make_typecast(expr.offset().type());
97  expr.id(),
98  o.root_object(),
99  plus_exprt(o.offset(), expr.offset()),
100  expr.type());
101 
102  return convert_bv(be);
103  }
104 
105  const exprt &op=expr.op();
106  const exprt &offset=expr.offset();
107  PRECONDITION(
108  expr.id() == ID_byte_extract_little_endian ||
109  expr.id() == ID_byte_extract_big_endian);
110  const bool little_endian = expr.id() == ID_byte_extract_little_endian;
111 
112  // first do op0
113  const bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
114  const bvt op_bv=map_bv(op_map, convert_bv(op));
115 
116  // do result
117  bv_endianness_mapt result_map(expr.type(), little_endian, ns, boolbv_width);
118  bvt bv;
119  bv.resize(width);
120 
121  // see if the byte number is constant
122  unsigned byte_width=8;
123 
124  if(index.has_value())
125  {
126  const mp_integer offset = *index * byte_width;
127 
128  for(std::size_t i=0; i<width; i++)
129  // out of bounds?
130  if(offset + i < 0 || offset + i >= op_bv.size())
131  bv[i]=prop.new_variable();
132  else
133  bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
134  }
135  else
136  {
137  std::size_t bytes=op_bv.size()/byte_width;
138 
139  if(prop.has_set_to())
140  {
141  // free variables
142  for(std::size_t i=0; i<width; i++)
143  bv[i]=prop.new_variable();
144 
145  // add implications
146 
148  equality.lhs()=offset; // index operand
149 
150  typet constant_type=offset.type(); // type of index operand
151 
152  bvt equal_bv;
153  equal_bv.resize(width);
154 
155  for(std::size_t i=0; i<bytes; i++)
156  {
157  equality.rhs()=from_integer(i, constant_type);
158 
159  std::size_t offset=i*byte_width;
160 
161  for(std::size_t j=0; j<width; j++)
162  if(offset+j<op_bv.size())
163  equal_bv[j]=prop.lequal(bv[j], op_bv[offset+j]);
164  else
165  equal_bv[j]=const_literal(true);
166 
168  prop.limplies(convert(equality), prop.land(equal_bv)));
169  }
170  }
171  else
172  {
174  equality.lhs()=offset; // index operand
175 
176  typet constant_type(offset.type()); // type of index operand
177 
178  for(std::size_t i=0; i<bytes; i++)
179  {
180  equality.rhs()=from_integer(i, constant_type);
181 
183 
184  std::size_t offset=i*byte_width;
185 
186  for(std::size_t j=0; j<width; j++)
187  {
188  literalt l;
189 
190  if(offset+j<op_bv.size())
191  l=op_bv[offset+j];
192  else
193  l=const_literal(false);
194 
195  if(i==0)
196  bv[j]=l;
197  else
198  bv[j]=prop.lselect(e, l, bv[j]);
199  }
200  }
201  }
202  }
203 
204  // shuffle the result
205  bv=map_bv(result_map, bv);
206 
207  return bv;
208 }
The type of an expression, extends irept.
Definition: type.h:27
BigInt mp_integer
Definition: mp_arith.h:22
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:92
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:624
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:49
Equality.
Definition: std_expr.h:1484
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:259
virtual literalt new_variable()=0
Expression classes for byte-level operators.
void util_throw_with_nested(T &&t)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:123
Exceptions that can be raised in bv_conversion.
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:123
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
const namespacet & ns
Map bytes according to the configured endianness.
Pointer Logic.
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
literalt const_literal(bool value)
Definition: literal.h:187
exprt lower_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...
size_t number_of_bits() const
Base class for all expressions.
Definition: expr.h:54
const exprt & root_object() const
Definition: std_expr.cpp:199
virtual bool has_set_to() const
Definition: prop.h:78
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1491
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
std::vector< literalt > bvt
Definition: literal.h:200