Skip to content

Commit

Permalink
feat(verifier): print inspections with fast solver (#5960)
Browse files Browse the repository at this point in the history 
This PR also gets rid of the compatibility API for
VerifyAllGoals that ignores the string_view (that the
fast solver fills with the pretty-printed value for the
inspection).

A future PR will change `saved_assignments_` and will
update the various graphviz printers to work with the fast
solver (again by using the pretty-printed values instead
of ast pointers, which we don't have anymore).
  • Loading branch information
@zrlk
zrlk committed Dec 7, 2023
1 parent 096ed9d commit cf876c3
Show file tree
Hide file tree
Showing 3 changed files with 57 additions and 65 deletions.
11 changes: 4 additions & 7 deletions kythe/cxx/verifier/verifier.cc
View file
Expand Up @@ -1011,14 +1011,11 @@ bool Verifier::VerifyAllGoals(
}

bool Verifier::VerifyAllGoals() {
return VerifyAllGoals([this](Verifier* context,
const Inspection& inspection) {
return VerifyAllGoals([this](Verifier* context, const Inspection& inspection,
std::string_view str) {
if (inspection.kind == Inspection::Kind::EXPLICIT) {
FileHandlePrettyPrinter printer(saving_assignments_ ? stderr : stdout);
printer.Print(inspection.label);
printer.Print(": ");
inspection.evar->Dump(symbol_table_, &printer);
printer.Print("\n");
absl::FPrintF(saving_assignments_ ? stderr : stdout, "%s: %s\n",
inspection.label, str);
}
if (inspection.evar->current()) {
saved_assignments_[inspection.label] = inspection.evar->current();
Expand Down
9 changes: 0 additions & 9 deletions kythe/cxx/verifier/verifier.h
View file
Expand Up @@ -99,15 +99,6 @@ class Verifier {
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::string_view) { return inspect(v, i); });
}

/// \brief Attempts to satisfy all goals from all loaded rule files and facts.
/// \return true if all goals could be satisfied.
bool VerifyAllGoals();
Expand Down
102 changes: 53 additions & 49 deletions kythe/cxx/verifier/verifier_unit_test.cc
View file
Expand Up @@ -1283,7 +1283,8 @@ fact_value: ""
bool evar_unset = false;
ASSERT_TRUE(v.PrepareDatabase());
ASSERT_TRUE(v.VerifyAllGoals(
[&call_count, &evar_unset](Verifier* cxt, const Inspection& inspection) {
[&call_count, &evar_unset](Verifier* cxt, const Inspection& inspection,
std::string_view) {
++call_count;
if (inspection.label == "Root" && !inspection.evar->current()) {
evar_unset = true;
Expand All @@ -1309,7 +1310,8 @@ fact_value: ""
bool evar_unset = false;
ASSERT_TRUE(v.PrepareDatabase());
ASSERT_TRUE(v.VerifyAllGoals(
[&call_count, &evar_unset](Verifier* cxt, const Inspection& inspection) {
[&call_count, &evar_unset](Verifier* cxt, const Inspection& inspection,
std::string_view) {
++call_count;
if (inspection.label == "Root" && !inspection.evar->current()) {
evar_unset = true;
Expand Down Expand Up @@ -1341,19 +1343,19 @@ fact_value: ""
size_t call_count = 0;
bool evar_set = false;
ASSERT_TRUE(v.PrepareDatabase());
ASSERT_FALSE(v.VerifyAllGoals(
[&call_count, &evar_set](Verifier* cxt, const Inspection& inspection) {
++call_count;
if (inspection.label == "Root" && inspection.evar->current()) {
if (Identifier* identifier =
inspection.evar->current()->AsIdentifier()) {
if (cxt->symbol_table()->text(identifier->symbol()) == "3") {
evar_set = true;
}
}
ASSERT_FALSE(v.VerifyAllGoals([&call_count, &evar_set](
Verifier* cxt, const Inspection& inspection,
std::string_view) {
++call_count;
if (inspection.label == "Root" && inspection.evar->current()) {
if (Identifier* identifier = inspection.evar->current()->AsIdentifier()) {
if (cxt->symbol_table()->text(identifier->symbol()) == "3") {
evar_set = true;
}
return true;
}));
}
}
return true;
}));
EXPECT_EQ(1, call_count);
EXPECT_TRUE(evar_set);
}
Expand All @@ -1379,19 +1381,19 @@ fact_value: ""
size_t call_count = 0;
bool evar_set = false;
ASSERT_TRUE(v.PrepareDatabase());
ASSERT_FALSE(v.VerifyAllGoals(
[&call_count, &evar_set](Verifier* cxt, const Inspection& inspection) {
++call_count;
if (inspection.label == "Root" && inspection.evar->current()) {
if (Identifier* identifier =
inspection.evar->current()->AsIdentifier()) {
if (cxt->symbol_table()->text(identifier->symbol()) == "3") {
evar_set = true;
}
}
ASSERT_FALSE(v.VerifyAllGoals([&call_count, &evar_set](
Verifier* cxt, const Inspection& inspection,
std::string_view) {
++call_count;
if (inspection.label == "Root" && inspection.evar->current()) {
if (Identifier* identifier = inspection.evar->current()->AsIdentifier()) {
if (cxt->symbol_table()->text(identifier->symbol()) == "3") {
evar_set = true;
}
return true;
}));
}
}
return true;
}));
EXPECT_EQ(1, call_count);
EXPECT_TRUE(evar_set);
}
Expand All @@ -1409,19 +1411,19 @@ fact_value: ""
size_t call_count = 0;
bool evar_set = false;
ASSERT_TRUE(v.PrepareDatabase());
ASSERT_FALSE(v.VerifyAllGoals(
[&call_count, &evar_set](Verifier* cxt, const Inspection& inspection) {
++call_count;
if (inspection.label == "Root" && inspection.evar->current()) {
if (Identifier* identifier =
inspection.evar->current()->AsIdentifier()) {
if (cxt->symbol_table()->text(identifier->symbol()) == "1") {
evar_set = true;
}
}
ASSERT_FALSE(v.VerifyAllGoals([&call_count, &evar_set](
Verifier* cxt, const Inspection& inspection,
std::string_view) {
++call_count;
if (inspection.label == "Root" && inspection.evar->current()) {
if (Identifier* identifier = inspection.evar->current()->AsIdentifier()) {
if (cxt->symbol_table()->text(identifier->symbol()) == "1") {
evar_set = true;
}
return true;
}));
}
}
return true;
}));
EXPECT_EQ(1, call_count);
EXPECT_TRUE(evar_set);
}
Expand Down Expand Up @@ -1889,8 +1891,8 @@ fact_name: "/"
fact_value: ""
})"));
ASSERT_TRUE(v.PrepareDatabase());
ASSERT_FALSE(
v.VerifyAllGoals([](Verifier* cxt, const Inspection&) { return false; }));
ASSERT_FALSE(v.VerifyAllGoals([](Verifier* cxt, const Inspection&,
std::string_view) { return false; }));
}

TEST(VerifierUnitTest, EvarsAreSharedAcrossInputFiles) {
Expand All @@ -1910,7 +1912,8 @@ fact_value: ""
EVar* seen_evar = nullptr;
int seen_count = 0;
ASSERT_TRUE(v.VerifyAllGoals(
[&seen_evar, &seen_count](Verifier* cxt, const Inspection& inspection) {
[&seen_evar, &seen_count](Verifier* cxt, const Inspection& inspection,
std::string_view) {
if (inspection.label == "SomeAnchor") {
++seen_count;
if (seen_evar == nullptr) {
Expand All @@ -1936,8 +1939,8 @@ fact_name: "/"
fact_value: ""
})"));
ASSERT_TRUE(v.PrepareDatabase());
ASSERT_TRUE(
v.VerifyAllGoals([](Verifier* cxt, const Inspection&) { return true; }));
ASSERT_TRUE(v.VerifyAllGoals(
[](Verifier* cxt, const Inspection&, std::string_view) { return true; }));
}

TEST_P(VerifierTest, ManyInspectionsDontUpsetSolver) {
Expand Down Expand Up @@ -1974,10 +1977,11 @@ fact_value: ""
})"));
int inspection_count = 0;
ASSERT_TRUE(v.PrepareDatabase());
ASSERT_TRUE(v.VerifyAllGoals([&](Verifier* cxt, const Inspection&) {
++inspection_count;
return true;
}));
ASSERT_TRUE(
v.VerifyAllGoals([&](Verifier* cxt, const Inspection&, std::string_view) {
++inspection_count;
return true;
}));
EXPECT_EQ(inspection_count, 21);
}

Expand All @@ -1994,8 +1998,8 @@ fact_value: ""
})"));
ASSERT_TRUE(v.PrepareDatabase());
size_t inspect_count = 0;
ASSERT_TRUE(
v.VerifyAllGoals([&inspect_count](Verifier* cxt, const Inspection&) {
ASSERT_TRUE(v.VerifyAllGoals(
[&inspect_count](Verifier* cxt, const Inspection&, std::string_view) {
++inspect_count;
return true;
}));
Expand Down

0 comments on commit cf876c3

Please sign in to comment.