cprover
boolbv_width.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_width.h"
10 
11 #include <algorithm>
12 
13 #include <util/arith_tools.h>
14 #include <util/exception_utils.h>
15 #include <util/invariant.h>
16 #include <util/std_types.h>
17 
19 {
20 }
21 
23 {
24 }
25 
27 {
28  // check cache first
29 
30  std::pair<cachet::iterator, bool> cache_result=
31  cache.insert(std::pair<typet, entryt>(type, entryt()));
32 
33  entryt &entry=cache_result.first->second;
34 
35  if(!cache_result.second) // found!
36  return entry;
37 
38  entry.total_width=0;
39 
40  const irep_idt type_id=type.id();
41 
42  if(type_id==ID_struct)
43  {
44  const struct_typet::componentst &components=
45  to_struct_type(type).components();
46 
47  std::size_t offset=0;
48  entry.members.resize(components.size());
49 
50  for(std::size_t i=0; i<entry.members.size(); i++)
51  {
52  std::size_t sub_width=operator()(components[i].type());
53  entry.members[i].offset=offset;
54  entry.members[i].width=sub_width;
55  offset+=sub_width;
56  }
57 
58  entry.total_width=offset;
59  }
60  else if(type_id==ID_union)
61  {
62  const union_typet::componentst &components=
63  to_union_type(type).components();
64 
65  entry.members.resize(components.size());
66 
67  std::size_t max_width=0;
68 
69  for(std::size_t i=0; i<entry.members.size(); i++)
70  {
71  std::size_t sub_width=operator()(components[i].type());
72  entry.members[i].width=sub_width;
73  max_width=std::max(max_width, sub_width);
74  }
75 
76  entry.total_width=max_width;
77  }
78  else if(type_id==ID_bool)
79  entry.total_width=1;
80  else if(type_id==ID_c_bool)
81  {
82  entry.total_width=to_c_bool_type(type).get_width();
83  }
84  else if(type_id==ID_signedbv)
85  {
87  }
88  else if(type_id==ID_unsignedbv)
89  {
91  }
92  else if(type_id==ID_floatbv)
93  {
95  }
96  else if(type_id==ID_fixedbv)
97  {
99  }
100  else if(type_id==ID_bv)
101  {
102  entry.total_width=to_bv_type(type).get_width();
103  }
104  else if(type_id==ID_verilog_signedbv ||
105  type_id==ID_verilog_unsignedbv)
106  {
107  // we encode with two bits
108  std::size_t size = type.get_size_t(ID_width);
110  size > 0, "verilog bitvector width shall be greater than zero");
111  entry.total_width = size * 2;
112  }
113  else if(type_id==ID_range)
114  {
115  mp_integer from=string2integer(type.get_string(ID_from)),
116  to=string2integer(type.get_string(ID_to));
117 
118  mp_integer size=to-from+1;
119 
120  if(size>=1)
121  {
122  entry.total_width = address_bits(size);
123  CHECK_RETURN(entry.total_width > 0);
124  }
125  }
126  else if(type_id==ID_array)
127  {
128  const array_typet &array_type=to_array_type(type);
129  std::size_t sub_width=operator()(array_type.subtype());
130 
131  const auto array_size = numeric_cast<mp_integer>(array_type.size());
132 
133  if(!array_size.has_value())
134  {
135  // we can still use the theory of arrays for this
136  entry.total_width=0;
137  }
138  else
139  {
140  mp_integer total = *array_size * sub_width;
141  if(total>(1<<30)) // realistic limit
142  throw analysis_exceptiont("array too large for flattening");
143 
144  entry.total_width = numeric_cast_v<std::size_t>(total);
145  }
146  }
147  else if(type_id==ID_vector)
148  {
149  const vector_typet &vector_type=to_vector_type(type);
150  std::size_t sub_width=operator()(vector_type.subtype());
151 
152  const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
153 
154  mp_integer total = vector_size * sub_width;
155  if(total > (1 << 30)) // realistic limit
156  throw analysis_exceptiont("vector too large for flattening");
157 
158  entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
159  }
160  else if(type_id==ID_complex)
161  {
162  const mp_integer sub_width = operator()(type.subtype());
163  entry.total_width = numeric_cast_v<std::size_t>(2 * sub_width);
164  }
165  else if(type_id==ID_code)
166  {
167  }
168  else if(type_id==ID_enumeration)
169  {
170  // get number of necessary bits
171  std::size_t size=to_enumeration_type(type).elements().size();
172  entry.total_width = address_bits(size);
173  CHECK_RETURN(entry.total_width > 0);
174  }
175  else if(type_id==ID_c_enum)
176  {
177  // these have a subtype
178  entry.total_width = type.subtype().get_size_t(ID_width);
179  CHECK_RETURN(entry.total_width > 0);
180  }
181  else if(type_id==ID_incomplete_c_enum)
182  {
183  // no width
184  }
185  else if(type_id==ID_pointer)
186  entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
187  else if(type_id == ID_symbol_type)
188  entry=get_entry(ns.follow(type));
189  else if(type_id==ID_struct_tag)
191  else if(type_id==ID_union_tag)
193  else if(type_id==ID_c_enum_tag)
195  else if(type_id==ID_c_bit_field)
196  {
198  }
199  else if(type_id==ID_string)
200  entry.total_width=32;
201  else if(type_id != ID_empty)
203 
204  return entry;
205 }
206 
208  const struct_typet &type,
209  const irep_idt &member) const
210 {
211  std::size_t component_number=type.component_number(member);
212 
213  return get_entry(type).members[component_number];
214 }
The type of an expression, extends irept.
Definition: type.h:27
BigInt mp_integer
Definition: mp_arith.h:22
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1316
std::vector< componentt > componentst
Definition: std_types.h:203
const componentst & components() const
Definition: std_types.h:205
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
Definition: expr_cast.h:198
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
Structure type, corresponds to C style structs.
Definition: std_types.h:276
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: std_types.h:1642
const irep_idt & id() const
Definition: irep.h:259
const membert & get_member(const struct_typet &type, const irep_idt &member) const
std::size_t operator()(const typet &type) const
Definition: boolbv_width.h:22
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:633
The pointer type These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1507
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:583
The vector type.
Definition: std_types.h:1755
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:123
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const exprt & size() const
Definition: std_types.h:1765
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const exprt & size() const
Definition: std_types.h:1010
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const namespacet & ns
Definition: boolbv_width.h:37
boolbv_widtht(const namespacet &_ns)
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1205
std::vector< membert > members
Definition: boolbv_width.h:42
const irept::subt & elements() const
Definition: std_types.h:605
std::size_t get_width() const
Definition: std_types.h:1117
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:737
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1262
Pre-defined types.
#define UNIMPLEMENTED
Definition: invariant.h:497
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1380
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:35
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
Arrays with given size.
Definition: std_types.h:1000
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:1491
const typet & subtype() const
Definition: type.h:38
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
std::size_t total_width
Definition: boolbv_width.h:41
const entryt & get_entry(const typet &type) const