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());
81static std::unordered_map<irep_idt, exprt>
84 std::unordered_map<irep_idt, exprt> pairs;
85 auto current_operand = struct_expr.
operands().begin();
88 while(current_operand != struct_expr.
operands().end())
91 current_operand->id() == ID_member_name,
92 "operand is expected to be the name of a member");
93 auto name = current_operand->find(ID_component_name).id();
96 current_operand != struct_expr.
operands().end(),
97 "every name is expected to be followed by a paired value");
98 pairs[name] = *current_operand;
108 const auto struct_type = ns.
follow_tag(tag_type);
110 const auto components =
113 const auto &update = updates.find(
component.get_name());
114 if(update != updates.end())
115 return update->second;
120 .collect<exprt::operandst>();
141 if(struct_expr.
operands().size() == 1)
142 return struct_expr.
operands().front();
149 const std::size_t union_width = bit_width(union_expr.
type());
151 const std::size_t component_width = bit_width(union_expr.
op().
type());
152 if(union_width == component_width)
155 union_width >= component_width,
156 "Union must be at least as wide as its component.");
167 auto member_component_rit = std::find_if(
171 return component.get_name() == name;
174 member_component_rit != type.
components().rend(),
175 "Definition of struct type should include named component.");
176 const auto trailing_widths =
181 return std::accumulate(
182 trailing_widths.begin(), trailing_widths.end(), std::size_t{0});
196 const auto &compound_type = member_expr.
compound().
type();
197 const auto offset_bits = [&]() -> std::size_t {
204 const auto &struct_type =
205 compound_type.id() == ID_struct_tag
206 ?
ns.get().follow_tag(
213 member_expr.
compound(), offset_bits, member_expr.
type()};
218 std::queue<exprt *> work_queue;
219 work_queue.push(&expr);
220 while(!work_queue.empty())
222 exprt ¤t = *work_queue.front();
229 std::optional<exprt> update;
242 "Updates in struct encoding are expected to be a change of state.");
243 current = std::move(*update);
250 for(
auto &operand : current.
operands())
251 work_queue.push(&operand);
257 const exprt &encoded,
272 "Structs are expected to be encoded into bit vectors.");
273 const struct_typet definition =
ns.get().follow_tag(original_type);
285 const exprt &encoded,
290 "Unions are expected to be encoded into bit vectors.");
291 const union_typet definition =
ns.get().follow_tag(original_type);
292 const auto &components = definition.
components();
293 if(components.empty())
299 const auto &component_for_definition = components[0];
302 component_for_definition.get_name(),
305 typecast_exprt{encoded, original_type}, component_for_definition}),
306 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.
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'.
#define POSTCONDITION(CONDITION)
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::unordered_map< irep_idt, exprt > extricate_updates(const with_exprt &struct_expr)
Extracts the component/field names and new values from a with_exprt which expresses a new struct valu...
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.