37static std::optional<std::size_t>
41 return boolbv_width(*struct_tag);
43 return boolbv_width(*union_tag);
49 std::queue<typet *> work_queue;
50 work_queue.push(&type);
51 while(!work_queue.empty())
53 typet ¤t = *work_queue.front();
62 if(*assigned_bit_width == 0)
63 assigned_bit_width = 8;
64 current =
bv_typet{*assigned_bit_width};
68 work_queue.push(&array->element_type());
77 const auto struct_type = ns.
follow_tag(tag_type);
79 with.
where().
id() == ID_member_name,
80 "operand is expected to be the name of a member");
81 const auto update_name = with.
where().
find(ID_component_name).
id();
82 const auto components =
93 .collect<exprt::operandst>();
114 if(struct_expr.
operands().size() == 1)
115 return struct_expr.
operands().front();
122 const std::size_t union_width = bit_width(union_expr.
type());
124 const std::size_t component_width = bit_width(union_expr.
op().
type());
125 if(union_width == component_width)
128 union_width >= component_width,
129 "Union must be at least as wide as its component.");
140 auto member_component_rit = std::find_if(
144 return component.get_name() == name;
147 member_component_rit != type.
components().rend(),
148 "Definition of struct type should include named component.");
149 const auto trailing_widths =
154 return std::accumulate(
155 trailing_widths.begin(), trailing_widths.end(), std::size_t{0});
169 const auto &compound_type = member_expr.
compound().
type();
170 const auto offset_bits = [&]() -> std::size_t {
177 const auto &struct_type =
178 compound_type.id() == ID_struct_tag
179 ?
ns.get().follow_tag(
186 member_expr.
compound(), offset_bits, member_expr.
type()};
191 std::queue<exprt *> work_queue;
192 work_queue.push(&expr);
193 while(!work_queue.empty())
195 exprt ¤t = *work_queue.front();
202 std::optional<exprt> update;
215 "Updates in struct encoding are expected to be a change of state.");
216 current = std::move(*update);
223 for(
auto &operand : current.
operands())
224 work_queue.push(&operand);
230 const exprt &encoded,
245 "Structs are expected to be encoded into bit vectors.");
246 const struct_typet definition =
ns.get().follow_tag(original_type);
258 const exprt &encoded,
263 "Unions are expected to be encoded into bit vectors.");
264 const union_typet definition =
ns.get().follow_tag(original_type);
265 const auto &components = definition.
components();
266 if(components.empty())
272 const auto &component_for_definition = components[0];
275 component_for_definition.get_name(),
278 typecast_exprt{encoded, original_type}, component_for_definition}),
279 component_for_definition.type()},
API to expression classes for bitvectors.
Pre-defined bitvector types.
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
Union constructor to support unions without any member (a GCC/Clang feature).
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const irept & find(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
const exprt & compound() const
irep_idt get_component_name() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
This expression serves as a placeholder for the bits which have non deterministic value in a larger b...
std::unique_ptr< boolbv_widtht > boolbv_width
std::reference_wrapper< const namespacet > ns
typet encode(typet type) const
exprt decode(const exprt &encoded, const struct_tag_typet &original_type) const
Reconstructs a struct expression of the original_type using the data from the bit vector encoded expr...
exprt encode_member(const member_exprt &member_expr) const
The member expression selects the value of a field from a struct or union.
struct_encodingt(const namespacet &ns)
Struct constructor from list of elements.
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
const componentst & components() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Union constructor from single element.
A union tag type, i.e., union_typet with an identifier.
Operator to update elements in structs and arrays.
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
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...
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Expressions for use in incremental SMT2 decision procedure.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
exprt simplify_expr(exprt src, const namespacet &ns)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
static exprt empty_encoding()
Empty structs and unions are encoded as a zero byte.
static exprt encode(const with_exprt &with, const namespacet &ns)
static std::size_t count_trailing_bit_width(const struct_typet &type, const irep_idt name, const boolbv_widtht &boolbv_width)
static std::optional< std::size_t > needs_width(const typet &type, const boolbv_widtht &boolbv_width)
If the given type needs re-encoding as a bit-vector then this function.