DLIR to Souffle Emitter

src/ir/auth_logic/BUILD

@@ -28,15 +28,24 @@ cc_library(
     deps = [
         "//src/common/logging",
         "//src/utils:overloaded",
+        "@absl//absl/hash",
         "@absl//absl/strings:str_format",
     ],
 )
 
+cc_test(
+    name = "predicate_test",
+    srcs = ["predicate_test.cc"],
+    deps = [
+        ":ast",
+        "//src/common/testing:gtest",
+    ],
+)
+
 cc_library(
     name = "lowering_ast_datalog",
     srcs = ["lowering_ast_datalog.cc"],
     hdrs = [
-        "ast.h",
         "datalog_ir.h",
         "lowering_ast_datalog.h",
         "map_iter.h",
@@ -45,11 +54,35 @@ cc_library(
     visibility = ["//test:__pkg__"],
     deps = [
         "//src/common/logging",
+        "//src/ir/auth_logic:ast",
         "//src/utils:overloaded",
         "@absl//absl/strings:str_format",
     ],
 )
 
+cc_library(
+    name = "souffle_emitter",
+    srcs = ["souffle_emitter_build_stub.cc"],
+    hdrs = [
+        "souffle_emitter.h",
+    ],
+    deps = [
+        "//src/ir/auth_logic:ast",
+        "//src/ir/auth_logic:lowering_ast_datalog",
+        "@absl//absl/container:flat_hash_set",
+        "@absl//absl/strings",
+    ],
+)
+
+cc_test(
+    name = "souffle_emitter_test",
+    srcs = ["souffle_emitter_test.cc"],
+    deps = [
+        ":souffle_emitter",
+        "//src/common/testing:gtest",
+    ],
+)
+
 cc_test(
     name = "ast_test",
     srcs = ["ast_test.cc"],

src/ir/auth_logic/ast.h

@@ -24,6 +24,8 @@
 #include <variant>
 #include <vector>
 
+#include "absl/hash/hash.h"
+
 namespace raksha::ir::auth_logic {
 
 class Principal {
@@ -53,6 +55,35 @@ class Predicate {
   const std::vector<std::string>& args() const { return args_; }
   Sign sign() const { return sign_; }
 
+  template <typename H>
+  friend H AbslHashValue(H h, const Predicate& p) {
+    return H::combine(std::move(h), p.name(), p.args(), p.sign());
+  }
+  // Equality is also needed to use a Predicate in a flat_hash_set
+  bool operator==(const Predicate& otherPredicate) const {
+    if (this->name() != otherPredicate.name()) {
+      return false;
+    }
+    if (this->sign() != otherPredicate.sign()) {
+      return false;
+    }
+    if (this->args().size() != otherPredicate.args().size()) {
+      return false;
+    }
+    for (int i = 0; i < this->args().size(); i++) {
+      if (this->args().at(i) != otherPredicate.args().at(i)) return false;
+    }
+    return true;
+  }
+
+  // < operator is needed for btree_set, which is only used for declarations.
+  // Since declarations are uniquely defined by the name of the predicate,
+  // this implementation that just uses < on the predicate names should be
+  // sufficent in the context where it is used.
+  bool operator<(const Predicate& otherPredicate) const {
+    return this->name() < otherPredicate.name();
+  }
+
  private:
   std::string name_;
   std::vector<std::string> args_;

src/ir/auth_logic/datalog_ir.h

@@ -31,6 +31,8 @@ class DLIRCondAssertion {
  public:
   explicit DLIRCondAssertion(Predicate lhs, std::vector<Predicate> rhs)
       : lhs_(std::move(lhs)), rhs_(std::move(rhs)) {}
+  const Predicate& lhs() const { return lhs_; }
+  const std::vector<Predicate>& rhs() const { return rhs_; }
 
  private:
   Predicate lhs_;
@@ -48,6 +50,7 @@ class DLIRAssertion {
   using DLIRAssertionVariantType = std::variant<Predicate, DLIRCondAssertion>;
   explicit DLIRAssertion(DLIRAssertionVariantType value)
       : value_(std::move(value)) {}
+  const DLIRAssertionVariantType& GetValue() const { return value_; }
 
  private:
   std::variant<Predicate, DLIRCondAssertion> value_;
@@ -58,6 +61,8 @@ class DLIRProgram {
   DLIRProgram(std::vector<DLIRAssertion> assertions,
               std::vector<std::string> outputs)
       : assertions_(std::move(assertions)), outputs_(std::move(outputs)) {}
+  const std::vector<DLIRAssertion>& assertions() const { return assertions_; }
+  const std::vector<std::string>& outputs() const { return outputs_; }
 
  private:
   std::vector<DLIRAssertion> assertions_;

src/ir/auth_logic/lowering_ast_datalog.cc

@@ -66,8 +66,6 @@ Predicate CanActAsToDLIR(const CanActAs& can_act_as) {
 
 DLIRAssertion LoweringToDatalogPass::SpokenAttributeToDLIR(
     const Principal& speaker, const Attribute& attribute) {
-  Predicate main_predicate = AttributeToDLIR(attribute);
-
   // Attributes interact with "canActAs" because if "Y canActAs X"
   // then Y also picks up X's attributes. We need to generate
   // an additional rule to implement this behavior. If the attribute
@@ -78,16 +76,17 @@ DLIRAssertion LoweringToDatalogPass::SpokenAttributeToDLIR(
   Principal prin_y(FreshVar());
 
   // This is `speaker says Y PredX`
-  Predicate generated_lhs = PushPrincipal("says_", prin_y, main_predicate);
-
-  Predicate y_can_act_as_x("canActAs",
-                           {prin_y.name(), attribute.principal().name()},
-                           Sign::kPositive);
+  Predicate y_predX = AttributeToDLIR(Attribute(prin_y, attribute.predicate()));
+  Predicate generated_lhs = PushPrincipal("says_", speaker, y_predX);
 
+  // This is `speaker says Y canActAs X`
+  Predicate y_can_act_as_x =
+      CanActAsToDLIR(CanActAs(prin_y, attribute.principal()));
   Predicate speaker_says_y_can_act_as_x =
       PushPrincipal("says_", speaker, y_can_act_as_x);
 
   // This is `speaker says X PredX`
+  Predicate main_predicate = AttributeToDLIR(attribute);
   Predicate speaker_says_x_pred =
       PushPrincipal("says_", speaker, main_predicate);
 
@@ -101,28 +100,28 @@ DLIRAssertion LoweringToDatalogPass::SpokenAttributeToDLIR(
 
 DLIRAssertion LoweringToDatalogPass::SpokenCanActAsToDLIR(
     const Principal& speaker, const CanActAs& can_act_as) {
-  Predicate main_predicate = CanActAsToDLIR(can_act_as);
-
   // "canActAs" facts are passed to principals via other canActAs facts in
   // essentially the same way as attributes. This function adds extra
   // rules to pass these around. If the `canActAs` under translation
   // is `X canActAs Z`, then the rule we need to generate is:
-  // `speaker says Y PredX :-
-  //    speaker says Y canActAs X, speaker says X canActAsZ`
+  // `speaker says Y canActAs Z :-
+  //    speaker says Y canActAs X, speaker says X canActAs Z`
   // (Where Y is a fresh variable)
   Principal prin_y(FreshVar());
 
-  // This is `speaker says Y PredX`
-  Predicate generated_lhs = PushPrincipal("says_", prin_y, main_predicate);
-
-  Predicate y_can_act_as_x("canActAs",
-                           {prin_y.name(), can_act_as.left_principal().name()},
-                           Sign::kPositive);
+  // This is `speaker says Y canActAs Z`
+  Predicate y_can_act_as_z =
+      CanActAsToDLIR(CanActAs(prin_y, can_act_as.right_principal()));
+  Predicate generated_lhs = PushPrincipal("says_", speaker, y_can_act_as_z);
 
+  // This is `speaker says Y canActAs X`
+  Predicate y_can_act_as_x =
+      CanActAsToDLIR(CanActAs(prin_y, can_act_as.left_principal()));
   Predicate speaker_says_y_can_act_as_x =
       PushPrincipal("says_", speaker, y_can_act_as_x);
 
   // This is `speaker says X canActAs Z`
+  Predicate main_predicate = CanActAsToDLIR(can_act_as);
   Predicate speaker_says_x_can_act_as_z =
       PushPrincipal("says_", speaker, main_predicate);
 

src/ir/auth_logic/predicate_test.cc

@@ -0,0 +1,65 @@
+//-----------------------------------------------------------------------------
+// Copyright 2022 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+//----------------------------------------------------------------------------
+
+#include "src/common/testing/gtest.h"
+#include "src/ir/auth_logic/ast.h"
+
+namespace raksha::ir::auth_logic {
+
+TEST(PredicateTest, EqualReturnsForIdenticalPredicates) {
+  Predicate p1("foo", {"bar", "baz"}, kPositive);
+  Predicate p2("foo", {"bar", "baz"}, kPositive);
+  EXPECT_TRUE(p1 == p2);
+}
+
+TEST(PredicateTest, UnequalReturnsForDifferntPredicateNames) {
+  Predicate p1("foo", {"bar", "baz"}, kPositive);
+  Predicate p2("food", {"bar", "baz"}, kPositive);
+  EXPECT_TRUE(!(p1 == p2));
+}
+
+TEST(PredicateTest, UnequalReturnsForDifferentlyOrderedParameters) {
+  Predicate p1("foo", {"bar", "baz"}, kPositive);
+  Predicate p2("foo", {"baz", "bar"}, kPositive);
+  EXPECT_TRUE(!(p1 == p2));
+}
+
+TEST(PredicateTest, UnequalReturnsForDifferentParameterNames) {
+  Predicate p1("foo", {"barrrrr", "baz"}, kPositive);
+  Predicate p2("foo", {"bar", "baz"}, kPositive);
+  EXPECT_TRUE(!(p1 == p2));
+}
+
+TEST(PredicateTest,
+     UnequalReturnsForDifferentParameterNamesInDifferentPosition) {
+  Predicate p1("foo", {"bar", "baz"}, kPositive);
+  Predicate p2("foo", {"bar", "bas"}, kPositive);
+  EXPECT_TRUE(!(p1 == p2));
+}
+
+TEST(PredicateTest, UnequalReturnsForDifferentPolarity) {
+  Predicate p1("foo", {"bar", "baz"}, kPositive);
+  Predicate p2("foo", {"bar", "baz"}, kNegated);
+  EXPECT_TRUE(!(p1 == p2));
+}
+
+TEST(PredicateTest, UnequalReturnsForPrefixingUnequalParameterList) {
+  Predicate p1("foo", {"bar", "baz"}, kPositive);
+  Predicate p2("foo", {"bar", "baz", "beef"}, kPositive);
+  EXPECT_TRUE(!(p1 == p2));
+}
+
+}  // namespace raksha::ir::auth_logic

src/ir/auth_logic/souffle_emitter.h

@@ -0,0 +1,127 @@
+/*
+ * Copyright 2022 Google LLC.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#ifndef SRC_IR_AUTH_LOGIC_SOUFFLE_EMITTER_H_
+#define SRC_IR_AUTH_LOGIC_SOUFFLE_EMITTER_H_
+
+#include "absl/container/flat_hash_set.h"
+#include "absl/strings/str_cat.h"
+#include "absl/strings/str_join.h"
+#include "src/ir/auth_logic/datalog_ir.h"
+#include "src/ir/auth_logic/map_iter.h"
+
+namespace raksha::ir::auth_logic {
+
+class SouffleEmitter {
+ public:
+  static std::string EmitProgram(const 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), "\n");
+  }
+
+ private:
+  SouffleEmitter() = default;
+
+  // 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(const Predicate& predicate) {
+    int i = 0;
+    return Predicate(predicate.name(),
+                     MapIter<std::string, std::string>(
+                         predicate.args(),
+                         [i](const std::string& arg) mutable {
+                           return absl::StrCat("x", std::to_string(i++));
+                         }),
+                     kPositive);
+  }
+
+  std::string EmitPredicate(const 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(const Predicate& predicate) {
+    return absl::StrCat(EmitPredicate(predicate), ".");
+  }
+
+  std::string EmitAssertionInner(const DLIRCondAssertion& cond_assertion) {
+    std::vector rhs_translated = MapIter<Predicate, std::string>(
+        cond_assertion.rhs(),
+        [this](const Predicate& arg) { return EmitPredicate(arg); });
+    return absl::StrCat(EmitPredicate(cond_assertion.lhs()), " :- ",
+                        absl::StrJoin(rhs_translated, ", "), ".");
+  }
+
+  std::string EmitAssertion(const DLIRAssertion& assertion) {
+    return std::visit([this](auto value) { return EmitAssertionInner(value); },
+                      assertion.GetValue());
+  }
+
+  std::string EmitProgramBody(const DLIRProgram& program) {
+    return absl::StrJoin(
+        MapIter<DLIRAssertion, std::string>(
+            program.assertions(),
+            [this](const DLIRAssertion& astn) { return EmitAssertion(astn); }),
+        "\n");
+  }
+
+  std::string EmitOutputs(const DLIRProgram& program) {
+    return absl::StrJoin(program.outputs(), "\n",
+                         [](std::string* out, const std::string& prog_out) {
+                           return absl::StrAppend(
+                               out, absl::StrCat(".output ", prog_out));
+                         });
+  }
+
+  std::string EmitDeclaration(const Predicate& predicate) {
+    std::string arguments = absl::StrJoin(
+        predicate.args(), ", ", [](std::string* out, const std::string& arg) {
+          return absl::StrAppend(out, absl::StrCat(arg, ": symbol"));
+        });
+    return absl::StrCat(".decl ", predicate.name(), "(", arguments, ")");
+  }
+
+  std::string EmitDeclarations() {
+    std::vector elements_vec(std::make_move_iterator(declarations_.begin()),
+                             std::make_move_iterator(declarations_.end()));
+    std::sort(elements_vec.begin(), elements_vec.end());
+    return absl::StrJoin(elements_vec, "\n",
+                         [this](std::string* out, auto decl) {
+                           return absl::StrAppend(out, EmitDeclaration(decl));
+                         });
+  }
+
+  absl::flat_hash_set<Predicate> declarations_;
+};
+
+}  // namespace raksha::ir::auth_logic
+
+#endif  // SRC_IR_AUTH_LOGIC_SOUFFLE_EMITTER_H_