chore(verifier): get rid of more direct ast access from inspections (#…

…5816)

This PR also reorders the fields of the vname tuple to
reflect the external documentation (the old solver reordered
them as an optimization; we don't need to do this anymore).
There's a fix to type ascription as well (fields of vnames
should be identifiers).

kythe/cxx/verifier/assertions_to_souffle.cc

@@ -29,8 +29,8 @@ constexpr absl::string_view kGlobalDecls = R"(
 .type vname = [
   signature:number,
   corpus:number,
-  path:number,
   root:number,
+  path:number,
   language:number
 ]
 .decl entry(source:vname, kind:number, target:vname, name:number, value:number)
@@ -54,7 +54,7 @@ bool SouffleProgram::LowerSubexpression(AstNode* node, EVarType type) {
       if (p != 0) {
         absl::StrAppend(&code_, ", ");
       }
-      if (!LowerSubexpression(tup->element(p), type)) {
+      if (!LowerSubexpression(tup->element(p), EVarType::kSymbol)) {
         return false;
       }
     }
@@ -147,7 +147,7 @@ bool SouffleProgram::LowerGoal(const SymbolTable& symbol_table, AstNode* goal) {
         absl::StrAppend(&code_, ", false");
       } else {
         absl::StrAppend(&code_, ", v", FindEVar(evar), "=[_, ", range->corpus(),
-                        ", ", range->path(), ", ", range->root(), ", _]");
+                        ", ", range->root(), ", ", range->path(), ", _]");
         absl::StrAppend(&code_, ", at(", *beginsym, ", ", *endsym, ", v",
                         FindEVar(evar), ")");
       }

kythe/cxx/verifier/souffle_interpreter.cc

@@ -108,12 +108,11 @@ class KytheReadStream : public souffle::ReadStream {
  private:
   void CopyVName(kythe::verifier::Tuple* vname,
                  souffle::RamDomain (&target)[5]) {
-    // output: sig, corp, path, root, lang
-    // input: sig, corp, root, path, lang
+    // sig, corp, root, path, lang
     target[0] = vname->element(0)->AsIdentifier()->symbol();
     target[1] = vname->element(1)->AsIdentifier()->symbol();
-    target[2] = vname->element(3)->AsIdentifier()->symbol();
-    target[3] = vname->element(2)->AsIdentifier()->symbol();
+    target[2] = vname->element(2)->AsIdentifier()->symbol();
+    target[3] = vname->element(3)->AsIdentifier()->symbol();
     target[4] = vname->element(4)->AsIdentifier()->symbol();
   }
   const AnchorMap& anchors_;
@@ -185,8 +184,8 @@ class KytheWriteStream : public souffle::WriteStream {
         case EVarType::kVName: {
           const auto* v = recordTable.unpack(tuple[ox], 5);
           absl::StrAppend(o, "vname(", get_symbol_(v[0]), ", ",
-                          get_symbol_(v[1]), ", ", get_symbol_(v[3]), ", ",
-                          get_symbol_(v[2]), ", ", get_symbol_(v[4]), ")");
+                          get_symbol_(v[1]), ", ", get_symbol_(v[2]), ", ",
+                          get_symbol_(v[3]), ", ", get_symbol_(v[4]), ")");
         } break;
         case EVarType::kSymbol: {
           *o = get_symbol_(tuple[ox]);
@@ -245,8 +244,7 @@ SouffleResult RunSouffle(
     const SymbolTable& symbol_table, const std::vector<GoalGroup>& goal_groups,
     const Database& database, const AnchorMap& anchors,
     const std::vector<Inspection>& inspections,
-    std::function<bool(const Inspection&, std::optional<std::string_view>)>
-        inspect,
+    std::function<bool(const Inspection&, std::string_view)> inspect,
     std::function<std::string(size_t)> get_symbol) {
   SouffleResult result{};
   SouffleProgram program;

kythe/cxx/verifier/souffle_interpreter.h

@@ -39,17 +39,15 @@ struct SouffleResult {
 /// \param inspect the inspection callback that will be used against the
 /// provided list of inspections; a false return value stops iterating through
 /// inspection results and fails the solution, while a true result continues.
-/// If set, `value` is a string representation of the assignment of the EVar to
+/// `value` is a string representation of the assignment of the EVar to
 /// which the inspection refers.
 /// \param get_symbol returns a string representation of the given symbol
 /// \return a `SouffleResult` describing how the run went.
 SouffleResult RunSouffle(
     const SymbolTable& symbol_table, const std::vector<GoalGroup>& goal_groups,
     const Database& database, const AnchorMap& anchors,
     const std::vector<Inspection>& inspections,
-    std::function<bool(const Inspection&,
-                       std::optional<std::string_view> value)>
-        inspect,
+    std::function<bool(const Inspection&, std::string_view value)> inspect,
     std::function<std::string(size_t)> get_symbol);
 }  // namespace kythe::verifier
 

kythe/cxx/verifier/verifier.cc

@@ -968,14 +968,13 @@ void Verifier::DumpErrorGoal(size_t group, size_t index) {
 }
 
 bool Verifier::VerifyAllGoals(
-    std::function<bool(Verifier*, const Inspection&,
-                       std::optional<std::string_view>)>
+    std::function<bool(Verifier*, const Inspection&, std::string_view)>
         inspect) {
   if (use_fast_solver_) {
     auto result = RunSouffle(
         symbol_table_, parser_.groups(), facts_, anchors_,
         parser_.inspections(),
-        [&](const Inspection& i, std::optional<std::string_view> o) {
+        [&](const Inspection& i, std::string_view o) {
           return inspect(this, i, o);
         },
         [&](Symbol s) { return symbol_table_.PrettyText(s); });
@@ -988,7 +987,7 @@ bool Verifier::VerifyAllGoals(
     }
     std::function<bool(Verifier*, const Inspection&)> wi =
         [&](Verifier* v, const Inspection& i) {
-          return inspect(v, i, std::nullopt);
+          return inspect(v, i, v->InspectionString(i));
         };
     Solver solver(this, facts_, anchors_, wi);
     bool result = solver.Solve();

kythe/cxx/verifier/verifier.h

@@ -96,18 +96,16 @@ class Verifier {
   /// \param inspect function to call on any inspection request
   /// \return true if all goals could be satisfied.
   bool VerifyAllGoals(std::function<bool(Verifier* context, const Inspection&,
-                                         std::optional<std::string_view>)>
+                                         std::string_view)>
                           inspect);
 
   /// \brief Attempts to satisfy all goals from all loaded rule files and facts.
   /// \param inspect function to call on any inspection request
   /// \return true if all goals could be satisfied.
   bool VerifyAllGoals(
       std::function<bool(Verifier* context, const Inspection&)> inspect) {
-    return VerifyAllGoals(
-        [&](Verifier* v, const Inspection& i, std::optional<std::string_view>) {
-          return inspect(v, i);
-        });
+    return VerifyAllGoals([&](Verifier* v, const Inspection& i,
+                              std::string_view) { return inspect(v, i); });
   }
 
   /// \brief Attempts to satisfy all goals from all loaded rule files and facts.

kythe/cxx/verifier/verifier_unit_test.cc

@@ -97,6 +97,8 @@ TEST(VerifierUnitTest, UnescapeStringLiterals) {
   EXPECT_EQ("\\", tmp);
 }
 
+bool CheckEVarInit(std::string_view s) { return s != "nil" && !s.empty(); }
+
 enum class Solver { Old, New };
 
 class VerifierTest : public testing::TestWithParam<Solver> {
@@ -1899,16 +1901,15 @@ fact_value: ""
   std::string some_anchor, some_node, another_anchor, another_node;
   ASSERT_TRUE(v.VerifyAllGoals(
       [&some_anchor, &some_node, &another_anchor, &another_node](
-          Verifier* cxt, const Inspection& inspection,
-          std::optional<std::string_view> s) {
+          Verifier* cxt, const Inspection& inspection, std::string_view s) {
         if (inspection.label == "SomeAnchor") {
-          some_anchor = s ? *s : cxt->InspectionString(inspection);
+          some_anchor = s;
         } else if (inspection.label == "SomeNode") {
-          some_node = s ? *s : cxt->InspectionString(inspection);
+          some_node = s;
         } else if (inspection.label == "AnotherAnchor") {
-          another_anchor = s ? *s : cxt->InspectionString(inspection);
+          another_anchor = s;
         } else if (inspection.label == "AnotherNode") {
-          another_node = s ? *s : cxt->InspectionString(inspection);
+          another_node = s;
         } else {
           return false;
         }
@@ -1934,24 +1935,16 @@ fact_value: "42"
   bool key_was_ordinal = false;
   bool evar_init = false;
   bool evar_init_to_correct_ordinal = false;
-  ASSERT_TRUE(v.VerifyAllGoals([&call_count, &key_was_ordinal, &evar_init,
-                                &evar_init_to_correct_ordinal](
-                                   Verifier* cxt, const Inspection& inspection,
-                                   std::optional<std::string_view> s) {
-    ++call_count;
-    key_was_ordinal = (inspection.label == "Ordinal");
-    if (s) {
-      evar_init = true;
-      evar_init_to_correct_ordinal = *s == "\"42\"";
-    } else if (AstNode* node = inspection.evar->current()) {
-      evar_init = true;
-      if (Identifier* identifier = node->AsIdentifier()) {
-        evar_init_to_correct_ordinal =
-            cxt->symbol_table()->text(identifier->symbol()) == "42";
-      }
-    }
-    return true;
-  }));
+  ASSERT_TRUE(v.VerifyAllGoals(
+      [&call_count, &key_was_ordinal, &evar_init,
+       &evar_init_to_correct_ordinal](
+          Verifier* cxt, const Inspection& inspection, std::string_view s) {
+        ++call_count;
+        key_was_ordinal = (inspection.label == "Ordinal");
+        evar_init = CheckEVarInit(s);
+        evar_init_to_correct_ordinal = s == "\"42\"";
+        return true;
+      }));
   EXPECT_EQ(1, call_count);
   EXPECT_TRUE(key_was_ordinal);
   EXPECT_TRUE(evar_init_to_correct_ordinal);
@@ -1971,28 +1964,22 @@ fact_name: "/"
   bool key_was_ordinal = false;
   bool evar_init = false;
   bool evar_init_to_correct_ordinal = false;
-  ASSERT_TRUE(
-      v.VerifyAllGoals([&call_count, &key_was_ordinal, &evar_init,
-                        &evar_init_to_correct_ordinal](
-                           Verifier* cxt, const Inspection& inspection) {
+  ASSERT_TRUE(v.VerifyAllGoals(
+      [&call_count, &key_was_ordinal, &evar_init,
+       &evar_init_to_correct_ordinal](
+          Verifier* cxt, const Inspection& inspection, std::string_view s) {
         ++call_count;
         key_was_ordinal = (inspection.label == "Ordinal");
-        if (AstNode* node = inspection.evar->current()) {
-          evar_init = true;
-          if (Identifier* identifier = node->AsIdentifier()) {
-            evar_init_to_correct_ordinal =
-                cxt->symbol_table()->text(identifier->symbol()) == "42";
-          }
-        }
+        evar_init = CheckEVarInit(s);
+        evar_init_to_correct_ordinal = s == "\"42\"";
         return true;
       }));
   EXPECT_EQ(1, call_count);
   EXPECT_TRUE(key_was_ordinal);
   EXPECT_TRUE(evar_init_to_correct_ordinal);
 }
 
-TEST(VerifierUnitTest, EvarsAndIdentifiersCanHaveTheSameText) {
-  Verifier v;
+TEST_P(VerifierTest, EvarsAndIdentifiersCanHaveTheSameText) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
 #- vname(Signature?, "Signature", Root?, Path?, Language?) defines SomeNode
 source {
@@ -2012,23 +1999,17 @@ fact_value: ""
   bool root = false;
   bool path = false;
   bool language = false;
-  ASSERT_TRUE(v.VerifyAllGoals([&signature, &root, &path, &language](
-                                   Verifier* cxt,
-                                   const Inspection& inspection) {
-    if (AstNode* node = inspection.evar->current()) {
-      if (Identifier* ident = node->AsIdentifier()) {
-        std::string ident_content = cxt->symbol_table()->text(ident->symbol());
-        if (ident_content == inspection.label) {
-          if (inspection.label == "Signature") signature = true;
-          if (inspection.label == "Root") root = true;
-          if (inspection.label == "Path") path = true;
-          if (inspection.label == "Language") language = true;
-        }
-      }
-      return true;
-    }
-    return false;
-  }));
+  ASSERT_TRUE(v.VerifyAllGoals(
+      [&signature, &root, &path, &language](
+          Verifier* cxt, const Inspection& inspection, std::string_view s) {
+        fprintf(stderr, "%s %s\n", inspection.label.c_str(),
+                std::string(s).c_str());
+        if (inspection.label == "Signature") signature = s == "Signature";
+        if (inspection.label == "Root") root = s == "Root";
+        if (inspection.label == "Path") path = s == "Path";
+        if (inspection.label == "Language") language = s == "Language";
+        return true;
+      }));
   EXPECT_TRUE(signature);
   EXPECT_TRUE(root);
   EXPECT_TRUE(path);