various minor fixes for classes (#406)

includes: * fix an enormous ocaml warning * add explicit keyword and default keyword to parser * add a fix to properrly detect value initialization in parser * fail the kompile build if we have warnings * fix alignment and size of class types * fix a minor confluence error in conversion.k * add semantics for this keyword in expressions to translation semantics * add some types to support for extern "C" * support calling 2-arg main function * fixes for constructors * value initialization of classes and arrays * direct initialization and copy initialization from derived class of class type objects * refactoring of new code to support class types better * fix broken overloading cases involving resolveEmptyOverload * substantial improvement to implicit conversion sequences for overloading * return statement with no operand * fix broken code for overloading for arguments which are BraceInit * support computing value category of overloaded operators * add sqrt function to ocaml backend
kframework · Mar 17, 2017 · c95b335 · c95b335
1 parent 80b1724
commit c95b335
Show file tree

Hide file tree

Showing 36 changed files with 487 additions and 220 deletions.
diff --git a/cpp-parser/ClangKast.cc b/cpp-parser/ClangKast.cc
@@ -524,18 +524,6 @@ bool TraverseDecl(Decl *D) {
       }
     }
 
-    if (CXXConstructorDecl *Ctor = dyn_cast<CXXConstructorDecl>(D)) {
-      if (Ctor->isExplicitSpecified()) {
-        AddSpecifier("Explicit");
-      }
-    }
-
-    if (CXXConversionDecl *Conv = dyn_cast<CXXConversionDecl>(D)) {
-      if (Conv->isExplicitSpecified()) {
-        AddSpecifier("Explicit");
-      }
-    }
-
     AddStorageClass(D->getStorageClass());
     if (D->isInlineSpecified()) {
       AddSpecifier("Inline");
@@ -544,7 +532,7 @@ bool TraverseDecl(Decl *D) {
       AddSpecifier("Constexpr");
     }
 
-    if (D->isThisDeclarationADefinition()) {
+    if (D->isThisDeclarationADefinition() || D->isExplicitlyDefaulted()) {
       AddKApplyNode("FunctionDefinition", 5);
     } else {
       AddKApplyNode("FunctionDecl", 4);
@@ -575,6 +563,18 @@ bool TraverseDecl(Decl *D) {
           if (Method->isVirtual()) {
             AddKApplyNode("Virtual", 1);
           }
+
+          if (CXXConversionDecl *Conv = dyn_cast<CXXConversionDecl>(D)) {
+            if (Conv->isExplicitSpecified()) {
+              AddKApplyNode("Explicit", 1);
+            }
+          }
+
+          if (CXXConstructorDecl *Ctor = dyn_cast<CXXConstructorDecl>(D)) {
+            if (Ctor->isExplicitSpecified()) {
+              AddKApplyNode("Explicit", 1);
+            }
+          }
         } else {
           AddKApplyNode("StaticMethodPrototype", 1);
         }
@@ -607,6 +607,9 @@ bool TraverseDecl(Decl *D) {
       }
       TRY_TO(TraverseStmt(D->getBody()));
     }
+    if (D->isExplicitlyDefaulted()) {
+      AddKApplyNode("Defaulted", 0);
+    }
     return true;
   }
 
@@ -1851,8 +1854,7 @@ bool TraverseDecl(Decl *D) {
     return false;
   }
 
-  bool TraverseCXXConstructHelper(const char *klabel, QualType T, Expr **begin, Expr **end) {
-    AddKApplyNode(klabel, 2);
+  bool TraverseCXXConstructHelper(QualType T, Expr **begin, Expr **end) {
     TRY_TO(TraverseType(T));
     int i = 0;
     for (Expr **iter = begin; iter != end; ++iter) {
@@ -1866,24 +1868,30 @@ bool TraverseDecl(Decl *D) {
   }
 
   bool TraverseCXXUnresolvedConstructExpr(CXXUnresolvedConstructExpr *E) {
-    return TraverseCXXConstructHelper("UnresolvedConstructorCall", E->getTypeAsWritten(), E->arg_begin(), E->arg_end());
+    AddKApplyNode("UnresolvedConstructorCall", 2);
+    return TraverseCXXConstructHelper(E->getTypeAsWritten(), E->arg_begin(), E->arg_end());
   }
 
   bool TraverseCXXFunctionalCastExpr(CXXFunctionalCastExpr *E) {
     Expr *arg = E->getSubExprAsWritten();
-    return TraverseCXXConstructHelper("FunctionalCast", E->getTypeInfoAsWritten()->getType(), &arg, &arg+1);
+    AddKApplyNode("FunctionalCast", 2);
+    return TraverseCXXConstructHelper(E->getTypeInfoAsWritten()->getType(), &arg, &arg+1);
   }
 
   bool TraverseCXXScalarValueInitExpr(CXXScalarValueInitExpr *E) {
-    return TraverseCXXConstructHelper("FunctionalCast", E->getTypeSourceInfo()->getType(), 0, 0);
+    AddKApplyNode("FunctionalCast", 2);
+    return TraverseCXXConstructHelper(E->getTypeSourceInfo()->getType(), 0, 0);
   }
 
   bool TraverseCXXConstructExpr(CXXConstructExpr *E) {
-    return TraverseCXXConstructHelper("ConstructorCall", E->getType(), E->getArgs(), E->getArgs() + E->getNumArgs());
+    AddKApplyNode("ConstructorCall", 3);
+    VisitBool(E->requiresZeroInitialization());
+    return TraverseCXXConstructHelper(E->getType(), E->getArgs(), E->getArgs() + E->getNumArgs());
   }
 
   bool TraverseCXXTemporaryObjectExpr(CXXTemporaryObjectExpr *E) { 
-    return TraverseCXXConstructHelper("TemporaryObjectExpr", E->getTypeSourceInfo()->getType(), E->getArgs(), E->getArgs() + E->getNumArgs());
+    AddKApplyNode("TemporaryObjectExpr", 2);
+    return TraverseCXXConstructHelper(E->getTypeSourceInfo()->getType(), E->getArgs(), E->getArgs() + E->getNumArgs());
   }
 
   bool VisitUnaryExprOrTypeTraitExpr(UnaryExprOrTypeTraitExpr *E) {
@@ -1935,8 +1943,9 @@ bool TraverseDecl(Decl *D) {
   }
 
   bool TraverseCXXNewExpr(CXXNewExpr *E) {
-    AddKApplyNode("NewExpr", 4);
-    TRY_TO(TraverseTypeLoc(E->getAllocatedTypeSourceInfo()->getTypeLoc()));
+    AddKApplyNode("NewExpr", 5);
+    VisitBool(E->isGlobalNew());
+    TRY_TO(TraverseType(E->getAllocatedType()));
     if (E->isArray()) {
       TRY_TO(TraverseStmt(E->getArraySize()));
     } else {

diff --git a/semantics/Makefile b/semantics/Makefile
@@ -1,7 +1,7 @@
 export K_OPTS := -Xmx2048m -Xss32m
 KOMPILE = kompile -O2
 KDEP = kdep
-KOMPILE_DEFAULT_FLAGS=--backend ocaml --non-strict --exit-code "<result-value> _:Int </result-value>"
+KOMPILE_DEFAULT_FLAGS=--backend ocaml --non-strict --exit-code "<result-value> _:Int </result-value>" -w2e
 CPP_KOMPILE_FLAGS=--opaque-klabels c11/c11-translation.k
 EXECUTION_KOMPILE_FLAGS=--opaque-klabels cpp14/cpp14-translation.k --no-expand-macros
 KDEP_DEFAULT_FLAGS=

diff --git a/semantics/common/compat.k b/semantics/common/compat.k
@@ -51,6 +51,7 @@ module COMPAT-SYNTAX
      syntax Set ::= listToSet(List) [function]
 
      syntax Bool ::= some(Set, K) [function]
+                   | some(Map, K) [function]
 
      //TODO(liyi): might not need this later
      syntax KItem ::= "dotK"
@@ -333,6 +334,9 @@ module COMPAT
                andBool (K =/=K .K)
      rule some'(.K, .Set, _) => false
 
+     rule some(.Map, Lbl:K) => false
+     rule some(K1:K |-> K2:K M:Map, #klabel(Lbl:KLabel)) => Lbl(K1, K2) orBool some(M, #klabel(Lbl))
+
      //TODO(liyi): might not need this
      rule dotK => .K [structural]
      rule lookup(Key |-> Val:K _:Map, Key:K) => Val

diff --git a/semantics/cpp14/language/common/alignment.k b/semantics/cpp14/language/common/alignment.k
@@ -22,9 +22,9 @@ module CPP-ALIGNMENT
      rule getAlignas(T::CPPType, _) => byteAlignofType(T) [owise]
 
      syntax Int ::= byteAlignofType(CPPSimpleType) [klabel(byteAlignofSimpleTypeCpp), function]
-     rule byteAlignofType(T:CPPClassType) => byteAlignofClass(getClassInfo(T))
-     rule byteAlignofType(t(_, _, T::CPPSimpleType)) => byteAlignofType(T) [owise]
+     rule byteAlignofType(t(_, _, T::CPPSimpleType)) => byteAlignofType(T)
 
+     rule byteAlignofType(classType(C::Class)) => byteAlignofClass(getClassInfo(C))
      syntax Int ::= byteAlignofClass(ClassInfo) [function]
      rule byteAlignofClass(<class>... <max-align> A::Int </max-align> ...</class>)
           => A

diff --git a/semantics/cpp14/language/common/bitsize.k b/semantics/cpp14/language/common/bitsize.k
@@ -20,9 +20,9 @@ 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:CPPClassType) => byteSizeofClass(getClassInfo(T))
-     rule byteSizeofType(t(_, _, T::CPPSimpleType)) => byteSizeofType(T) [owise]
+     rule byteSizeofType(t(_, _, T::CPPSimpleType)) => byteSizeofType(T)
 
+     rule byteSizeofType(classType(C::Class)) => byteSizeofClass(getClassInfo(C))
      syntax Int ::= byteSizeofClass(ClassInfo) [function]
      rule byteSizeofClass(<class>... <max-offset> V::Int </max-offset> <max-align> A::Int </max-align> ...</class>)
           => maxInt(1, padTo(V,A) /Int cfg:bitsPerByte)

diff --git a/semantics/cpp14/language/common/class.k b/semantics/cpp14/language/common/class.k
@@ -11,8 +11,8 @@ module CPP-CLASS-SYNTAX
      syntax Expr ::= contrivedObject(CPPType)
      syntax ValResult ::= noObject()
      syntax CId ::= unnamedObject(Class)
-     syntax Expr ::= beginConstruction(LVal)
-     syntax Expr ::= endConstruction(LVal)
+     syntax Expr ::= beginConstruction(Expr) [strict]
+     syntax Expr ::= endConstruction(Expr) [strict]
 endmodule
 
 module CPP-CLASS

diff --git a/semantics/cpp14/language/common/conversion.k b/semantics/cpp14/language/common/conversion.k
@@ -278,7 +278,7 @@ module CPP-CONVERSION
      rule isNullPointerConstant(prv(_, _, _:CPPNullPtrTType)) => true
      rule isNullPointerConstant(pre(_, _, _:CPPNullPtrTType)) => true
      rule isNullPointerConstant(V::PRVal) => false
-          requires trace(V) =/=K noTrace
+          requires trace(V) =/=K noTrace [owise]
 
      rule isCompositePointerType(T::CPPType) => isCPPPointerType(T) orBool isCPPMemberPointerType(T) orBool isCPPNullPtrTType(T)
 

diff --git a/semantics/cpp14/language/common/dynamic.k b/semantics/cpp14/language/common/dynamic.k
@@ -78,8 +78,9 @@ module CPP-DYNAMIC-SYNTAX
      syntax PRValueCategory ::= "prvalue"
      syntax GLValueCategory ::= LValueCategory | XValueCategory
      syntax RValueCategory ::= XValueCategory | PRValueCategory
-     syntax ValueCategory ::= GLValueCategory | RValueCategory
+     syntax ValueCategory ::= GLValueCategory | RValueCategory | InitListCategory
      syntax KResult ::= ValueCategory
+     syntax InitListCategory ::= initListCat(List)
 
      syntax Expr ::= stripHold(Expr) [function, klabel(stripHoldCpp)]
 
@@ -144,6 +145,7 @@ module CPP-DYNAMIC-SYNTAX
 
      syntax QualId ::= Class "::" CId
      syntax QualId ::= mkQualId(NNSVal, CId) [function]
+     syntax NNSVal ::= getQual(QualId) [function]
      syntax CId ::= getId(QualId) [function]
 
      syntax NamespaceScope ::= namespaceScope(Namespace)
@@ -186,6 +188,7 @@ module CPP-DYNAMIC-SYNTAX
 
      syntax NotFoundNameRef ::= notFound(CId)
      syntax CandidateSet ::= NotFoundNameRef
+     syntax ResolvedExpr ::= NotFoundNameRef
      syntax NameRef ::= nsRef(Namespace) | NotFoundNameRef
                       | templateRef(QualId, CPPTypeExpr)
      syntax Val ::= NameRef
@@ -228,6 +231,8 @@ module CPP-DYNAMIC-SYNTAX
      syntax Val ::= ValResult
      syntax KResult ::= ValResult
 
+     syntax KItem ::= resolve(Expr)
+
 endmodule
 
 module CPP-DYNAMIC
@@ -461,5 +466,9 @@ module CPP-DYNAMIC
 
      rule getId(N:Namespace :: X::CId) => X
      rule getId(C:Class :: X::CId) => X
+     rule getQual(N:Namespace :: X::CId) => N
+     rule getQual(C:Class :: X::CId) => C
+
+     context resolve(HOLE:Expr) [result(ResolvedExpr), structural]
 
 endmodule
diff --git a/semantics/cpp14/language/common/expr/members.k b/semantics/cpp14/language/common/expr/members.k
@@ -17,6 +17,9 @@ module CPP-EXPR-MEMBERS
      imports SETTINGS-SYNTAX
      imports SYMLOC-SYNTAX
 
+     rule <k> This() => Obj ...</k>
+          <this> Obj::Expr </this>
+
      context HOLE:Expr . _ _
 
      rule LV:LVal . no-template (Name(C:Class, X::CId) #as N::Name)