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/c_types.h>
12 #include <util/namespace.h>
13 
15  const member_exprt &expr,
16  const bvt &struct_bv,
17  const std::function<std::size_t(const typet &)> boolbv_width,
18  const namespacet &ns)
19 {
20  const exprt &struct_op=expr.struct_op();
21  const typet &struct_op_type=ns.follow(struct_op.type());
22 
23  const irep_idt &component_name = expr.get_component_name();
24  const struct_typet::componentst &components =
25  to_struct_type(struct_op_type).components();
26 
27  std::size_t offset = 0;
28 
29  for(const auto &c : components)
30  {
31  const typet &subtype = c.type();
32  const std::size_t sub_width = boolbv_width(subtype);
33 
34  if(c.get_name() == component_name)
35  {
37  subtype == expr.type(),
38  "component type shall match the member expression type",
39  subtype.pretty(),
40  expr.type().pretty());
41  INVARIANT(
42  offset + sub_width <= struct_bv.size(),
43  "bitvector part corresponding to element shall be contained within the "
44  "full aggregate bitvector");
45 
46  return bvt(
47  struct_bv.begin() + offset, struct_bv.begin() + offset + sub_width);
48  }
49 
50  offset += sub_width;
51  }
52 
54  false,
55  "struct type shall contain component accessed by member expression",
56  expr.find_source_location(),
57  id2string(component_name));
58 }
59 
61  const member_exprt &expr,
62  const bvt &union_bv,
63  const boolbvt &boolbv,
64  const namespacet &ns)
65 {
66  const exprt &union_op = expr.compound();
67  const union_typet &union_op_type =
68  ns.follow_tag(to_union_tag_type(union_op.type()));
69 
70  const irep_idt &component_name = expr.get_component_name();
72  union_op_type.get_component(component_name);
74  component.is_not_nil(),
75  "union type shall contain component accessed by member expression",
76  expr.find_source_location(),
77  id2string(component_name));
78 
79  const typet &subtype = component.type();
80  const std::size_t sub_width = boolbv.boolbv_width(subtype);
81 
82  endianness_mapt map_u = boolbv.endianness_map(union_op_type);
83  endianness_mapt map_component = boolbv.endianness_map(subtype);
84 
85  bvt result(sub_width, literalt{});
86  for(std::size_t i = 0; i < sub_width; ++i)
87  result[map_u.map_bit(i)] = union_bv[map_component.map_bit(i)];
88 
89  return result;
90 }
91 
93 {
94  const bvt &compound_bv = convert_bv(expr.compound());
95 
96  if(expr.compound().type().id() == ID_struct_tag)
97  return convert_member_struct(
98  expr,
99  compound_bv,
100  [this](const typet &t) { return boolbv_width(t); },
101  ns);
102  else
103  {
104  PRECONDITION(expr.compound().type().id() == ID_union_tag);
105  return convert_member_union(expr, compound_bv, *this, ns);
106  }
107 }
static bvt convert_member_union(const member_exprt &expr, const bvt &union_bv, const boolbvt &boolbv, const namespacet &ns)
static bvt convert_member_struct(const member_exprt &expr, const bvt &struct_bv, const std::function< std::size_t(const typet &)> boolbv_width, const namespacet &ns)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
const namespacet & ns
Definition: arrays.h:56
Definition: boolbv.h:44
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:40
virtual bvt convert_member(const member_exprt &expr)
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition: boolbv.h:105
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Maps a big-endian offset to a little-endian offset.
size_t map_bit(size_t bit) const
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
typet & type()
Return the type of the expression.
Definition: expr.h:82
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & id() const
Definition: irep.h:396
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & compound() const
Definition: std_expr.h:2708
const exprt & struct_op() const
Definition: std_expr.h:2697
irep_idt get_component_name() const
Definition: std_expr.h:2681
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:57
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
The type of an expression, extends irept.
Definition: type.h:29
The union type.
Definition: c_types.h:125
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::vector< literalt > bvt
Definition: literal.h:201
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#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:437
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308