diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 8ea42d94cec..6beadef8790 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -616,8 +616,9 @@ void rw_range_sett::get_objects_rec(const typet &type) // TODO should recurse into various composite types if(type.id()==ID_array) { - get_objects_rec(type.subtype()); - get_objects_rec(get_modet::READ, to_array_type(type).size()); + const auto &array_type = to_array_type(type); + get_objects_rec(array_type.subtype()); + get_objects_rec(get_modet::READ, array_type.size()); } } diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index 10c4dfff1f5..8a29048a732 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -140,5 +140,7 @@ void mutex_init_instrumentation(goto_modelt &goto_model) Forall_goto_functions(f_it, goto_model.goto_functions) mutex_init_instrumentation( - goto_model.symbol_table, f_it->second.body, lock_type.subtype()); + goto_model.symbol_table, + f_it->second.body, + to_pointer_type(lock_type).subtype()); } diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index 3485b8ce3a3..cf396af0d1b 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/src/goto-symex/auto_objects.cpp @@ -57,7 +57,7 @@ void goto_symext::initialize_auto_object( else if(type.id()==ID_pointer) { const pointer_typet &pointer_type=to_pointer_type(type); - const typet &subtype=ns.follow(type.subtype()); + const typet &subtype = ns.follow(pointer_type.subtype()); // we don't like function pointers and // we don't like void * @@ -67,7 +67,7 @@ void goto_symext::initialize_auto_object( // could be NULL nondeterministically address_of_exprt address_of_expr( - make_auto_object(type.subtype(), state), pointer_type); + make_auto_object(pointer_type.subtype(), state), pointer_type); if_exprt rhs( side_effect_expr_nondett(bool_typet(), expr.source_location()), diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 7a7530274dd..5381f9df3b1 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -211,7 +211,7 @@ static bool check_renaming(const typet &type) return true; } else if(type.has_subtype()) - return check_renaming(type.subtype()); + return check_renaming(to_type_with_subtype(type).subtype()); return false; } @@ -489,7 +489,7 @@ void goto_symex_statet::rename( { auto &address_of_expr = to_address_of_expr(expr); rename_address(address_of_expr.object(), ns, level); - expr.type().subtype() = address_of_expr.object().type(); + to_pointer_type(expr.type()).subtype() = address_of_expr.object().type(); } else { @@ -725,7 +725,7 @@ void goto_symex_statet::rename_address( rename_address(index_expr.array(), ns, level); PRECONDITION(index_expr.array().type().id() == ID_array); - expr.type()=index_expr.array().type().subtype(); + expr.type() = to_array_type(index_expr.array().type()).subtype(); // the index is not an address rename(index_expr.index(), ns, level); @@ -810,8 +810,9 @@ void goto_symex_statet::rename( if(type.id()==ID_array) { - rename(type.subtype(), irep_idt(), ns, level); - rename(to_array_type(type).size(), ns, level); + auto &array_type = to_array_type(type); + rename(array_type.subtype(), irep_idt(), ns, level); + rename(array_type.size(), ns, level); } else if(type.id()==ID_struct || type.id()==ID_union || @@ -832,7 +833,7 @@ void goto_symex_statet::rename( } else if(type.id()==ID_pointer) { - rename(type.subtype(), irep_idt(), ns, level); + rename(to_pointer_type(type).subtype(), irep_idt(), ns, level); } else if(type.id() == ID_symbol_type) { @@ -876,8 +877,9 @@ void goto_symex_statet::get_original_name(typet &type) const if(type.id()==ID_array) { - get_original_name(type.subtype()); - get_original_name(to_array_type(type).size()); + auto &array_type = to_array_type(type); + get_original_name(array_type.subtype()); + get_original_name(array_type.size()); } else if(type.id()==ID_struct || type.id()==ID_union || @@ -894,7 +896,7 @@ void goto_symex_statet::get_original_name(typet &type) const } else if(type.id()==ID_pointer) { - get_original_name(type.subtype()); + get_original_name(to_pointer_type(type).subtype()); } } diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index b168c0f6d7d..9e918fec7fd 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -60,9 +60,11 @@ void goto_symext::symex_allocate( const irep_idt &mode = function_symbol->mode; // is the type given? - if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty) + if( + code.type().id() == ID_pointer && + to_pointer_type(code.type()).subtype().id() != ID_empty) { - object_type=code.type().subtype(); + object_type = to_pointer_type(code.type()).subtype(); } else { @@ -190,11 +192,11 @@ void goto_symext::symex_allocate( if(object_type.id()==ID_array) { - index_exprt index_expr(value_symbol.type.subtype()); + const auto &array_type = to_array_type(object_type); + index_exprt index_expr(array_type.subtype()); index_expr.array()=value_symbol.symbol_expr(); index_expr.index()=from_integer(0, index_type()); - rhs=address_of_exprt( - index_expr, pointer_type(value_symbol.type.subtype())); + rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype())); } else { @@ -391,6 +393,8 @@ void goto_symext::symex_cpp_new( PRECONDITION(code.type().id() == ID_pointer); + const auto &pointer_type = to_pointer_type(code.type()); + do_array = (code.get(ID_statement) == ID_cpp_new_array || code.get(ID_statement) == ID_java_new_array_data); @@ -418,10 +422,10 @@ void goto_symext::symex_cpp_new( { exprt size_arg = static_cast(code.find(ID_size)); clean_expr(size_arg, state, false); - symbol.type = array_typet(code.type().subtype(), size_arg); + symbol.type = array_typet(pointer_type.subtype(), size_arg); } else - symbol.type=code.type().subtype(); + symbol.type = pointer_type.subtype(); symbol.type.set(ID_C_dynamic, true); @@ -429,8 +433,7 @@ void goto_symext::symex_cpp_new( // make symbol expression - exprt rhs(ID_address_of, code.type()); - rhs.type().subtype()=code.type().subtype(); + exprt rhs(ID_address_of, pointer_type); if(do_array) { diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index b7cc65310e9..01acd5faf53 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -321,8 +321,11 @@ void goto_symext::dereference_rec( exprt &object=address_of_expr.object(); const typet &expr_type=ns.follow(expr.type()); - expr=address_arithmetic(object, state, guard, - expr_type.subtype().id()==ID_array); + expr = address_arithmetic( + object, + state, + guard, + to_pointer_type(expr_type).subtype().id() == ID_array); } else if(expr.id()==ID_typecast) { diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 90a958b50d0..f46bc4b3598 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -72,7 +72,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value) } else if(type_id==ID_c_bit_field) { - const typet &subtype=type.subtype(); + const typet &subtype = to_c_bit_field_type(type).subtype(); if(subtype.id()==ID_signedbv) { int_value=binary2integer(id2string(value), true); diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 35ce2144dd1..035488a6690 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -116,7 +116,8 @@ exprt expr_initializert::expr_initializer_rec( result = side_effect_expr_nondett(type, source_location); else { - exprt sub_zero = expr_initializer_rec(type.subtype(), source_location); + exprt sub_zero = + expr_initializer_rec(to_complex_type(type).subtype(), source_location); result = complex_exprt(sub_zero, sub_zero, to_complex_type(type)); } diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index a240805db31..6efc7c41c77 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -124,7 +124,7 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest) src.id()!=ID_pointer) { if(src.has_subtype()) - find_symbols(kind, src.subtype(), dest); + find_symbols(kind, to_type_with_subtype(src).subtype(), dest); forall_subtypes(it, src) find_symbols(kind, *it, dest); diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp index 5ed08da63e2..c0f331a223f 100644 --- a/src/util/format_type.cpp +++ b/src/util/format_type.cpp @@ -60,14 +60,14 @@ std::ostream &format_rec(std::ostream &os, const typet &type) const auto &id = type.id(); if(id == ID_pointer) - return os << '*' << format(type.subtype()); + return os << '*' << format(to_pointer_type(type).subtype()); else if(id == ID_array) { const auto &t = to_array_type(type); if(t.is_complete()) - return os << format(type.subtype()) << '[' << format(t.size()) << ']'; + return os << format(t.subtype()) << '[' << format(t.size()) << ']'; else - return os << format(type.subtype()) << "[]"; + return os << format(t.subtype()) << "[]"; } else if(id == ID_struct) return format_rec(os, to_struct_type(type)); diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index 3043ad59ef4..528aa43d709 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -154,7 +154,10 @@ json_objectt json( else if(type.id()==ID_c_enum_tag) { // we return the base type - return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode); + return json( + to_c_enum_type(ns.follow_tag(to_c_enum_tag_type(type))).subtype(), + ns, + mode); } else if(type.id()==ID_fixedbv) { @@ -165,7 +168,7 @@ json_objectt json( else if(type.id()==ID_pointer) { result["name"]=json_stringt("pointer"); - result["subtype"]=json(type.subtype(), ns, mode); + result["subtype"] = json(to_pointer_type(type).subtype(), ns, mode); } else if(type.id()==ID_bool) { @@ -174,12 +177,12 @@ json_objectt json( else if(type.id()==ID_array) { result["name"]=json_stringt("array"); - result["subtype"]=json(type.subtype(), ns, mode); + result["subtype"] = json(to_array_type(type).subtype(), ns, mode); } else if(type.id()==ID_vector) { result["name"]=json_stringt("vector"); - result["subtype"]=json(type.subtype(), ns, mode); + result["subtype"] = json(to_vector_type(type).subtype(), ns, mode); result["size"]=json(to_vector_type(type).size(), ns, mode); } else if(type.id()==ID_struct) @@ -242,9 +245,8 @@ json_objectt json( lang=std::unique_ptr(get_default_language()); } - const typet &underlying_type= - type.id()==ID_c_bit_field?type.subtype(): - type; + const typet &underlying_type = + type.id() == ID_c_bit_field ? to_c_bit_field_type(type).subtype() : type; std::string type_string; bool error=lang->from_type(underlying_type, type_string, ns); @@ -270,7 +272,8 @@ json_objectt json( { result["name"]=json_stringt("integer"); result["binary"] = json_stringt(constant_expr.get_value()); - result["width"]=json_numbert(type.subtype().get_string(ID_width)); + result["width"] = + json_numbert(to_c_enum_type(type).subtype().get_string(ID_width)); result["type"]=json_stringt("enum"); result["data"]=json_stringt(value_string); } diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 61666197150..8c4b1886fc3 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -120,7 +120,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns) { if(type.id()==ID_array) { - auto sub = pointer_offset_bits(type.subtype(), ns); + auto sub = pointer_offset_bits(to_array_type(type).subtype(), ns); if(!sub.has_value()) return {}; @@ -137,7 +137,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns) } else if(type.id()==ID_vector) { - auto sub = pointer_offset_bits(type.subtype(), ns); + auto sub = pointer_offset_bits(to_vector_type(type).subtype(), ns); if(!sub.has_value()) return {}; @@ -154,7 +154,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns) } else if(type.id()==ID_complex) { - auto sub = pointer_offset_bits(type.subtype(), ns); + auto sub = pointer_offset_bits(to_complex_type(type).subtype(), ns); if(sub.has_value()) return (*sub) * 2; @@ -212,7 +212,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns) } else if(type.id()==ID_c_enum) { - return mp_integer(to_bitvector_type(type.subtype()).get_width()); + return mp_integer(to_bitvector_type(to_c_enum_type(type).subtype()).get_width()); } else if(type.id()==ID_c_enum_tag) { @@ -313,12 +313,14 @@ exprt size_of_expr( { if(type.id()==ID_array) { - exprt sub=size_of_expr(type.subtype(), ns); + const auto &array_type = to_array_type(type); + + exprt sub = size_of_expr(array_type.subtype(), ns); if(sub.is_nil()) return nil_exprt(); // get size - exprt size=to_array_type(type).size(); + exprt size = array_type.size(); if(size.is_nil()) return nil_exprt(); @@ -333,7 +335,7 @@ exprt size_of_expr( } else if(type.id()==ID_vector) { - exprt sub=size_of_expr(type.subtype(), ns); + exprt sub = size_of_expr(to_vector_type(type).subtype(), ns); if(sub.is_nil()) return nil_exprt(); @@ -353,7 +355,7 @@ exprt size_of_expr( } else if(type.id()==ID_complex) { - exprt sub=size_of_expr(type.subtype(), ns); + exprt sub = size_of_expr(to_complex_type(type).subtype(), ns); if(sub.is_nil()) return nil_exprt(); @@ -465,7 +467,8 @@ exprt size_of_expr( } else if(type.id()==ID_c_enum) { - std::size_t width=to_bitvector_type(type.subtype()).get_width(); + std::size_t width = + to_bitvector_type(to_c_enum_type(type).subtype()).get_width(); std::size_t bytes=width/8; if(bytes*8!=width) bytes++; @@ -529,15 +532,16 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns) else if(expr.id()==ID_index) { const index_exprt &index_expr=to_index_expr(expr); - const typet &array_type=ns.follow(index_expr.array().type()); DATA_INVARIANT( - array_type.id()==ID_array, - "index into array expected, found "+array_type.id_string()); + index_expr.array().type().id() == ID_array, + "index into array expected, found " + + index_expr.array().type().id_string()); auto o = compute_pointer_offset(index_expr.array(), ns); if(o.has_value()) { + const auto &array_type = to_array_type(index_expr.array().type()); auto sub_size = pointer_offset_size(array_type.subtype(), ns); mp_integer i; diff --git a/src/util/refined_string_type.h b/src/util/refined_string_type.h index bc597556b2d..349ac56d440 100644 --- a/src/util/refined_string_type.h +++ b/src/util/refined_string_type.h @@ -29,10 +29,10 @@ class refined_string_typet: public struct_typet refined_string_typet(const typet &index_type, const typet &char_type); // Type for the content (list of characters) of a string - const typet &get_content_type() const + const array_typet &get_content_type() const { PRECONDITION(components().size()==2); - return components()[1].type(); + return to_array_type(components()[1].type()); } const typet &get_char_type() const diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 4a06c1d03c7..5fd878f83aa 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -321,7 +321,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) (expr.op0().op0().is_constant() && to_constant_expr(expr.op0().op0()).get_value()==ID_NULL))) { - auto sub_size = pointer_offset_size(op_type.subtype(), ns); + auto sub_size = pointer_offset_size(to_pointer_type(op_type).subtype(), ns); if(sub_size.has_value()) { // void* @@ -393,7 +393,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) op_type.id()==ID_pointer && expr.op0().id()==ID_plus) { - const auto step = pointer_offset_size(op_type.subtype(), ns); + const auto step = pointer_offset_size(to_pointer_type(op_type).subtype(), ns); if(step.has_value() && *step != 0) { @@ -684,8 +684,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr) } else if(op_type_id==ID_c_enum_tag) // enum to int { - const typet &base_type= - ns.follow_tag(to_c_enum_tag_type(op_type)).subtype(); + const typet &base_type = + to_c_enum_type(ns.follow_tag(to_c_enum_tag_type(op_type))).subtype(); if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv) { // enum constants use the representation of their base type @@ -1504,7 +1504,7 @@ exprt simplify_exprt::bits2expr( } else if(type.id()==ID_c_enum) { - exprt val=bits2expr(bits, type.subtype(), little_endian); + exprt val = bits2expr(bits, to_c_enum_type(type).subtype(), little_endian); val.type()=type; return val; } @@ -1570,7 +1570,7 @@ exprt simplify_exprt::bits2expr( UNREACHABLE; std::size_t n_el=integer2size_t(size); - const auto el_size_opt = pointer_offset_bits(type.subtype(), ns); + const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns); CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0); const std::size_t el_size = integer2size_t(*el_size_opt); @@ -1581,7 +1581,7 @@ exprt simplify_exprt::bits2expr( for(std::size_t i=0; i