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