feat(verifier): avoid the arity ceiling in outputs (kythe#5939)

* feat(verifier): avoid the arity ceiling in outputs

The new solver/Souffle has a hard limit on the arity of relations.
This is tunable but requires a change to the library. Before this PR,
that limit (20 as I write this) was easy to reach through inspections,
especially when `--annotated_graphviz` is on (which adds an inspection
to *every* evar). Luckily, this limit does not apply to records.
This PR changes lowering to use a unary output relation when
inspections are on. The single element is a record containing the
values of the inspected evars.

kythe/cxx/verifier/assertions_to_souffle.cc

@@ -47,8 +47,9 @@ sym(n + 1) :- sym(n), n >= 1.
 at(s, e, v) :- entry(v, $0, nil, $1, $2),
                entry(v, $0, nil, $3, s),
                entry(v, $0, nil, $4, e).
-.decl result($5)
-result($6) :- true
+$5
+.decl result($6)
+result($7) :- true$8
 )";
 }  // namespace
 
@@ -267,8 +268,11 @@ bool SouffleProgram::Lower(const SymbolTable& symbol_table,
   if (emit_prelude_) {
     std::string code;
     code_.swap(code);
-    std::string result_tyspec;
-    std::string result_spec;
+    std::string result_tyspec;  // ".type result_ty = ..." or ""
+    std::string result_spec;    // .decl result($result_spec)
+    std::string
+        result_argspec;  // result($result_argspec) :- true$result_clause
+    std::string result_clause;
     absl::flat_hash_set<size_t> inspected_vars;
     for (const auto& i : inspections) {
       auto type = evar_types_.find(i.evar);
@@ -294,19 +298,34 @@ bool SouffleProgram::Lower(const SymbolTable& symbol_table,
       }
       auto id = FindEVar(i.evar);
       if (inspected_vars.insert(id).second) {
-        absl::StrAppend(&result_spec, result_spec.empty() ? "" : ", ", "v", id);
-        absl::StrAppend(&result_tyspec, result_tyspec.empty() ? "" : ", ", "v",
-                        id, ":",
+        if (result_spec.empty()) {
+          result_spec = "rrec : result_ty";
+          result_argspec = "rrec";
+        }
+        absl::StrAppend(&result_clause,
+                        result_clause.empty() ? ", rrec=[" : ", ", "v", id);
+        absl::StrAppend(&result_tyspec,
+                        result_tyspec.empty() ? ".type result_ty = [" : ", ",
+                        "rv", id, ":",
                         type->second == EVarType::kVName ? "vname" : "number");
+
         inspections_.push_back(i.evar);
       }
     }
+    if (!result_spec.empty()) {
+      // result_ty has been defined and will always be a record with at least
+      // one element; we need to terminate both the type definition and the
+      // record expression.
+      absl::StrAppend(&result_tyspec, "]");
+      absl::StrAppend(&result_clause, "]");
+    }
     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"),
-                             result_tyspec, result_spec);
+                             result_tyspec, result_spec, result_argspec,
+                             result_clause);
     absl::StrAppend(&code_, code);
   }
   absl::StrAppend(&code_, ".\n");

kythe/cxx/verifier/souffle_interpreter.cc

@@ -168,11 +168,13 @@ class KytheWriteStream : public souffle::WriteStream {
  protected:
   void writeNullary() override { output_->outputs.push_back(""); }
 
-  void writeNextTuple(const souffle::RamDomain* tuple) override {
+  void writeNextTuple(const souffle::RamDomain* result_tuple) override {
     if (output_types_.empty()) {
       output_->outputs.push_back("");
       return;
     }
+    const auto* tuple =
+        recordTable.unpack(result_tuple[0], output_types_.size());
     for (size_t ox = 0; ox < output_types_.size(); ++ox) {
       output_->outputs.push_back("");
       auto* o = &output_->outputs.back();

kythe/cxx/verifier/verifier_unit_test.cc

@@ -1906,6 +1906,47 @@ fact_value: ""
       v.VerifyAllGoals([](Verifier* cxt, const Inspection&) { return true; }));
 }
 
+TEST_P(VerifierTest, ManyInspectionsDontUpsetSolver) {
+  // Souffle ships with a default max arity of 20 and will abort if it hits a
+  // larger (output) relation. Check that we handle this.
+  ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
+#- I01? defines SomeNode
+#- I02? defines SomeNode
+#- I03? defines SomeNode
+#- I04? defines SomeNode
+#- I05? defines SomeNode
+#- I06? defines SomeNode
+#- I07? defines SomeNode
+#- I08? defines SomeNode
+#- I09? defines SomeNode
+#- I10? defines SomeNode
+#- I11? defines SomeNode
+#- I12? defines SomeNode
+#- I13? defines SomeNode
+#- I14? defines SomeNode
+#- I15? defines SomeNode
+#- I16? defines SomeNode
+#- I17? defines SomeNode
+#- I18? defines SomeNode
+#- I19? defines SomeNode
+#- I20? defines SomeNode
+#- I21? defines SomeNode
+
+source { root:"1" }
+edge_kind: "/kythe/edge/defines"
+target { root:"2" }
+fact_name: "/"
+fact_value: ""
+})"));
+  int inspection_count = 0;
+  ASSERT_TRUE(v.PrepareDatabase());
+  ASSERT_TRUE(v.VerifyAllGoals([&](Verifier* cxt, const Inspection&) {
+    ++inspection_count;
+    return true;
+  }));
+  EXPECT_EQ(inspection_count, 21);
+}
+
 TEST(VerifierUnitTest, InspectionHappensMoreThanOnceAndThatsOk) {
   Verifier v;
   ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {