introduce typedef_type in the C/C++ frontend

Author: Daniel Kroening

src/ansi-c/ansi_c_declaration.cpp

@@ -22,12 +22,12 @@ void ansi_c_declaratort::build(irept &src)
 {
   typet *p=static_cast<typet *>(&src);
 
-  // walk down subtype until we hit symbol_type or "abstract"
+  // walk down subtype until we hit typedef_type, symbol or "abstract"
   while(true)
   {
     typet &t=*p;
 
-    if(t.id() == ID_symbol_type || t.id() == ID_symbol)
+    if(t.id() == ID_typedef_type || t.id() == ID_symbol)
     {
       set_base_name(t.get(ID_C_base_name));
       add_source_location()=t.source_location();

src/ansi-c/c_typecheck_base.h

@@ -209,7 +209,8 @@ class c_typecheck_baset:
   virtual void typecheck_c_enum_type(typet &type);
   virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
   virtual void typecheck_code_type(code_typet &type);
-  virtual void typecheck_symbol_type(typet &type);
+  virtual void typecheck_symbol_type(symbol_typet &type);
+  virtual void typecheck_typedef_type(typet &type);
   virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
   virtual void typecheck_typeof_type(typet &type);
   virtual void typecheck_array_type(array_typet &type);

src/ansi-c/c_typecheck_type.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include "gcc_types.h"
 #include "padding.h"
 #include "type2name.h"
+#include "typedef_type.h"
 
 void c_typecheck_baset::typecheck_type(typet &type)
 {
@@ -89,7 +90,9 @@ void c_typecheck_baset::typecheck_type(typet &type)
   else if(type.id()==ID_typeof)
     typecheck_typeof_type(type);
   else if(type.id() == ID_symbol_type)
-    typecheck_symbol_type(type);
+    typecheck_symbol_type(to_symbol_type(type));
+  else if(type.id() == ID_typedef_type)
+    typecheck_typedef_type(type);
   else if(type.id()==ID_vector)
     typecheck_vector_type(to_vector_type(type));
   else if(type.id()==ID_custom_unsignedbv ||
@@ -1425,10 +1428,10 @@ void c_typecheck_baset::typecheck_typeof_type(typet &type)
   c_qualifiers.write(type);
 }
 
-void c_typecheck_baset::typecheck_symbol_type(typet &type)
+void c_typecheck_baset::typecheck_symbol_type(symbol_typet &type)
 {
-  const irep_idt &identifier=
-    to_symbol_type(type).get_identifier();
+  // we do some consistency checking only
+  const irep_idt &identifier=type.get_identifier();
 
   symbol_tablet::symbolst::const_iterator s_it=
     symbol_table.symbols.find(identifier);
@@ -1449,25 +1452,48 @@ void c_typecheck_baset::typecheck_symbol_type(typet &type)
     error() << "expected type symbol" << eom;
     throw 0;
   }
+}
 
-  if(symbol.is_macro)
-  {
-    // overwrite, but preserve (add) any qualifiers and other flags
+void c_typecheck_baset::typecheck_typedef_type(typet &type)
+{
+  const irep_idt &identifier=
+    to_typedef_type(type).get_identifier();
 
-    c_qualifierst c_qualifiers(type);
-    bool is_packed=type.get_bool(ID_C_packed);
-    irept alignment=type.find(ID_C_alignment);
+  symbol_tablet::symbolst::const_iterator s_it=
+    symbol_table.symbols.find(identifier);
 
-    c_qualifiers+=c_qualifierst(symbol.type);
-    type=symbol.type;
-    c_qualifiers.write(type);
+  if(s_it==symbol_table.symbols.end())
+  {
+    error().source_location=type.source_location();
+    error() << "typedef symbol `" << identifier << "' not found"
+            << eom;
+    throw 0;
+  }
 
-    if(is_packed)
-      type.set(ID_C_packed, true);
-    if(alignment.is_not_nil())
-      type.set(ID_C_alignment, alignment);
+  const symbolt &symbol=s_it->second;
+
+  if(!symbol.is_type)
+  {
+    error().source_location=type.source_location();
+    error() << "expected type symbol for typedef" << eom;
+    throw 0;
   }
 
+  // overwrite, but preserve (add) any qualifiers and other flags
+
+  c_qualifierst c_qualifiers(type);
+  bool is_packed=type.get_bool(ID_C_packed);
+  irept alignment=type.find(ID_C_alignment);
+
+  c_qualifiers+=c_qualifierst(symbol.type);
+  type=symbol.type;
+  c_qualifiers.write(type);
+
+  if(is_packed)
+    type.set(ID_C_packed, true);
+  if(alignment.is_not_nil())
+    type.set(ID_C_alignment, alignment);
+
   // CPROVER extensions
   if(symbol.base_name=="__CPROVER_rational")
   {

src/ansi-c/scanner.l

@@ -98,7 +98,7 @@ int make_identifier()
 
     if(result==ansi_c_id_classt::ANSI_C_TYPEDEF)
     {
-      stack(yyansi_clval).id(ID_symbol_type);
+      stack(yyansi_clval).id(ID_typedef_type);
       return TOK_TYPEDEFNAME;
     }
     else

src/ansi-c/typedef_type.h

@@ -0,0 +1,66 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANSI_C_TYPEDEF_TYPE_H
+#define CPROVER_ANSI_C_TYPEDEF_TYPE_H
+
+#include <util/type.h>
+
+/*! \brief A typedef
+*/
+class typedef_typet:public typet
+{
+public:
+  explicit typedef_typet(const irep_idt &identifier) : typet(ID_typedef_type)
+  {
+    set_identifier(identifier);
+  }
+
+  void set_identifier(const irep_idt &identifier)
+  {
+    set(ID_identifier, identifier);
+  }
+
+  const irep_idt &get_identifier() const
+  {
+    return get(ID_identifier);
+  }
+};
+
+/*! \brief Cast a generic typet to a \ref typedef_typet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * typedef_typet.
+ *
+ * \param type Source type
+ * \return Object of type \ref typedef_typet
+ *
+ * \ingroup gr_std_types
+*/
+inline const typedef_typet &to_typedef_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_typedef_type);
+  return static_cast<const typedef_typet &>(type);
+}
+
+/*! \copydoc to_typedef_type(const typet &)
+ * \ingroup gr_std_types
+*/
+inline typedef_typet &to_typedef_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_typedef_type);
+  return static_cast<typedef_typet &>(type);
+}
+
+template <>
+inline bool can_cast_type<typedef_typet>(const typet &type)
+{
+  return type.id() == ID_typedef_type;
+}
+
+#endif // CPROVER_ANSI_C_TYPEDEF_TYPE_H

src/util/irep_ids.def

@@ -245,6 +245,7 @@ IREP_ID_ONE(concatenation)
 IREP_ID_ONE(infinity)
 IREP_ID_ONE(return_type)
 IREP_ID_ONE(typedef)
+IREP_ID_ONE(typedef_type)
 IREP_ID_TWO(C_typedef, #typedef)
 IREP_ID_ONE(extern)
 IREP_ID_ONE(static)