Skip to content

Commit

Permalink
feat(verifier): begin supporting some forms (#5665)
Browse files Browse the repository at this point in the history 
* feat(verifier): begin supporting some forms

anchor() should probably be defined in terms of entry();
see the various TODOs for details.

In service of #4748
  • Loading branch information
@zrlk
zrlk committed May 30, 2023
1 parent c1a4536 commit 91d7cd0
Show file tree
Hide file tree
Showing 5 changed files with 172 additions and 54 deletions.
106 changes: 105 additions & 1 deletion kythe/cxx/verifier/assertions_to_souffle.cc
View file
Expand Up @@ -34,11 +34,115 @@ constexpr absl::string_view kGlobalDecls = R"(
result() :- true
)";
}

bool SouffleProgram::LowerSubexpression(AstNode* node) {
if (auto* app = node->AsApp()) {
auto* tup = app->rhs()->AsTuple();
absl::StrAppend(&code_, "[");
for (size_t p = 0; p < 5; ++p) {
if (p != 0) {
absl::StrAppend(&code_, ", ");
}
if (!LowerSubexpression(tup->element(p))) {
return false;
}
}
absl::StrAppend(&code_, "]");
return true;
} else if (auto* id = node->AsIdentifier()) {
absl::StrAppend(&code_, id->symbol());
return true;
} else if (auto* evar = node->AsEVar()) {
if (auto* evc = evar->current()) {
return LowerSubexpression(evc);
}
absl::StrAppend(&code_, "v", FindEVar(evar));
return true;
} else {
LOG(ERROR) << "unknown subexpression kind";
return false;
}
}

bool SouffleProgram::LowerGoalGroup(const SymbolTable& symbol_table,
const GoalGroup& group) {
auto eq_sym = const_cast<SymbolTable&>(symbol_table).intern("=");
auto empty_sym = const_cast<SymbolTable&>(symbol_table).intern("");
#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();
#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()) {
absl::StrAppend(&code_, ", v", FindEVar(evar), "=[_, ", range->corpus(),
", ", range->path(), ", ", range->root(), ", _]");
// TODO(zarko): derive an anchor relation (will need to convert
// range->begin, end to symbols; also need to get the relevant symbols
// included in the prelude) or populate the anchor map (would require
// sorting input, which is a huge time sink).
absl::StrAppend(&code_, ", anchor(", range->begin(), ", ", range->end(),
", v", FindEVar(evar), ")");
} 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));
}
} 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_, ")");
}
#ifdef DEBUG_LOWERING
dprinter.Print(" => <");
dprinter.Print(code_.substr(ccode, code_.size() - ccode));
dprinter.Print("> \n");
#endif
}
absl::StrAppend(&code_, ".\n");
return true;
}

bool SouffleProgram::Lower(const SymbolTable& symbol_table,
const std::vector<GoalGroup>& goal_groups) {
code_ = emit_prelude_ ? std::string(kGlobalDecls) : "";
CHECK_LE(goal_groups.size(), 1) << "(unimplemented)";
absl::StrAppend(&code_, ".\n");
if (goal_groups.size() == 0) {
absl::StrAppend(&code_, ".\n");
return true;
}
for (const auto& group : goal_groups) {
if (!LowerGoalGroup(symbol_table, group)) return false;
}
return true;
}
} // namespace kythe::verifier
15 changes: 15 additions & 0 deletions kythe/cxx/verifier/assertions_to_souffle.h
View file
Expand Up @@ -19,6 +19,7 @@

#include <string>

#include "absl/container/flat_hash_map.h"
#include "absl/strings/string_view.h"
#include "kythe/cxx/verifier/assertion_ast.h"

Expand All @@ -39,11 +40,25 @@ class SouffleProgram {
void set_emit_prelude(bool emit_prelude) { emit_prelude_ = emit_prelude; }

private:
/// \brief Lowers `node`.
bool LowerSubexpression(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;

/// Known evars.
absl::flat_hash_map<EVar*, size_t> evars_;
};

} // namespace kythe::verifier
Expand Down
32 changes: 26 additions & 6 deletions kythe/cxx/verifier/souffle_interpreter.cc
View file
Expand Up @@ -35,7 +35,8 @@ class KytheReadStream : public souffle::ReadStream {
explicit KytheReadStream(
const std::map<std::string, std::string>& rw_operation,
souffle::SymbolTable& symbol_table, souffle::RecordTable& record_table,
const AnchorMap& anchors, const Database& database)
const AnchorMap& anchors, const Database& database,
const SymbolTable& dst)
: souffle::ReadStream(rw_operation, symbol_table, record_table),
anchors_(anchors),
database_(database) {
Expand All @@ -46,6 +47,20 @@ class KytheReadStream : public souffle::ReadStream {
database_it_ = database_.cbegin();
anchor_it_ = anchors_.cend();
}
#ifdef DEBUG_LOWERING
FileHandlePrettyPrinter dprinter(stderr);
for (const auto& d : database) {
dprinter.Print("- ");
d->Dump(dst, &dprinter);
dprinter.Print("\n");
}
for (const auto& a : anchors) {
dprinter.Print(
absl::StrCat("@ ", a.first.first, ", ", a.first.second, " "));
a.second->Dump(dst, &dprinter);
dprinter.Print("\n");
}
#endif
std::array<souffle::RamDomain, 5> fields = {0, 0, 0, 0, 0};
empty_vname_ = record_table.pack(fields.data(), fields.size());
}
Expand All @@ -60,6 +75,7 @@ class KytheReadStream : public souffle::ReadStream {
tuple[0] = recordTable.pack(vname, 5);
tuple[1] = t->element(1)->AsIdentifier()->symbol();
if (auto* id = t->element(2)->AsIdentifier(); id != nullptr) {
// TODO(zarko): this should possibly be an explicit nil.
tuple[2] = id->symbol();
} else {
CopyVName(t->element(2)->AsApp()->rhs()->AsTuple(), vname);
Expand Down Expand Up @@ -102,15 +118,16 @@ class KytheReadStream : public souffle::ReadStream {

class KytheReadStreamFactory : public souffle::ReadStreamFactory {
public:
KytheReadStreamFactory(const AnchorMap& anchors, const Database& database)
: anchors_(anchors), database_(database) {}
KytheReadStreamFactory(const AnchorMap& anchors, const Database& database,
const SymbolTable& dst)
: anchors_(anchors), database_(database), dst_(dst) {}

souffle::Own<souffle::ReadStream> getReader(
const std::map<std::string, std::string>& rw_operation,
souffle::SymbolTable& symbol_table,
souffle::RecordTable& record_table) override {
return souffle::mk<KytheReadStream>(rw_operation, symbol_table,
record_table, anchors_, database_);
return souffle::mk<KytheReadStream>(
rw_operation, symbol_table, record_table, anchors_, database_, dst_);
}

const std::string& getName() const override {
Expand All @@ -121,6 +138,7 @@ class KytheReadStreamFactory : public souffle::ReadStreamFactory {
private:
const AnchorMap& anchors_;
const Database& database_;
const SymbolTable& dst_;
};

class KytheWriteStream : public souffle::WriteStream {
Expand Down Expand Up @@ -190,10 +208,12 @@ SouffleResult RunSouffle(const SymbolTable& symbol_table,
souffle::IOSystem::getInstance().registerWriteStreamFactory(
write_stream_factory);
souffle::IOSystem::getInstance().registerReadStreamFactory(
std::make_shared<KytheReadStreamFactory>(anchors, database));
std::make_shared<KytheReadStreamFactory>(anchors, database,
symbol_table));
auto ram_tu = souffle::ParseTransform(absl::StrCat(
program.code(), ".output result(IO=kythe, id=", output_id, ")\n"));
if (ram_tu == nullptr) {
LOG(ERROR) << "no ram_tu for program <" << program.code() << ">";
return result;
}
souffle::Own<souffle::interpreter::Engine> interpreter(
Expand Down
7 changes: 3 additions & 4 deletions kythe/cxx/verifier/verifier.cc
View file
Expand Up @@ -1108,7 +1108,7 @@ static bool EncodedFactHasValidForm(Verifier* cxt, AstNode* a) {
}

Verifier::InternedVName Verifier::InternVName(AstNode* node) {
auto* tuple = node->AsTuple();
auto* tuple = node->AsApp()->rhs()->AsTuple();
return {tuple->element(0)->AsIdentifier()->symbol(),
tuple->element(1)->AsIdentifier()->symbol(),
tuple->element(2)->AsIdentifier()->symbol(),
Expand Down Expand Up @@ -1152,11 +1152,10 @@ bool Verifier::ProcessFactTupleForFastSolver(Tuple* tuple) {
}

bool Verifier::PrepareDatabase() {
if (database_prepared_) {
if (database_prepared_ || use_fast_solver_) {
LOG(WARNING) << "PrepareDatabase() called when fast solver was enabled";
return true;
}
CHECK(!use_fast_solver_)
<< "This configuration is not supported when --use_fast_solver is on.";
// TODO(zarko): Make this configurable.
FileHandlePrettyPrinter printer(stderr);
// First, sort the tuples. As an invariant, we know they will be of the form
Expand Down

0 comments on commit 91d7cd0

Please sign in to comment.