Merge pull request #3018 from diffblue/merged_type

tautschnig · web-flow · commit fcff35b830d7 · 2018-09-24T07:22:14.000+01:00
introduce merged_typet
diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
@@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/invariant.h>
 
+#include "merged_type.h"
+
 void ansi_c_declaratort::build(irept &src)
 {
   typet *p=static_cast<typet *>(&src);
@@ -47,8 +49,8 @@ void ansi_c_declaratort::build(irept &src)
     else if(t.id()==ID_merged_type)
     {
       // we always walk down the _last_ member of a merged type
-      assert(!t.subtypes().empty());
-      p=&(t.subtypes().back());
+      auto &merged_type = to_merged_type(t);
+      p = &merged_type.last_type();
     }
     else
       p=&t.subtype();
@@ -105,8 +107,8 @@ typet ansi_c_declarationt::full_type(
     else if(p->id()==ID_merged_type)
     {
       // we always go down on the right-most subtype
-      assert(!p->subtypes().empty());
-      p=&(p->subtypes().back());
+      auto &merged_type = to_merged_type(*p);
+      p = &merged_type.last_type();
     }
     else
       UNREACHABLE;
diff --git a/src/ansi-c/merged_type.h b/src/ansi-c/merged_type.h
@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+Module: A type that holds a combination of types
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANSI_C_MERGED_TYPE_H
+#define CPROVER_ANSI_C_MERGED_TYPE_H
+
+#include <util/type.h>
+
+/// holds a combination of types
+class merged_typet : public type_with_subtypest
+{
+public:
+  merged_typet() : type_with_subtypest(ID_merged_type)
+  {
+  }
+
+  typet &last_type()
+  {
+    return subtypes().back();
+  }
+};
+
+/// conversion to merged_typet
+inline const merged_typet &to_merged_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_merged_type);
+  DATA_INVARIANT(
+    !static_cast<const type_with_subtypest &>(type).subtypes().empty(),
+    "merge_typet has at least one subtype");
+  return static_cast<const merged_typet &>(type);
+}
+
+/// conversion to merged_typet
+inline merged_typet &to_merged_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_merged_type);
+  DATA_INVARIANT(
+    !static_cast<const type_with_subtypest &>(type).subtypes().empty(),
+    "merge_typet has at least one subtype");
+  return static_cast<merged_typet &>(type);
+}
+
+#endif // CPROVER_ANSI_C_MERGED_TYPE_H
diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc
@@ -4,6 +4,8 @@
 #include <util/std_expr.h>
 #include <util/string2int.h>
 
+#include "merged_type.h"
+
 #define YYSTYPE unsigned
 #define YYSTYPE_IS_TRIVIAL 1
 
@@ -115,7 +117,7 @@ static void merge_types(irept &dest, irept &src)
   if(dest.id()!=ID_merged_type)
   {
     source_locationt location=static_cast<const exprt &>(dest).source_location();
-    typet new_type(ID_merged_type);
+    merged_typet new_type;
     new_type.move_to_subtypes((typet &)(dest));
     dest.swap(new_type);
     static_cast<exprt &>(dest).add_source_location()=location;
@@ -203,8 +205,8 @@ static void make_subtype(typet &dest, typet &src)
     if(p->id()==ID_merged_type)
     {
       // do last one
-      assert(!p->subtypes().empty());
-      sub=&(p->subtypes().back());
+      auto &merged_type = to_merged_type(*p);
+      sub = &merged_type.last_type();
     }
 
     if(sub->id()==ID_frontend_pointer ||
@@ -243,8 +245,8 @@ static void make_subtype(typet &dest, typet &src)
           }
           else if(p->id()==ID_merged_type)
           {
-            assert(!p->subtypes().empty());
-            p=&(p->subtypes().back());
+            auto &merged_type = to_merged_type(*p);
+            p=&merged_type.last_type();
           }
           else if(p->id()==irep_idt())
             assert(false);
diff --git a/src/cpp/cpp_declarator.cpp b/src/cpp/cpp_declarator.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_declarator.h"
 
+#include <ansi-c/merged_type.h>
+
 #include <ostream>
 #include <cassert>
 
@@ -44,8 +46,8 @@ typet cpp_declaratort::merge_type(const typet &declaration_type) const
     else if(t.id()==ID_merged_type)
     {
       // the chain continues with the last one
-      assert(!t.subtypes().empty());
-      p=&t.subtypes().back();
+      auto &merged_type = to_merged_type(t);
+      p = &merged_type.last_type();
     }
     else
     {
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
@@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/string_constant.h>
 
 #include <ansi-c/anonymous_member.h>
+#include <ansi-c/merged_type.h>
 
 #include "cpp_typecheck.h"
 #include "cpp_template_type.h"
@@ -1892,12 +1893,9 @@ void cpp_typecheck_resolvet::guess_template_args(
   else if(template_type.id()==ID_merged_type)
   {
     // look at subtypes
-    for(typet::subtypest::const_iterator
-        it=template_type.subtypes().begin();
-        it!=template_type.subtypes().end();
-        it++)
+    for(const auto &t : to_merged_type(template_type).subtypes())
     {
-      guess_template_args(*it, desired_type);
+      guess_template_args(t, desired_type);
     }
   }
   else if(is_reference(template_type) ||
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
@@ -14,13 +14,14 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <cassert>
 #include <map>
 
+#include <util/c_types.h>
 #include <util/expr.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 
 #include <ansi-c/ansi_c_y.tab.h>
-#include <util/c_types.h>
+#include <ansi-c/merged_type.h>
 
 #include "cpp_token_buffer.h"
 #include "cpp_member_spec.h"
@@ -401,8 +402,8 @@ class Parser // NOLINT(readability/identifiers)
     {
       if(p->id()==ID_merged_type)
       {
-        assert(!p->subtypes().empty());
-        p=&p->subtypes().back();
+        auto &merged_type = to_merged_type(*p);
+        p = &merged_type.last_type();
       }
       else
         p=&p->subtype();
@@ -470,7 +471,7 @@ void Parser::merge_types(const typet &src, typet &dest)
     if(dest.id()!=ID_merged_type)
     {
       source_locationt location=dest.source_location();
-      typet tmp(ID_merged_type);
+      merged_typet tmp;
       tmp.move_to_subtypes(dest);
       tmp.add_source_location()=location;
       dest=tmp;
@@ -481,7 +482,6 @@ void Parser::merge_types(const typet &src, typet &dest)
     // merged_types
     typet::subtypest &sub=dest.subtypes();
     sub.emplace(sub.begin(), src);
-    POSTCONDITION(!dest.subtypes().empty());
   }
 }
 
@@ -3344,8 +3344,8 @@ bool Parser::optPtrOperator(typet &ptrs)
   {
     if(it->id()==ID_merged_type)
     {
-      assert(!it->subtypes().empty());
-      it->subtypes().back().subtype().swap(ptrs);
+      auto &merged_type = to_merged_type(*it);
+      merged_type.last_type().subtype().swap(ptrs);
     }
     else
     {

Original file line number	Diff line number	Diff line change
`@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]`
`18`	`18`	`#include <util/std_types.h>`
`19`	`19`	`#include <util/invariant.h>`
`20`	`20`
	`21`	`+#include "merged_type.h"`
	`22`	`+`
`21`	`23`	`void ansi_c_declaratort::build(irept &src)`
`22`	`24`	`{`
`23`	`25`	`typet p=static_cast<typet >(&src);`
`@@ -47,8 +49,8 @@ void ansi_c_declaratort::build(irept &src)`
`47`	`49`	`else if(t.id()==ID_merged_type)`
`48`	`50`	`{`
`49`	`51`	`// we always walk down the _last_ member of a merged type`
`50`		`- assert(!t.subtypes().empty());`
`51`		`- p=&(t.subtypes().back());`
	`52`	`+ auto &merged_type = to_merged_type(t);`
	`53`	`+ p = &merged_type.last_type();`
`52`	`54`	`}`
`53`	`55`	`else`
`54`	`56`	`p=&t.subtype();`
`@@ -105,8 +107,8 @@ typet ansi_c_declarationt::full_type(`
`105`	`107`	`else if(p->id()==ID_merged_type)`
`106`	`108`	`{`
`107`	`109`	`// we always go down on the right-most subtype`
`108`		`- assert(!p->subtypes().empty());`
`109`		`- p=&(p->subtypes().back());`
	`110`	`+ auto &merged_type = to_merged_type(*p);`
	`111`	`+ p = &merged_type.last_type();`
`110`	`112`	`}`
`111`	`113`	`else`
`112`	`114`	`UNREACHABLE;`
Original file line number	Diff line number	Diff line change
`@@ -4,6 +4,8 @@`
`4`	`4`	`#include <util/std_expr.h>`
`5`	`5`	`#include <util/string2int.h>`
`6`	`6`
	`7`	`+#include "merged_type.h"`
	`8`	`+`
`7`	`9`	`#define YYSTYPE unsigned`
`8`	`10`	`#define YYSTYPE_IS_TRIVIAL 1`
`9`	`11`
`@@ -115,7 +117,7 @@ static void merge_types(irept &dest, irept &src)`
`115`	`117`	`if(dest.id()!=ID_merged_type)`
`116`	`118`	`{`
`117`	`119`	`source_locationt location=static_cast<const exprt &>(dest).source_location();`
`118`		`- typet new_type(ID_merged_type);`
	`120`	`+ merged_typet new_type;`
`119`	`121`	`new_type.move_to_subtypes((typet &)(dest));`
`120`	`122`	`dest.swap(new_type);`
`121`	`123`	`static_cast<exprt &>(dest).add_source_location()=location;`
`@@ -203,8 +205,8 @@ static void make_subtype(typet &dest, typet &src)`
`203`	`205`	`if(p->id()==ID_merged_type)`
`204`	`206`	`{`
`205`	`207`	`// do last one`
`206`		`- assert(!p->subtypes().empty());`
`207`		`- sub=&(p->subtypes().back());`
	`208`	`+ auto &merged_type = to_merged_type(*p);`
	`209`	`+ sub = &merged_type.last_type();`
`208`	`210`	`}`
`209`	`211`
`210`	`212`	`if(sub->id()==ID_frontend_pointer \|\|`
`@@ -243,8 +245,8 @@ static void make_subtype(typet &dest, typet &src)`
`243`	`245`	`}`
`244`	`246`	`else if(p->id()==ID_merged_type)`
`245`	`247`	`{`
`246`		`- assert(!p->subtypes().empty());`
`247`		`- p=&(p->subtypes().back());`
	`248`	`+ auto &merged_type = to_merged_type(*p);`
	`249`	`+ p=&merged_type.last_type();`
`248`	`250`	`}`
`249`	`251`	`else if(p->id()==irep_idt())`
`250`	`252`	`assert(false);`
Original file line number	Diff line number	Diff line change
`@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]`
`11`	`11`
`12`	`12`	`#include "cpp_declarator.h"`
`13`	`13`
	`14`	`+#include <ansi-c/merged_type.h>`
	`15`	`+`
`14`	`16`	`#include <ostream>`
`15`	`17`	`#include <cassert>`
`16`	`18`
`@@ -44,8 +46,8 @@ typet cpp_declaratort::merge_type(const typet &declaration_type) const`
`44`	`46`	`else if(t.id()==ID_merged_type)`
`45`	`47`	`{`
`46`	`48`	`// the chain continues with the last one`
`47`		`- assert(!t.subtypes().empty());`
`48`		`- p=&t.subtypes().back();`
	`49`	`+ auto &merged_type = to_merged_type(t);`
	`50`	`+ p = &merged_type.last_type();`
`49`	`51`	`}`
`50`	`52`	`else`
`51`	`53`	`{`
Original file line number	Diff line number	Diff line change
`@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]`
`26`	`26`	`#include <util/string_constant.h>`
`27`	`27`
`28`	`28`	`#include <ansi-c/anonymous_member.h>`
	`29`	`+#include <ansi-c/merged_type.h>`
`29`	`30`
`30`	`31`	`#include "cpp_typecheck.h"`
`31`	`32`	`#include "cpp_template_type.h"`
`@@ -1892,12 +1893,9 @@ void cpp_typecheck_resolvet::guess_template_args(`
`1892`	`1893`	`else if(template_type.id()==ID_merged_type)`
`1893`	`1894`	`{`
`1894`	`1895`	`// look at subtypes`
`1895`		`- for(typet::subtypest::const_iterator`
`1896`		`- it=template_type.subtypes().begin();`
`1897`		`- it!=template_type.subtypes().end();`
`1898`		`- it++)`
	`1896`	`+ for(const auto &t : to_merged_type(template_type).subtypes())`
`1899`	`1897`	`{`
`1900`		`- guess_template_args(*it, desired_type);`
	`1898`	`+ guess_template_args(t, desired_type);`
`1901`	`1899`	`}`
`1902`	`1900`	`}`
`1903`	`1901`	`else if(is_reference(template_type) \|\|`
Original file line number	Diff line number	Diff line change
`@@ -14,13 +14,14 @@ Author: Daniel Kroening, [email protected]`
`14`	`14`	`#include <cassert>`
`15`	`15`	`#include <map>`
`16`	`16`
	`17`	`+#include <util/c_types.h>`
`17`	`18`	`#include <util/expr.h>`
`18`	`19`	`#include <util/std_code.h>`
`19`	`20`	`#include <util/std_expr.h>`
`20`	`21`	`#include <util/std_types.h>`
`21`	`22`
`22`	`23`	`#include <ansi-c/ansi_c_y.tab.h>`
`23`		`-#include <util/c_types.h>`
	`24`	`+#include <ansi-c/merged_type.h>`
`24`	`25`
`25`	`26`	`#include "cpp_token_buffer.h"`
`26`	`27`	`#include "cpp_member_spec.h"`
`@@ -401,8 +402,8 @@ class Parser // NOLINT(readability/identifiers)`
`401`	`402`	`{`
`402`	`403`	`if(p->id()==ID_merged_type)`
`403`	`404`	`{`
`404`		`- assert(!p->subtypes().empty());`
`405`		`- p=&p->subtypes().back();`
	`405`	`+ auto &merged_type = to_merged_type(*p);`
	`406`	`+ p = &merged_type.last_type();`
`406`	`407`	`}`
`407`	`408`	`else`
`408`	`409`	`p=&p->subtype();`
`@@ -470,7 +471,7 @@ void Parser::merge_types(const typet &src, typet &dest)`
`470`	`471`	`if(dest.id()!=ID_merged_type)`
`471`	`472`	`{`
`472`	`473`	`source_locationt location=dest.source_location();`
`473`		`- typet tmp(ID_merged_type);`
	`474`	`+ merged_typet tmp;`
`474`	`475`	`tmp.move_to_subtypes(dest);`
`475`	`476`	`tmp.add_source_location()=location;`
`476`	`477`	`dest=tmp;`
`@@ -481,7 +482,6 @@ void Parser::merge_types(const typet &src, typet &dest)`
`481`	`482`	`// merged_types`
`482`	`483`	`typet::subtypest &sub=dest.subtypes();`
`483`	`484`	`sub.emplace(sub.begin(), src);`
`484`		`- POSTCONDITION(!dest.subtypes().empty());`
`485`	`485`	`}`
`486`	`486`	`}`
`487`	`487`
`@@ -3344,8 +3344,8 @@ bool Parser::optPtrOperator(typet &ptrs)`
`3344`	`3344`	`{`
`3345`	`3345`	`if(it->id()==ID_merged_type)`
`3346`	`3346`	`{`
`3347`		`- assert(!it->subtypes().empty());`
`3348`		`- it->subtypes().back().subtype().swap(ptrs);`
	`3347`	`+ auto &merged_type = to_merged_type(*it);`
	`3348`	`+ merged_type.last_type().subtype().swap(ptrs);`
`3349`	`3349`	`}`
`3350`	`3350`	`else`
`3351`	`3351`	`{`