Skip to content

Commit

Permalink
Enums in functions
Browse files Browse the repository at this point in the history
  • Loading branch information
@h0nzZik
h0nzZik committed Apr 15, 2017
1 parent 51b1a12 commit 41bd465
Show file tree
Hide file tree
Showing 5 changed files with 78 additions and 4 deletions.
2 changes: 2 additions & 0 deletions semantics/common/configuration.k
View file
Expand Up @@ -106,6 +106,8 @@ module COMMON-CONFIGURATION
<max-offset> 0 </max-offset>
<max-align> 1 </max-align>
<access-specifier> .K </access-specifier>
// CId |-> EnumId
<cl-unscoped-enumerators> .Map </cl-unscoped-enumerators>
</class>
</classes>

Expand Down
2 changes: 2 additions & 0 deletions semantics/cpp14/language/translation/configuration.k
View file
Expand Up @@ -58,6 +58,8 @@ module C-CONFIGURATION
<types color="lightgray"> .Map </types>
<block-history> .List </block-history>
<this> .K </this>
// CId |-> EnumId
<bl-unscoped-enumerators> .Map </bl-unscoped-enumerators>
</block-control>

<template-deduction> .Map </template-deduction>
Expand Down
39 changes: 35 additions & 4 deletions semantics/cpp14/language/translation/decl/enum.k
View file
Expand Up @@ -37,6 +37,8 @@ module CPP-DECL-ENUM

syntax Scope ::= getEnumScope(EnumId) [function]
rule getEnumScope(enumId(N:Namespace :: _)) => namespaceScope(N)
rule getEnumScope(enumId(C:Class :: _)) => classScope(C)
rule getEnumScope(enumId(localQual(B:BlockScope) :: _)) => B

syntax KItem ::= addEnumToEnv(CId, CPPEnumType)
rule addEnumToEnv(X::CId, E::CPPEnumType) => #addEnumToEnv(X, getEnumScope(getEnumId(E)), E)
Expand All @@ -48,12 +50,29 @@ module CPP-DECL-ENUM
<ns-id> N </ns-id>
<ntypes> NT::Map => NT[X, Enum() <- E] </ntypes>

rule <k> #addEnumToEnv(X::CId, classScope(C::Class), E::CPPEnumType) => . ... </k>
<curr-tu> Tu::String </curr-tu>
<tu-id> Tu </tu-id>
<class-id> C </class-id>
<ctypes> NT::Map => NT[X, Enum() <- E] </ctypes>

rule <k> #addEnumToEnv(X::CId, blockScope(_, _, _), E::CPPEnumType) => . ... </k>
<curr-tu> Tu::String </curr-tu>
<tu-id> Tu </tu-id>
<types> NT::Map => NT[X, Enum() <- E] </types>


syntax KItem ::= enumContext(CId, CPPEnumType, List, fixed: Bool, ut: CPPIntegerType) [strict(2)]

rule enumContext(X::CId, E::CPPEnumType, Enumerators:List, Fixed::Bool, UT::CPPIntegerType)
=> newEnum(E, Fixed)
~> addEnumToEnv(X, E)
~> scope(enumScope(getEnumId(E)), declareEnumerators(E, 0, 0, 0, int, Enumerators, Fixed, true))
~> inEnumScope(E, declareEnumerators(E, 0, 0, 0, int, Enumerators, Fixed, true))

syntax KItem ::= inEnumScope(CPPEnumType, K)
rule <k> inEnumScope(E::CPPEnumType, K:K) => K ~> setScope(OldScope) ... </k>
<curr-scope> OldScope::Scope => enumScope(getEnumId(E)) </curr-scope>


// second param -underlying type
syntax KItem ::= newEnum(CPPEnumType, fixed: Bool)
Expand Down Expand Up @@ -153,20 +172,32 @@ module CPP-DECL-ENUM
<enum-id> E </enum-id>
<scoped> true </scoped>

rule <k> addEnumeratorToEnv(enumId(N::Namespace :: Enum(_)) #as EId::EnumId, X::CId) => addUnscopedEnumeratorToNamespace(X, EId, N) ...</k>
rule <k> addEnumeratorToEnv(enumId(E::Enum) #as EId::EnumId, X::CId) => addUnscopedEnumeratorToEnv(X, E) ...</k>
<curr-tu> Tu::String </curr-tu>
<tu-id> Tu </tu-id>
<enum-id> EId </enum-id>
<scoped> false </scoped>

syntax KItem ::= addUnscopedEnumeratorToNamespace(CId, EnumId, Namespace)
syntax KItem ::= addUnscopedEnumeratorToEnv(CId, Enum)

rule <k> addUnscopedEnumeratorToNamespace(X::CId, enumId(E::Enum), N::Namespace) => . ... </k>
rule <k> addUnscopedEnumeratorToEnv(X::CId, (N:Namespace :: _) #as E::Enum) => . ... </k>
<curr-tu> Tu::String </curr-tu>
<tu-id> Tu </tu-id>
<ns-id> N </ns-id>
<unscoped-enumerators> UE::Map (.Map => X |-> E ) </unscoped-enumerators>

rule <k> addUnscopedEnumeratorToEnv(X::CId, (C:Class :: _) #as E::Enum) => . ... </k>
<curr-tu> Tu::String </curr-tu>
<tu-id> Tu </tu-id>
<class-id> C </class-id>
<cl-unscoped-enumerators> UE::Map (.Map => X |-> E ) </cl-unscoped-enumerators>

rule <k> addUnscopedEnumeratorToEnv(X::CId, (localQual(_:BlockScope) :: _) #as E::Enum) => . ... </k>
<curr-tu> Tu::String </curr-tu>
<tu-id> Tu </tu-id>
<bl-unscoped-enumerators> UE::Map (.Map => X |-> E ) </bl-unscoped-enumerators>


// For unscoped enums without fixed type,
// compute their minimal and maximal value
// as well as their underlying type
Expand Down
8 changes: 8 additions & 0 deletions semantics/cpp14/language/translation/name.k
View file
Expand Up @@ -156,8 +156,13 @@ module CPP-TRANSLATION-NAME
orIfNotFound guardedFind(X, hasParentNamespace(N), nameLookupInFullNamespace(X, getParentNamespace(N), T, IsNNS))

// unqualified name lookup
rule <k> lookupNameInBlock(X::CId, NoTag(), false) => lookupEnumerator(X, E) ...</k>
<bl-unscoped-enumerators>... X |-> E::Enum ...</bl-unscoped-enumerators>

rule <k> lookupNameInBlock(X::CId, NoTag(), false) => cSet(S, NoNamespace() :: X, .K) ...</k>
<env>... X |-> S::Map ...</env>
<bl-unscoped-enumerators> UE::Map </bl-unscoped-enumerators>
requires notBool X in_keys(UE)

rule <k> lookupNameInBlock(X::CId, NoTag(), _) => T ...</k>
<types>... X |-> (_ |-> T::CPPType) ...</types>
Expand All @@ -168,8 +173,11 @@ module CPP-TRANSLATION-NAME
rule <k> lookupNameInBlock(X::CId, _, IsNNS:Bool) => notFound(X) ...</k>
<env> Env::Map </env>
<types> Types::Map </types>
<bl-unscoped-enumerators> UE::Map </bl-unscoped-enumerators>

requires (notBool X in_keys(Env) orBool IsNNS)
andBool notBool X in_keys(Types)
andBool notBool X in_keys(UE)

rule <k> lookupEnumerator(X::CId, E::Enum) => V ... </k>
<curr-scope> enumScope(enumId(E)) </curr-scope>
Expand Down
31 changes: 31 additions & 0 deletions tests/unit-pass/enum-in-block.C
View file
@@ -0,0 +1,31 @@
extern "C" void abort();
#define assert(e) if(!(e)) abort();

int foo()
{
enum E { A = 5 };
return (int)A;
}

int bar()
{
enum E { A = 7 };
{ int x = (int)E::A + 1;} // nested block
return (int)A + 1;
}

int main()
{
enum E { A = 4, B };
E e = A;
int x = (int)A;
assert(x == 4);

int y = foo();
assert(y == 5);

assert(bar() == 8);

x = (int)B;
assert(x == 5);
}

0 comments on commit 41bd465

Please sign in to comment.