Skip to content

Commit

Permalink
initial draft of some stuff relating to templates (#227)
Browse files Browse the repository at this point in the history 
* inline namespaces + a refactoring of the global cell

* add imports missing in rebase

* fix error reporting when sub-configuration has a parsing error

* initial draft of some stuff relating to templates

* fix bugs

* patch to make semantics compile faster

* fix tests that no longer have implicit error recovery
  • Loading branch information
@dwightguth
dwightguth committed Aug 12, 2016
1 parent da5dd06 commit ef547ba
Show file tree
Hide file tree
Showing 56 changed files with 1,420 additions and 548 deletions.
93 changes: 81 additions & 12 deletions cpp-parser/ClangKast.cc
View file
Expand Up @@ -393,7 +393,27 @@ class GetKASTVisitor
}
} else if (FTSI->getTemplateSpecializationKind() != TSK_Undeclared &&
FTSI->getTemplateSpecializationKind() != TSK_ImplicitInstantiation) {
doThrow("unimplemented: explicit template instantiation");
if (const ASTTemplateArgumentListInfo *TALI =
FTSI->TemplateArgumentsAsWritten) {
if (FTSI->getTemplateSpecializationKind() == TSK_ExplicitInstantiationDefinition) {
AddKApplyNode("TemplateInstantiationDefinition", 2);
} else {
AddKApplyNode("TemplateInstantiationDeclaration", 2);
}
AddKApplyNode("TemplateSpecializationType", 2);
TRY_TO(TraverseDeclarationName(FTSI->getTemplate()->getDeclName()));
AddKSequenceNode(TALI->NumTemplateArgs);
TRY_TO(TraverseTemplateArgumentLocs(TALI->getTemplateArgs(),
TALI->NumTemplateArgs));
} else {
if (FTSI->getTemplateSpecializationKind() == TSK_ExplicitInstantiationDefinition) {
AddKApplyNode("TemplateInstantiationDefinition", 2);
} else {
AddKApplyNode("TemplateInstantiationDeclaration", 2);
}
AddKApplyNode("TemplateSpecializationType", 1);
TRY_TO(TraverseDeclarationName(FTSI->getTemplate()->getDeclName()));
}
}
}

Expand Down Expand Up @@ -435,9 +455,9 @@ class GetKASTVisitor
}

if (D->isThisDeclarationADefinition()) {
AddKApplyNode("FunctionDefinition", 4);
AddKApplyNode("FunctionDefinition", 5);
} else {
AddKApplyNode("FunctionDecl", 3);
AddKApplyNode("FunctionDecl", 4);
}

TRY_TO(TraverseNestedNameSpecifierLoc(D->getQualifierLoc()));
Expand All @@ -449,6 +469,11 @@ class GetKASTVisitor
doThrow("something implicit in functions??");
}

AddKSequenceNode(D->parameters().size());
for (unsigned i = 0; i < D->parameters().size(); i++) {
TRY_TO(TraverseDecl(D->parameters()[i]));
}

if (D->isThisDeclarationADefinition()) {
TRY_TO(TraverseStmt(D->getBody()));
}
Expand Down Expand Up @@ -590,7 +615,7 @@ class GetKASTVisitor

#define TRAVERSE_TEMPLATE_DECL(DeclKind) \
bool Traverse##DeclKind##TemplateDecl(DeclKind##TemplateDecl *D) { \
AddKApplyNode("Template", 2); \
AddKApplyNode("TemplateWithInstantiations", 3); \
TRY_TO(TraverseDecl(D->getTemplatedDecl())); \
TemplateParameterList *TPL = D->getTemplateParameters(); \
if (TPL) { \
Expand All @@ -601,12 +626,56 @@ class GetKASTVisitor
TRY_TO(TraverseDecl(*I)); \
} \
} \
TRY_TO(TraverseTemplateInstantiations(D)); \
return true; \
}
TRAVERSE_TEMPLATE_DECL(Class)
TRAVERSE_TEMPLATE_DECL(Function)
TRAVERSE_TEMPLATE_DECL(TypeAlias)

bool TraverseTemplateInstantiations(ClassTemplateDecl *D) {
AddKSequenceNode(0);
return true;
}

bool TraverseTemplateInstantiations(TypeAliasTemplateDecl *D) {
AddKSequenceNode(0);
return true;
}

bool TraverseTemplateInstantiations(VarTemplateDecl *D) {
AddKSequenceNode(0);
return true;
}

//TODO(dwightguth): we need to fix this so that clang actually
// has an AST for function template instantiations, because
// the point of instantiation can have an effect on whether
// the instantiation is undefined or not.
bool TraverseTemplateInstantiations(FunctionTemplateDecl *D) {
unsigned i = 0;
for (auto *FD : D->specializations()) {
switch(FD->getTemplateSpecializationKind()) {
case TSK_ExplicitInstantiationDeclaration:
case TSK_ExplicitInstantiationDefinition:
i++;
default:
break;
}
}
AddKSequenceNode(i);
for (auto *FD : D->specializations()) {
switch(FD->getTemplateSpecializationKind()) {
case TSK_ExplicitInstantiationDeclaration:
case TSK_ExplicitInstantiationDefinition:
TRY_TO(TraverseDecl(FD));
default:
break;
}
}
return true;
}

bool TraverseTemplateTypeParmDecl(TemplateTypeParmDecl *D) {
AddKApplyNode("TypeTemplateParam", 4);
VisitBool(D->wasDeclaredWithTypename());
Expand Down Expand Up @@ -691,7 +760,6 @@ class GetKASTVisitor
bool TraverseTemplateName(TemplateName Name) {
switch(Name.getKind()) {
case TemplateName::Template:
AddKApplyNode("TemplateName", 1);
TRY_TO(TraverseDeclarationName(Name.getAsTemplateDecl()->getDeclName()));
break;
default:
Expand Down Expand Up @@ -799,8 +867,10 @@ class GetKASTVisitor
AddKApplyNode("TemplateSpecialization", 2);
break;
case TSK_ExplicitInstantiationDeclaration:
AddKApplyNode("TemplateInstantiationDeclaration", 2);
break;
case TSK_ExplicitInstantiationDefinition:
AddKApplyNode("TemplateInstantiation", 2);
AddKApplyNode("TemplateInstantiationDefinition", 2);
break;
default:
doThrow("unimplemented: implicit template instantiation");
Expand Down Expand Up @@ -1064,7 +1134,7 @@ class GetKASTVisitor
AddKApplyNode("QualifiedTypeName", 3);
VisitTypeKeyword(T->getKeyword());
if(!T->getQualifier()) {
AddKApplyNode("NoNamespace", 0);
AddKApplyNode("NoNNS", 0);
}
return false;
}
Expand All @@ -1080,16 +1150,15 @@ class GetKASTVisitor
return false;
}

bool VisitSubstTemplateTypeParmType(SubstTemplateTypeParmType *T) {
AddKApplyNode("TemplateParameterType", 1);
TRY_TO(TraverseIdentifierInfo(T->getReplacedParameter()->getIdentifier()));
return false;
bool TraverseSubstTemplateTypeParmType(SubstTemplateTypeParmType *T) {
TRY_TO(TraverseType(T->getReplacementType()));
return true;
}

bool VisitTagType(TagType *T) {
TagDecl *D = T->getDecl();
AddKApplyNode("Name", 2);
AddKApplyNode("NoNamespace", 0);
AddKApplyNode("NoNNS", 0);
TRY_TO(TraverseDeclarationName(D->getDeclName()));
return false;
}
Expand Down
7 changes: 4 additions & 3 deletions semantics/Makefile
View file
Expand Up @@ -3,6 +3,7 @@ KOMPILE = kompile -O2
KDEP = kdep
KOMPILE_DEFAULT_FLAGS=--backend ocaml --non-strict --exit-code "<result-value> _:Int </result-value>"
CPP_KOMPILE_FLAGS=--opaque-klabels c11/c11-translation.k
EXECUTION_KOMPILE_FLAGS=--opaque-klabels cpp14/cpp14-translation.k
KDEP_DEFAULT_FLAGS=

C11_TRANSLATION_FILES = $(wildcard *.k) \
Expand All @@ -28,15 +29,15 @@ $(PROFILE)/cpp14-translation-kompiled/cpp14-translation-kompiled/timestamp:

$(PROFILE)/c11-cpp14-kompiled/c11-cpp14-kompiled/timestamp:
@echo "Kompiling the dynamic C and C++ semantics..."
$(KOMPILE) $(KOMPILE_DEFAULT_FLAGS) --smt none c11-cpp14.k -d "$(PROFILE)/c11-cpp14-kompiled" --no-prelude -w all -v --transition "interpRule" --debug -I $(PROFILE_DIR)/semantics -I $(PROFILE_DIR)/cpp-semantics
$(KOMPILE) $(KOMPILE_DEFAULT_FLAGS) $(EXECUTION_KOMPILE_FLAGS) --smt none c11-cpp14.k -d "$(PROFILE)/c11-cpp14-kompiled" --no-prelude -w all -v --transition "interpRule" --debug -I $(PROFILE_DIR)/semantics -I $(PROFILE_DIR)/cpp-semantics

$(PROFILE)/c11-nd-kompiled/c11-nd-kompiled/timestamp:
@echo "Kompiling the dynamic C and C++ semantics with expression sequencing non-determinism..."
$(KOMPILE) $(KOMPILE_DEFAULT_FLAGS) --smt none c11-cpp14.k -d "$(PROFILE)/c11-nd-kompiled" --no-prelude --transition "observable ndtrans" --superheat "ndheat" --supercool "ndlocal" -I $(PROFILE_DIR)/semantics -I $(PROFILE_DIR)/cpp-semantics
$(KOMPILE) $(KOMPILE_DEFAULT_FLAGS) $(EXECUTION_KOMPILE_FLAGS) --smt none c11-cpp14.k -d "$(PROFILE)/c11-nd-kompiled" --no-prelude --transition "observable ndtrans" --superheat "ndheat" --supercool "ndlocal" -I $(PROFILE_DIR)/semantics -I $(PROFILE_DIR)/cpp-semantics

$(PROFILE)/c11-nd-thread-kompiled/c11-nd-thread-kompiled/timestamp:
@echo "Kompiling the dynamic C and C++ semantics with thread-interleaving non-determinism..."
$(KOMPILE) $(KOMPILE_DEFAULT_FLAGS) --smt none c11-cpp14.k -d "$(PROFILE)/c11-nd-thread-kompiled" --no-prelude --transition "observable ndtrans ndthread" -I $(PROFILE_DIR)/semantics -I $(PROFILE_DIR)/cpp-semantics
$(KOMPILE) $(KOMPILE_DEFAULT_FLAGS) $(EXECUTION_KOMPILE_FLAGS) --smt none c11-cpp14.k -d "$(PROFILE)/c11-nd-thread-kompiled" --no-prelude --transition "observable ndtrans ndthread" -I $(PROFILE_DIR)/semantics -I $(PROFILE_DIR)/cpp-semantics

all: fast nd thread

Expand Down
57 changes: 3 additions & 54 deletions semantics/c11/language/execution/configuration.k
View file
Expand Up @@ -5,65 +5,14 @@ module C-CONFIGURATION
imports MAP
imports SET
imports COMMON-INIT-SYNTAX
imports COMMON-CONFIGURATION
imports COMMON-SYNTAX
imports SYMLOC-SYNTAX
imports C-EXECUTION-INIT-SYNTAX
imports C-CONFIGURATION-EXTENSIONS

configuration
<global>
<mem> .Map </mem>
<functions color="lightgray"> .Map </functions>

<main-tu color="lightgray"> .Set </main-tu>

<global-state>
// CId |-> Types
<external-types> .Map </external-types>
// CId |-> Loc
<external-defs> .Map </external-defs>
// QualId |-> (Type |-> Loc)
<odr-defs> .Map </odr-defs>
// dummy link base |-> real base
<linkings> .Map </linkings>
</global-state>

// placeholder from translation semantics
<linking-state multiplicity="?"> .K </linking-state>

<structs color="lightgray"> .Map </structs>

<translation-units>
<tu multiplicity="*" type="Map">
<tu-id> "" </tu-id>
<genv color="lightgray"> .Map </genv>
<gtypes color="lightgray"> .Map </gtypes>

// kpair(CId, Scope) |-> kpair(SymBase, Type)
<local-statics> .Map </local-statics>

// placeholder from translation semantics
<tu-linking-state multiplicity="?"> .K </tu-linking-state>

<next-unnamed color="black"> 0 </next-unnamed>

<goto-map color="lightgray"> .Map </goto-map>

// TODO(chathhorn): remove.
<incomplete-tags> .Set </incomplete-tags>

// C++ stuff
<namespaces>
<ns multiplicity="*" type="Map">
<ns-id> GlobalNamespace() </ns-id>
<nenv> .Map </nenv>
<using-namespaces> .Set </using-namespaces>
<inline-namespaces> .Set </inline-namespaces>
</ns>
</namespaces>
</tu>
</translation-units>
</global>
<global/>
<result-value color="red"> 139:EffectiveValue </result-value>
<T>
<exec multiplicity="?">
Expand Down Expand Up @@ -211,7 +160,7 @@ module C-CONFIGURATION
<next-byte> .K </next-byte>
<buff> "" </buff>
<sending> .List </sending>
<done> ListItem("") </done>
<done> "" </done>
</file>
</files>
<input color="lightgray"> .List </input>
Expand Down
12 changes: 0 additions & 12 deletions semantics/c11/language/execution/error.k
View file
Expand Up @@ -43,13 +43,6 @@ module C-EXECUTION-ERROR
requires isErrorRecovery andBool notBool isCSV
andBool error(Msg, printStackTrace(L, Loc, S)) in Errors

rule <result-value> unknown(I:Int) => {I ~> #write(2, ErrorMsg("USP-CEER6", "Unspecified value returned from main function.", "Unspecified value or behavior.", "C11", "5.1.2.2.3:1") +String "\n")}:>Int </result-value>
requires notBool isCSV

rule <file-commands> openWriteThenClose(File::String, Line::String) => writeThenClose(#open(File, "wac"), Line) ...</file-commands>
rule <file-commands> writeThenClose(Fd::Int, Line::String) => #write(Fd, Line) ~> close(Fd) ...</file-commands>
rule <file-commands> close(Fd::Int) => #close(Fd) ...</file-commands>

rule <k> EXIT(Msg:String) => openWriteThenClose(Report, Msg +String ",\"" +String printStackTrace(L, Loc, S) +String "\"\r\n") ~> HALT ...</k>
<call-stack> L:List </call-stack>
<curr-program-loc> Loc:CabsLoc </curr-program-loc>
Expand All @@ -66,11 +59,6 @@ module C-EXECUTION-ERROR
rule stackSeparator(ListItem(_)) => ""
rule stackSeparator(_) => "\n" [owise]

rule <result-value> unknown(I:Int) => I </result-value>
<file-commands> .K => openWriteThenClose(Report, ErrorMsg("USP-CEER6", "Unspecified value returned from main function.", "Unspecified value or behavior.", "C11", "5.1.2.2.3:1") +String ",unknown\r\n") ...</file-commands>
<options>... SetItem(CSV(Report::String)) ...</options>
<status> terminated </status>

rule printStackTrace(L:List, UnknownCabsLoc, none)
=> printStackTrace(L, .K, .K)
rule printStackTrace(L:List, Loc:CabsLoc, fileScope)
Expand Down
12 changes: 10 additions & 2 deletions semantics/c11/language/execution/init.k
View file
Expand Up @@ -12,9 +12,11 @@ module C-EXECUTION-INIT
imports C-CONFIGURATION
imports K-EQUAL
imports STRING
imports BITS-SYNTAX
imports C-CHECK-LOC-SYNTAX
imports C-DYNAMIC-SYNTAX
imports C-ENV-SYNTAX
imports C-ERROR-SYNTAX
imports C-MEMORY-ALLOC-SYNTAX
imports C-MEMORY-WRITING-SYNTAX
imports C-SEQUENCE-POINT-SYNTAX
Expand Down Expand Up @@ -233,17 +235,23 @@ module C-EXECUTION-INIT
(<thread>...
// main's thread, not the global "thread"
<thread-id> 0 </thread-id>
<k> reval(V:RValue) </k>
<k> reval(tv(I:Int, _)) </k>
...</thread> => .Bag)
...</exec>
<status> _ => terminated </status>
<result-value> _ => {value(V)}:>CValue </result-value>
<result-value> _ => I </result-value>
<files>...
// Flush stdout.
<file-commands>... (.K => f-flush(1)) </file-commands>
...</files>
[ndtrans]

rule <thread>...
<thread-id> 0 </thread-id>
<k> (.K => UNSPEC("CEER6", "Unspecified value returned from main function.", "5.1.2.2.3:1"))
~> reval(tv(unknown(I:Int), _)) </k>
...</thread>

rule <k> L:CabsLoc => .K ...</k>
<curr-program-loc> _ => L </curr-program-loc>
[structural]
Expand Down

0 comments on commit ef547ba

Please sign in to comment.