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): support error recovery with the fast solver #5915

Merged
merged 1 commit into from
Nov 2, 2023
Merged

feat(verifier): support error recovery with the fast solver #5915

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 2 additions & 0 deletions kythe/cxx/verifier/BUILD
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ cc_library(
":lexparse",
"//third_party/souffle:parse_transform",
"@com_google_absl//absl/container:flat_hash_map",
"@com_google_absl//absl/log",
"@com_google_absl//absl/log:check",
"@com_google_absl//absl/strings",
"@souffle",
Expand Down Expand Up @@ -95,6 +96,7 @@ cc_library(
deps = [
":lexparse",
":pretty_printer",
"@com_google_absl//absl/base:core_headers",
"@com_google_absl//absl/container:flat_hash_map",
"@com_google_absl//absl/container:flat_hash_set",
"@com_google_absl//absl/strings",
Expand Down
40 changes: 37 additions & 3 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 @@ -50,6 +50,29 @@ result($6) :- true
)";
}

bool SouffleErrorState::NextStep() {
if (goal_groups_->empty()) return false;
if (target_group_ < 0) {
target_group_ = static_cast<int>(goal_groups_->size()) - 1;
target_goal_ = (*goal_groups_)[target_group_].goals.size();
}
--target_goal_;
if (target_goal_ >= 0) {
return true;
}
// We need to handle empty groups.
while (target_goal_ < 0) {
--target_group_;
if (target_group_ < 0) {
return false;
}
target_goal_ =
static_cast<int>((*goal_groups_)[target_group_].goals.size()) - 1;
}
// target_group_ and target_goal_ >= 0.
return true;
}

bool SouffleProgram::LowerSubexpression(AstNode* node, EVarType type) {
if (auto* app = node->AsApp()) {
auto* tup = app->rhs()->AsTuple();
Expand Down Expand Up @@ -99,7 +122,7 @@ bool SouffleProgram::AssignEVarType(EVar* evar, EVar* oevar) {
}

bool SouffleProgram::LowerGoalGroup(const SymbolTable& symbol_table,
const GoalGroup& group) {
const GoalGroup& group, int target_goal) {
#ifdef DEBUG_LOWERING
FileHandlePrettyPrinter dprinter(stderr);
for (const auto& goal : group.goals) {
Expand All @@ -111,15 +134,20 @@ bool SouffleProgram::LowerGoalGroup(const SymbolTable& symbol_table,
#endif
if (group.goals.empty()) return true;
bool pos = group.accept_if != GoalGroup::AcceptanceCriterion::kSomeMustFail;
int cur_goal = 0;
if (pos) {
absl::StrAppend(&code_, ", (true");
for (const auto& goal : group.goals) {
if (target_goal >= 0 && cur_goal > target_goal) break;
++cur_goal;
if (!LowerGoal(symbol_table, goal)) return false;
}
absl::StrAppend(&code_, ")\n");
} else {
absl::StrAppend(&code_, ", 0 = count:{true, sym(_)");
for (const auto& goal : group.goals) {
if (target_goal >= 0 && cur_goal > target_goal) break;
++cur_goal;
if (!LowerGoal(symbol_table, goal)) return false;
}
absl::StrAppend(&code_, "}\n");
Expand Down Expand Up @@ -215,10 +243,16 @@ bool SouffleProgram::LowerGoal(const SymbolTable& symbol_table, AstNode* goal) {

bool SouffleProgram::Lower(const SymbolTable& symbol_table,
const std::vector<GoalGroup>& goal_groups,
const std::vector<Inspection>& inspections) {
const std::vector<Inspection>& inspections,
const SouffleErrorState& error_state) {
code_.clear();
int cur_group = 0;
for (const auto& group : goal_groups) {
if (!LowerGoalGroup(symbol_table, group)) return false;
if (error_state.IsFinished(cur_group)) break;
if (!LowerGoalGroup(symbol_table, group,
error_state.GoalForGroup(cur_group)))
return false;
++cur_group;
}
if (emit_prelude_) {
std::string code;
Expand Down
45 changes: 43 additions & 2 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 @@ -20,6 +20,7 @@
#include <optional>
#include <string>

#include "absl/base/attributes.h"
#include "absl/container/flat_hash_map.h"
#include "absl/strings/string_view.h"
#include "kythe/cxx/verifier/assertion_ast.h"
Expand All @@ -28,6 +29,44 @@ namespace kythe::verifier {
/// \brief Inferred type for an EVar.
enum class EVarType { kVName, kSymbol, kUnknown };

/// The error recovery state for a particular list of goal groups.
class SouffleErrorState {
public:
/// Creates a new error state for `goal_groups`. `goal_groups` should equal or
/// exceed the lifetime of any bound `SouffleErrorState`.
explicit SouffleErrorState(
const std::vector<GoalGroup>* goal_groups ABSL_ATTRIBUTE_LIFETIME_BOUND)
: goal_groups_(goal_groups) {}
SouffleErrorState(const SouffleErrorState&) = delete;
SouffleErrorState& operator=(const SouffleErrorState&) = delete;
/// Advances the error state by one step.
/// \return true if the solver should continue to run.
bool NextStep();
/// \return the current highest group to solve (or -1 if uninitialized).
int target_group() const { return target_group_; }
/// \return the current highest goal to solve (ignored if target_group is
/// invalid).
int target_goal() const { return target_goal_; }
/// \return whether `group` (and subsequent groups) have already been
/// explored during error recovery.
bool IsFinished(int group) const {
return target_group_ >= 0 && group > target_group_;
}
/// \return the target goal for `group`, or -1 if all goals should be
/// explored given a valid `group`.
int GoalForGroup(int group) const {
return group == target_group_ ? target_goal_ : -1;
}

private:
/// The goal groups being solved. Not owned.
const std::vector<GoalGroup>* goal_groups_;
/// The current highest group to solve (or -1 if uninitialized).
int target_group_ = -1;
/// The current highest goal to solve (ignored if target_group_ is invalid).
int target_goal_ = -1;
};

/// \brief Packages together for a possibly multistage Souffle program.
class SouffleProgram {
public:
Expand All @@ -37,7 +76,8 @@ class SouffleProgram {
/// \param inspections inspections to perform.
bool Lower(const SymbolTable& symbol_table,
const std::vector<GoalGroup>& goal_groups,
const std::vector<Inspection>& inspections);
const std::vector<Inspection>& inspections,
const SouffleErrorState& error_state);

/// \return the lowered Souffle code.
absl::string_view code() { return code_; }
Expand All @@ -61,7 +101,8 @@ class SouffleProgram {
bool LowerGoal(const SymbolTable& symbol_table, AstNode* goal);

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

/// \brief Assigns or checks `evar`'s type against `type`.
bool AssignEVarType(EVar* evar, EVarType type);
Expand Down
104 changes: 103 additions & 1 deletion kythe/cxx/verifier/assertions_to_souffle_test.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,12 @@

#include "kythe/cxx/verifier/assertions_to_souffle.h"

#include <cstddef>
#include <string>
#include <vector>

#include "absl/log/check.h"
#include "absl/strings/string_view.h"
#include "absl/strings/strip.h"
#include "absl/types/span.h"
#include "gtest/gtest.h"
Expand Down Expand Up @@ -67,7 +72,9 @@ class AstTest : public ::testing::Test {

/// \return the generated program without boilerplate
absl::string_view MustGenerateProgram() {
CHECK(p_.Lower(symbol_table_, {}, {}));
std::vector<GoalGroup> groups;
SouffleErrorState error_state(&groups);
CHECK(p_.Lower(symbol_table_, groups, {}, error_state));
auto code = p_.code();
CHECK(absl::ConsumeSuffix(&code, ".\n"));
return code;
Expand All @@ -87,5 +94,100 @@ TEST_F(AstTest, SelfTest) {
}

TEST_F(AstTest, EmptyProgramTest) { EXPECT_EQ("", MustGenerateProgram()); }

TEST(ErrorStateTest, NoGroups) {
std::vector<GoalGroup> groups;
SouffleErrorState error_state(&groups);
EXPECT_FALSE(error_state.NextStep());
}

TEST(ErrorStateTest, Empty) {
std::vector<GoalGroup> groups{{}};
SouffleErrorState error_state(&groups);
EXPECT_FALSE(error_state.NextStep());
}

TEST(ErrorStateTest, SimpleStep) {
std::vector<GoalGroup> groups{{.goals = {nullptr}}};
SouffleErrorState error_state(&groups);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 0);
EXPECT_EQ(error_state.target_goal(), 0);
EXPECT_EQ(error_state.GoalForGroup(0), 0);
EXPECT_FALSE(error_state.NextStep());
}

TEST(ErrorStateTest, MultiStep) {
std::vector<GoalGroup> groups{{.goals = {nullptr, nullptr}}};
SouffleErrorState error_state(&groups);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 0);
EXPECT_EQ(error_state.target_goal(), 1);
EXPECT_EQ(error_state.GoalForGroup(0), 1);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 0);
EXPECT_EQ(error_state.target_goal(), 0);
EXPECT_EQ(error_state.GoalForGroup(0), 0);
EXPECT_FALSE(error_state.NextStep());
}

TEST(ErrorStateTest, MultiGroupSingleStep) {
std::vector<GoalGroup> groups{{.goals = {nullptr}}, {.goals = {nullptr}}};
SouffleErrorState error_state(&groups);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 1);
EXPECT_EQ(error_state.target_goal(), 0);
EXPECT_EQ(error_state.GoalForGroup(1), 0);
EXPECT_EQ(error_state.GoalForGroup(0), -1);
EXPECT_EQ(error_state.IsFinished(1), false);
EXPECT_EQ(error_state.IsFinished(0), false);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 0);
EXPECT_EQ(error_state.target_goal(), 0);
EXPECT_EQ(error_state.GoalForGroup(0), 0);
EXPECT_EQ(error_state.IsFinished(1), true);
EXPECT_EQ(error_state.IsFinished(0), false);
EXPECT_FALSE(error_state.NextStep());
}

TEST(ErrorStateTest, MultiGroupMultiStep) {
std::vector<GoalGroup> groups{{.goals = {nullptr, nullptr}},
{.goals = {nullptr, nullptr}}};
SouffleErrorState error_state(&groups);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 1);
EXPECT_EQ(error_state.target_goal(), 1);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 1);
EXPECT_EQ(error_state.target_goal(), 0);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 0);
EXPECT_EQ(error_state.target_goal(), 1);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 0);
EXPECT_EQ(error_state.target_goal(), 0);
EXPECT_FALSE(error_state.NextStep());
}

TEST(ErrorStateTest, SkipEmptyGroups) {
std::vector<GoalGroup> groups{
{}, {}, {.goals = {nullptr}}, {}, {}, {.goals = {nullptr}}, {}, {}};
SouffleErrorState error_state(&groups);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 5);
EXPECT_EQ(error_state.target_goal(), 0);
EXPECT_EQ(error_state.GoalForGroup(5), 0);
EXPECT_EQ(error_state.GoalForGroup(4), -1);
EXPECT_EQ(error_state.IsFinished(5), false);
EXPECT_EQ(error_state.IsFinished(6), true);
EXPECT_EQ(error_state.IsFinished(7), true);
ASSERT_TRUE(error_state.NextStep());
EXPECT_EQ(error_state.target_group(), 2);
EXPECT_EQ(error_state.target_goal(), 0);
EXPECT_EQ(error_state.IsFinished(5), true);
EXPECT_EQ(error_state.IsFinished(2), false);
EXPECT_EQ(error_state.GoalForGroup(2), 0);
EXPECT_FALSE(error_state.NextStep());
}
} // anonymous namespace
} // namespace kythe::verifier