Skip to content

Commit

Permalink
Byte-operator lowering: struct and union constants are not ID_constant
Browse files Browse the repository at this point in the history
These are struct- and union expressions, or possible empty_union_exprt.
Creating constant_exprt resulted in a segmentation fault in simplifying
member expressions, as witnessed when working on
model-checking/kani#705.
  • Loading branch information
tautschnig committed Nov 16, 2022
1 parent 20535ad commit 54369a6
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 20 deletions.
14 changes: 7 additions & 7 deletions src/util/lower_byte_operators.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,8 @@ static struct_exprt bv_to_struct_expr(

if(component_bits == 0)
{
operands.push_back(constant_exprt{irep_idt{}, comp.type()});
operands.push_back(
bv_to_expr(bitvector_expr, comp.type(), endianness_map, ns));
continue;
}

Expand All @@ -123,17 +124,16 @@ static struct_exprt bv_to_struct_expr(

/// Convert a bitvector-typed expression \p bitvector_expr to a union-typed
/// expression. See \ref bv_to_expr for an overview.
static union_exprt bv_to_union_expr(
static exprt bv_to_union_expr(
const exprt &bitvector_expr,
const union_typet &union_type,
const endianness_mapt &endianness_map,
const namespacet &ns)
{
const union_typet::componentst &components = union_type.components();

// empty union, handled the same way as done in expr_initializert
if(components.empty())
return union_exprt{irep_idt{}, nil_exprt{}, union_type};
return empty_union_exprt{union_type};

const auto widest_member = union_type.find_widest_union_component(ns);

Expand All @@ -147,7 +147,7 @@ static union_exprt bv_to_union_expr(
{
return union_exprt{
components.front().get_name(),
constant_exprt{irep_idt{}, components.front().type()},
bv_to_expr(bitvector_expr, components.front().type(), endianness_map, ns),
union_type};
}

Expand Down Expand Up @@ -371,13 +371,13 @@ static exprt bv_to_expr(
}
else if(target_type.id() == ID_union_tag)
{
union_exprt result = bv_to_union_expr(
exprt result = bv_to_union_expr(
bitvector_expr,
ns.follow_tag(to_union_tag_type(target_type)),
endianness_map,
ns);
result.type() = target_type;
return std::move(result);
return result;
}
else if(target_type.id() == ID_array)
{
Expand Down
25 changes: 12 additions & 13 deletions src/util/simplify_expr_struct.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -104,21 +104,20 @@ simplify_exprt::simplify_member(const member_exprt &expr)
}
}
}
else if(op.id()==ID_struct ||
op.id()==ID_constant)
else if(op.id() == ID_struct)
{
if(op_type.id()==ID_struct)
// pull out the right member
const struct_typet &struct_type = to_struct_type(op_type);
if(struct_type.has_component(component_name))
{
// pull out the right member
const struct_typet &struct_type=to_struct_type(op_type);
if(struct_type.has_component(component_name))
{
std::size_t number=struct_type.component_number(component_name);
DATA_INVARIANT(
op.operands()[number].type() == expr.type(),
"member expression type must match component type");
return op.operands()[number];
}
std::size_t number = struct_type.component_number(component_name);
DATA_INVARIANT(
op.operands().size() > number,
"struct expression must have sufficiently many operands");
DATA_INVARIANT(
op.operands()[number].type() == expr.type(),
"member expression type must match component type");
return op.operands()[number];
}
}
else if(op.id()==ID_byte_extract_little_endian ||
Expand Down

0 comments on commit 54369a6

Please sign in to comment.