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>
15 #include <util/expr_util.h>
17 #include <util/std_expr.h>
18 
20 
21 #include "bv_endianness_map.h"
22 
23 bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
24 {
25  PRECONDITION(map.number_of_bits() == src.size());
26  bvt result;
27  result.reserve(src.size());
28 
29  for(std::size_t i=0; i<src.size(); i++)
30  {
31  const size_t mapped_index = map.map_bit(i);
32  CHECK_RETURN(mapped_index < src.size());
33  result.push_back(src[mapped_index]);
34  }
35 
36  return result;
37 }
38 
40 {
41  // array logic does not handle byte operators, thus lower when operating on
42  // unbounded arrays
43  if(is_unbounded_array(expr.op().type()))
44  {
45  return convert_bv(lower_byte_extract(expr, ns));
46  }
47 
48  const std::size_t width = boolbv_width(expr.type());
49 
50  // special treatment for bit-fields and big-endian:
51  // we need byte granularity
52  #if 0
53  if(expr.id()==ID_byte_extract_big_endian &&
54  expr.type().id()==ID_c_bit_field &&
55  (width%8)!=0)
56  {
57  byte_extract_exprt tmp=expr;
58  // round up
59  to_c_bit_field_type(tmp.type()).set_width(width+8-width%8);
60  convert_byte_extract(tmp, bv);
61  bv.resize(width); // chop down
62  return;
63  }
64  #endif
65 
66  if(width==0)
67  return conversion_failed(expr);
68 
69  // see if the byte number is constant and within bounds, else work from the
70  // root object
71  const auto op_bytes_opt = pointer_offset_size(expr.op().type(), ns);
72  auto index = numeric_cast<mp_integer>(expr.offset());
73 
74  if(
75  (!index.has_value() || !op_bytes_opt.has_value() ||
76  *index < 0 || *index >= *op_bytes_opt) &&
77  (expr.op().id() == ID_member ||
78  expr.op().id() == ID_index ||
79  expr.op().id() == ID_byte_extract_big_endian ||
80  expr.op().id() == ID_byte_extract_little_endian))
81  {
83  o.build(expr.op(), ns);
84  CHECK_RETURN(o.offset().id() != ID_unknown);
85 
86  o.offset() =
88 
90  expr.id(),
91  o.root_object(),
92  plus_exprt(o.offset(), expr.offset()),
93  expr.type());
94 
95  return convert_bv(be);
96  }
97 
98  const exprt &op=expr.op();
100  expr.id() == ID_byte_extract_little_endian ||
101  expr.id() == ID_byte_extract_big_endian);
102  const bool little_endian = expr.id() == ID_byte_extract_little_endian;
103 
104  // first do op0
105  const bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
106  const bvt op_bv=map_bv(op_map, convert_bv(op));
107 
108  // do result
109  bv_endianness_mapt result_map(expr.type(), little_endian, ns, boolbv_width);
110  bvt bv;
111  bv.resize(width);
112 
113  // see if the byte number is constant
114  unsigned byte_width=8;
115 
116  if(index.has_value())
117  {
118  const mp_integer offset = *index * byte_width;
119 
120  for(std::size_t i=0; i<width; i++)
121  // out of bounds?
122  if(offset + i < 0 || offset + i >= op_bv.size())
123  bv[i]=prop.new_variable();
124  else
125  bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
126  }
127  else
128  {
129  std::size_t bytes=op_bv.size()/byte_width;
130 
131  if(prop.has_set_to())
132  {
133  // free variables
134  for(std::size_t i=0; i<width; i++)
135  bv[i]=prop.new_variable();
136 
137  // add implications
138 
139  // type of index operand
140  const typet &constant_type = expr.offset().type();
141 
142  bvt equal_bv;
143  equal_bv.resize(width);
144 
145  for(std::size_t i=0; i<bytes; i++)
146  {
147  std::size_t offset=i*byte_width;
148 
149  for(std::size_t j=0; j<width; j++)
150  if(offset+j<op_bv.size())
151  equal_bv[j]=prop.lequal(bv[j], op_bv[offset+j]);
152  else
153  equal_bv[j]=const_literal(true);
154 
156  convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
157  prop.land(equal_bv)));
158  }
159  }
160  else
161  {
162  // type of index operand
163  const typet &constant_type = expr.offset().type();
164 
165  for(std::size_t i=0; i<bytes; i++)
166  {
167  literalt e =
168  convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
169 
170  std::size_t offset=i*byte_width;
171 
172  for(std::size_t j=0; j<width; j++)
173  {
174  literalt l;
175 
176  if(offset+j<op_bv.size())
177  l=op_bv[offset+j];
178  else
179  l=const_literal(false);
180 
181  if(i==0)
182  bv[j]=l;
183  else
184  bv[j]=prop.lselect(e, l, bv[j]);
185  }
186  }
187  }
188  }
189 
190  // shuffle the result
191  bv=map_bv(result_map, bv);
192 
193  return bv;
194 }
pointer_offset_size.h
Pointer Logic.
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
map_bv
bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
Definition: boolbv_byte_extract.cpp:23
arith_tools.h
bv_endianness_map.h
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: std_expr.cpp:141
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bv_endianness_mapt
Map bytes according to the configured endianness.
Definition: bv_endianness_map.h:21
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1832
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
lower_byte_extract
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...
Definition: byte_operators.cpp:999
propt::new_variable
virtual literalt new_variable()=0
exprt
Base class for all expressions.
Definition: expr.h:53
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:52
propt::land
virtual literalt land(literalt a, literalt b)=0
equal_exprt
Equality.
Definition: std_expr.h:1190
expr_lowering.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::convert_byte_extract
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
Definition: boolbv_byte_extract.cpp:39
byte_operators.h
Expression classes for byte-level operators.
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
endianness_mapt::number_of_bits
size_t number_of_bits() const
Definition: endianness_map.h:56
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:48
to_c_bit_field_type
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:1471
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
irept::id
const irep_idt & id() const
Definition: irep.h:418
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:119
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:218
bitvector_typet::set_width
void set_width(std::size_t width)
Definition: std_types.h:1046
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
expr_util.h
Deprecated expression utility functions.
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
pointer_offset_size
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.
Definition: pointer_offset_size.cpp:89
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
literalt
Definition: literal.h:26
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:81
boolbv.h
std_expr.h
API to expression classes.
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1870