From 102285806d5891adb177cfa88e755515292f5dcc Mon Sep 17 00:00:00 2001 From: zrlk Date: Thu, 16 Nov 2023 17:55:11 -0500 Subject: [PATCH] feat(verifier): avoid the arity ceiling in outputs (#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 | 35 ++++++++++++++---- kythe/cxx/verifier/souffle_interpreter.cc | 4 +- kythe/cxx/verifier/verifier_unit_test.cc | 41 +++++++++++++++++++++ 3 files changed, 71 insertions(+), 9 deletions(-) diff --git a/kythe/cxx/verifier/assertions_to_souffle.cc b/kythe/cxx/verifier/assertions_to_souffle.cc index 8a43bbc996..5d95dfbb2a 100644 --- a/kythe/cxx/verifier/assertions_to_souffle.cc +++ b/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 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"); diff --git a/kythe/cxx/verifier/souffle_interpreter.cc b/kythe/cxx/verifier/souffle_interpreter.cc index 020bb8be49..8c9a16a917 100644 --- a/kythe/cxx/verifier/souffle_interpreter.cc +++ b/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(); diff --git a/kythe/cxx/verifier/verifier_unit_test.cc b/kythe/cxx/verifier/verifier_unit_test.cc index a5c36aceb3..7d82825d7c 100644 --- a/kythe/cxx/verifier/verifier_unit_test.cc +++ b/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 {