feat(verifier): set up a library/tests for lowering assertions to sou…

…ffle (#4832)

kythe/cxx/verifier/BUILD

@@ -83,11 +83,43 @@ cc_library(
     name = "ast",
     hdrs = [
         "assertion_ast.h",
+        ":parser",  # for location.hh
     ],
     deps = [
         ":pretty_printer",
+        "@com_github_google_glog//:glog",
         "@com_google_absl//absl/strings",
         "@com_google_absl//absl/strings:str_format",
+        "@com_googlesource_code_re2//:re2",
+    ],
+)
+
+cc_library(
+    name = "assertions_to_souffle",
+    srcs = [
+        "assertions_to_souffle.cc",
+    ],
+    hdrs = [
+        "assertions_to_souffle.h",
+    ],
+    deps = [
+        ":ast",
+        ":lib",
+        "@com_google_absl//absl/strings",
+    ],
+)
+
+cc_test(
+    name = "assertions_to_souffle_test",
+    srcs = [
+        "assertions_to_souffle_test.cc",
+    ],
+    deps = [
+        ":assertions_to_souffle",
+        ":ast",
+        ":pretty_printer",
+        "//third_party:gtest",
+        "//third_party:gtest_main",
     ],
 )
 

kythe/cxx/verifier/assertions_to_souffle.cc

@@ -0,0 +1,29 @@
+/*
+ * Copyright 2021 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/assertions_to_souffle.h"
+
+namespace kythe::verifier {
+
+/// \brief Turns `goal_groups` into a Souffle program.
+/// \param symbol_table the symbol table used by `goal_groups`.
+/// \param goal_groups the goal groups to lower.
+std::string LowerGoalsToSouffle(const SymbolTable& symbol_table,
+                                const std::vector<GoalGroup>& goal_groups) {
+  return "(unimplemented)";
+}
+
+}  // namespace kythe::verifier

kythe/cxx/verifier/assertions_to_souffle.h

@@ -0,0 +1,34 @@
+/*
+ * Copyright 2021 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_ASSERTIONS_TO_SOUFFLE_
+#define KYTHE_CXX_VERIFIER_ASSERTIONS_TO_SOUFFLE_
+
+#include <string>
+
+#include "kythe/cxx/verifier/assertion_ast.h"
+
+namespace kythe::verifier {
+
+/// \brief Turns `goal_groups` into a Souffle program.
+/// \param symbol_table the symbol table used by `goal_groups`.
+/// \param goal_groups the goal groups to lower.
+std::string LowerGoalsToSouffle(const SymbolTable& symbol_table,
+                                const std::vector<GoalGroup>& goal_groups);
+
+}  // namespace kythe::verifier
+
+#endif  // defined(KYTHE_CXX_VERIFIER_ASSERTIONS_TO_SOUFFLE_)

kythe/cxx/verifier/assertions_to_souffle_test.cc

@@ -0,0 +1,50 @@
+/*
+ * Copyright 2021 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/assertions_to_souffle.h"
+
+#include "gtest/gtest.h"
+#include "kythe/cxx/verifier/assertion_ast.h"
+#include "kythe/cxx/verifier/pretty_printer.h"
+
+namespace kythe::verifier {
+namespace {
+
+/// \brief a test fixture that makes it easy to manipulate verifier ASTs.
+class AstTest : public ::testing::Test {
+ protected:
+  /// \return an `Identifier` node with value `string`.
+  Identifier* Id(const std::string& string) {
+    auto symbol = symbol_table_.intern(string);
+    return new (&arena_) Identifier(yy::location{}, symbol);
+  }
+
+  /// \return a string representation of `node`
+  std::string Dump(AstNode* node) {
+    StringPrettyPrinter printer;
+    node->Dump(symbol_table_, &printer);
+    return printer.str();
+  }
+
+ private:
+  Arena arena_;
+  SymbolTable symbol_table_;
+};
+
+TEST_F(AstTest, SelfTest) { EXPECT_EQ("test", Dump(Id("test"))); }
+
+}  // anonymous namespace
+}  // namespace kythe::verifier