miscellaneous fixes for Boeing demo (#409)

* miscellaneous fixes for Boeing demo includes: * k++ wrapper script which includes libstdc++ * fixes for value category conversions * unify QualId between Namespace and Class * improved error reporting of types * calling std::terminate * fixes for implicit object parameter conversion * calling via a function pointer * fix a bug where asignment expressions were being evaluated at translation * incomplete draft of destructor functionality * variadic arguments to functions * noexcept exception specification * a few other very minor fixes to stuck configurations * fix test failures * minor test fixes * fix broken test
kframework · Mar 29, 2017 · 8c2641b · 8c2641b
1 parent 095c475
commit 8c2641b
Show file tree

Hide file tree

Showing 50 changed files with 410 additions and 258 deletions.
diff --git a/Makefile b/Makefile
@@ -14,6 +14,7 @@ FAIL_COMPILE_TESTS_DIR = tests/unit-fail-compilation
 
 FILES_TO_DIST = \
 	$(SCRIPTS_DIR)/kcc \
+	$(SCRIPTS_DIR)/k++ \
 	$(SCRIPTS_DIR)/kranlib \
 	$(SCRIPTS_DIR)/ignored-flags \
 	$(SCRIPTS_DIR)/program-runner \
@@ -27,7 +28,7 @@ FILES_TO_DIST = \
 
 default: test-build
 
-fast: $(DIST_DIR)/$(PROFILE)/lib/libc.so $(DIST_DIR)/$(PROFILE)/c11-cpp14-kompiled/c11-cpp14-kompiled/timestamp
+fast: $(DIST_DIR)/$(PROFILE)/lib/libc.so $(DIST_DIR)/$(PROFILE)/lib/libstdc++.so $(DIST_DIR)/$(PROFILE)/c11-cpp14-kompiled/c11-cpp14-kompiled/timestamp
 
 check-vars:
 	@if ! ocaml -version > /dev/null 2>&1; then echo "ERROR: You don't seem to have ocaml installed.  You need to install this before continuing.  Please see INSTALL.md for more information."; false; fi
@@ -45,6 +46,7 @@ $(DIST_DIR)/kcc: $(FILES_TO_DIST) $(wildcard $(PROFILE_DIR)/include/*) $(PROFILE
 	@-cp -Lp $(PROFILE_DIR)/cpp-pp $(DIST_DIR)/$(PROFILE)
 	@cp -RLp $(PROFILE_DIR)/include $(DIST_DIR)/$(PROFILE)
 	@cp -RLp $(PROFILE_DIR)/src $(DIST_DIR)/$(PROFILE)
+	@cp -RLp $(PROFILE_DIR)/compiler-src $(DIST_DIR)/$(PROFILE)
 	@cp -RLp $(FILES_TO_DIST) $(DIST_DIR)
 	@cp -p $(SCRIPTS_DIR)/kcc $(DIST_DIR)/kclang
 
@@ -65,8 +67,13 @@ $(DIST_DIR)/$(PROFILE)/c11-nd-kompiled/c11-nd-kompiled/timestamp: semantics
 $(DIST_DIR)/$(PROFILE)/c11-nd-thread-kompiled/c11-nd-thread-kompiled/timestamp: semantics
 	@cp -RL $(SEMANTICS_DIR)/$(PROFILE)/c11-nd-thread-kompiled $(DIST_DIR)/$(PROFILE)
 
+$(DIST_DIR)/$(PROFILE)/lib/libstdc++.so: $(DIST_DIR)/$(PROFILE)/cpp14-translation-kompiled/cpp14-translation-kompiled/timestamp $(wildcard $(PROFILE_DIR)/compiler-src/*.C) $(DIST_DIR)/kcc
+	@echo "Translating the C++ standard library... ($(PROFILE_DIR))"
+	cd $(PROFILE_DIR)/compiler-src && $(shell pwd)/$(DIST_DIR)/kcc -nodefaultlibs -Xbuiltins -shared -o $(shell pwd)/$(DIST_DIR)/$(PROFILE)/lib/libstdc++.so *.C $(KCCFLAGS) -I .
+	@echo "Done."
+
 $(DIST_DIR)/$(PROFILE)/lib/libc.so: $(DIST_DIR)/$(PROFILE)/cpp14-translation-kompiled/cpp14-translation-kompiled/timestamp $(DIST_DIR)/$(PROFILE)/c11-translation-kompiled/c11-translation-kompiled/timestamp $(wildcard $(PROFILE_DIR)/src/*.c) $(DIST_DIR)/kcc
-	@echo "Translating the standard library... ($(PROFILE_DIR))"
+	@echo "Translating the C standard library... ($(PROFILE_DIR))"
 	cd $(PROFILE_DIR)/src && $(shell pwd)/$(DIST_DIR)/kcc -nodefaultlibs -Xbuiltins -shared -o $(shell pwd)/$(DIST_DIR)/$(PROFILE)/lib/libc.so *.c $(KCCFLAGS) -I .
 	@echo "Done."
 

diff --git a/cpp-parser/ClangKast.cc b/cpp-parser/ClangKast.cc
@@ -437,7 +437,7 @@ bool TraverseDecl(Decl *D) {
       }
     case DeclarationName::CXXDestructorName:
       {
-        AddKApplyNode("DestructorId", 1);
+        AddKApplyNode("DestructorTypeId", 1);
         TRY_TO(TraverseType(Name.getCXXNameType()));
         return true;
       }
@@ -560,7 +560,7 @@ bool TraverseDecl(Decl *D) {
             break;
           }
           AddKApplyNode("MethodPrototype", 4);
-          VisitBool(true);
+          VisitBool(Method->isUserProvided());
           VisitBool(dyn_cast<CXXConstructorDecl>(D)); // converts to true if this is a constructor
           TRY_TO(TraverseType(Method->getThisType(*Context)));
           if (Method->isVirtual()) {

diff --git a/scripts/k++ b/scripts/k++
@@ -0,0 +1,3 @@
+#!/bin/sh
+export KCC_COMMAND_NAME=`basename "$0"`
+"$(dirname "$0")/kcc" "$@" -Xk++
diff --git a/scripts/kcc b/scripts/kcc
@@ -33,6 +33,8 @@ my $MAGIC = "\x7fKAST";
 my $distDirectory = dirname(rel2abs($0));
 if (defined $ENV{KCC_COMMAND_NAME}) {
   $0 = $ENV{KCC_COMMAND_NAME};
+} else {
+  $0 = basename($0);
 }
 
 our $profile;
@@ -283,7 +285,7 @@ my $spec = q(
   -fmessage-length=0	Write all error messages on a single line.
   -frunner-script	Compile program to perl script with analysis tool options. [undocumented]
   -fissue-report=<file>	Write issues to the specified file in CSV format.
-  -fworkspace=<dir>	Use <dir> for the workspace of kcc when reporting
+  -fworkspace=<dir>	Use <dir> for the workspace of ) . $0 . q( when reporting
 			errors.
   -Wlint		Generate lint errors for potentially undesirable
 			behaviors.*
@@ -388,13 +390,13 @@ my $spec = q(
                         Setting the environment error KCC_NO_LICENCE_MESSAGE
                         has the same effect.
   -Xbuiltins		[undocumented]
+  -Xk++			[undocumented]
   -soname <name>	[undocumented]
 
   * Indicates flags that require RV-Match from
     http://www.runtimeverification.com/match to run.
 
-  For a complete list of other flags ignored by kcc, refer to ) 
-  . "\n  $distDirectory" . q(/ignored-flags,
+  For a complete list of other flags ignored by ) . "$0, refer to\n  $distDirectory" . q(/ignored-flags,
   which contains one regular expression per line.
 
   The following lines of output are added to this message for compatibility
@@ -411,6 +413,11 @@ exit main();
 
 sub main {
   @originalArgv = @ARGV;
+  if ($originalArgv[-1] eq '-Xk++') {
+    # special case for k++ wrapper script which we don't want
+    # to display as an argument
+    pop(@originalArgv);
+  }
   $args->parse() or error("Failed to parse the command line.\n");
 
   my $noLicense = exists($args->{'--no-license-message'})
@@ -509,9 +516,12 @@ sub main {
     return 0;
   }
 
-  if (!$args->{'-s'}) {
+  if (!$args->{'-nodefaultlibs'}) {
     $xLang = "none";
     classify(catfile($profileDirectory, 'lib', 'libc.so'));
+    if ($args->{'-Xk++'}) {
+      classify(catfile($profileDirectory, 'lib', 'libstdc++.so'));
+    }
   }
 
   # Reduce our remaining source files to object files
@@ -815,7 +825,7 @@ sub getKRunCommand {
     push(@krun_args, '--debug');
   }
   my @options = initOptions();
-  if ($lang ne 'c++' && !$hasBuiltins && $args->{'-Xbuiltins'}) {
+  if (!$hasBuiltins && $args->{'-Xbuiltins'}) {
     push(@options, "`XBuiltins`(.KList)");
     $hasBuiltins = 1;
   }
@@ -973,7 +983,7 @@ sub checkError {
       print STDERR "Translation failed (config dumped). Refer to last command run for details.\n";
       exit $retval;
     } else {
-      print STDERR "Translation failed (config dumped). Run kcc -d @originalArgv to see commands run.\n";
+      print STDERR "Translation failed (config dumped). Run $0 -d @originalArgv to see commands run.\n";
       exit $retval;
     }
   }

diff --git a/semantics/c11/language/execution/init.k b/semantics/c11/language/execution/init.k
@@ -25,6 +25,7 @@ module C-EXECUTION-INIT
      imports K-IO
      imports LIBC-BUILTIN-SYNTAX
      imports LIBC-IO-SYNTAX
+     imports LIBCPP-BOOTSTRAP-SYNTAX
      imports STRING
 
      syntax TCell ::= ".TCell" [klabel(.TCell)]
@@ -125,6 +126,7 @@ module C-EXECUTION-INIT
                <thread>...
                     <k> initMainThread'(MainTU:String)
                          => initBuiltins
+                         ~> initCPPBuiltins
                          ~> populateFromGlobal(.K)
                     ...</k>
                     <duration> _ => auto(0) </duration>

diff --git a/semantics/c11/library/builtin.k b/semantics/c11/library/builtin.k
@@ -134,7 +134,7 @@ module LIBC-BUILTIN
 
      rule initBuiltins => initStdio
 
-     syntax KItem ::= "initStdio" [function]
+     syntax K ::= "initStdio" [function]
      rule initStdio
           => alloc(bnew(!Stdin:Int, file, stdio), file, byteSizeofType(file))
           ~> allowInit(Computation(fileLVal(bnew(!Stdin, file, stdio)) := stdin))

diff --git a/semantics/common/compat.k b/semantics/common/compat.k
@@ -15,7 +15,6 @@ module COMPAT-SYNTAX
      syntax String ::= listToString(List) [function]
 
      syntax String ::= idToString(CId) [function]
-                     | idToString(QualId) [function, klabel(qualIdToString)]
 
      syntax String ::= toUpperCase(String) [function]
 
@@ -95,85 +94,6 @@ module COMPAT
      rule idToString(unnamed(_, _)) => "<anonymous>"
      rule idToString(_::CId) => "<unknown>" [owise]
 
-     rule idToString(GlobalNamespace() :: X::CId)
-          => "::" +String idToString(X)
-
-     rule [firstChar]:
-          firstChar(S:String) => substrString(S, 0, 1)
-
-     rule [nthChar]:
-          nthChar(S:String, N:Int) => substrString(S, N, N +Int 1)
-
-     rule [butFirstChar]:
-          butFirstChar(S:String)
-          => substrString(S:String, 1, lengthString(S:String))
-
-     rule all(ListItem(K:K) L:List, #klabel(Lbl:KLabel))
-          => Lbl(K:K) andBool all(L, #klabel(Lbl))
-     rule all(.List, _) => true
-
-     rule some(ListItem(K:K) L:List, #klabel(Lbl:KLabel))
-          => Lbl(K:K) orBool some(L, #klabel(Lbl))
-     rule some(.List, _) => false
-
-     rule toUpperCase(S:String)
-          => toUpperCase(firstChar(S:String))
-               +String toUpperCase(butFirstChar(S:String))
-          requires lengthString(S) >Int 1
-
-     rule toUpperCase(C:String)
-          => C:String
-          requires (lengthString(C) ==Int 1)
-               andBool (ordChar(C) <Int ordChar("a")
-                    orBool ordChar(C) >Int ordChar("z"))
-     rule toUpperCase(C:String)
-          => chrChar(absInt(ordChar(C)
-               -Int (ordChar("a") -Int ordChar("A"))))
-          requires (lengthString(C) ==Int 1)
-               andBool (ordChar(C) >=Int ordChar("a")
-                    andBool ordChar(C) <=Int ordChar("z"))
-
-     rule removeListItem(.List, _) => .List
-     rule removeListItem(ListItem(A:K) M:List, A) => M
-     rule removeListItem(ListItem(A:K) M:List, A':K)
-          => ListItem(A) removeListItem(M, A')
-          requires A =/=K A'
-
-     syntax Bool ::= subset(K, Set, Set) [function]
-
-     rule subset(K:K, S1:Set, S2:Set) => S1 <=Set (S2 -Set SetItem(K))
-          requires K in S2
-     rule subset(K:K, _, S2:Set) => false
-          requires notBool (K in S2)
-
-     syntax Map ::= removeBagItemFromMap(Map, K) [function]
-     rule removeBagItemFromMap(K |-> 1 M::Map, K:K) => M
-     rule removeBagItemFromMap(K |-> I::Int M::Map, K:K) => K |-> (I -Int 1) M
-
-     syntax KItem ::= "seqstrict()"
-     rule seqstrict(list(HOLE:List)) => toSSList(HOLE) ~> seqstrict() [heat]
-     rule HOLE:SSList ~> seqstrict() => seqstrict(krlist(ofSSList(HOLE))) [cool]
-
-     syntax SSList ::= K "seqstrict::" SSList [seqstrict]
-                     | ".SSList"
-     rule isKResult(.SSList) => true
-     rule isKResult(S1::SSList seqstrict:: S2::SSList) => isKResult(S1) andBool isKResult(S2)
-     rule toSSList(ListItem(K:K) L::List) => K seqstrict:: toSSList(L)
-     rule toSSList(.List) => .SSList
-     rule ofSSList(krlist(L1::List) seqstrict:: L2::SSList) => L1 ofSSList(L2)
-     rule ofSSList(.SSList) => .List
-     rule ofSSList(K:K seqstrict:: L::SSList) => ListItem(K) ofSSList(L) [owise]
-
-     syntax KItem ::= "strict()"
-     rule list(HOLE:List) => toSList(HOLE) ~> strict() [heat]
-     rule HOLE:SList ~> strict() => krlist(ofSList(HOLE)) [cool]
-
-     syntax SList ::= K "strict::" SList [strict]
-     rule idToString(_::CId) => "<unknown>" [owise]
-
-     rule idToString(GlobalNamespace() :: X::CId)
-          => "::" +String idToString(X)
-
      rule firstChar(S::String) => substrString(S, 0, 1)
           requires lengthString(S) >=Int 1
      rule firstChar(_) => "" [owise]

diff --git a/semantics/common/resolution.k b/semantics/common/resolution.k
@@ -3,8 +3,9 @@ module COMMON-RESOLUTION-SYNTAX
      imports SYMLOC-SORTS
 
      syntax KItem ::= resolveCPPReference(SymBase)
+                    | "resolveMain"
 endmodule
 
 module COMMON-RESOLUTION
      imports COMMON-RESOLUTION-SYNTAX
-endmodule
+endmodule
diff --git a/semantics/common/syntax.k b/semantics/common/syntax.k
@@ -48,7 +48,6 @@ module COMMON-SYNTAX
      syntax Bool ::= Quals "<=Quals" Quals [function]
 
      syntax Namespace ::= GlobalNamespace()
-     syntax QualId ::= Namespace "::" CId
 
      syntax Scope ::= "none" | FileScope
      syntax FileScope ::= "fileScope"
@@ -60,8 +59,6 @@ module COMMON-SYNTAX
      syntax KItem ::= allowInit(K)
      syntax Expr ::= allowInit(Expr)
 
-     syntax String ::= signatureToString(QualId, K) [function]
-
      syntax KItem ::= CodeLoc(K, CabsLoc)
 
 endmodule
diff --git a/semantics/cpp14/language/common/builtin.k b/semantics/cpp14/language/common/builtin.k
@@ -1,10 +1,12 @@
 module CPP-BUILTIN-SYNTAX
+     imports COMMON-SORTS
      imports CPP-DYNAMIC-SORTS
      imports CPP-TYPING-SORTS
      syntax K ::= "weakCppBuiltins" [function]
                 | "cppBuiltins" [function]
      syntax CPPType ::= func(CPPTypes) [function, klabel(funcCpp)]
      syntax CPPType ::= func(CPPTypes, ExceptionSet) [function, klabel(funcExcCpp)]
+     syntax CPPType ::= func(CPPTypes, LanguageLinkage) [function, klabel(funcLinkCpp)]
      syntax CPPType ::= ptr(CPPType) [function, klabel(ptrCpp)]
      syntax NameTypePairs ::= List{NameTypePair,";"}
      syntax NameTypePair ::= QualId "->" CPPType
@@ -18,17 +20,21 @@ module CPP-BUILTIN
      imports CPP-SYNTAX
      imports CPP-TYPING-SYNTAX
 
-     rule cppBuiltins => .K
+     rule cppBuiltins
+       => GlobalNamespace() :: Namespace(Identifier("std")) :: Identifier("terminate") -> func(type(void))
+       ~> GlobalNamespace() :: Identifier("__cpp_abort") -> func(type(void))
 
      rule func(T::CPPType, Ts::CPPTypes) => type(functionType(T, Ts, noMethod, CPPLinkage, noexcept(false)))
      rule func(T::CPPType, Ts::CPPTypes, E::ExceptionSet) => type(functionType(T, Ts, noMethod, CPPLinkage, E))
+     rule func(T::CPPType, Ts::CPPTypes, L::LanguageLinkage) => type(functionType(T, Ts, noMethod, L, noexcept(false)))
      rule ptr(T::CPPType) => type(pointerType(T))
 
-     rule weakCppBuiltins => GlobalNamespace() :: operatornew -> func(ptr(type(void)), type(size_t))
-                          ~> GlobalNamespace() :: operatornew[] -> func(ptr(type(void)), type(size_t))
-                          ~> GlobalNamespace() :: operatordelete -> func(type(void), ptr(type(void)), noexcept(true))
-                          ~> GlobalNamespace() :: operatordelete[] -> func(type(void), ptr(type(void)), noexcept(true))
-                          ~> GlobalNamespace() :: operatordelete -> func(type(void), ptr(type(void)), type(size_t), noexcept(true))
-                          ~> GlobalNamespace() :: operatordelete[] -> func(type(void), ptr(type(void)), type(size_t), noexcept(true))
+     rule weakCppBuiltins
+       => GlobalNamespace() :: operatornew -> func(ptr(type(void)), type(size_t))
+       ~> GlobalNamespace() :: operatornew[] -> func(ptr(type(void)), type(size_t))
+       ~> GlobalNamespace() :: operatordelete -> func(type(void), ptr(type(void)), noexcept(true))
+       ~> GlobalNamespace() :: operatordelete[] -> func(type(void), ptr(type(void)), noexcept(true))
+       ~> GlobalNamespace() :: operatordelete -> func(type(void), ptr(type(void)), type(size_t), noexcept(true))
+       ~> GlobalNamespace() :: operatordelete[] -> func(type(void), ptr(type(void)), type(size_t), noexcept(true))
 
 endmodule
diff --git a/semantics/cpp14/language/common/conversion.k b/semantics/cpp14/language/common/conversion.k
@@ -177,6 +177,10 @@ module CPP-CONVERSION
 
      rule convertArray(lv(Loc::SymLoc, Tr::Trace, t(Q::Quals, Mods::Set, T::CPPSimpleArrayType)))
           => prv(arrayToPtrLoc(Loc, t(Q, Mods, T)), Tr, t(Q, Mods, pointerType(innerType(t(Q, Mods, T)))))
+     rule convertArray(xv(Loc::SymLoc, Tr::Trace, t(Q::Quals, Mods::Set, T::CPPSimpleArrayType)))
+          => prv(arrayToPtrLoc(Loc, t(Q, Mods, T)), Tr, t(Q, Mods, pointerType(innerType(t(Q, Mods, T)))))
+     rule convertArray(prv(Loc::SymLoc, Tr::Trace, t(Q::Quals, Mods::Set, T::CPPSimpleArrayType)))
+          => prv(arrayToPtrLoc(Loc, t(Q, Mods, T)), Tr, t(Q, Mods, pointerType(innerType(t(Q, Mods, T)))))
 
      syntax SymLoc ::= arrayToPtrLoc(SymLoc, CPPType) [function, klabel(arrayToPtrLocCpp)]
      rule arrayToPtrLoc(Loc::SymLoc, t(_, _, arrayType(T::CPPType, N::Int)))
@@ -192,8 +196,12 @@ module CPP-CONVERSION
 
      rule convertLVal(lv(Loc::SymLoc, Tr::Trace, T::CPPType))
           => instantiate(Loc, Tr, T)
+     rule convertLVal(xv(Loc::SymLoc, Tr::Trace, T::CPPType))
+          => instantiate(Loc, Tr, T)
      rule convertLVal(le(E::Expr, Tr::Trace, T::CPPType))
           => pre(E, Tr, prvalType(T))
+     rule convertLVal(xe(E::Expr, Tr::Trace, T::CPPType))
+          => pre(E, Tr, prvalType(T))
 
      syntax Int ::= rank(CPPType) [function, klabel(rankcpp)]
      rule rank(t(_, _, bool)) => 0