diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp index 1e709ffd312..5da09322801 100644 --- a/jbmc/src/java_bytecode/remove_java_new.cpp +++ b/jbmc/src/java_bytecode/remove_java_new.cpp @@ -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)); @@ -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 = diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 425d30113f3..cb5beb98a2c 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -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); } diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 4ba9d045427..7d45ee0a1df 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -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(src); @@ -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 diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 0905542f377..a7f00526236 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -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= diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 9941c9e7184..66231f4c673 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -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); } ; @@ -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: @@ -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, $$); @@ -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, $$); @@ -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); } ; @@ -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; @@ -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); } @@ -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(); @@ -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 @@ -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(); @@ -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 ']' @@ -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); } @@ -3550,7 +3550,7 @@ 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 ']' @@ -3558,7 +3558,7 @@ array_abstract_declarator: $$=$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 ']' { @@ -3566,7 +3566,7 @@ array_abstract_declarator: // 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 ']' @@ -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 '[' '*' ']' @@ -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); } ; @@ -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 { @@ -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 @@ -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; @@ -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); } ; @@ -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 { @@ -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 @@ -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; @@ -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); } ; diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc index df32d8aa2ef..1716fa5fd43 100644 --- a/src/ansi-c/parser_static.inc +++ b/src/ansi-c/parser_static.inc @@ -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 { @@ -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; } @@ -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); } /*******************************************************************\ diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index ff79b21a576..a39616be24d 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -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) { @@ -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); @@ -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()) @@ -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); @@ -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; } diff --git a/src/cpp/cpp_declarator.cpp b/src/cpp/cpp_declarator.cpp index 4d465954c07..8d070f3c88f 100644 --- a/src/cpp/cpp_declarator.cpp +++ b/src/cpp/cpp_declarator.cpp @@ -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(); } } diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index 4065997d636..ff2531ea3ed 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -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); @@ -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); } diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index 1dcccb3d87c..18c5c9ddf9f 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -128,7 +128,8 @@ void cpp_typecheckt::typecheck_try_catch(codet &code) cpp_declaratort &declarator=cpp_declaration.declarators().front(); if(is_reference(declarator.type())) - declarator.type()=declarator.type().subtype(); + declarator.type() = + to_reference_type(declarator.type()).base_type(); } // typecheck the body @@ -309,7 +310,9 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) // maybe the name of the member collides with a parameter of the // constructor exprt dereference( - ID_dereference, cpp_scopes.current_scope().this_expr.type().subtype()); + ID_dereference, + to_pointer_type(cpp_scopes.current_scope().this_expr.type()) + .base_type()); dereference.copy_to_operands(cpp_scopes.current_scope().this_expr); cpp_typecheck_fargst deref_fargs; deref_fargs.add_object(dereference); diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 193f1515dfc..7de63ed395b 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -315,7 +315,7 @@ void cpp_typecheckt::typecheck_compound_declarator( declarator.name().get_sub().front().id()==ID_operator); typet type=static_cast(declarator.name().get_sub()[1]); - declarator.type().subtype()=type; + declarator.type().add_subtype() = type; cpp_namet::namet name("(" + cpp_type2name(type) + ")"); declarator.name().get_sub().back().swap(name); @@ -638,7 +638,9 @@ void cpp_typecheckt::typecheck_compound_declarator( // change the type of the 'this' pointer code_typet &code_type=to_code_type(func_symb.type); code_typet::parametert &this_parameter = code_type.parameters().front(); - this_parameter.type().subtype().set(ID_identifier, virtual_base); + to_pointer_type(this_parameter.type()) + .base_type() + .set(ID_identifier, virtual_base); // create symbols for the parameters code_typet::parameterst &args=code_type.parameters(); diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index 2879af7662c..0c006ef9df7 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -39,7 +39,7 @@ static void copy_parent( "explicit-typecast", pointer_type(cpp_namet(parent_base_name, source_location).as_type())); op1.type().set(ID_C_reference, true); - op1.type().subtype().set(ID_C_constant, true); + to_pointer_type(op1.type()).base_type().set(ID_C_constant, true); op1.get_sub().push_back(cpp_namet(arg_name, source_location)); op1.add_source_location()=source_location; @@ -123,7 +123,7 @@ void cpp_typecheckt::default_ctor( cpp_declaratort decl; decl.name() = cpp_namet(base_name, source_location); decl.type()=typet(ID_function_type); - decl.type().subtype().make_nil(); + decl.type().add_subtype().make_nil(); decl.add_source_location()=source_location; decl.value() = code_blockt(); @@ -308,8 +308,11 @@ void cpp_typecheckt::default_assignop( declarator_name.get_sub().push_back(irept("=")); declarator_type.id(ID_function_type); - declarator_type.subtype() = reference_type(uninitialized_typet{}); - declarator_type.subtype().add(ID_C_qualifier).make_nil(); + declarator_type.add_subtype() = reference_type(uninitialized_typet{}); + to_type_with_subtype(declarator_type) + .subtype() + .add(ID_C_qualifier) + .make_nil(); exprt &args=static_cast(declarator.type().add(ID_parameters)); args.add_source_location()=source_location; diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index b53e65e988f..8817ed686aa 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -145,10 +145,10 @@ bool cpp_typecheckt::standard_conversion_qualification( if(qual_from!=qual_to && !const_to) return false; - typet tmp1=sub_from.subtype(); + typet tmp1 = to_pointer_type(sub_from).base_type(); sub_from.swap(tmp1); - typet tmp2=sub_to.subtype(); + typet tmp2 = sub_to.add_subtype(); sub_to.swap(tmp2); } @@ -497,7 +497,7 @@ bool cpp_typecheckt::standard_conversion_pointer( c_qualifierst qual_from; qual_from.read(to_pointer_type(expr.type()).base_type()); new_expr = typecast_exprt::conditional_cast(expr, type); - qual_from.write(new_expr.type().subtype()); + qual_from.write(to_pointer_type(new_expr.type()).base_type()); return true; } @@ -512,7 +512,7 @@ bool cpp_typecheckt::standard_conversion_pointer( qual_from.read(to_pointer_type(expr.type()).base_type()); new_expr=expr; make_ptr_typecast(new_expr, type); - qual_from.write(new_expr.type().subtype()); + qual_from.write(to_pointer_type(new_expr.type()).base_type()); return true; } } @@ -586,8 +586,9 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member( INVARIANT(this2.get_this(), "first parameter should be `this'"); code2.parameters().erase(code2.parameters().begin()); - if(this2.type().subtype().get_bool(ID_C_constant) && - !this1.type().subtype().get_bool(ID_C_constant)) + if( + to_pointer_type(this2.type()).base_type().get_bool(ID_C_constant) && + !to_pointer_type(this1.type()).base_type().get_bool(ID_C_constant)) return false; // give a second chance ignoring `this' @@ -692,7 +693,8 @@ bool cpp_typecheckt::standard_conversion_sequence( // we turn bit fields into their underlying type if(curr_expr.type().id()==ID_c_bit_field) - curr_expr = typecast_exprt(curr_expr, curr_expr.type().subtype()); + curr_expr = typecast_exprt( + curr_expr, to_c_bit_field_type(curr_expr.type()).underlying_type()); if(curr_expr.type().id()==ID_array) { @@ -818,9 +820,9 @@ bool cpp_typecheckt::standard_conversion_sequence( do { - typet tmp_from=sub_from.subtype(); + typet tmp_from = to_pointer_type(sub_from).base_type(); sub_from.swap(tmp_from); - typet tmp_to=sub_to.subtype(); + typet tmp_to = sub_to.add_subtype(); sub_to.swap(tmp_to); c_qualifierst qual_from; @@ -951,7 +953,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence( if(is_reference(arg1_type)) { - typet tmp=arg1_type.subtype(); + typet tmp = to_reference_type(arg1_type).base_type(); arg1_type.swap(tmp); } @@ -1272,7 +1274,7 @@ bool cpp_typecheckt::reference_binding( c_qualifierst qual_from; qual_from.read(expr.type()); new_expr = typecast_exprt::conditional_cast(new_expr, type); - qual_from.write(new_expr.type().subtype()); + qual_from.write(to_reference_type(new_expr.type()).base_type()); } return true; @@ -1349,7 +1351,7 @@ bool cpp_typecheckt::reference_binding( c_qualifierst qual_from; qual_from.read(returned_value.type()); make_ptr_typecast(new_expr, type); - qual_from.write(new_expr.type().subtype()); + qual_from.write(to_reference_type(new_expr.type()).base_type()); } rank+=4+tmp_rank; return true; @@ -1598,7 +1600,7 @@ bool cpp_typecheckt::cast_away_constness( while(snt1.back().has_subtype()) { snt1.reserve(snt1.size()+1); - snt1.push_back(snt1.back().subtype()); + snt1.push_back(to_type_with_subtype(snt1.back()).subtype()); } c_qualifierst q1; @@ -1613,7 +1615,7 @@ bool cpp_typecheckt::cast_away_constness( while(snt2.back().has_subtype()) { snt2.reserve(snt2.size()+1); - snt2.push_back(snt2.back().subtype()); + snt2.push_back(to_type_with_subtype(snt2.back()).subtype()); } c_qualifierst q2; @@ -1627,10 +1629,12 @@ bool cpp_typecheckt::cast_away_constness( for(std::size_t i=k; i > 1; i--) { - snt1[snt1.size()-2].subtype()=snt1[snt1.size()-1]; + to_type_with_subtype(snt1[snt1.size() - 2]).subtype() = + snt1[snt1.size() - 1]; snt1.pop_back(); - snt2[snt2.size()-2].subtype()=snt2[snt2.size()-1]; + to_type_with_subtype(snt2[snt2.size() - 2]).subtype() = + snt2[snt2.size() - 1]; snt2.pop_back(); } diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index 4a7683a5f9e..90393460a0a 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -37,7 +37,7 @@ void cpp_typecheckt::default_dtor( cpp_declaratort decl; decl.name() = cpp_namet("~" + id2string(symbol.base_name), symbol.location); decl.type().id(ID_function_type); - decl.type().subtype().make_nil(); + decl.type().add_subtype().make_nil(); decl.value() = code_blockt(); decl.add(ID_cv).make_nil(); diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp index 3134d986e36..4e2f54fe76c 100644 --- a/src/cpp/cpp_typecheck_enum_type.cpp +++ b/src/cpp/cpp_typecheck_enum_type.cpp @@ -151,15 +151,15 @@ void cpp_typecheckt::typecheck_enum_type(typet &type) // C++11 enumerations have an underlying type, // which defaults to int. // enums without underlying type may be 'packed'. - if(type.subtype().is_nil()) - type.subtype()=signed_int_type(); + if(type.add_subtype().is_nil()) + type.add_subtype() = signed_int_type(); else { - typecheck_type(type.subtype()); + typecheck_type(to_type_with_subtype(type).subtype()); if( - type.subtype().id() != ID_signedbv && - type.subtype().id() != ID_unsignedbv && - type.subtype().id() != ID_c_bool) + to_type_with_subtype(type).subtype().id() != ID_signedbv && + to_type_with_subtype(type).subtype().id() != ID_unsignedbv && + to_type_with_subtype(type).subtype().id() != ID_c_bool) { error().source_location=type.source_location(); error() << "underlying type must be integral" << eom; diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index a43e24c7c7d..fe1062f9798 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -250,9 +250,11 @@ void cpp_typecheckt::typecheck_expr_trinary(if_exprt &expr) expr.type()=e2.type(); expr.op2().swap(e2); } - else if(expr.op1().type().id()==ID_array && - expr.op2().type().id()==ID_array && - expr.op1().type().subtype() == expr.op2().type().subtype()) + else if( + expr.op1().type().id() == ID_array && + expr.op2().type().id() == ID_array && + to_array_type(expr.op1().type()).element_type() == + to_array_type(expr.op2().type()).element_type()) { // array-to-pointer conversion @@ -409,7 +411,7 @@ bool cpp_typecheckt::overloadable(const exprt &expr) typet t = it->type(); if(is_reference(t)) - t=t.subtype(); + t = to_reference_type(t).base_type(); if( t.id() == ID_struct || t.id() == ID_union || t.id() == ID_c_enum || @@ -693,7 +695,8 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr) if(op.id() == ID_address_of && op.get_bool(ID_C_implicit)) { // must be the address of a function - code_typet &code_type=to_code_type(op.type().subtype()); + code_typet &code_type = + to_code_type(to_pointer_type(op.type()).base_type()); code_typet::parameterst &args=code_type.parameters(); if(!args.empty() && args.front().get_this()) @@ -714,7 +717,8 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr) else if(op.id() == ID_ptrmember && to_unary_expr(op).op().id() == "cpp-this") { expr.type() = pointer_type(op.type()); - expr.type().add(ID_to_member) = to_unary_expr(op).op().type().subtype(); + expr.type().add(ID_to_member) = + to_pointer_type(to_unary_expr(op).op().type()).base_type(); return; } @@ -722,7 +726,7 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr) const bool is_ref=is_reference(expr.type()); c_typecheck_baset::typecheck_expr_address_of(expr); if(is_ref) - expr.type()=reference_type(expr.type().subtype()); + expr.type() = reference_type(to_pointer_type(expr.type()).base_type()); } void cpp_typecheckt::typecheck_expr_throw(exprt &expr) @@ -756,8 +760,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr) if(expr.type().id()==ID_array) { - // first typecheck subtype - typecheck_type(expr.type().subtype()); + // first typecheck the element type + typecheck_type(to_array_type(expr.type()).element_type()); // typecheck the size exprt &size=to_array_type(expr.type()).size(); @@ -774,8 +778,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr) expr.set(ID_size, to_array_type(expr.type()).size()); // new actually returns a pointer, not an array - pointer_typet ptr_type= - pointer_type(expr.type().subtype()); + pointer_typet ptr_type = + pointer_type(to_array_type(expr.type()).element_type()); expr.type().swap(ptr_type); } else @@ -789,7 +793,7 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr) expr.type().swap(ptr_type); } - exprt object_expr(ID_new_object, expr.type().subtype()); + exprt object_expr(ID_new_object, to_pointer_type(expr.type()).base_type()); object_expr.set(ID_C_lvalue, true); already_typechecked_exprt::make_already_typechecked(object_expr); @@ -817,13 +821,15 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr) // we add the size of the object for convenience of the // runtime library - auto size_of_opt = size_of_expr(expr.type().subtype(), *this); + auto size_of_opt = + size_of_expr(to_pointer_type(expr.type()).base_type(), *this); if(size_of_opt.has_value()) { auto &sizeof_expr = static_cast(expr.add(ID_sizeof)); sizeof_expr = size_of_opt.value(); - sizeof_expr.add(ID_C_c_sizeof_type) = expr.type().subtype(); + sizeof_expr.add(ID_C_c_sizeof_type) = + to_pointer_type(expr.type()).base_type(); } } @@ -1024,14 +1030,14 @@ void cpp_typecheckt::typecheck_expr_delete(exprt &expr) // remove any const-ness of the argument // (which would impair the call to the destructor) - pointer_type.subtype().remove(ID_C_constant); + to_pointer_type(pointer_type).base_type().remove(ID_C_constant); // delete expressions are always void expr.type()=typet(ID_empty); // we provide the right destructor, for the convenience // of later stages - exprt new_object(ID_new_object, pointer_type.subtype()); + exprt new_object(ID_new_object, to_pointer_type(pointer_type).base_type()); new_object.add_source_location()=expr.source_location(); new_object.set(ID_C_lvalue, true); @@ -1636,13 +1642,13 @@ void cpp_typecheckt::typecheck_side_effect_function_call( } // get the virtual table - typet this_type= - to_code_type(expr.function().type()).parameters().front().type(); - irep_idt vtable_name= - this_type.subtype().get_string(ID_identifier) +"::@vtable_pointer"; + auto this_type = to_pointer_type( + to_code_type(expr.function().type()).parameters().front().type()); + irep_idt vtable_name = + this_type.base_type().get_string(ID_identifier) + "::@vtable_pointer"; - const struct_typet &vt_struct= - to_struct_type(follow(this_type.subtype())); + const struct_typet &vt_struct = + to_struct_type(follow(this_type.base_type())); const struct_typet::componentt &vt_compo= vt_struct.get_component(vtable_name); @@ -2011,7 +2017,7 @@ void cpp_typecheckt::typecheck_side_effect_assignment(side_effect_exprt &expr) typet type0 = to_binary_expr(expr).op0().type(); if(is_reference(type0)) - type0=type0.subtype(); + type0 = to_reference_type(type0).base_type(); if(cpp_is_pod(type0)) { @@ -2188,7 +2194,9 @@ void cpp_typecheckt::convert_pmop(exprt &expr) throw 0; } - typet t0 = op0.type().id() == ID_pointer ? op0.type().subtype() : op0.type(); + typet t0 = op0.type().id() == ID_pointer + ? to_pointer_type(op0.type()).base_type() + : op0.type(); typet t1((const typet &)op1.type().find(ID_to_member)); diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 2fbda5d90a9..e2685095254 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -79,7 +79,8 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol) else if(cpp_is_pod(symbol.type)) { if( - symbol.type.id() == ID_pointer && symbol.type.subtype().id() == ID_code && + symbol.type.id() == ID_pointer && + to_pointer_type(symbol.type).base_type().id() == ID_code && symbol.value.id() == ID_address_of && to_address_of_expr(symbol.value).object().id() == ID_cpp_name) { @@ -90,7 +91,8 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol) cpp_typecheck_fargst fargs; fargs.in_use = true; - const code_typet &code_type=to_code_type(symbol.type.subtype()); + const code_typet &code_type = + to_code_type(to_pointer_type(symbol.type).base_type()); for(const auto ¶meter : code_type.parameters()) { diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 12a32023232..885791d799e 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -526,13 +526,13 @@ void cpp_typecheck_resolvet::disambiguate_functions( if(type1.id()==ID_pointer) { - typet tmp=type1.subtype(); + typet tmp = to_pointer_type(type1).base_type(); type1=tmp; } if(type2.id()==ID_pointer) { - typet tmp=type2.subtype(); + typet tmp = to_pointer_type(type2).base_type(); type2=tmp; } diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index ee84285ca0f..0ec59432b39 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -82,7 +82,7 @@ void cpp_typecheckt::typecheck_type(typet &type) // the pointer/reference might have a qualifier, // but do subtype first - typecheck_type(type.subtype()); + typecheck_type(to_pointer_type(type).base_type()); // Check if it is a pointer-to-member if(type.find(ID_to_member).is_not_nil()) @@ -101,10 +101,10 @@ void cpp_typecheckt::typecheck_type(typet &type) typecheck_type(class_object); // there may be parameters if this is a pointer to member function - if(type.subtype().id()==ID_code) + if(to_pointer_type(type).base_type().id() == ID_code) { code_typet::parameterst ¶meters = - to_code_type(type.subtype()).parameters(); + to_code_type(to_pointer_type(type).base_type()).parameters(); if(parameters.empty() || !parameters.front().get_this()) { @@ -132,12 +132,12 @@ void cpp_typecheckt::typecheck_type(typet &type) simplify(size_expr, *this); } - typecheck_type(type.subtype()); + typecheck_type(to_array_type(type).element_type()); - if(type.subtype().get_bool(ID_C_constant)) + if(to_array_type(type).element_type().get_bool(ID_C_constant)) type.set(ID_C_constant, true); - if(type.subtype().get_bool(ID_C_volatile)) + if(to_array_type(type).element_type().get_bool(ID_C_volatile)) type.set(ID_C_volatile, true); } else if(type.id()==ID_vector) @@ -169,7 +169,7 @@ void cpp_typecheckt::typecheck_type(typet &type) } else if(type.id()==ID_template) { - typecheck_type(type.subtype()); + typecheck_type(to_template_type(type).subtype()); } else if(type.id()==ID_c_enum) { @@ -245,7 +245,7 @@ void cpp_typecheckt::typecheck_type(typet &type) typecheck_expr(e); if(e.type().id() == ID_c_bit_field) - type = e.type().subtype(); + type = to_c_bit_field_type(e.type()).underlying_type(); else type = e.type(); } @@ -276,7 +276,7 @@ void cpp_typecheckt::typecheck_type(typet &type) { PRECONDITION(type.has_subtype()); merged_typet as_parsed; - as_parsed.move_to_subtypes(type.subtype()); + as_parsed.move_to_subtypes(to_type_with_subtype(type).subtype()); type.get_sub().clear(); as_parsed.move_to_subtypes(type); type.swap(as_parsed); diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index f6728ed6763..cc5eff8807b 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -401,7 +401,7 @@ class Parser // NOLINT(readability/identifiers) p = &merged_type.last_type(); } else - p=&p->subtype(); + p = &p->add_subtype(); } *p=src; @@ -1604,10 +1604,12 @@ bool Parser::rIntegralDeclaration( declaration.type().id() == ID_auto && declaration.declarators().size() == 1 && declaration.declarators().front().type().id() == ID_function_type && - declaration.declarators().front().type().subtype().is_not_nil()) + declaration.declarators().front().type().add_subtype().is_not_nil()) { - declaration.type() = declaration.declarators().front().type().subtype(); - declaration.declarators().front().type().subtype().make_nil(); + declaration.type() = + to_type_with_subtype(declaration.declarators().front().type()) + .subtype(); + declaration.declarators().front().type().add_subtype().make_nil(); } #ifdef DEBUG @@ -2643,7 +2645,7 @@ bool Parser::rConstructorDecl( trailing_return_type.make_nil(); constructor=cpp_declaratort(typet(ID_function_type)); - constructor.type().subtype().make_nil(); + constructor.type().add_subtype().make_nil(); constructor.name().swap(type_name); cpp_tokent op; @@ -2874,7 +2876,7 @@ bool Parser::rDeclaratorWithInit( typet bit_field_type(ID_c_bit_field); bit_field_type.set(ID_size, e); - bit_field_type.subtype().make_nil(); + bit_field_type.add_subtype().make_nil(); set_location(bit_field_type, tk); merge_types(bit_field_type, dw.type()); @@ -2949,7 +2951,7 @@ bool Parser::rDeclaratorWithInit( typet bit_field_type(ID_c_bit_field); bit_field_type.set(ID_size, e); - bit_field_type.subtype().make_nil(); + bit_field_type.add_subtype().make_nil(); set_location(bit_field_type, tk); merge_types(bit_field_type, declarator.type()); @@ -3122,7 +3124,7 @@ bool Parser::rDeclarator( if(is_args) { typet function_type(ID_function_type); - function_type.subtype().swap(d_outer); + function_type.add_subtype().swap(d_outer); function_type.add(ID_parameters).swap(args); // make this subtype of d_inner @@ -3159,10 +3161,10 @@ bool Parser::rDeclarator( if(!rTypeSpecifier(return_type, false)) return false; - if(d_outer.subtype().is_not_nil()) + if(d_outer.add_subtype().is_not_nil()) return false; - d_outer.subtype().swap(return_type); + d_outer.add_subtype().swap(return_type); } if(lex.LookAhead(0)==':') @@ -3205,7 +3207,7 @@ bool Parser::rDeclarator( tl.push_back(d_outer); while(tl.back().id() == ID_array) { - tl.push_back(tl.back().subtype()); + tl.push_back(tl.back().add_subtype()); } array_typet array_type(tl.back(), expr); @@ -3213,7 +3215,7 @@ bool Parser::rDeclarator( d_outer.swap(array_type); while(!tl.empty()) { - tl.back().subtype().swap(d_outer); + tl.back().add_subtype().swap(d_outer); d_outer.swap(tl.back()); tl.pop_back(); } @@ -3357,12 +3359,12 @@ bool Parser::optPtrOperator(typet &ptrs) if(it->id()==ID_merged_type) { auto &merged_type = to_merged_type(*it); - merged_type.last_type().subtype().swap(ptrs); + merged_type.last_type().add_subtype().swap(ptrs); } else { assert(it->is_not_nil()); - it->subtype().swap(ptrs); + it->add_subtype().swap(ptrs); } ptrs.swap(*it); @@ -4302,7 +4304,7 @@ bool Parser::rEnumSpec(typet &spec) spec=cpp_enum_typet(); set_location(spec, tk); - spec.subtype().make_nil(); + spec.add_subtype().make_nil(); // C++11 enum classes if(lex.LookAhead(0)==TOK_CLASS) @@ -4332,7 +4334,7 @@ bool Parser::rEnumSpec(typet &spec) if(lex.LookAhead(0)==':') { lex.get_token(tk); // read the colon - if(!rTypeName(spec.subtype())) + if(!rTypeName(spec.add_subtype())) return false; } diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp index 60fa77887d7..82152a749ac 100644 --- a/src/cpp/template_map.cpp +++ b/src/cpp/template_map.cpp @@ -11,14 +11,15 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "template_map.h" -#include - +#include #include #include #include "cpp_template_parameter.h" #include "cpp_template_type.h" +#include + void template_mapt::apply(typet &type) const { if(type.id()==ID_array) @@ -28,7 +29,7 @@ void template_mapt::apply(typet &type) const } else if(type.id()==ID_pointer) { - apply(type.subtype()); + apply(to_pointer_type(type).base_type()); } else if(type.id()==ID_struct || type.id()==ID_union) diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 62c76c17369..7f7f25eb52d 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -63,7 +63,7 @@ exprt goto_symext::address_arithmetic( address_of_exprt &a=to_address_of_expr(result); // turn &a of type T[i][j] into &(a[0][0]) - for(const typet *t = &(a.type().subtype()); + for(const typet *t = &(to_type_with_subtype(a.type()).subtype()); t->id() == ID_array && expr.type() != *t; t = &(to_array_type(*t).element_type())) a.object() = index_exprt(a.object(), from_integer(0, c_index_type())); diff --git a/src/util/type.h b/src/util/type.h index 8c870fb3fc8..ed519174c8f 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -54,8 +54,6 @@ class typet:public irept return static_cast(get_sub().front()); } -public: - // This method will be protected eventually. typet &subtype() { subt &sub=get_sub(); @@ -64,6 +62,20 @@ class typet:public irept return static_cast(sub.front()); } +public: + // This method allows the construction of a type with a subtype by + // starting from a type without subtype. It avoids copying the contents + // of the type. The primary use-case are parsers, where a copy could be + // too expensive. Consider type_with_subtypet(id, subtype) for other + // use-cases. + typet &add_subtype() + { + subt &sub = get_sub(); + if(sub.empty()) + sub.resize(1); + return static_cast(sub.front()); + } + bool has_subtypes() const { return !get_sub().empty(); }