LLVM backend support

Dockerfile

@@ -4,12 +4,25 @@ FROM runtimeverificationinc/kframework:ubuntu-bionic
 # Install packages. #
 #####################
 
-RUN     apt-get update -q \
-    &&  apt install --yes \
-          libstdc++6      \
-          llvm-6.0        \
-          clang++-6.0     \
-          clang-6.0
+RUN   apt-get update -q     \
+  &&  apt-get install --yes \
+        libstdc++6          \
+        llvm-6.0            \
+        clang++-6.0         \
+        clang-6.0           \
+        clang-8             \
+        libclang-8-dev      \
+        llvm-8-tools        \
+        lld-8               \
+        zlib1g-dev          \
+        bison               \
+        flex                \
+        libboost-test-dev   \
+        libgmp-dev          \
+        libmpfr-dev         \
+        libyaml-dev         \
+        libjemalloc-dev     \
+        pkg-config
 
 RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.7 \
     && cd z3                                                        \
@@ -41,20 +54,21 @@ COPY --from=runtimeverificationinc/ocaml:ubuntu-bionic \
      /home/user/.opam \
      /home/user/.opam
 
-
-# This is where the rest of the dependencies go.
-ENV DEPS_DIR="/home/user/c-semantics-deps"
-
 ############
 # Build K. #
 ############
 
+# This is where the rest of the dependencies go.
+ENV DEPS_DIR="/home/user/c-semantics-deps"
+ENV PATH="${DEPS_DIR}/k/llvm-backend/src/main/native/llvm-backend/build/bin:${PATH}"
+ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin"
+
 COPY --chown=user:user ./.build/k/ ${DEPS_DIR}/k
 
 RUN cd ${DEPS_DIR}/k \
-  && mvn package -q -U \
+  && mvn package -e -q -U \
       -DskipTests -DskipKTest \
-      -Dhaskell.backend.skip -Dllvm.backend.skip \
-      -Dcheckstyle.skip
+      -Dhaskell.backend.skip \
+      -Dcheckstyle.skip \
+      -Dproject.build.type=FastBuild
 
-ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin"

Jenkinsfile

@@ -34,13 +34,10 @@ pipeline {
                 eval $(opam config env)
                 eval $(perl -I "~/perl5/lib/perl5" -Mlocal::lib)
                 export KOMPILE_FLAGS=-O2
-                make -j4 profile-rule-parsing --output-sync=line
+                make -j4 --output-sync=line
               '''
             } }
           }
-          post { success {
-            archiveArtifacts 'dist/timelogs.d/timelogs.csv'
-          } }
         }
         stage ( 'Re-compile w/ timeout' ) { steps {
           timeout(time: 8, unit: 'SECONDS' ) {

Makefile

@@ -6,7 +6,7 @@ export KOMPILE := $(K_BIN)/kompile
 export KDEP := $(K_BIN)/kdep
 
 # Appending to whatever the environment provided.
-K_OPTS += -Xmx8g
+K_OPTS += -Xmx16g
 K_OPTS += -Xss32m
 export K_OPTS
 

clang-tools/ClangKast/ClangKast.cc

@@ -91,6 +91,7 @@ std::ostream& operator<<(std::ostream & os, const Sort & sort) {
     case Sort::NAMESPACE:             os << "Namespeace"; break;
     case Sort::NNS:                   os << "NNS"; break;
     case Sort::NNSSPECIFIER:          os << "NNSSpecifier"; break;
+    case Sort::NOINIT:                os << "NoInit"; break;
     case Sort::NONAME:                os << "NoName"; break;
     case Sort::OPID:                  os << "OpId"; break;
     case Sort::QUALIFIER:             os << "Qualifier"; break;
@@ -140,7 +141,7 @@ string Kast::Node::escapeKLabel(const string & label) {
       case '#':  subst = "Hash'"; break;
       case '$':  subst = "Dolr'"; break;
       case '%':  subst = "Perc'"; break;
-      case '&':  subst = "And'" ; break;
+      case '&':  subst = "And-'"; break;
       case '\'': subst = "Apos'"; break;
       case '(':  subst = "LPar'"; break;
       case ')':  subst = "RPar'"; break;
@@ -223,7 +224,7 @@ void Kast::KApply::print(Sort parentSort, function<void (Sort)> printChild) cons
 // *** Kast::KToken ***
 
 string Kast::KToken::toKString(const string & s) {
-  return string(Kore ? escape(s) : "\"" + escape(s) + "\"");
+  return string(Kore ? s : "\"" + escape(s) + "\"");
 }
 
 string Kast::KToken::toKString(bool b) {
@@ -330,7 +331,7 @@ void Kast::add(const T & node) {
   Kast::Nodes.push_back(make_unique<T>(node));
 }
 
-void Kast::print() { print(Sort::K, 0); }
+void Kast::print() { print(Sort::KITEM, 0); }
 
 int Kast::print(Sort parentSort, int idx) {
   if (!Nodes[idx]) throw logic_error("parse error");

clang-tools/ClangKast/ClangKast.h

@@ -39,6 +39,7 @@ enum class Sort {
   NAMESPACE,
   NNS,
   NNSSPECIFIER,
+  NOINIT,
   NONAME,
   OPID,
   QUALIFIER,

clang-tools/ClangKast/GetKastVisitor.h

@@ -224,22 +224,21 @@ class GetKastVisitor
       Kast::add(Kast::KApply("NestedName", Sort::NNS, {Sort::NNS, Sort::NNSSPECIFIER}));
       TRY_TO(TraverseNestedNameSpecifier(NNS->getPrefix()));
     }
-    auto nns = Kast::KApply("NNS", Sort::NNSSPECIFIER, {Sort::CID});
     switch (NNS->getKind()) {
       case NestedNameSpecifier::Identifier:
-        Kast::add(nns);
+        Kast::add(Kast::KApply("NNSCId", Sort::NNSSPECIFIER, {Sort::CID}));
         TRY_TO(TraverseIdentifierInfo(NNS->getAsIdentifier()));
         break;
       case NestedNameSpecifier::Namespace:
-        Kast::add(nns);
+        Kast::add(Kast::KApply("NNSName", Sort::NNSSPECIFIER, {Sort::NAME}));
         TRY_TO(TraverseDeclarationName(NNS->getAsNamespace()->getDeclName()));
         break;
       case NestedNameSpecifier::NamespaceAlias:
-        Kast::add(nns);
+        Kast::add(Kast::KApply("NNSName", Sort::NNSSPECIFIER, {Sort::NAME}));
         TRY_TO(TraverseDeclarationName(NNS->getAsNamespaceAlias()->getDeclName()));
         break;
       case NestedNameSpecifier::TypeSpec:
-        Kast::add(nns);
+        Kast::add(Kast::KApply("NNSName", Sort::NNSSPECIFIER, {Sort::NAME}));
         TRY_TO(TraverseType(QualType(NNS->getAsType(), 0)));
         break;
       case NestedNameSpecifier::TypeSpecWithTemplate:
@@ -266,7 +265,7 @@ class GetKastVisitor
   bool TraverseIdentifierInfo(const IdentifierInfo *info, uintptr_t decl) {
     if (!info) {
       if (decl == 0) {
-        Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX", Sort::NONAME));
+        Kast::add(Kast::KApply("#NoName_COMMON-SYNTAX_NoName", Sort::NONAME));
       } else {
         Kast::add(Kast::KApply("unnamed", Sort::UNNAMEDCID, {Sort::INT, Sort::STRING}));
         VisitUnsigned((unsigned long long)decl);
@@ -456,7 +455,7 @@ class GetKastVisitor
 
     if (D->isThisDeclarationADefinition()) {
       if (CXXConstructorDecl *Ctor = dyn_cast<CXXConstructorDecl>(D)) {
-        Kast::add(Kast::KApply("Constructor", Sort::STMT, {Sort::LIST, Sort::STMT}));
+        Kast::add(Kast::KApply("Constructor", Sort::STMT, {Sort::LIST, Sort::ASTMT}));
         int i = 0;
         for (auto *I : Ctor->inits()) {
           if (I->isWritten()) i++;
@@ -498,6 +497,10 @@ class GetKastVisitor
     return TraverseFunctionHelper(D);
   }
 
+  void NoInit() {
+      Kast::add(Kast::KApply("NoInit", Sort::NOINIT));
+  }
+
   bool TraverseVarHelper(VarDecl *D) {
     StorageClass(D->getStorageClass());
     ThreadStorageClass(D->getTSCSpec());
@@ -518,7 +521,7 @@ class GetKastVisitor
     if (D->getInit()) {
       TRY_TO(TraverseStmt(D->getInit()));
     } else {
-      Kast::add(Kast::KApply("NoInit", Sort::INIT));
+      NoInit();
     }
     VisitBool(D->isDirectInit());
     return true;
@@ -545,7 +548,7 @@ class GetKastVisitor
     } else if (D->hasInClassInitializer()) {
       TRY_TO(TraverseStmt(D->getInClassInitializer()));
     } else {
-      Kast::add(Kast::KApply("NoInit", Sort::INIT));
+      NoInit();
     }
     return true;
   }
@@ -561,21 +564,16 @@ class GetKastVisitor
   }
 
   void VisitAccessSpecifier(AccessSpecifier Spec) {
-    const char *spec;
-    switch (Spec) {
-      case AS_public:
-        spec = "Public";
-        break;
-      case AS_protected:
-        spec = "Protected";
-        break;
-      case AS_private:
-        spec = "Private";
-        break;
-      case AS_none:
-        spec = "NoAccessSpec";
-        break;
-    }
+    const char * const spec = [&]{
+      switch (Spec) {
+        case AS_public:    return "Public";
+        case AS_protected: return "Protected";
+        case AS_private:   return "Private";
+        case AS_none:      return "NoAccessSpec";
+      }
+      assert(false && "Unknown access specifier");
+      return (const char *)nullptr;
+    }();
     Kast::add(Kast::KApply(spec, Sort::ACCESSSPECIFIER));
   }
 
@@ -1283,7 +1281,7 @@ class GetKastVisitor
   bool VisitReturnStmt(ReturnStmt *S) {
     Kast::add(Kast::KApply("ReturnStmt", Sort::STMT, {Sort::INIT}));
     if (!S->getRetValue()) {
-      Kast::add(Kast::KApply("NoInit", Sort::INIT));
+      NoInit();
     }
     return false;
   }
@@ -1344,10 +1342,11 @@ class GetKastVisitor
   }
 
   bool TraverseIfStmt(IfStmt *S) {
-    Kast::add(Kast::KApply("IfAStmt", Sort::ASTMT, {Sort::DECL, Sort::ASTMT, Sort::ASTMT}));
     if (VarDecl *D = S->getConditionVariable()) {
+      Kast::add(Kast::KApply("IfAStmtD", Sort::ASTMT, {Sort::DECL, Sort::ASTMT, Sort::ASTMT}));
       TRY_TO(TraverseDecl(D));
     } else {
+      Kast::add(Kast::KApply("IfAStmt", Sort::ASTMT, {Sort::EXPR, Sort::ASTMT, Sort::ASTMT}));
       TRY_TO(TraverseStmt(S->getCond()));
     }
     TRY_TO(TraverseStmt(S->getThen()));
@@ -1360,10 +1359,11 @@ class GetKastVisitor
   }
 
   bool TraverseSwitchStmt(SwitchStmt *S) {
-    Kast::add(Kast::KApply("SwitchAStmt", Sort::ASTMT, {Sort::DECL, Sort::ASTMT}));
     if (VarDecl *D = S->getConditionVariable()) {
+      Kast::add(Kast::KApply("SwitchAStmtD", Sort::ASTMT, {Sort::DECL, Sort::ASTMT}));
       TRY_TO(TraverseDecl(D));
     } else {
+      Kast::add(Kast::KApply("SwitchAStmt", Sort::ASTMT, {Sort::EXPR, Sort::ASTMT}));
       TRY_TO(TraverseStmt(S->getCond()));
     }
     TRY_TO(TraverseStmt(S->getBody()));
@@ -1444,19 +1444,23 @@ class GetKastVisitor
 
   bool TraverseCallExpr(CallExpr *E) {
     Kast::add(Kast::KApply("CallExpr", Sort::RESOLVEDEXPR, {Sort::EXPR, Sort::STRICTLIST, Sort::STRICTLISTRESULT}));
-    unsigned i = 0;
-    for (Stmt *SubStmt : E->children()) {
-      i++;
-    }
-    if (i-1 != E->getNumArgs()) {
-      throw std::logic_error("unimplemented: pre_args???");
-    }
-    bool first = true;
-    for (Stmt *SubStmt : E->children()) {
-      TRY_TO(TraverseStmt(SubStmt));
-      if (first) List(i-1);
-      first = false;
-    }
+
+    // 1
+    TRY_TO(TraverseStmt(E->getCallee()));
+
+    // 2
+    Kast::add(Kast::KApply("list", Sort::STRICTLIST, {Sort::LIST}));
+	for (unsigned int i = 0; i < E->getNumArgs(); i++) {
+	    clang::Expr * arg = E->getArg(i);
+		if (!isa<CXXDefaultArgExpr>(arg)) {
+            Kast::add(Kast::KApply("_List_", Sort::LIST, {Sort::LIST, Sort::LIST}));
+            Kast::add(Kast::KApply("ListItem", Sort::LIST, {Sort::KITEM}));
+            TRY_TO(TraverseStmt(arg));
+        }
+	}
+    Kast::add(Kast::KApply(".List", Sort::LIST));
+
+    // 3
     Kast::add(Kast::KApply("krlist", Sort::STRICTLISTRESULT, {Sort::LIST}));
     Kast::add(Kast::KApply(".List", Sort::LIST));
     return true;
@@ -1503,7 +1507,7 @@ class GetKastVisitor
     switch (Kind) {
       #define OVERLOADED_OPERATOR(Name,Spelling,Token,Unary,Binary,MemberOnly) \
       case OO_##Name:                                                          \
-        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID));                                 \
+        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID));                                 \
         break;
       #include "clang/Basic/OperatorKinds.def"
       default:
@@ -1515,7 +1519,7 @@ class GetKastVisitor
     switch (Kind) {
       #define UNARY_OP(Name, Spelling)         \
       case UO_##Name:                          \
-        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \
+        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \
         break;
       UNARY_OP(PostInc, "_++")
       UNARY_OP(PostDec, "_--")
@@ -1548,7 +1552,7 @@ class GetKastVisitor
     switch (Kind) {
       #define BINARY_OP(Name, Spelling)        \
       case BO_##Name:                          \
-        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX", Sort::OPID)); \
+        Kast::add(Kast::KApply("operator" Spelling "_CPP-SYNTAX_OpId", Sort::OPID)); \
         break;
       BINARY_OP(PtrMemD, ".*")
       BINARY_OP(PtrMemI, "->*")
@@ -1838,7 +1842,7 @@ class GetKastVisitor
     if (E->hasInitializer()) {
       TRY_TO(TraverseStmt(E->getInitializer()));
     } else {
-      Kast::add(Kast::KApply("NoInit", Sort::INIT));
+      NoInit();
     }
     KSeqList(E->getNumPlacementArgs());
     for (unsigned i = 0; i < E->getNumPlacementArgs(); i++) {
@@ -2022,7 +2026,7 @@ class GetKastVisitor
 
   bool TraverseInitListExpr(InitListExpr *E) {
     InitListExpr *Syntactic = E->isSemanticForm() ? E->getSyntacticForm() ? E->getSyntacticForm() : E : E;
-    Kast::add(Kast::KApply("BraceInit", Sort::BRACEINIT, {Sort::LIST}));
+    Kast::add(Kast::KApply("BraceInit", Sort::INIT, {Sort::LIST}));
     KSeqList(Syntactic->getNumInits());
     for (Stmt *SubStmt : Syntactic->children()) {
       TRY_TO(TraverseStmt(SubStmt));
@@ -2250,7 +2254,7 @@ class GetKastVisitor
       VisitUnsigned(presumed.getColumn());
       VisitBool(mgr.isInSystemHeader(loc));
     } else {
-      Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX", Sort::CABSLOC));
+      Kast::add(Kast::KApply("UnknownCabsLoc_COMMON-SYNTAX_CabsLoc", Sort::CABSLOC));
     }
   }
 

scripts/RV_Kcc/Opts.pm

@@ -447,7 +447,9 @@ sub parseOpts {
 			for GCC.
       { RV_Kcc::Opts::pushArg('cppArgs', "-d$chars"); }
   -ftranslation-depth=<depth>	Compile program up to a given depth. [undocumented]
+  -fdebug-translation	Run translation semantics with GDB. [undocumented]
   -flinking-depth=<depth>	Link program up to a given depth. [undocumented]
+  -fdebug-linking	Run linking semantics with GDB. [undocumented]
   -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.