cprover
boolbv_member.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/base_type.h>
12 #include <util/byte_operators.h>
13 #include <util/arith_tools.h>
14 #include <util/c_types.h>
15 
17 {
18  const exprt &struct_op=expr.struct_op();
19  const typet &struct_op_type=ns.follow(struct_op.type());
20 
21  const bvt &struct_bv=convert_bv(struct_op);
22 
23  if(struct_op_type.id()==ID_union)
24  {
25  return convert_bv(
27  struct_op,
29  expr.type()));
30  }
31  else
32  {
33  INVARIANT(
34  struct_op_type.id() == ID_struct,
35  "member_exprt should denote access to a union or struct");
36 
37  const irep_idt &component_name=expr.get_component_name();
38  const struct_typet::componentst &components=
39  to_struct_type(struct_op_type).components();
40 
41  std::size_t offset=0;
42 
43  for(const auto &c : components)
44  {
45  const typet &subtype = c.type();
46  std::size_t sub_width=boolbv_width(subtype);
47 
48  if(c.get_name() == component_name)
49  {
51  base_type_eq(subtype, expr.type(), ns),
52  "struct component type shall match the member expression type",
53  subtype.pretty(),
54  expr.type().pretty());
55 
56  bvt bv;
57  bv.resize(sub_width);
58  INVARIANT(
59  offset + sub_width <= struct_bv.size(),
60  "bitvector part corresponding to struct element shall be contained "
61  "within the full struct bitvector");
62 
63  for(std::size_t i=0; i<sub_width; i++)
64  bv[i]=struct_bv[offset+i];
65 
66  return bv;
67  }
68 
69  offset+=sub_width;
70  }
71 
73  false,
74  "struct type shall contain component accessed by member expression",
75  expr.find_source_location(),
76  id2string(component_name));
77  }
78 }
The type of an expression, extends irept.
Definition: type.h:27
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
boolbv_widtht boolbv_width
Definition: boolbv.h:92
std::vector< componentt > componentst
Definition: std_types.h:203
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
Extract member of struct or union.
Definition: std_expr.h:3890
const irep_idt & id() const
Definition: irep.h:259
Expression classes for byte-level operators.
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:486
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
const namespacet & ns
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
bitvector_typet index_type()
Definition: c_types.cpp:16
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
Base class for all expressions.
Definition: expr.h:54
const exprt & struct_op() const
Definition: std_expr.h:3931
irep_idt get_component_name() const
Definition: std_expr.h:3915
virtual bvt convert_member(const member_exprt &expr)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:414
Base Type Computation.
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:200
irep_idt byte_extract_id()