Skip to content

Introduce typet::add_subtype #7110

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kroening merged 4 commits into from
Sep 9, 2022
Merged

Introduce typet::add_subtype #7110

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
040c93c
replace uses of typet::subtype() nonconst
kroening Sep 7, 2022
d2c1f4b
introduce typet::add_subtype()
kroening Sep 7, 2022
61acf6c
use typet::add_subtype
kroening Sep 7, 2022
8b7b7a9
protect typet::subtype() nonconst
kroening Sep 8, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/remove_java_new.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -280,7 +280,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
if(!rhs.get_bool(ID_skip_initialize))
{
const auto zero_element =
zero_initializer(data.type().subtype(), location, ns);
zero_initializer(to_pointer_type(data.type()).base_type(), location, ns);
CHECK_RETURN(zero_element.has_value());
codet array_set{ID_array_set, {new_array_data_symbol, *zero_element}};
dest.insert_before(next, goto_programt::make_other(array_set, location));
Expand Down Expand Up @@ -316,7 +316,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(

plus_exprt(tmp_i, from_integer(1, tmp_i.type()));
dereference_exprt deref_expr(
plus_exprt(data, tmp_i), data.type().subtype());
plus_exprt(data, tmp_i), to_pointer_type(data.type()).base_type());

code_blockt for_body;
symbol_exprt init_sym =
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/ansi_c_convert_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -673,7 +673,7 @@ void ansi_c_convert_typet::set_attributes(typet &type) const
if(gcc_attribute_mode.is_not_nil())
{
typet new_type=gcc_attribute_mode;
new_type.subtype()=type;
new_type.add_subtype() = type;
type.swap(new_type);
}

Expand Down
6 changes: 4 additions & 2 deletions src/ansi-c/ansi_c_declaration.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ void ansi_c_declaratort::build(irept &src)
p = &merged_type.last_type();
}
else
p=&t.subtype();
p = &t.add_subtype();
}

type()=static_cast<const typet &>(src);
Expand Down Expand Up @@ -103,7 +103,9 @@ typet ansi_c_declarationt::full_type(
if(p->id()==ID_frontend_pointer || p->id()==ID_array ||
p->id()==ID_vector || p->id()==ID_c_bit_field ||
p->id()==ID_block_pointer || p->id()==ID_code)
p=&p->subtype();
{
p = &p->add_subtype();
}
else if(p->id()==ID_merged_type)
{
// we always go down on the right-most subtype
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1364,7 +1364,7 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
for(const auto &member : enum_members)
body.push_back(member);

enum_tag_symbol.type.subtype()=underlying_type;
enum_tag_symbol.type.add_subtype() = underlying_type;

// is it in the symbol table already?
symbol_tablet::symbolst::const_iterator s_it=
Expand Down
50 changes: 25 additions & 25 deletions src/ansi-c/parser.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1340,7 +1340,7 @@ atomic_specifier:
{
$$=$1;
parser_stack($$).id(ID_atomic_type_specifier);
stack_type($$).subtype()=stack_type($3);
stack_type($$).add_subtype()=stack_type($3);
}
;

Expand Down Expand Up @@ -1530,7 +1530,7 @@ elaborated_type_name:

array_of_construct:
TOK_ARRAY_OF '<' type_name '>'
{ $$=$1; stack_type($$).subtype().swap(parser_stack($2)); }
{ $$=$1; stack_type($$).add_subtype().swap(parser_stack($2)); }
;

pragma_packed:
Expand Down Expand Up @@ -1787,7 +1787,7 @@ member_declarator:
| bit_field_size gcc_type_attribute_opt
{
$$=$1;
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);

if(parser_stack($2).is_not_nil()) // type attribute
$$=merge($2, $$);
Expand All @@ -1807,7 +1807,7 @@ member_identifier_declarator:
| bit_field_size gcc_type_attribute_opt
{
$$=$1;
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);

if(parser_stack($2).is_not_nil()) // type attribute
$$=merge($2, $$);
Expand All @@ -1828,7 +1828,7 @@ bit_field_size:
$$=$1;
set($$, ID_c_bit_field);
stack_type($$).set(ID_size, parser_stack($2));
stack_type($$).subtype().id(ID_abstract);
stack_type($$).add_subtype().id(ID_abstract);
}
;

Expand Down Expand Up @@ -3235,7 +3235,7 @@ unary_identifier_declarator:
// The below is deliberately not using pointer_type();
// the width is added during conversion.
stack_type($1).id(ID_frontend_pointer);
stack_type($1).subtype()=typet(ID_abstract);
stack_type($1).add_subtype()=typet(ID_abstract);
$2=merge($2, $1); // dest=$2
make_subtype($3, $2); // dest=$3
$$=$3;
Expand Down Expand Up @@ -3431,7 +3431,7 @@ postfixing_abstract_declarator:
{
$$=$1;
set($$, ID_code);
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);
stack_type($$).add(ID_parameters);
stack_type($$).set(ID_C_KnR, true);
}
Expand All @@ -3448,7 +3448,7 @@ postfixing_abstract_declarator:
{
$$=$1;
set($$, ID_code);
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);
stack_type($$).add(ID_parameters).get_sub().
swap((irept::subt &)(to_type_with_subtypes(stack_type($3)).subtypes()));
PARSER.pop_scope();
Expand Down Expand Up @@ -3476,7 +3476,7 @@ parameter_postfixing_abstract_declarator:
{
set($1, ID_code);
stack_type($1).add(ID_parameters);
stack_type($1).subtype()=typet(ID_abstract);
stack_type($1).add_subtype()=typet(ID_abstract);
PARSER.pop_scope();

// Clear function name in source location after parsing if
Expand Down Expand Up @@ -3506,7 +3506,7 @@ parameter_postfixing_abstract_declarator:
cprover_function_contract_sequence_opt
{
set($1, ID_code);
stack_type($1).subtype()=typet(ID_abstract);
stack_type($1).add_subtype()=typet(ID_abstract);
stack_type($1).add(ID_parameters).get_sub().
swap((irept::subt &)(to_type_with_subtypes(stack_type($3)).subtypes()));
PARSER.pop_scope();
Expand All @@ -3532,7 +3532,7 @@ array_abstract_declarator:
{
$$=$1;
set($$, ID_array);
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);
stack_type($$).add(ID_size).make_nil();
}
| '[' attribute_type_qualifier_storage_class_list ']'
Expand All @@ -3541,7 +3541,7 @@ array_abstract_declarator:
// The type qualifier belongs to the array, not the
// contents of the array, nor the size.
set($1, ID_array);
stack_type($1).subtype()=typet(ID_abstract);
stack_type($1).add_subtype()=typet(ID_abstract);
stack_type($1).add(ID_size).make_nil();
$$=merge($2, $1);
}
Expand All @@ -3550,23 +3550,23 @@ array_abstract_declarator:
// these should be allowed in prototypes only
$$=$1;
set($$, ID_array);
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);
stack_type($$).add(ID_size).make_nil();
}
| '[' constant_expression ']'
{
$$=$1;
set($$, ID_array);
stack_type($$).add(ID_size).swap(parser_stack($2));
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);
}
| '[' attribute_type_qualifier_storage_class_list constant_expression ']'
{
// The type qualifier belongs to the array, not the
// contents of the array, nor the size.
set($1, ID_array);
stack_type($1).add(ID_size).swap(parser_stack($3));
stack_type($1).subtype()=typet(ID_abstract);
stack_type($1).add_subtype()=typet(ID_abstract);
$$=merge($2, $1); // dest=$2
}
| array_abstract_declarator '[' constant_expression ']'
Expand All @@ -3575,7 +3575,7 @@ array_abstract_declarator:
$$=$1;
set($2, ID_array);
stack_type($2).add(ID_size).swap(parser_stack($3));
stack_type($2).subtype()=typet(ID_abstract);
stack_type($2).add_subtype()=typet(ID_abstract);
make_subtype($1, $2);
}
| array_abstract_declarator '[' '*' ']'
Expand All @@ -3585,7 +3585,7 @@ array_abstract_declarator:
$$=$1;
set($2, ID_array);
stack_type($2).add(ID_size).make_nil();
stack_type($2).subtype()=typet(ID_abstract);
stack_type($2).add_subtype()=typet(ID_abstract);
make_subtype($1, $2);
}
;
Expand All @@ -3597,7 +3597,7 @@ unary_abstract_declarator:
// The below is deliberately not using pointer_type();
// the width is added during conversion.
stack_type($$).id(ID_frontend_pointer);
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);
}
| '*' attribute_type_qualifier_list
{
Expand All @@ -3606,7 +3606,7 @@ unary_abstract_declarator:
// The below is deliberately not using pointer_type();
// the width is added during conversion.
stack_type($1).id(ID_frontend_pointer);
stack_type($1).subtype()=typet(ID_abstract);
stack_type($1).add_subtype()=typet(ID_abstract);
$$=merge($2, $1);
}
| '*' abstract_declarator
Expand All @@ -3621,7 +3621,7 @@ unary_abstract_declarator:
// The below is deliberately not using pointer_type();
// the width is added during conversion.
stack_type($1).id(ID_frontend_pointer);
stack_type($1).subtype()=typet(ID_abstract);
stack_type($1).add_subtype()=typet(ID_abstract);
$2=merge($2, $1); // dest=$2
make_subtype($3, $2); // dest=$3
$$=$3;
Expand All @@ -3632,7 +3632,7 @@ unary_abstract_declarator:
// http://en.wikipedia.org/wiki/Blocks_(C_language_extension)
$$=$1;
set($$, ID_block_pointer);
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);
}
;

Expand All @@ -3643,7 +3643,7 @@ parameter_unary_abstract_declarator:
// The below is deliberately not using pointer_type();
// the width is added during conversion.
stack_type($$).id(ID_frontend_pointer);
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);
}
| '*' attribute_type_qualifier_list
{
Expand All @@ -3652,7 +3652,7 @@ parameter_unary_abstract_declarator:
// The below is deliberately not using pointer_type();
// the width is added during conversion.
stack_type($1).id(ID_frontend_pointer);
stack_type($1).subtype()=typet(ID_abstract);
stack_type($1).add_subtype()=typet(ID_abstract);
$$=merge($2, $1);
}
| '*' parameter_abstract_declarator
Expand All @@ -3667,7 +3667,7 @@ parameter_unary_abstract_declarator:
// The below is deliberately not using pointer_type();
// the width is added during conversion.
stack_type($1).id(ID_frontend_pointer);
stack_type($1).subtype()=typet(ID_abstract);
stack_type($1).add_subtype()=typet(ID_abstract);
$2=merge($2, $1); // dest=$2
make_subtype($3, $2); // dest=$3
$$=$3;
Expand All @@ -3678,7 +3678,7 @@ parameter_unary_abstract_declarator:
// http://en.wikipedia.org/wiki/Blocks_(C_language_extension)
$$=$1;
set($$, ID_block_pointer);
stack_type($$).subtype()=typet(ID_abstract);
stack_type($$).add_subtype()=typet(ID_abstract);
}
;

Expand Down
6 changes: 3 additions & 3 deletions src/ansi-c/parser_static.inc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ static void make_subtype(typet &dest, typet &src)
sub->id()==ID_code)
{
// walk down
p=&sub->subtype();
p=&sub->add_subtype();
}
else
{
Expand Down Expand Up @@ -250,7 +250,7 @@ static void make_subtype(typet &dest, typet &src)
else if(p->is_nil())
assert(false);
else
p=&p->subtype();
p=&p->add_subtype();
}
break;
}
Expand Down Expand Up @@ -292,7 +292,7 @@ static void make_pointer(const YYSTYPE dest)
// The below deliberately avoids pointer_type().
// The width is set during conversion.
stack_type(dest).id(ID_frontend_pointer);
stack_type(dest).subtype()=typet(ID_abstract);
stack_type(dest).add_subtype()=typet(ID_abstract);
}

/*******************************************************************\
Expand Down
13 changes: 8 additions & 5 deletions src/cpp/cpp_convert_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,8 @@ void cpp_convert_typet::read_rec(const typet &type)
else if(type.id()==ID_array)
{
other.push_back(type);
cpp_convert_plain_type(other.back().subtype(), get_message_handler());
cpp_convert_plain_type(
to_array_type(other.back()).element_type(), get_message_handler());
}
else if(type.id()==ID_template)
{
Expand Down Expand Up @@ -124,7 +125,8 @@ void cpp_convert_typet::read_template(const typet &type)
other.push_back(type);
typet &t=other.back();

cpp_convert_plain_type(t.subtype(), get_message_handler());
cpp_convert_plain_type(
to_type_with_subtype(t).subtype(), get_message_handler());

irept &arguments=t.add(ID_arguments);

Expand Down Expand Up @@ -157,7 +159,7 @@ void cpp_convert_typet::read_function_type(const typet &type)
// change subtype to return_type
typet &return_type = t.return_type();

return_type.swap(t.subtype());
return_type.swap(to_type_with_subtype(t).subtype());
t.remove_subtype();

if(return_type.is_not_nil())
Expand Down Expand Up @@ -203,7 +205,7 @@ void cpp_convert_typet::read_function_type(const typet &type)
if(final_type.id()==ID_array)
{
// turn into pointer type
final_type=pointer_type(final_type.subtype());
final_type = pointer_type(to_array_type(final_type).element_type());
}

code_typet::parametert new_parameter(final_type);
Expand Down Expand Up @@ -352,7 +354,8 @@ void cpp_convert_auto(
{
if(dest.id() != ID_merged_type && dest.has_subtype())
{
cpp_convert_auto(dest.subtype(), src, message_handler);
cpp_convert_auto(
to_type_with_subtype(dest).subtype(), src, message_handler);
return;
}

Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cpp_declarator.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ typet cpp_declaratort::merge_type(const typet &declaration_type) const
else
{
assert(!t.id().empty());
p=&t.subtype();
p = &t.add_subtype();
}
}

Expand Down
4 changes: 2 additions & 2 deletions src/cpp/cpp_declarator_converter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ symbolt &cpp_declarator_convertert::convert(
{
typet type;
type.swap(declarator.name().get_sub().back());
declarator.type().subtype()=type;
declarator.type().add_subtype() = type;
cpp_typecheck.typecheck_type(type);
cpp_namet::namet name("(" + cpp_type2name(type) + ")");
declarator.name().get_sub().back().swap(name);
Expand Down Expand Up @@ -110,7 +110,7 @@ symbolt &cpp_declarator_convertert::convert(
{
UNREACHABLE;
typet tmp;
tmp.swap(final_type.subtype());
tmp.swap(to_template_type(final_type).subtype());
final_type.swap(tmp);
}

Expand Down
Loading