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 &byte_extract_flatten_exception)
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  const bool little_endian = expr.id() == ID_byte_extract_little_endian;
104 
105  // first do op0
106  const bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
107  const bvt op_bv=map_bv(op_map, convert_bv(op));
108 
109  // do result
110  bv_endianness_mapt result_map(expr.type(), little_endian, ns, boolbv_width);
111  bvt bv;
112  bv.resize(width);
113 
114  // see if the byte number is constant
115  unsigned byte_width=8;
116 
117  if(index.has_value())
118  {
119  const mp_integer offset = *index * byte_width;
120 
121  for(std::size_t i=0; i<width; i++)
122  // out of bounds?
123  if(offset + i < 0 || offset + i >= op_bv.size())
124  bv[i]=prop.new_variable();
125  else
126  bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
127  }
128  else
129  {
130  std::size_t bytes=op_bv.size()/byte_width;
131 
132  if(prop.has_set_to())
133  {
134  // free variables
135  for(std::size_t i=0; i<width; i++)
136  bv[i]=prop.new_variable();
137 
138  // add implications
139 
141  equality.lhs()=offset; // index operand
142 
143  typet constant_type=offset.type(); // type of index operand
144 
145  bvt equal_bv;
146  equal_bv.resize(width);
147 
148  for(std::size_t i=0; i<bytes; i++)
149  {
150  equality.rhs()=from_integer(i, constant_type);
151 
152  std::size_t offset=i*byte_width;
153 
154  for(std::size_t j=0; j<width; j++)
155  if(offset+j<op_bv.size())
156  equal_bv[j]=prop.lequal(bv[j], op_bv[offset+j]);
157  else
158  equal_bv[j]=const_literal(true);
159 
161  prop.limplies(convert(equality), prop.land(equal_bv)));
162  }
163  }
164  else
165  {
167  equality.lhs()=offset; // index operand
168 
169  typet constant_type(offset.type()); // type of index operand
170 
171  for(std::size_t i=0; i<bytes; i++)
172  {
173  equality.rhs()=from_integer(i, constant_type);
174 
176 
177  std::size_t offset=i*byte_width;
178 
179  for(std::size_t j=0; j<width; j++)
180  {
181  literalt l;
182 
183  if(offset+j<op_bv.size())
184  l=op_bv[offset+j];
185  else
186  l=const_literal(false);
187 
188  if(i==0)
189  bv[j]=l;
190  else
191  bv[j]=prop.lselect(e, l, bv[j]);
192  }
193  }
194  }
195  }
196 
197  // shuffle the result
198  bv=map_bv(result_map, bv);
199 
200  return bv;
201 }
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:245
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:189
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:230
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:1402
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