feat(verifier): add a relation for anchors (#5667)

* feat(verifier): add a relation for anchors

In service of #4748

kythe/cxx/verifier/assertion_ast.h

@@ -25,6 +25,7 @@
 
 #include "absl/strings/escaping.h"
 #include "absl/strings/str_cat.h"
+#include "absl/types/optional.h"
 #include "glog/logging.h"
 #include "kythe/cxx/verifier/location.hh"
 #include "pretty_printer.h"
@@ -42,6 +43,20 @@ class SymbolTable {
  public:
   explicit SymbolTable() : id_regex_("[%#]?[_a-zA-Z/][a-zA-Z_0-9/]*") {}
 
+  /// \brief Returns the `Symbol` associated with `string` or `nullopt`.
+  absl::optional<Symbol> FindInterned(absl::string_view string) const {
+    const auto old = symbols_.find(std::string(string));
+    if (old == symbols_.end()) return absl::nullopt;
+    return old->second;
+  }
+
+  /// \brief Returns the `Symbol` associated with `string`, or aborts.
+  Symbol MustIntern(absl::string_view string) const {
+    auto sym = FindInterned(string);
+    CHECK(sym) << "no symbol for " << string;
+    return *sym;
+  }
+
   /// \brief Returns the `Symbol` associated with `string`, or makes a new one.
   Symbol intern(const std::string& string) {
     const auto old = symbols_.find(string);

kythe/cxx/verifier/assertions_to_souffle.cc

@@ -16,6 +16,8 @@
 
 #include "kythe/cxx/verifier/assertions_to_souffle.h"
 
+#include "absl/strings/substitute.h"
+
 namespace kythe::verifier {
 namespace {
 constexpr absl::string_view kGlobalDecls = R"(
@@ -30,6 +32,10 @@ constexpr absl::string_view kGlobalDecls = R"(
 .input entry(IO=kythe)
 .decl anchor(begin:number, end:number, vname:vname)
 .input anchor(IO=kythe, anchors=1)
+.decl at(startsym:number, endsym:number, vname:vname)
+at(s, e, v) :- entry(v, $0, nil, $1, $2),
+               entry(v, $0, nil, $3, s),
+               entry(v, $0, nil, $4, e).
 .decl result()
 result() :- true
 )";
@@ -66,8 +72,8 @@ bool SouffleProgram::LowerSubexpression(AstNode* node) {
 
 bool SouffleProgram::LowerGoalGroup(const SymbolTable& symbol_table,
                                     const GoalGroup& group) {
-  auto eq_sym = const_cast<SymbolTable&>(symbol_table).intern("=");
-  auto empty_sym = const_cast<SymbolTable&>(symbol_table).intern("");
+  auto eq_sym = symbol_table.MustIntern("=");
+  auto empty_sym = symbol_table.MustIntern("");
 #ifdef DEBUG_LOWERING
   FileHandlePrettyPrinter dprinter(stderr);
 #endif
@@ -87,14 +93,19 @@ bool SouffleProgram::LowerGoalGroup(const SymbolTable& symbol_table,
         return false;
       }
       if (auto* range = tup->element(0)->AsRange()) {
-        absl::StrAppend(&code_, ", v", FindEVar(evar), "=[_, ", range->corpus(),
-                        ", ", range->path(), ", ", range->root(), ", _]");
-        // TODO(zarko): derive an anchor relation (will need to convert
-        // range->begin, end to symbols; also need to get the relevant symbols
-        // included in the prelude) or populate the anchor map (would require
-        // sorting input, which is a huge time sink).
-        absl::StrAppend(&code_, ", anchor(", range->begin(), ", ", range->end(),
-                        ", v", FindEVar(evar), ")");
+        auto beginsym =
+            symbol_table.FindInterned(std::to_string(range->begin()));
+        auto endsym = symbol_table.FindInterned(std::to_string(range->end()));
+        if (!beginsym || !endsym) {
+          // TODO(zarko): emit a warning here (if we're in a positive goal)?
+          absl::StrAppend(&code_, ", false");
+        } else {
+          absl::StrAppend(&code_, ", v", FindEVar(evar), "=[_, ",
+                          range->corpus(), ", ", range->path(), ", ",
+                          range->root(), ", _]");
+          absl::StrAppend(&code_, ", at(", *beginsym, ", ", *endsym, ", v",
+                          FindEVar(evar), ")");
+        }
       } else {
         auto* oevar = tup->element(0)->AsEVar();
         if (oevar == nullptr) {
@@ -134,7 +145,14 @@ bool SouffleProgram::LowerGoalGroup(const SymbolTable& symbol_table,
 
 bool SouffleProgram::Lower(const SymbolTable& symbol_table,
                            const std::vector<GoalGroup>& goal_groups) {
-  code_ = emit_prelude_ ? std::string(kGlobalDecls) : "";
+  code_.clear();
+  if (emit_prelude_) {
+    code_ = absl::Substitute(kGlobalDecls, symbol_table.MustIntern(""),
+                             symbol_table.MustIntern("/kythe/node/kind"),
+                             symbol_table.MustIntern("anchor"),
+                             symbol_table.MustIntern("/kythe/loc/start"),
+                             symbol_table.MustIntern("/kythe/loc/end"));
+  }
   CHECK_LE(goal_groups.size(), 1) << "(unimplemented)";
   if (goal_groups.size() == 0) {
     absl::StrAppend(&code_, ".\n");

kythe/cxx/verifier/souffle_interpreter_test.cc

@@ -22,6 +22,12 @@
 namespace kythe::verifier {
 TEST(SouffleInterpreterTest, SmokeTest) {
   SymbolTable symbols;
+  // Intern the symbols required by the prelude.
+  symbols.intern("");
+  symbols.intern("/kythe/node/kind");
+  symbols.intern("anchor");
+  symbols.intern("/kythe/loc/start");
+  symbols.intern("/kythe/loc/end");
   Database db;
   AnchorMap anchors;
   std::vector<GoalGroup> groups;

kythe/cxx/verifier/verifier.cc

@@ -716,7 +716,10 @@ bool Verifier::SetGoalCommentRegex(const std::string& regex,
   return true;
 }
 
-bool Verifier::LoadInlineProtoFile(const std::string& file_data) {
+bool Verifier::LoadInlineProtoFile(const std::string& file_data,
+                                   absl::string_view path,
+                                   absl::string_view root,
+                                   absl::string_view corpus) {
   kythe::proto::Entries entries;
   bool ok = google::protobuf::TextFormat::ParseFromString(file_data, &entries);
   if (!ok) {
@@ -730,8 +733,10 @@ bool Verifier::LoadInlineProtoFile(const std::string& file_data) {
     }
   }
   Symbol empty = symbol_table_.intern("");
-  return parser_.ParseInlineRuleString(file_data, *kStandardIn, empty, empty,
-                                       empty, "\\s*\\#\\-(.*)");
+  return parser_.ParseInlineRuleString(
+      file_data, *kStandardIn, symbol_table_.intern(std::string(path)),
+      symbol_table_.intern(std::string(root)),
+      symbol_table_.intern(std::string(corpus)), "\\s*\\#\\-(.*)");
 }
 
 bool Verifier::LoadInlineRuleFile(const std::string& filename) {

kythe/cxx/verifier/verifier.h

@@ -57,8 +57,14 @@ class Verifier {
   /// \brief Loads a text proto with goal comments indicating rules and data.
   /// The VName for the source file will be blank.
   /// \param file_data The data to load
+  /// \param path the path to use for anchors
+  /// \param root the root to use for anchors
+  /// \param corpus the corpus to use for anchors
   /// \return false if we failed
-  bool LoadInlineProtoFile(const std::string& file_data);
+  bool LoadInlineProtoFile(const std::string& file_data,
+                           absl::string_view path = "",
+                           absl::string_view root = "",
+                           absl::string_view corpus = "");
 
   /// \brief During verification, ignore duplicate facts.
   void IgnoreDuplicateFacts();

kythe/cxx/verifier/verifier_unit_test.cc

@@ -516,8 +516,7 @@ fact_value: ""
 }
 
 // TODO(zarko): See comments in souffle_interpreter re: the anchor() relation.
-TEST(VerifierUnitTest, GenerateAnchorEvar) {
-  Verifier v;
+TEST_P(VerifierTest, GenerateAnchorEvar) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
 #- @text defines SomeNode
 ##text (line 3 column 2 offset 38-42)
@@ -541,7 +540,8 @@ edge_kind: "/kythe/edge/defines"
 target { root:"2" }
 fact_name: "/"
 fact_value: ""
-})"));
+})",
+                                    "", "1"));
   ASSERT_TRUE(v.PrepareDatabase());
   ASSERT_TRUE(v.VerifyAllGoals());
 }