cprover
boolbv_array_of.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/invariant.h>
13 #include <util/std_types.h>
14 
17 {
19  expr.type().id() == ID_array, "array_of expression shall have array type");
20 
21  const array_typet &array_type = expr.type();
22 
23  if(is_unbounded_array(array_type))
24  return conversion_failed(expr);
25 
26  std::size_t width=boolbv_width(array_type);
27 
28  if(width==0)
29  {
30  // A zero-length array is acceptable;
31  // an element with unknown size is not.
32  if(boolbv_width(array_type.subtype())==0)
33  return conversion_failed(expr);
34  else
35  return bvt();
36  }
37 
38  const exprt &array_size=array_type.size();
39 
40  const auto size = numeric_cast<mp_integer>(array_size);
41 
42  if(!size.has_value())
43  return conversion_failed(expr);
44 
45  const bvt &tmp = convert_bv(expr.what());
46 
47  INVARIANT(
48  *size * tmp.size() == width,
49  "total array bit width shall equal the number of elements times the "
50  "element bit with");
51 
52  bvt bv;
53  bv.resize(width);
54 
55  auto b_it = tmp.begin();
56 
57  for(auto &b : bv)
58  {
59  b = *b_it;
60 
61  b_it++;
62 
63  if(b_it == tmp.end())
64  b_it = tmp.begin();
65  }
66 
67  return bv;
68 }
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
boolbvt::convert_array_of
virtual bvt convert_array_of(const array_of_exprt &expr)
Flatten arrays constructed from a single element.
Definition: boolbv_array_of.cpp:16
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1384
bvt
std::vector< literalt > bvt
Definition: literal.h:201
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
array_of_exprt::type
const array_typet & type() const
Definition: std_expr.h:1374
array_typet::size
const exprt & size() const
Definition: std_types.h:973
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1367
std_types.h
Pre-defined types.
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
array_typet
Arrays with given size.
Definition: std_types.h:965
boolbv.h
validation_modet::INVARIANT
@ INVARIANT