Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(verifier): naive implementation of groups for new solver #5680

Merged
merged 6 commits into from
May 31, 2023
Merged

feat(verifier): naive implementation of groups for new solver #5680

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
b2e9cab
feat(verifier): naive implementation of groups for new solver
zrlk May 31, 2023
eafda3c
fix: we want an aggregate, not negation
zrlk May 31, 2023
894fcb6
fix: clean up
zrlk May 31, 2023
2b51d67
fix: clean up again
zrlk May 31, 2023
d85ed67
fix: clean up again x2
zrlk May 31, 2023
f9081c5
git push origin svgroupsMerge branch 'master' into svgroups
zrlk May 31, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
133 changes: 73 additions & 60 deletions kythe/cxx/verifier/assertions_to_souffle.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,74 +72,88 @@ bool SouffleProgram::LowerSubexpression(AstNode* node) {

bool SouffleProgram::LowerGoalGroup(const SymbolTable& symbol_table,
const GoalGroup& group) {
auto eq_sym = symbol_table.MustIntern("=");
auto empty_sym = symbol_table.MustIntern("");
#ifdef DEBUG_LOWERING
FileHandlePrettyPrinter dprinter(stderr);
#endif
for (const auto& goal : group.goals) {
#ifdef DEBUG_LOWERING
dprinter.Print("goal <");
goal->Dump(symbol_table, &dprinter);
dprinter.Print(">\n");
size_t ccode = code_.size();
}
size_t ccode = code_.size();
#endif
auto* app = goal->AsApp();
auto* tup = app->rhs()->AsTuple();
if (app->lhs()->AsIdentifier()->symbol() == eq_sym) {
auto* evar = tup->element(1)->AsEVar();
if (evar == nullptr) {
LOG(ERROR) << "expected evar on rhs of eq";
return false;
}
if (auto* range = tup->element(0)->AsRange()) {
auto beginsym =
symbol_table.FindInterned(std::to_string(range->begin()));
auto endsym = symbol_table.FindInterned(std::to_string(range->end()));
if (!beginsym || !endsym) {
// 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->path(), ", ",
range->root(), ", _]");
absl::StrAppend(&code_, ", at(", *beginsym, ", ", *endsym, ", v",
FindEVar(evar), ")");
}
if (group.goals.empty()) return true;
bool pos = group.accept_if != GoalGroup::AcceptanceCriterion::kSomeMustFail;
if (pos) {
absl::StrAppend(&code_, ", (true");
for (const auto& goal : group.goals) {
if (!LowerGoal(symbol_table, goal)) return false;
}
absl::StrAppend(&code_, ")\n");
} else {
absl::StrAppend(&code_, ", 0 = count:{true");
for (const auto& goal : group.goals) {
if (!LowerGoal(symbol_table, goal)) return false;
}
absl::StrAppend(&code_, "}\n");
}
#ifdef DEBUG_LOWERING
dprinter.Print(" => <");
dprinter.Print(code_.substr(ccode, code_.size() - ccode));
dprinter.Print("> \n");
#endif
return true;
}

bool SouffleProgram::LowerGoal(const SymbolTable& symbol_table, AstNode* goal) {
auto eq_sym = symbol_table.MustIntern("=");
auto empty_sym = symbol_table.MustIntern("");
auto* app = goal->AsApp();
auto* tup = app->rhs()->AsTuple();
if (app->lhs()->AsIdentifier()->symbol() == eq_sym) {
auto* evar = tup->element(1)->AsEVar();
if (evar == nullptr) {
LOG(ERROR) << "expected evar on rhs of eq";
return false;
}
if (auto* range = tup->element(0)->AsRange()) {
auto beginsym = symbol_table.FindInterned(std::to_string(range->begin()));
auto endsym = symbol_table.FindInterned(std::to_string(range->end()));
if (!beginsym || !endsym) {
// TODO(zarko): emit a warning here (if we're in a positive goal)?
absl::StrAppend(&code_, ", false");
} else {
auto* oevar = tup->element(0)->AsEVar();
if (oevar == nullptr) {
LOG(ERROR) << "expected evar or range on lhs of eq";
return false;
}
absl::StrAppend(&code_, ", v", FindEVar(evar), "=v", FindEVar(oevar));
absl::StrAppend(&code_, ", v", FindEVar(evar), "=[_, ", range->corpus(),
", ", range->path(), ", ", range->root(), ", _]");
absl::StrAppend(&code_, ", at(", *beginsym, ", ", *endsym, ", v",
FindEVar(evar), ")");
}
} else {
// This is an edge or fact pattern.
absl::StrAppend(&code_, ", entry(");
for (size_t p = 0; p < 5; ++p) {
if (p != 0) {
absl::StrAppend(&code_, ", ");
}
if (p == 2 && tup->element(p)->AsIdentifier() &&
tup->element(p)->AsIdentifier()->symbol() == empty_sym) {
// Facts have nil vnames in the target position.
absl::StrAppend(&code_, "nil");
continue;
}
if (!LowerSubexpression(tup->element(p))) {
return false;
}
auto* oevar = tup->element(0)->AsEVar();
if (oevar == nullptr) {
LOG(ERROR) << "expected evar or range on lhs of eq";
return false;
}
absl::StrAppend(&code_, ")");
absl::StrAppend(&code_, ", v", FindEVar(evar), "=v", FindEVar(oevar));
}
#ifdef DEBUG_LOWERING
dprinter.Print(" => <");
dprinter.Print(code_.substr(ccode, code_.size() - ccode));
dprinter.Print("> \n");
#endif
} else {
// This is an edge or fact pattern.
absl::StrAppend(&code_, ", entry(");
for (size_t p = 0; p < 5; ++p) {
if (p != 0) {
absl::StrAppend(&code_, ", ");
}
if (p == 2 && tup->element(p)->AsIdentifier() &&
tup->element(p)->AsIdentifier()->symbol() == empty_sym) {
// Facts have nil vnames in the target position.
absl::StrAppend(&code_, "nil");
continue;
}
if (!LowerSubexpression(tup->element(p))) {
return false;
}
}
absl::StrAppend(&code_, ")");
}
absl::StrAppend(&code_, ".\n");
return true;
}

Expand All @@ -153,14 +167,13 @@ bool SouffleProgram::Lower(const SymbolTable& symbol_table,
symbol_table.MustIntern("/kythe/loc/start"),
symbol_table.MustIntern("/kythe/loc/end"));
}
CHECK_LE(goal_groups.size(), 1) << "(unimplemented)";
if (goal_groups.size() == 0) {
absl::StrAppend(&code_, ".\n");
return true;
}
for (const auto& group : goal_groups) {
if (!LowerGoalGroup(symbol_table, group)) return false;
}
absl::StrAppend(&code_, ".\n");
#ifdef DEBUG_LOWERING
fprintf(stderr, "<%s>\n", code_.c_str());
#endif
return true;
}
} // namespace kythe::verifier
13 changes: 8 additions & 5 deletions kythe/cxx/verifier/assertions_to_souffle.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,20 +43,23 @@ class SouffleProgram {
/// \brief Lowers `node`.
bool LowerSubexpression(AstNode* node);

/// \brief Lowers a goal from `group`.
bool LowerGoal(const SymbolTable& symbol_table, AstNode* node);

/// \brief Lowers `group`.
bool LowerGoalGroup(const SymbolTable& symbol_table, const GoalGroup& group);

/// \return a stable short name for `ev`.
size_t FindEVar(EVar* ev) {
return evars_.try_emplace(ev, evars_.size()).first->second;
}

/// The current finished code buffer.
std::string code_;

/// Whether to emit the prelude.
bool emit_prelude_ = true;

/// \return a stable short name for `evar`.
size_t FindEVar(EVar* evar) {
return evars_.try_emplace(evar, evars_.size()).first->second;
}

/// Known evars.
absl::flat_hash_map<EVar*, size_t> evars_;
};
Expand Down
35 changes: 17 additions & 18 deletions kythe/cxx/verifier/verifier_unit_test.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1321,8 +1321,7 @@ fact_value: ""
EXPECT_TRUE(evar_set);
}

TEST(VerifierUnitTest, GroupFactFails) {
Verifier v;
TEST_P(VerifierTest, GroupFactFails) {
ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
#- { SomeNode.content 43 }
source { root:"1" }
Expand All @@ -1334,8 +1333,11 @@ fact_value: "42"
}

// Slightly brittle in that it depends on the order we try facts.
TEST(VerifierUnitTest, FailWithCutInGroups) {
Verifier v;
TEST_P(VerifierTest, FailWithCutInGroups) {
if (GetParam() == Solver::New) {
// The new solver will pick the second entry.
GTEST_SKIP();
}
ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
#- { SomeNode.content SomeValue }
#- { SomeNode.content 43 }
Expand All @@ -1353,8 +1355,11 @@ fact_value: "43"
}

// Slightly brittle in that it depends on the order we try facts.
TEST(VerifierUnitTest, FailWithCut) {
Verifier v;
TEST_P(VerifierTest, FailWithCut) {
if (GetParam() == Solver::New) {
// The new solver will pick the second entry.
GTEST_SKIP();
}
ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
#- SomeNode.content SomeValue
#- { SomeNode.content 43 }
Expand Down Expand Up @@ -1388,8 +1393,7 @@ fact_value: "43"
ASSERT_TRUE(v.VerifyAllGoals());
}

TEST(VerifierUnitTest, GroupFactPasses) {
Verifier v;
TEST_P(VerifierTest, GroupFactPasses) {
ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
#- { SomeNode.content 42 }
source { root:"1" }
Expand All @@ -1400,8 +1404,7 @@ fact_value: "42"
ASSERT_TRUE(v.VerifyAllGoals());
}

TEST(VerifierUnitTest, CompoundGroups) {
Verifier v;
TEST_P(VerifierTest, CompoundGroups) {
ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
#- SomeNode.content 42
#- !{ OtherNode.content 43
Expand All @@ -1421,8 +1424,7 @@ fact_value: "43"
ASSERT_TRUE(v.VerifyAllGoals());
}

TEST(VerifierUnitTest, ConjunctionInsideNegatedGroupPassFail) {
Verifier v;
TEST_P(VerifierTest, ConjunctionInsideNegatedGroupPassFail) {
ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
#- !{ SomeNode.content 42
#- OtherNode.content 44 }
Expand All @@ -1440,8 +1442,7 @@ fact_value: "43"
ASSERT_TRUE(v.VerifyAllGoals());
}

TEST(VerifierUnitTest, ConjunctionInsideNegatedGroupPassPass) {
Verifier v;
TEST_P(VerifierTest, ConjunctionInsideNegatedGroupPassPass) {
ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
#- !{ SomeNode.content 42
#- OtherNode.content 43 }
Expand All @@ -1459,8 +1460,7 @@ fact_value: "43"
ASSERT_FALSE(v.VerifyAllGoals());
}

TEST(VerifierUnitTest, AntiContentFactFails) {
Verifier v;
TEST_P(VerifierTest, AntiContentFactFails) {
ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
#- !{ SomeNode.content 42 }
source { root:"1" }
Expand All @@ -1471,8 +1471,7 @@ fact_value: "42"
ASSERT_FALSE(v.VerifyAllGoals());
}

TEST(VerifierUnitTest, AntiContentFactPasses) {
Verifier v;
TEST_P(VerifierTest, AntiContentFactPasses) {
ASSERT_TRUE(v.LoadInlineProtoFile(R"(entries {
#- !{ SomeNode.content 43 }
source { root:"1" }
Expand Down