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 
20 #include "bv_endianness_map.h"
22 #include "flatten_byte_operators.h"
23 
24 bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
25 {
26  PRECONDITION(map.number_of_bits() == src.size());
27  bvt result;
28  result.reserve(src.size());
29 
30  for(std::size_t i=0; i<src.size(); i++)
31  {
32  const size_t mapped_index = map.map_bit(i);
33  CHECK_RETURN(mapped_index < src.size());
34  result.push_back(src[mapped_index]);
35  }
36 
37  return result;
38 }
39 
41 {
42  // if we extract from an unbounded array, call the flattening code
43  if(is_unbounded_array(expr.op().type()))
44  {
45  try
46  {
47  return convert_bv(flatten_byte_extract(expr, ns));
48  }
49  catch(const flatten_byte_extract_exceptiont &)
50  {
52  bitvector_conversion_exceptiont("Can't convert byte_extraction", expr));
53  }
54  }
55 
56  const std::size_t width = boolbv_width(expr.type());
57 
58  // special treatment for bit-fields and big-endian:
59  // we need byte granularity
60  #if 0
61  if(expr.id()==ID_byte_extract_big_endian &&
62  expr.type().id()==ID_c_bit_field &&
63  (width%8)!=0)
64  {
65  byte_extract_exprt tmp=expr;
66  // round up
67  to_c_bit_field_type(tmp.type()).set_width(width+8-width%8);
68  convert_byte_extract(tmp, bv);
69  bv.resize(width); // chop down
70  return;
71  }
72  #endif
73 
74  if(width==0)
75  return conversion_failed(expr);
76 
77  // see if the byte number is constant and within bounds, else work from the
78  // root object
79  const mp_integer op_bytes = pointer_offset_size(expr.op().type(), ns);
80  auto index = numeric_cast<mp_integer>(expr.offset());
81  if(
82  (!index.has_value() || (*index < 0 || *index >= op_bytes)) &&
83  (expr.op().id() == ID_member || expr.op().id() == ID_index ||
84  expr.op().id() == ID_byte_extract_big_endian ||
85  expr.op().id() == ID_byte_extract_little_endian))
86  {
88  o.build(expr.op(), ns);
89  CHECK_RETURN(o.offset().id() != ID_unknown);
90  if(o.offset().type() != expr.offset().type())
91  o.offset().make_typecast(expr.offset().type());
93  expr.id(),
94  o.root_object(),
95  plus_exprt(o.offset(), expr.offset()),
96  expr.type());
97 
98  return convert_bv(be);
99  }
100 
101  const exprt &op=expr.op();
102  const exprt &offset=expr.offset();
103  PRECONDITION(
104  expr.id() == ID_byte_extract_little_endian ||
105  expr.id() == ID_byte_extract_big_endian);
106  const bool little_endian = expr.id() == ID_byte_extract_little_endian;
107 
108  // first do op0
109  const bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
110  const bvt op_bv=map_bv(op_map, convert_bv(op));
111 
112  // do result
113  bv_endianness_mapt result_map(expr.type(), little_endian, ns, boolbv_width);
114  bvt bv;
115  bv.resize(width);
116 
117  // see if the byte number is constant
118  unsigned byte_width=8;
119 
120  if(index.has_value())
121  {
122  const mp_integer offset = *index * byte_width;
123 
124  for(std::size_t i=0; i<width; i++)
125  // out of bounds?
126  if(offset + i < 0 || offset + i >= op_bv.size())
127  bv[i]=prop.new_variable();
128  else
129  bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
130  }
131  else
132  {
133  std::size_t bytes=op_bv.size()/byte_width;
134 
135  if(prop.has_set_to())
136  {
137  // free variables
138  for(std::size_t i=0; i<width; i++)
139  bv[i]=prop.new_variable();
140 
141  // add implications
142 
144  equality.lhs()=offset; // index operand
145 
146  typet constant_type=offset.type(); // type of index operand
147 
148  bvt equal_bv;
149  equal_bv.resize(width);
150 
151  for(std::size_t i=0; i<bytes; i++)
152  {
153  equality.rhs()=from_integer(i, constant_type);
154 
155  std::size_t offset=i*byte_width;
156 
157  for(std::size_t j=0; j<width; j++)
158  if(offset+j<op_bv.size())
159  equal_bv[j]=prop.lequal(bv[j], op_bv[offset+j]);
160  else
161  equal_bv[j]=const_literal(true);
162 
164  prop.limplies(convert(equality), prop.land(equal_bv)));
165  }
166  }
167  else
168  {
170  equality.lhs()=offset; // index operand
171 
172  typet constant_type(offset.type()); // type of index operand
173 
174  for(std::size_t i=0; i<bytes; i++)
175  {
176  equality.rhs()=from_integer(i, constant_type);
177 
179 
180  std::size_t offset=i*byte_width;
181 
182  for(std::size_t j=0; j<width; j++)
183  {
184  literalt l;
185 
186  if(offset+j<op_bv.size())
187  l=op_bv[offset+j];
188  else
189  l=const_literal(false);
190 
191  if(i==0)
192  bv[j]=l;
193  else
194  bv[j]=prop.lselect(e, l, bv[j]);
195  }
196  }
197  }
198  }
199 
200  // shuffle the result
201  bv=map_bv(result_map, bv);
202 
203  return bv;
204 }
The type of an expression.
Definition: type.h:22
BigInt mp_integer
Definition: mp_arith.h:22
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
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:632
const exprt & root_object() const
Definition: std_expr.h:1966
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:56
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:49
equality
Definition: std_expr.h:1354
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)
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:121
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:122
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
The plus expression.
Definition: std_expr.h:893
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
size_t number_of_bits() const
Base class for all expressions.
Definition: expr.h:42
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 generic typet to a c_bit_field_typet.
Definition: std_types.h:1411
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)
Definition: expr.cpp:84
std::vector< literalt > bvt
Definition: literal.h:200