Skip to content

Commit

Permalink
linters
Browse files Browse the repository at this point in the history
  • Loading branch information
Andrew Ferraiuolo committed Feb 7, 2022
1 parent abff6d4 commit 4203ac2
Show file tree
Hide file tree
Showing 2 changed files with 86 additions and 92 deletions.
2 changes: 1 addition & 1 deletion src/ir/auth_logic/BUILD
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,8 @@ cc_library(
],
visibility = ["//test:__pkg__"],
deps = [
"//src/ir/auth_logic:ast",
"//src/common/logging",
"//src/ir/auth_logic:ast",
"//src/utils:overloaded",
"@absl//absl/strings:str_format",
],
Expand Down
176 changes: 85 additions & 91 deletions src/ir/auth_logic/souffle_emitter.h
Original file line number Diff line number Diff line change
Expand Up @@ -25,108 +25,102 @@
namespace raksha::ir::auth_logic {

class SouffleEmitter {
public:
std::string EmitProgram(DLIRProgram program) {
SouffleEmitter emitter;
std::string body = emitter.EmitProgramBody(program);
std::string outputs = emitter.EmitOutputs(program);
std::string decls = emitter.EmitDeclarations();
return absl::StrCat(std::move(body),
"\n",
std::move(outputs),
"\n",
std::move(decls));
}

private:
SouffleEmitter()
public:
std::string EmitProgram(DLIRProgram program) {
SouffleEmitter emitter;
std::string body = emitter.EmitProgramBody(program);
std::string outputs = emitter.EmitOutputs(program);
std::string decls = emitter.EmitDeclarations();
return absl::StrCat(std::move(body), "\n", std::move(outputs), "\n",
std::move(decls));
}

private:
SouffleEmitter()
: declarations_(
absl::flat_hash_set<Predicate, Predicate::HashFunction>())
{};

// This function produces a normalized version of predicates to
// be used when generating declarations of the predicates. It replaces
// argument names with generic numbered ones. It is applied
// to predicates before they are added to the set of declarations so that
// there are no duplicate delcarations (which would otherwise happen
// whenever a predicate is referenced more than once with different
// arguments).
// To prevent instances of negated and non-negated uses of the predicate
// from generating two declarations, the sign here is always positive.
Predicate PredToDeclaration(Predicate predicate) {
std::vector<std::string> decl_args;
for( int i=0; i < predicate.args().size(); i++ ) {
decl_args.push_back("x" + std::to_string(i));
}
return Predicate(predicate.name(), decl_args, kPositive);
}

std::string EmitPredicate(Predicate predicate) {
// Whenever a new predicate is encountered, it is added to the set of
// declarations (which does not include duplicates because it is a set).
declarations_.insert(PredToDeclaration(predicate));
return absl::StrCat(
predicate.sign() == kNegated ? "!" : "",
predicate.name(),
"(", absl::StrJoin(predicate.args(), ", "), ")");
absl::flat_hash_set<Predicate, Predicate::HashFunction>()){};

// This function produces a normalized version of predicates to
// be used when generating declarations of the predicates. It replaces
// argument names with generic numbered ones. It is applied
// to predicates before they are added to the set of declarations so that
// there are no duplicate delcarations (which would otherwise happen
// whenever a predicate is referenced more than once with different
// arguments).
// To prevent instances of negated and non-negated uses of the predicate
// from generating two declarations, the sign here is always positive.
Predicate PredToDeclaration(Predicate predicate) {
std::vector<std::string> decl_args;
for (int i = 0; i < predicate.args().size(); i++) {
decl_args.push_back("x" + std::to_string(i));
}

std::string EmitAssertionInner(Predicate predicate) {
return EmitPredicate(predicate) + ".";
return Predicate(predicate.name(), decl_args, kPositive);
}

std::string EmitPredicate(Predicate predicate) {
// Whenever a new predicate is encountered, it is added to the set of
// declarations (which does not include duplicates because it is a set).
declarations_.insert(PredToDeclaration(predicate));
return absl::StrCat(predicate.sign() == kNegated ? "!" : "",
predicate.name(), "(",
absl::StrJoin(predicate.args(), ", "), ")");
}

std::string EmitAssertionInner(Predicate predicate) {
return EmitPredicate(predicate) + ".";
}

std::string EmitAssertionInner(DLIRCondAssertion cond_assertion) {
std::string lhs = EmitPredicate(cond_assertion.lhs());
std::vector<std::string> rhs_translated;
for (auto arg : cond_assertion.rhs()) {
rhs_translated.push_back(EmitPredicate(arg));
}

std::string EmitAssertionInner(DLIRCondAssertion cond_assertion) {
std::string lhs = EmitPredicate(cond_assertion.lhs());
std::vector<std::string> rhs_translated;
for(auto arg: cond_assertion.rhs()) {
rhs_translated.push_back(EmitPredicate(arg));
}
return absl::StrCat(std::move(lhs), " :- ",
absl::StrJoin(rhs_translated, ", "), ".");
return absl::StrCat(std::move(lhs), " :- ",
absl::StrJoin(rhs_translated, ", "), ".");
}

std::string EmitAssertion(DLIRAssertion assertion) {
return std::visit([this](auto value) { return EmitAssertionInner(value); },
assertion.GetValue());
}

std::string EmitProgramBody(DLIRProgram program) {
std::vector<std::string> body_translated;
for (auto assertion : program.assertions()) {
body_translated.push_back(EmitAssertion(assertion));
}
return absl::StrJoin(body_translated, "\n");
}

std::string EmitAssertion(DLIRAssertion assertion) {
return std::visit(
[this](auto value) { return EmitAssertionInner(value); },
assertion.GetValue());
std::string EmitOutputs(DLIRProgram program) {
std::string ret;
for (auto out : program.outputs()) {
absl::StrAppend(&ret, absl::StrCat(".output", out, "\n"));
}
return ret;
}

std::string EmitProgramBody(DLIRProgram program) {
std::vector<std::string> body_translated;
for(auto assertion : program.assertions()) {
body_translated.push_back(EmitAssertion(assertion));
}
return absl::StrJoin(body_translated, "\n");
std::string EmitDeclaration(Predicate predicate) {
std::vector<std::string> args_with_types;
for (auto elm : predicate.args()) {
args_with_types.push_back(absl::StrCat(elm, ": symbol"));
}

std::string EmitOutputs(DLIRProgram program) {
std::string ret;
for (auto out : program.outputs()) {
absl::StrAppend(&ret, absl::StrCat(".output", out, "\n"));
}
return ret;
}

std::string EmitDeclaration(Predicate predicate) {
std::vector<std::string> args_with_types;
for(auto elm : predicate.args()) {
args_with_types.push_back(absl::StrCat(elm, ": symbol"));
}
return absl::StrCat(".decl ", predicate.name(),
"(", absl::StrJoin(args_with_types, ", "), ")");
}

std::string EmitDeclarations() {
std::vector<std::string> ret;
for(auto decl : declarations_) {
ret.push_back(EmitDeclaration(decl));
}
return absl::StrJoin(ret, "\n");
return absl::StrCat(".decl ", predicate.name(), "(",
absl::StrJoin(args_with_types, ", "), ")");
}

std::string EmitDeclarations() {
std::vector<std::string> ret;
for (auto decl : declarations_) {
ret.push_back(EmitDeclaration(decl));
}
return absl::StrJoin(ret, "\n");
}

absl::flat_hash_set<Predicate, Predicate::HashFunction> declarations_;
absl::flat_hash_set<Predicate, Predicate::HashFunction> declarations_;
};

} // namespace raksha::ir::auth_logic

#endif //SRC_IR_AUTH_LOGIC_SOUFFLE_EMITTER_H_
#endif // SRC_IR_AUTH_LOGIC_SOUFFLE_EMITTER_H_

0 comments on commit 4203ac2

Please sign in to comment.