Repository: kythe/kythe
Pull request #4767 (2020-11-25 01:33:17)

feat(verifier): compile and run a simple datalog program
This PR extracts code from Souffle that transforms an input
program string into an optimized representation. It was necessary
to do this because the code in question is not exported as
a library but is instead inlined in main(). It then checks that
running a simple example program produces the correct results.


Patch:
diff --git a/kythe/cxx/verifier/BUILD b/kythe/cxx/verifier/BUILD
index dba49d29a..fa95e52e2 100644
--- a/kythe/cxx/verifier/BUILD
+++ b/kythe/cxx/verifier/BUILD
@@ -50,6 +50,35 @@ cc_library(
     ],
 )
 
+cc_library(
+    name = "souffle_interpreter",
+    srcs = [
+        "souffle_interpreter.cc",
+    ],
+    hdrs = [
+        "souffle_interpreter.h",
+    ],
+    deps = [
+        "//third_party/souffle:parse_transform",
+        "@com_github_google_glog//:glog",
+        "@com_google_absl//absl/strings",
+        "@souffle",
+    ],
+)
+
+cc_test(
+    name = "souffle_interpreter_test",
+    srcs = [
+        "souffle_interpreter_test.cc",
+    ],
+    deps = [
+        ":souffle_interpreter",
+        "//third_party:gtest",
+        "//third_party:gtest_main",
+        "@com_github_google_glog//:glog",
+    ],
+)
+
 cc_library(
     name = "lib",
     srcs = [
diff --git a/kythe/cxx/verifier/souffle_interpreter.cc b/kythe/cxx/verifier/souffle_interpreter.cc
new file mode 100644
index 000000000..649c3852f
--- /dev/null
+++ b/kythe/cxx/verifier/souffle_interpreter.cc
@@ -0,0 +1,162 @@
+/*
+ * Copyright 2020 The Kythe Authors. All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *   http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include "kythe/cxx/verifier/souffle_interpreter.h"
+
+#include <array>
+#include <memory>
+
+#include "absl/strings/numbers.h"
+#include "absl/strings/str_cat.h"
+#include "glog/logging.h"
+#include "interpreter/Engine.h"
+#include "souffle/RamTypes.h"
+#include "souffle/io/IOSystem.h"
+#include "third_party/souffle/parse_transform.h"
+
+namespace kythe::verifier {
+namespace {
+constexpr std::array<int, 4> kInputData = {1, 2, 2, 3};
+
+class KytheReadStream : public souffle::ReadStream {
+ public:
+  explicit KytheReadStream(
+      const std::map<std::string, std::string>& rw_operation,
+      souffle::SymbolTable& symbol_table, souffle::RecordTable& record_table)
+      : souffle::ReadStream(rw_operation, symbol_table, record_table) {}
+
+ protected:
+  souffle::Own<souffle::RamDomain[]> readNextTuple() override {
+    if (pos_ >= kInputData.size()) {
+      return nullptr;
+    }
+    auto tuple = std::make_unique<souffle::RamDomain[]>(2);
+    tuple[0] = kInputData[pos_++];
+    tuple[1] = kInputData[pos_++];
+    return tuple;
+  }
+
+ private:
+  int pos_ = 0;
+};
+
+class KytheReadStreamFactory : public souffle::ReadStreamFactory {
+ public:
+  souffle::Own<souffle::ReadStream> getReader(
+      const std::map<std::string, std::string>& rw_operation,
+      souffle::SymbolTable& symbol_table,
+      souffle::RecordTable& record_table) override {
+    return souffle::mk<KytheReadStream>(rw_operation, symbol_table,
+                                        record_table);
+  }
+
+  const std::string& getName() const override {
+    static const std::string name = "kythe";
+    return name;
+  }
+};
+
+class KytheWriteStream : public souffle::WriteStream {
+ public:
+  explicit KytheWriteStream(
+      const std::map<std::string, std::string>& rw_operation,
+      const souffle::SymbolTable& symbol_table,
+      const souffle::RecordTable& record_table,
+      std::vector<std::pair<int, int>>* output)
+      : souffle::WriteStream(rw_operation, symbol_table, record_table),
+        output_(output) {}
+
+ protected:
+  void writeNullary() override {}
+
+  void writeNextTuple(const souffle::RamDomain* tuple) override {
+    output_->push_back({tuple[0], tuple[1]});
+  }
+
+ private:
+  std::vector<std::pair<int, int>>* output_;
+};
+
+class KytheWriteStreamFactory : public souffle::WriteStreamFactory {
+ public:
+  souffle::Own<souffle::WriteStream> getWriter(
+      const std::map<std::string, std::string>& rw_operation,
+      const souffle::SymbolTable& symbol_table,
+      const souffle::RecordTable& record_table) override {
+    auto output = rw_operation.find("id");
+    CHECK(output != rw_operation.end());
+    size_t output_id;
+    CHECK(absl::SimpleAtoi(output->second, &output_id));
+    CHECK(output_id < outputs_.size());
+    return souffle::mk<KytheWriteStream>(rw_operation, symbol_table,
+                                         record_table, &outputs_[output_id]);
+  }
+
+  const std::string& getName() const override {
+    static const std::string name = "kythe";
+    return name;
+  }
+
+  size_t NewOutput() {
+    outputs_.push_back({});
+    return outputs_.size() - 1;
+  }
+
+  const std::vector<std::pair<int, int>>& GetOutput(size_t id) const {
+    return outputs_[id];
+  }
+
+ private:
+  std::vector<std::vector<std::pair<int, int>>> outputs_;
+};
+}  // anonymous namespace
+
+// TODO(zarko): This is a temporary hack that only demonstrates that the
+// Souffle library is working. It bakes in the inputs and outputs for a
+// simple example program and checks that the interpreter calculates the
+// correct result. `Kythe{Write,Read}StreamFactory` will need to be moved
+// to separate files and updated to accept the Datalog relations that the
+// verifier -> datalog compiler produces.
+bool RunSouffle() {
+  auto write_stream_factory = std::make_shared<KytheWriteStreamFactory>();
+  size_t output_id = write_stream_factory->NewOutput();
+  souffle::IOSystem::getInstance().registerWriteStreamFactory(
+      write_stream_factory);
+  souffle::IOSystem::getInstance().registerReadStreamFactory(
+      std::make_shared<KytheReadStreamFactory>());
+  auto ram_tu = souffle::ParseTransform(absl::StrCat(R"(
+        .decl edge(x:number, y:number)
+        .input edge(IO=kythe)
+
+        .decl path(x:number, y:number)
+        .output path(IO=kythe, id=)",
+                                                     output_id, R"()
+
+        path(x, y) :- edge(x, y).
+        path(x, y) :- path(x, z), edge(z, y).
+    )"));
+  if (ram_tu == nullptr) {
+    return false;
+  }
+  souffle::Own<souffle::interpreter::Engine> interpreter(
+      souffle::mk<souffle::interpreter::Engine>(*ram_tu));
+  interpreter->executeMain();
+  std::set<std::pair<int, int>> expected = {{1, 2}, {1, 3}, {2, 3}};
+  const auto& actual = write_stream_factory->GetOutput(output_id);
+  std::set<std::pair<int, int>> actual_set(actual.begin(), actual.end());
+  return (expected == actual_set);
+}
+}  // namespace kythe::verifier
diff --git a/kythe/cxx/verifier/souffle_interpreter.h b/kythe/cxx/verifier/souffle_interpreter.h
new file mode 100644
index 000000000..f1832ad68
--- /dev/null
+++ b/kythe/cxx/verifier/souffle_interpreter.h
@@ -0,0 +1,24 @@
+/*
+ * Copyright 2020 The Kythe Authors. All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *   http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#ifndef KYTHE_CXX_VERIFIER_SOUFFLE_INTERPRETER_H_
+#define KYTHE_CXX_VERIFIER_SOUFFLE_INTERPRETER_H_
+
+namespace kythe::verifier {
+bool RunSouffle();
+}  // namespace kythe::verifier
+
+#endif  // defined(KYTHE_CXX_VERIFIER_SOUFFLE_INTERPRETER_H_)
diff --git a/third_party/souffle.BUILD b/third_party/souffle.BUILD
index 0450dc782..13c9a08fd 100644
--- a/third_party/souffle.BUILD
+++ b/third_party/souffle.BUILD
@@ -48,6 +48,13 @@ cc_library(
         "src",
         "src/include",
     ],
+    linkopts = select({
+        "@bazel_tools//src/conditions:linux_x86_64": [
+            "-ldl",
+        ],
+        "//conditions:default": [
+        ],
+    }),
     deps = [
         "@org_sourceware_libffi//:libffi",
     ],
diff --git a/third_party/souffle/BUILD b/third_party/souffle/BUILD
new file mode 100644
index 000000000..ee76aef64
--- /dev/null
+++ b/third_party/souffle/BUILD
@@ -0,0 +1,27 @@
+package(
+    default_visibility = ["//kythe:default_visibility"],
+    features = ["layering_check"],
+)
+
+licenses(["notice"])  # The Universal Permissive License (UPL), Version 1.0
+
+load("//:visibility.bzl", "PUBLIC_VISIBILITY")
+
+filegroup(
+    name = "license",
+    srcs = ["LICENSE"],
+)
+
+cc_library(
+    name = "parse_transform",
+    srcs = [
+        "parse_transform.cc",
+    ],
+    hdrs = [
+        "parse_transform.h",
+    ],
+    deps = [
+        "@com_github_google_glog//:glog",
+        "@souffle",
+    ],
+)
diff --git a/third_party/souffle/LICENSE b/third_party/souffle/LICENSE
new file mode 100644
index 000000000..e75033266
--- /dev/null
+++ b/third_party/souffle/LICENSE
@@ -0,0 +1,25 @@
+Copyright (c) 2016 Oracle and/or its affiliates. All Rights reserved
+
+The Universal Permissive License (UPL), Version 1.0
+
+Subject to the condition set forth below, permission is hereby granted to any person obtaining a copy of this software,
+associated documentation and/or data (collectively the "Software"), free of charge and under any and all copyright rights in the 
+Software, and any and all patent rights owned or freely licensable by each licensor hereunder covering either (i) the unmodified 
+Software as contributed to or provided by such licensor, or (ii) the Larger Works (as defined below), to deal in both
+
+(a) the Software, and
+(b) any piece of software and/or hardware listed in the lrgrwrks.txt file if one is included with the Software (each a “Larger
+Work” to which the Software is contributed by such licensors),
+
+without restriction, including without limitation the rights to copy, create derivative works of, display, perform, and 
+distribute the Software and make, use, sell, offer for sale, import, export, have made, and have sold the Software and the 
+Larger Work(s), and to sublicense the foregoing rights on either these or other terms.
+
+This license is subject to the following condition:
+The above copyright notice and either this complete permission notice or at a minimum a reference to the UPL must be included in 
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR
+IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/third_party/souffle/README.google b/third_party/souffle/README.google
new file mode 100644
index 000000000..356753846
--- /dev/null
+++ b/third_party/souffle/README.google
@@ -0,0 +1,7 @@
+URL: https://github.com/souffle-lang/souffle/archive/fbb4c4b967bf58cccb7aca58e3d200a799218d98.zip
+Version: fbb4c4b967bf58cccb7aca58e3d200a799218d98.
+License: The Universal Permissive License (UPL), Version 1.0
+License File: LICENSE
+Description: Soufflé • A Datalog Synthesis Tool for Static Analysis
+Local Modifications:
+  Extracted the parse/AST lowering pipeline code from src/main.cpp.
diff --git a/third_party/souffle/parse_transform.cc b/third_party/souffle/parse_transform.cc
new file mode 100644
index 000000000..f776fdbb1
--- /dev/null
+++ b/third_party/souffle/parse_transform.cc
@@ -0,0 +1,281 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2013, 2015, Oracle and/or its affiliates. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+// This code was originally in <souffle root>/src/main.cpp.
+
+#include "glog/logging.h"
+#include "third_party/souffle/parse_transform.h"
+
+#include "Global.h"
+#include "ast/Node.h"
+#include "ast/Program.h"
+#include "ast/TranslationUnit.h"
+#include "ast/analysis/PrecedenceGraph.h"
+#include "ast/analysis/SCCGraph.h"
+#include "ast/analysis/Type.h"
+#include "ast/transform/ADTtoRecords.h"
+#include "ast/transform/AddNullariesToAtomlessAggregates.h"
+#include "ast/transform/ComponentChecker.h"
+#include "ast/transform/ComponentInstantiation.h"
+#include "ast/transform/Conditional.h"
+#include "ast/transform/ExecutionPlanChecker.h"
+#include "ast/transform/Fixpoint.h"
+#include "ast/transform/FoldAnonymousRecords.h"
+#include "ast/transform/GroundWitnesses.h"
+#include "ast/transform/GroundedTermsChecker.h"
+#include "ast/transform/IOAttributes.h"
+#include "ast/transform/IODefaults.h"
+#include "ast/transform/InlineRelations.h"
+#include "ast/transform/MagicSet.h"
+#include "ast/transform/MaterializeAggregationQueries.h"
+#include "ast/transform/MaterializeSingletonAggregation.h"
+#include "ast/transform/MinimiseProgram.h"
+#include "ast/transform/NameUnnamedVariables.h"
+#include "ast/transform/NormaliseMultiResultFunctors.h"
+#include "ast/transform/PartitionBodyLiterals.h"
+#include "ast/transform/Pipeline.h"
+#include "ast/transform/PolymorphicObjects.h"
+#include "ast/transform/PragmaChecker.h"
+#include "ast/transform/Provenance.h"
+#include "ast/transform/ReduceExistentials.h"
+#include "ast/transform/RemoveBooleanConstraints.h"
+#include "ast/transform/RemoveEmptyRelations.h"
+#include "ast/transform/RemoveRedundantRelations.h"
+#include "ast/transform/RemoveRedundantSums.h"
+#include "ast/transform/RemoveRelationCopies.h"
+#include "ast/transform/RemoveTypecasts.h"
+#include "ast/transform/ReorderLiterals.h"
+#include "ast/transform/ReplaceSingletonVariables.h"
+#include "ast/transform/ResolveAliases.h"
+#include "ast/transform/ResolveAnonymousRecordAliases.h"
+#include "ast/transform/SemanticChecker.h"
+#include "ast/transform/SimplifyAggregateTargetExpression.h"
+#include "ast/transform/UniqueAggregationVariables.h"
+#include "ast2ram/AstToRamTranslator.h"
+#include "interpreter/Engine.h"
+#include "interpreter/ProgInterface.h"
+#include "parser/ParserDriver.h"
+#include "ram/Node.h"
+#include "ram/Program.h"
+#include "ram/TranslationUnit.h"
+#include "ram/transform/ChoiceConversion.h"
+#include "ram/transform/CollapseFilters.h"
+#include "ram/transform/Conditional.h"
+#include "ram/transform/EliminateDuplicates.h"
+#include "ram/transform/ExpandFilter.h"
+#include "ram/transform/HoistAggregate.h"
+#include "ram/transform/HoistConditions.h"
+#include "ram/transform/IfConversion.h"
+#include "ram/transform/IndexedInequality.h"
+#include "ram/transform/Loop.h"
+#include "ram/transform/MakeIndex.h"
+#include "ram/transform/Parallel.h"
+#include "ram/transform/ReorderConditions.h"
+#include "ram/transform/ReorderFilterBreak.h"
+#include "ram/transform/ReportIndex.h"
+#include "ram/transform/Sequence.h"
+#include "ram/transform/Transformer.h"
+#include "ram/transform/TupleId.h"
+#include "reports/DebugReport.h"
+#include "reports/ErrorReport.h"
+#include "souffle/RamTypes.h"
+#include "souffle/profile/Tui.h"
+#include "souffle/provenance/Explain.h"
+#include "souffle/utility/ContainerUtil.h"
+#include "souffle/utility/FileUtil.h"
+#include "souffle/utility/MiscUtil.h"
+#include "souffle/utility/StreamUtil.h"
+#include "souffle/utility/StringUtil.h"
+#include "synthesiser/Synthesiser.h"
+#include <cassert>
+#include <chrono>
+#include <cstdio>
+#include <cstdlib>
+#include <ctime>
+#include <iomanip>
+#include <iostream>
+#include <map>
+#include <memory>
+#include <set>
+#include <sstream>
+#include <stdexcept>
+#include <string>
+#include <thread>
+#include <utility>
+#include <vector>
+
+namespace souffle {
+
+std::unique_ptr<ram::TranslationUnit> ParseTransform(const std::string& code) {
+  Global::config().set("jobs", "1");
+  Global::config().has("verbose", "1");
+  souffle::ErrorReport errorReport(/*nowarn=*/true);
+  souffle::DebugReport debugReport;
+  souffle::Own<souffle::ast::TranslationUnit> astTranslationUnit =
+      souffle::ParserDriver::parseTranslationUnit(code, errorReport, debugReport);
+  auto& report = astTranslationUnit->getErrorReport();
+  if (report.getNumIssues() != 0) {
+      LOG(ERROR) << "Souffle parser reported a nonzero diagnostic count.";
+      std::stringstream diagnostics;
+      diagnostics << report;
+      LOG(ERROR) << diagnostics.str();
+      return nullptr;
+  }
+
+  // ------- rewriting / optimizations -------------
+
+  /* set up additional global options based on pragma declaratives */
+  (mk<ast::transform::PragmaChecker>())->apply(*astTranslationUnit);
+
+  /* construct the transformation pipeline */
+
+  // Equivalence pipeline
+  auto equivalencePipeline =
+          mk<ast::transform::PipelineTransformer>(mk<ast::transform::NameUnnamedVariablesTransformer>(),
+                  mk<ast::transform::FixpointTransformer>(mk<ast::transform::MinimiseProgramTransformer>()),
+                  mk<ast::transform::ReplaceSingletonVariablesTransformer>(),
+                  mk<ast::transform::RemoveRelationCopiesTransformer>(),
+                  mk<ast::transform::RemoveEmptyRelationsTransformer>(),
+                  mk<ast::transform::RemoveRedundantRelationsTransformer>());
+
+  // Magic-Set pipeline
+  auto magicPipeline = mk<ast::transform::PipelineTransformer>(mk<ast::transform::MagicSetTransformer>(),
+          mk<ast::transform::ResolveAliasesTransformer>(),
+          mk<ast::transform::RemoveRelationCopiesTransformer>(),
+          mk<ast::transform::RemoveEmptyRelationsTransformer>(),
+          mk<ast::transform::RemoveRedundantRelationsTransformer>(), souffle::clone(equivalencePipeline));
+
+  // Partitioning pipeline
+  auto partitionPipeline =
+          mk<ast::transform::PipelineTransformer>(mk<ast::transform::NameUnnamedVariablesTransformer>(),
+                  mk<ast::transform::PartitionBodyLiteralsTransformer>(),
+                  mk<ast::transform::ReplaceSingletonVariablesTransformer>());
+
+  // Provenance pipeline
+  auto provenancePipeline = mk<ast::transform::ConditionalTransformer>(Global::config().has("provenance"),
+          mk<ast::transform::PipelineTransformer>(mk<ast::transform::ProvenanceTransformer>(),
+                  mk<ast::transform::PolymorphicObjectsTransformer>()));
+
+  // Main pipeline
+  auto pipeline = mk<ast::transform::PipelineTransformer>(mk<ast::transform::ComponentChecker>(),
+          mk<ast::transform::ComponentInstantiationTransformer>(),
+          mk<ast::transform::IODefaultsTransformer>(),
+          mk<ast::transform::SimplifyAggregateTargetExpressionTransformer>(),
+          mk<ast::transform::UniqueAggregationVariablesTransformer>(),
+          mk<ast::transform::FixpointTransformer>(mk<ast::transform::PipelineTransformer>(
+                  mk<ast::transform::ResolveAnonymousRecordAliasesTransformer>(),
+                  mk<ast::transform::FoldAnonymousRecords>())),
+          mk<ast::transform::PolymorphicObjectsTransformer>(), mk<ast::transform::SemanticChecker>(),
+          mk<ast::transform::ADTtoRecordsTransformer>(), mk<ast::transform::GroundWitnessesTransformer>(),
+          mk<ast::transform::UniqueAggregationVariablesTransformer>(),
+          mk<ast::transform::NormaliseMultiResultFunctorsTransformer>(),
+          mk<ast::transform::MaterializeSingletonAggregationTransformer>(),
+          mk<ast::transform::FixpointTransformer>(
+                  mk<ast::transform::MaterializeAggregationQueriesTransformer>()),
+          mk<ast::transform::ResolveAliasesTransformer>(), mk<ast::transform::RemoveTypecastsTransformer>(),
+          mk<ast::transform::RemoveBooleanConstraintsTransformer>(),
+          mk<ast::transform::ResolveAliasesTransformer>(), mk<ast::transform::MinimiseProgramTransformer>(),
+          mk<ast::transform::InlineRelationsTransformer>(),
+          mk<ast::transform::PolymorphicObjectsTransformer>(), mk<ast::transform::GroundedTermsChecker>(),
+          mk<ast::transform::ResolveAliasesTransformer>(),
+          mk<ast::transform::RemoveRedundantRelationsTransformer>(),
+          mk<ast::transform::RemoveRelationCopiesTransformer>(),
+          mk<ast::transform::RemoveEmptyRelationsTransformer>(),
+          mk<ast::transform::ReplaceSingletonVariablesTransformer>(),
+          mk<ast::transform::FixpointTransformer>(mk<ast::transform::PipelineTransformer>(
+                  mk<ast::transform::ReduceExistentialsTransformer>(),
+                  mk<ast::transform::RemoveRedundantRelationsTransformer>())),
+          mk<ast::transform::RemoveRelationCopiesTransformer>(), std::move(partitionPipeline),
+          std::move(equivalencePipeline), mk<ast::transform::RemoveRelationCopiesTransformer>(),
+          std::move(magicPipeline), mk<ast::transform::ReorderLiteralsTransformer>(),
+          mk<ast::transform::RemoveRedundantSumsTransformer>(),
+          mk<ast::transform::RemoveEmptyRelationsTransformer>(),
+          mk<ast::transform::AddNullariesToAtomlessAggregatesTransformer>(),
+          mk<ast::transform::PolymorphicObjectsTransformer>(),
+          mk<ast::transform::ReorderLiteralsTransformer>(), mk<ast::transform::ExecutionPlanChecker>(),
+          std::move(provenancePipeline), mk<ast::transform::IOAttributesTransformer>());
+
+  // Disable unwanted transformations
+  if (Global::config().has("disable-transformers")) {
+      std::vector<std::string> givenTransformers =
+              splitString(Global::config().get("disable-transformers"), ',');
+      pipeline->disableTransformers(
+              std::set<std::string>(givenTransformers.begin(), givenTransformers.end()));
+  }
+
+  // Toggle pipeline verbosity
+  pipeline->setVerbosity(Global::config().has("verbose"));
+
+  // Apply all the transformations
+  pipeline->apply(*astTranslationUnit);
+
+  if (Global::config().has("show")) {
+      // Output the transformed datalog and return
+      if (Global::config().get("show") == "transformed-datalog") {
+          std::cout << astTranslationUnit->getProgram() << std::endl;
+          return 0;
+      }
+
+      // Output the precedence graph in graphviz dot format and return
+      if (Global::config().get("show") == "precedence-graph") {
+          astTranslationUnit->getAnalysis<ast::analysis::PrecedenceGraphAnalysis>()->print(std::cout);
+          std::cout << std::endl;
+          return 0;
+      }
+
+      // Output the scc graph in graphviz dot format and return
+      if (Global::config().get("show") == "scc-graph") {
+          astTranslationUnit->getAnalysis<ast::analysis::SCCGraphAnalysis>()->print(std::cout);
+          std::cout << std::endl;
+          return 0;
+      }
+
+      // Output the type analysis
+      if (Global::config().get("show") == "type-analysis") {
+          astTranslationUnit->getAnalysis<ast::analysis::TypeAnalysis>()->print(std::cout);
+          std::cout << std::endl;
+          return 0;
+      }
+  }
+
+  // ------- execution -------------
+  /* translate AST to RAM */
+  debugReport.startSection();
+  auto ramTranslationUnit = ast2ram::AstToRamTranslator().translateUnit(*astTranslationUnit);
+  debugReport.endSection("ast-to-ram", "Translate AST to RAM");
+
+  // Apply RAM transforms
+  {
+      using namespace ram::transform;
+      Own<Transformer> ramTransform = mk<TransformerSequence>(
+              mk<LoopTransformer>(mk<TransformerSequence>(mk<ExpandFilterTransformer>(),
+                      mk<HoistConditionsTransformer>(), mk<MakeIndexTransformer>())),
+              mk<LoopTransformer>(mk<IndexedInequalityTransformer>()), mk<IfConversionTransformer>(),
+              mk<ChoiceConversionTransformer>(), mk<CollapseFiltersTransformer>(), mk<TupleIdTransformer>(),
+              mk<LoopTransformer>(
+                      mk<TransformerSequence>(mk<HoistAggregateTransformer>(), mk<TupleIdTransformer>())),
+              mk<ExpandFilterTransformer>(), mk<HoistConditionsTransformer>(),
+              mk<CollapseFiltersTransformer>(), mk<EliminateDuplicatesTransformer>(),
+              mk<ReorderConditionsTransformer>(), mk<LoopTransformer>(mk<ReorderFilterBreak>()),
+              mk<ConditionalTransformer>(
+                      // job count of 0 means all cores are used.
+                      []() -> bool { return std::stoi(Global::config().get("jobs")) != 1; },
+                      mk<ParallelTransformer>()),
+              mk<ReportIndexTransformer>());
+
+      ramTransform->apply(*ramTranslationUnit);
+  }
+
+  if (ramTranslationUnit->getErrorReport().getNumIssues() != 0) {
+      std::cerr << ramTranslationUnit->getErrorReport();
+  }
+
+  return ramTranslationUnit;
+}
+
+}
diff --git a/third_party/souffle/parse_transform.h b/third_party/souffle/parse_transform.h
new file mode 100644
index 000000000..702fe980c
--- /dev/null
+++ b/third_party/souffle/parse_transform.h
@@ -0,0 +1,16 @@
+#ifndef THIRD_PARTY_SOUFFLE_PARSE_TRANSFORM_H_
+#define THIRD_PARTY_SOUFFLE_PARSE_TRANSFORM_H_
+
+#include "ram/TranslationUnit.h"
+
+#include <memory>
+#include <string>
+
+namespace souffle {
+/// \brief Parses and transforms `code` into a `ram::TranslationUnit`.
+/// \param code the Souffle program to transform.
+/// \return the resulting translation unit or null on error.
+std::unique_ptr<ram::TranslationUnit> ParseTransform(const std::string& code);
+}  // namespace souffle
+
+#endif  // defined(THIRD_PARTY_SOUFFLE_PARSE_TRANSFORM_H_)


Test patch:
diff --git a/kythe/cxx/verifier/souffle_interpreter_test.cc b/kythe/cxx/verifier/souffle_interpreter_test.cc
new file mode 100644
index 000000000..f2df8195f
--- /dev/null
+++ b/kythe/cxx/verifier/souffle_interpreter_test.cc
@@ -0,0 +1,24 @@
+/*
+ * Copyright 2020 The Kythe Authors. All rights reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *   http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include "kythe/cxx/verifier/souffle_interpreter.h"
+
+#include "glog/logging.h"
+#include "gtest/gtest.h"
+
+namespace kythe::verifier {
+TEST(SouffleInterpreterTest, SmokeTest) { ASSERT_TRUE(RunSouffle()); }
+}  // namespace kythe::verifier