fix(verifier): various fixes for new solver (#5830)

* improve some diagnostics (evar numbers instead of <nil>)
  * don't run inspections on empty output
  * make range expressions work under equalities
  * pass in a proper root in a test (the old solver by default didn't care)
  * document the need to deal with evar type equality

kythe/cxx/verifier/assertions_to_souffle.cc

@@ -142,8 +142,11 @@ bool SouffleProgram::LowerGoal(const SymbolTable& symbol_table, AstNode* goal) {
         // 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->root(), ", ", range->path(), ", _]");
+        // We need to name the elements of the range; otherwise the compiler
+        // will complain that they are ungrounded in certain cases.
+        absl::StrAppend(&code_, ", v", FindEVar(evar), "=[v", FindEVar(evar),
+                        "r1, ", range->corpus(), ", ", range->root(), ", ",
+                        range->path(), ", v", FindEVar(evar), "r2]");
         // TODO(zarko): there might be a cleaner way to handle eq_sym; it would
         // need LowerSubexpression to be able to emit this as a side-clause.
         absl::StrAppend(&code_, ", at(", *beginsym, ", ", *endsym, ", v",
@@ -223,15 +226,11 @@ bool SouffleProgram::Lower(const SymbolTable& symbol_table,
     for (const auto& i : inspections) {
       auto type = evar_types_.find(i.evar);
       if (type == evar_types_.end()) {
-        StringPrettyPrinter sp;
-        i.evar->Dump(symbol_table, &sp);
-        LOG(ERROR) << "evar typing missing for " << sp.str();
+        LOG(ERROR) << "evar typing missing for v" << FindEVar(i.evar);
         return false;
       }
       if (type->second == EVarType::kUnknown) {
-        StringPrettyPrinter sp;
-        i.evar->Dump(symbol_table, &sp);
-        LOG(ERROR) << "evar typing unknown for " << sp.str();
+        LOG(ERROR) << "evar typing unknown for v" << FindEVar(i.evar);
         return false;
       }
       auto id = FindEVar(i.evar);

kythe/cxx/verifier/souffle_interpreter.cc

@@ -276,6 +276,8 @@ SouffleResult RunSouffle(
       souffle::mk<souffle::interpreter::Engine>(*ram_tu));
   interpreter->executeMain();
   const auto& actual = write_stream_factory->GetOutput(output_id);
+  result.success = (!actual.outputs.empty());
+  if (!result.success) return result;
   for (const auto& i : inspections) {
     auto ix = output_indices.find(i.evar);
     if (ix != output_indices.end()) {
@@ -287,7 +289,6 @@ SouffleResult RunSouffle(
                  << i.label;
     }
   }
-  result.success = (!actual.outputs.empty());
   return result;
 }
 }  // namespace kythe::verifier

kythe/cxx/verifier/verifier_unit_test.cc

@@ -2072,8 +2072,7 @@ target { root:"3" }
       }));
 }
 
-TEST(VerifierUnitTest, EqualityConstraintWorksOnAnchors) {
-  Verifier v;
+TEST_P(VerifierTest, EqualityConstraintWorksOnAnchors) {
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
 #- Tx?=@text defines SomeNode
 ##text (line 3 column 2 offset 42-46)
@@ -2097,11 +2096,50 @@ edge_kind: "/kythe/edge/defines"
 target { root:"2" }
 fact_name: "/"
 fact_value: ""
-})"));
+})",
+                                    "", "1"));
   ASSERT_TRUE(v.PrepareDatabase());
-  ASSERT_TRUE(v.VerifyAllGoals([](Verifier* cxt, const Inspection& inspection) {
-    return (inspection.label == "Tx" && inspection.evar->current() != nullptr);
-  }));
+  ASSERT_TRUE(v.VerifyAllGoals(
+      [](Verifier* cxt, const Inspection& inspection, std::string_view s) {
+        return (inspection.label == "Tx" && !s.empty());
+      }));
+}
+
+TEST_P(VerifierTest, EqualityConstraintWorksOnAnchorsRev) {
+  if (GetParam() == Solver::New) {
+    // TODO: Turns out that we do need to propagate (type) equality constraints.
+    GTEST_SKIP();
+  }
+  ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
+#- @text=Tx? defines SomeNode
+##text (line 3 column 2 offset 42-46)
+source { root:"1" }
+fact_name: "/kythe/node/kind"
+fact_value: "anchor"
+}
+entries {
+source { root:"1" }
+fact_name: "/kythe/loc/start"
+fact_value: "42"
+}
+entries {
+source { root:"1" }
+fact_name: "/kythe/loc/end"
+fact_value: "46"
+}
+entries {
+source { root:"1" }
+edge_kind: "/kythe/edge/defines"
+target { root:"2" }
+fact_name: "/"
+fact_value: ""
+})",
+                                    "", "1"));
+  ASSERT_TRUE(v.PrepareDatabase());
+  ASSERT_TRUE(v.VerifyAllGoals(
+      [](Verifier* cxt, const Inspection& inspection, std::string_view s) {
+        return (inspection.label == "Tx" && !s.empty());
+      }));
 }
 
 // It's possible to match Tx against {root:7}: