Enums.

cpp-parser/ClangKast.cc

@@ -129,6 +129,9 @@ class GetKASTVisitor
   }
 
   bool TraverseStmt(Stmt *S) {
+    if (!S)
+      return RecursiveASTVisitor::TraverseStmt(S);
+
     if (Expr *E = dyn_cast<Expr>(S)) {
       AddKApplyNode("ExprLoc", 2);
       AddCabsLoc(E->getExprLoc());
@@ -988,19 +991,23 @@ bool TraverseDecl(Decl *D) {
   }
 
   bool TraverseEnumDecl(EnumDecl *D) {
-    if (D->isCompleteDefinition()) {
-      AddKApplyNode("EnumDef", 3);
-    } else {
-      AddKApplyNode("TypeDecl", 1);
-      AddKApplyNode("ElaboratedTypeSpecifier", 3);
-      VisitTagKind(D->getTagKind());
+    if (!D->isCompleteDefinition()) {
+      AddKApplyNode("OpaqueEnumDeclaration", 3);
+      TRY_TO(TraverseDeclarationName(D->getDeclName()));
+      VisitBool(D->isScoped());
+      TraverseType(D->getIntegerType());
+      return true;
     }
+
+    AddKApplyNode("EnumDef", 6);
     TRY_TO(TraverseDeclarationName(D->getDeclName()));
     TRY_TO(TraverseNestedNameSpecifierLoc(D->getQualifierLoc()));
-    if (D->isCompleteDefinition()) {
-      AddDeclContextNode(D);
-      TraverseDeclContextNode(D);
-    }
+    VisitBool(D->isScoped());
+    VisitBool(D->isFixed());
+    TraverseType(D->getIntegerType());
+
+    AddDeclContextNode(D);
+    TraverseDeclContextNode(D);
     return true;
   }
 

semantics/common/configuration.k

@@ -100,6 +100,16 @@ module COMMON-CONFIGURATION
                          <access-specifier> .K </access-specifier>
                     </class>
                </classes>
+
+               <cpp-enums>
+                    <cppenum multiplicity="*" type="Map">
+                         <enum-id> .K </enum-id>
+                         <enum-type> .K </enum-type>
+                         <scoped> false </scoped>
+                         <enumerators> .List </enumerators>
+                    </cppenum>
+               </cpp-enums>
+
           </tu>
      </translation-units>
    </global>

semantics/cpp14/language/common/alignment.k

@@ -54,6 +54,7 @@ module CPP-ALIGNMENT
      rule byteAlignofType(double) => cfg:alignofDouble
      rule byteAlignofType(long-double) => cfg:alignofLongDouble
      rule byteAlignofType(T:CPPSimpleWideCharType) => byteAlignofType(underlyingType(T))
+     rule byteAlignofType(T:CPPSimpleEnumType) => byteAlignofType(underlyingType(T))
      rule byteAlignofType(functionType(...)) => 0
      rule byteAlignofType(no-type) => cfg:alignofMalloc
 

semantics/cpp14/language/common/bitsize.k

@@ -20,6 +20,7 @@ module CPP-BITSIZE
           => N +Int ((A *Int cfg:bitsPerByte) -Int (N %Int (A *Int cfg:bitsPerByte))) [owise]
 
      syntax Int ::= byteSizeofType(CPPSimpleType) [klabel(byteSizeofSimpleTypeCpp), function]
+     rule byteSizeofType(T:CPPEnumType) => byteSizeofType(underlyingType(T))
      rule byteSizeofType(T:CPPClassType) => byteSizeofClass(getClassInfo(T))
      rule byteSizeofType(t(_, _, T::CPPSimpleType)) => byteSizeofType(T) [owise]
 

semantics/cpp14/language/common/dynamic.k

@@ -151,7 +151,8 @@ module CPP-DYNAMIC-SYNTAX
      syntax BlockScope ::= blockScope(QualId, SymBase, Int) [klabel(blockScopeCpp)]
      syntax TemplateParameterScope ::= "templateParameterScope"
      syntax FunctionPrototypeScope ::= "prototypeScope"
-     syntax Scope ::= NamespaceScope | ClassScope | BlockScope | TemplateParameterScope | FunctionPrototypeScope
+     syntax EnumScope ::= enumScope(Namespace, CId)
+     syntax Scope ::= NamespaceScope | ClassScope | BlockScope | TemplateParameterScope | FunctionPrototypeScope | EnumScope
 
      syntax Bool ::= inClassScope(Scope) [function]
      rule inClassScope(_:NamespaceScope) => false

semantics/cpp14/language/common/memory/reading.k

@@ -47,4 +47,8 @@ module CPP-MEMORY-READING
      rule interpret(prv(0, Tr::Trace, T:CPPNullPtrTType)) => prv(nullptrVal, Tr, T)
      rule interpret(prv(0, Tr::Trace, T:CPPPointerType)) => prv(NullPointer, Tr, T)
 
+     syntax PRVal ::= interpretEnum(PRVal, CPPEnumType)
+     rule interpret(prv(I:Int, Tr::Trace, T:CPPEnumType)) => interpretEnum(interpret(prv(I, Tr, underlyingType(T))), T)
+     rule interpretEnum(prv(I:Int, Tr::Trace, T:CPPIntegerType), E:CPPEnumType) => prv(I, Tr, E)
+
 endmodule

semantics/cpp14/language/common/typing.k

@@ -110,6 +110,11 @@ module CPP-TYPING-SYNTAX
                                 | "decltype(auto)"
      syntax CPPSimpleArrayTypeExpr ::= dynamicArrayType(CPPType, Expr)
 
+     syntax CPPSimpleScopedEnumType ::= scopedEnum(id: EnumId, underlyingType: CPPIntegerType)
+     syntax CPPSimpleUnscopedEnumType ::= unscopedEnum(id: EnumId, underlyingType: CPPIntegerType)
+     syntax CPPSimpleEnumType ::= CPPSimpleScopedEnumType | CPPSimpleUnscopedEnumType
+     syntax CPPSimpleCompoundType ::= CPPSimpleEnumType
+
      syntax CPPFunctionType ::= t(q: Quals, m: Set, st: CPPSimpleFunctionType) [klabel(tcpp)]
      syntax CPPArithmeticType ::= CPPIntegerType | CPPFloatingType
      syntax CPPScalarType ::= CPPArithmeticType | CPPEnumType | CPPPointerType | CPPMemberPointerType | CPPNullPtrTType
@@ -133,16 +138,19 @@ module CPP-TYPING-SYNTAX
      syntax CPPClassType ::= t(q: Quals, m: Set, st: CPPSimpleClassType) [klabel(tcpp)]
      syntax CPPWideCharType ::= t(q: Quals, m: Set, st: CPPSimpleWideCharType) [klabel(tcpp)]
      syntax CPPBitfieldType
+
      syntax CPPEnumType ::= CPPScopedEnumType | CPPUnscopedEnumType
-     syntax CPPScopedEnumType
-     syntax CPPUnscopedEnumType
+     syntax CPPScopedEnumType ::= t(q: Quals, m: Set, st: CPPSimpleScopedEnumType) [klabel(tcpp)]
+     syntax CPPUnscopedEnumType ::= t(q: Quals, m: Set, st: CPPSimpleUnscopedEnumType) [klabel(tcpp)]
+
      syntax CPPType ::= CPPFunctionType
                       | CPPScalarType
                       | CPPRefType
                       | CPPArrayType 
                       | CPPClassType 
                       | CPPFundamentalType
 
+
      syntax CPPFunctionTypeExpr ::= CPPFunctionType | t(q: Quals, m: Set, st: CPPSimpleFunctionTypeExpr) [klabel(tcpp)]
      syntax CPPClassTypeExpr ::= CPPClassType | t(q: Quals, m: Set, st: CPPSimpleClassTypeExpr) [klabel(tcpp)]
      syntax CPPArrayTypeExpr ::= CPPArrayType | t(q: Quals, m: Set, st: CPPSimpleArrayTypeExpr) [klabel(tcpp)]
@@ -226,6 +234,12 @@ module CPP-TYPING-SYNTAX
                    | isBaseClassOf(Class, Class) [function, klabel(isClassBaseClassOf)]
                    | hasVirtualMembers(CPPClassType) [function]
 
+     syntax EnumInfo ::= getEnumInfo(CPPEnumType) [function]
+                       | #getEnumInfo(EnumId, K) [function]
+     syntax EnumInfo ::= CppenumCell | "#incomplete"
+
+     syntax EnumId ::= enumId(QualId)
+
      syntax Bool ::= CPPType "==Type" CPPType [function]
                    | CPPType "=/=Type" CPPType [function]
 
@@ -237,6 +251,8 @@ module CPP-TYPING-SYNTAX
                    | isUnnamedXValue(CPPType) [function]
                    | isUnnamedPRValue(CPPType) [function]
 
+     syntax EnumId ::= getEnumId(CPPEnumType) [function]
+     syntax Bool ::= getScoped(CPPEnumType) [function]
 endmodule
 
 module CPP-TYPING
@@ -366,8 +382,14 @@ module CPP-TYPING
      rule #getClassInfo(t(_, _, classType(C::Class)), <generatedTop>... <class> <class-id> C </class-id> B::Bag </class> ...</generatedTop>) => <class> <class-id> C </class-id> B </class>
      rule #getClassInfo(_, _) => #incomplete [owise]
 
+     rule getEnumInfo(E::CPPEnumType) => #getEnumInfo(getEnumId(E), #configuration)
+
+     rule #getEnumInfo(X::EnumId, <generatedTop>... <cppenum> <enum-id> X </enum-id> B::Bag </cppenum> ...</generatedTop>) => <cppenum> <enum-id> X </enum-id> B </cppenum>
+     rule #getEnumInfo(_, _) => #incomplete [owise]
+
      rule isCompleteType(t(_, _, incompleteArrayType(_))) => false
-     rule isCompleteType(T:CPPEnumType) => false //TODO(dwightguth): true in certain cases
+     rule isCompleteType(T:CPPEnumType) => getEnumInfo(T) =/=K #incomplete //TODO(h0nzZik): false in 7.2, par 6
+
      rule isCompleteType(T:CPPClassType) => getClassInfo(T) =/=K #incomplete
      rule isCompleteType(T:CPPArrayType) => false
           requires notBool isCompleteType(innerType(T))
@@ -403,6 +425,9 @@ module CPP-TYPING
      rule noMethod ==Type methodInfo(... refQual: RQ::RefQualifier, cvQuals: Q::Quals) => RQ ==K RefNone() andBool Q ==K noQuals 
 
      rule t(Q::Quals, _, classType(N1::Namespace :: Class(T1::Tag, X1::CId, Ts1::TemplateArgs))) ==Type t(Q::Quals, _, classType(N2::Namespace :: Class(T2::Tag, X2::CId, Ts2::TemplateArgs))) => N1 ==K N2 andBool T1 ==K T2 andBool X1 ==K X2 andBool Ts1 ==Types Ts2
+     rule t(Q::Quals, _, scopedEnum(X::EnumId, _)) ==Type t(Q, _, scopedEnum(X::EnumId, _)) => true
+     rule t(Q::Quals, _, unscopedEnum(X::EnumId, _)) ==Type t(Q, _, unscopedEnum(X::EnumId, _)) => true
+
      syntax Bool ::= TemplateArgs "==Types" TemplateArgs [function]
      rule T1::CPPType, Ts1::TemplateArgs ==Types T2::CPPType, Ts2::TemplateArgs => T1 ==Type T2 andBool Ts1 ==Types Ts2
      rule .TemplateArgs ==Types .TemplateArgs => true
@@ -414,6 +439,9 @@ module CPP-TYPING
      rule underlyingType(T::CPPSimpleType) => T [owise]
      rule underlyingType(t(Q::Quals, Mods::Set, T::CPPSimpleType))
           => t(Q, Mods, underlyingType(T))
+     rule underlyingType(scopedEnum(_, T::CPPIntegerType)) => simpleType(T)
+     rule underlyingType(unscopedEnum(_, T::CPPIntegerType)) => simpleType(T)
+
 
      rule inRange(I:Int, T::CPPIntegerType)
           => I <=Int max(T) andBool I >=Int min(T)
@@ -488,6 +516,11 @@ module CPP-TYPING
      rule setType(T::CPPType, lv(Loc::SymLoc, Tr::Trace, _)) => lv(Loc, Tr, T)
      rule setType(T::CPPType, prv(Loc::SymLoc, Tr::Trace, _)) => prv(Loc, Tr, T)
 
+     rule getScoped(t(_, _, scopedEnum(_, _))) => true
+     rule getScoped(t(_, _, unscopedEnum(_, _))) => false
+     rule getEnumId(t(_, _, scopedEnum(X::EnumId, _))) => X
+     rule getEnumId(t(_, _, unscopedEnum(X::EnumId, _))) => X
+
 endmodule
 
 module C-CPP-TYPING

semantics/cpp14/language/translation/decl/class.k

@@ -36,7 +36,7 @@ module CPP-DECL-CLASS
              requires notBool isClassNameElabSpecifier(HOLE) [result(CPPTypeExpr)]
      context TypeDecl(HOLE:CPPTypeExpr)
              requires notBool isDependentInScope(HOLE)
-                  andBool notBool isClassNameElabSpecifier(HOLE) [resullt(CPPType)]
+                  andBool notBool isClassNameElabSpecifier(HOLE) [result(CPPType)]
 
      syntax Bool ::= isClassNameElabSpecifier(K) [function]
      rule isClassNameElabSpecifier(ElaboratedTypeSpecifier(_:ClassKey, _, NoNNS())) => true

semantics/cpp14/language/translation/decl/enum.k

@@ -0,0 +1,56 @@
+module CPP-DECL-ENUM-SYNTAX
+     imports BOOL-SYNTAX
+     imports LIST
+     imports COMMON-SORTS
+     imports CPP-SORTS
+     imports CPP-TYPING-SYNTAX
+endmodule
+
+module CPP-DECL-ENUM
+     imports CPP-DECL-ENUM-SYNTAX
+     imports C-CONFIGURATION
+     imports COMMON-SYNTAX
+     imports COMPAT-SYNTAX
+     imports CPP-ABSTRACT-SYNTAX
+     imports CPP-DYNAMIC-SYNTAX
+     imports CPP-ENV-SYNTAX
+     imports CPP-SYNTAX
+     imports CPP-BITSIZE-SYNTAX
+
+     syntax CPPEnumType ::= declareEnumName(ns: Namespace, id: CId, ut: CPPIntegerType, scoped: Bool) [function]
+     rule declareEnumName(N::Namespace, X::CId, UT::CPPIntegerType, false) => t(noQuals, .Set, unscopedEnum(enumId(N::Namespace :: X), UT))
+     rule declareEnumName(N::Namespace, X::CId, UT::CPPIntegerType, true)  => t(noQuals, .Set,   scopedEnum(enumId(N::Namespace :: X), UT))
+
+     syntax KItem ::= addToCurrentNamespace(CId, CPPEnumType)
+     rule <k> addToCurrentNamespace(X::CId, E::CPPEnumType) => . ... </k>
+          <curr-scope> namespaceScope(N::Namespace) </curr-scope>
+          <curr-tu> Tu::String </curr-tu>
+          <tu-id> Tu </tu-id>
+          <ns-id> N </ns-id>
+          <ntypes> NT::Map => NT[X, Enum() <- E] </ntypes>
+
+     // second param -underlying type
+     syntax KItem ::= newEnum(CPPEnumType)
+
+     rule <k> newEnum(E:CPPEnumType) => . ... </k>
+          <curr-tu> Tu::String </curr-tu>
+          <tu-id> Tu </tu-id>
+          (.Bag => <cppenum>...
+               <enum-id> getEnumId(E) </enum-id>
+               <enum-type> E </enum-type>
+               <scoped> getScoped(E) </scoped>
+           ...</cppenum>)
+
+     syntax KItem ::= enumContext(CId, CPPEnumType) [strict(2)]
+
+     // We do not support enumerators yet
+     rule <k> EnumDef(X::CId, NoNNS(), Scoped::Bool, Fixed::Bool, UT::CPPIntegerType, .List)
+          => enumContext(X, declareEnumName(N, X, UT, Scoped)) ...</k>
+          <curr-scope> namespaceScope(N::Namespace) </curr-scope>
+          <curr-tu> Tu::String </curr-tu>
+          <tu-id> Tu </tu-id>
+
+     rule enumContext(X::CId, E::CPPEnumType) => newEnum(E) ~> addToCurrentNamespace(X, E)
+
+endmodule
+

semantics/cpp14/language/translation/syntax.k

@@ -16,6 +16,8 @@ module CPP-ABSTRACT-SYNTAX
      imports CPP-DEPENDENT-SYNTAX
      imports CPP-CLASS-SYNTAX
 
+     syntax CPPIntegerType
+
      syntax LVal ::= LExpr
      syntax XVal ::= XExpr
      syntax PRVal ::= PRExpr
@@ -82,7 +84,8 @@ module CPP-ABSTRACT-SYNTAX
 
      syntax Decl ::= ClassDef(Tag, CId, NNS, List, List)
                    | TypeDecl(AType)
-                   | EnumDef(CId, NNS, List)
+                   | EnumDef(id: CId, nns: NNS, scoped: Bool, fixed: Bool, ut: AType, List) [strict(5)]
+                   | OpaqueEnumDeclaration(id: CId, scoped: Bool, ut: AType)
                    | AccessSpec(AccessSpecifier)
                    | StaticAssert(Expr, Expr)
                    | UsingDecl(Bool, NNS, CId)

semantics/cpp14/language/translation/translation.k

@@ -16,6 +16,7 @@ require "configuration.k"
 
 require "decl/class.k"
 require "decl/declarator.k"
+require "decl/enum.k"
 require "decl/initializer.k"
 require "decl/linkage.k"
 require "decl/namespace.k"
@@ -75,6 +76,7 @@ module CPP-TRANSLATION
      imports CPP-VALUE-CATEGORY
 
      imports CPP-DECL-CLASS
+     imports CPP-DECL-ENUM
      imports CPP-DECL-DECLARATOR
      imports CPP-DECL-INITIALIZER
      imports CPP-DECL-LINKAGE

tests/unit-pass/enum-empty.C

@@ -0,0 +1,13 @@
+extern "C" void abort();
+
+enum E : int {};
+
+E e;
+
+int main() {
+	E f = e;
+	E * g = nullptr;
+
+	if (sizeof(e) != sizeof(int))
+		abort();
+}