cprover
Loading...
Searching...
No Matches
boolbv_member.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 =
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());
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",
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();
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",
77 id2string(component_name));
78
79 const typet &subtype = component.type();
80 const std::size_t sub_width = boolbv.boolbv_width(subtype);
81
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)
98 expr,
100 [this](const typet &t) { return boolbv_width(t); },
101 ns);
102 else
103 {
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
const namespacet & ns
Definition arrays.h:56
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.
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 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