add correct type conversion when using subtype() or subtypes()

Author: Daniel Kroening

src/analyses/goto_rw.cpp

@@ -594,8 +594,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());
   }
 }
 

src/cpp/cpp_template_type.h

@@ -50,15 +50,15 @@ inline const template_typet &to_template_type(const typet &type)
 inline const typet &template_subtype(const typet &type)
 {
   if(type.id()==ID_template)
-    return type.subtype();
+    return static_cast<const type_with_subtypet &>(type).subtype();
 
   return type;
 }
 
 inline typet &template_subtype(typet &type)
 {
   if(type.id()==ID_template)
-    return type.subtype();
+    return static_cast<type_with_subtypet &>(type).subtype();
 
   return type;
 }

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());
 }

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()),

src/goto-symex/goto_symex_state.cpp

@@ -220,7 +220,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;
 }
@@ -501,7 +501,7 @@ void goto_symex_statet::rename(
     DATA_INVARIANT(
       expr.type().id() == ID_pointer,
       "type of address_of should be ID_pointer");
-    expr.type().subtype()=expr.op0().type();
+    to_pointer_type(expr.type()).subtype() = expr.op0().type();
   }
   else
   {
@@ -737,7 +737,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);
@@ -822,8 +822,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 ||
@@ -844,7 +845,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)
   {
@@ -888,8 +889,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 ||
@@ -906,7 +908,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());
   }
 }
 

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
   {
@@ -194,11 +196,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
   {
@@ -400,6 +402,8 @@ void goto_symext::symex_cpp_new(
   if(code.type().id()!=ID_pointer)
     throw "new expected to return 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);
@@ -427,19 +431,18 @@ void goto_symext::symex_cpp_new(
   {
     exprt size_arg = static_cast<const exprt &>(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);
 
   state.symbol_table.add(symbol);
 
   // 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)
   {

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)
   {

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);

src/util/expr_initializer.cpp

@@ -112,7 +112,8 @@ exprt expr_initializert<nondet>::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));
     }
 

src/util/expr_util.cpp

@@ -181,7 +181,7 @@ bool has_subtype(
     }
     else
     {
-      for(const auto &subtype : top.subtypes())
+      for(const auto &subtype : to_type_with_subtypes(top).subtypes())
         push_if_not_visited(subtype);
     }
   }

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);

src/util/format_type.cpp

@@ -40,14 +40,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));

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<languaget>(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);
     }