-
Notifications
You must be signed in to change notification settings - Fork 17
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add C++ types to express Souffle facts using C++ Souffle value types. (…
…#529) Adds a `Fact` class that allows expressing a Souffle fact as a C++ type, with the layout expressed in terms of the C++ Souffle value types provided in an earlier PR. Using these Souffle value types in templates to describe the layout allows the C++ compiler to check our work for us. Provides methods for printing `Fact`s out as datalog. Closes #529 COPYBARA_INTEGRATE_REVIEW=#529 from google-research:souffle_fact@winterrowd cfd0adf PiperOrigin-RevId: 444293149
- Loading branch information
Showing
3 changed files
with
158 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,56 @@ | ||
//----------------------------------------------------------------------------- | ||
// 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. | ||
//---------------------------------------------------------------------------- | ||
|
||
#ifndef SRC_IR_DATALOG_INPUT_RELATION_FACT_H_ | ||
#define SRC_IR_DATALOG_INPUT_RELATION_FACT_H_ | ||
|
||
#include <utility> | ||
|
||
#include "absl/strings/str_format.h" | ||
#include "absl/strings/str_join.h" | ||
#include "src/ir/datalog/value.h" | ||
|
||
namespace raksha::ir::datalog { | ||
|
||
// A fact that is built to be fed into an input relation for Souffle. | ||
// Although the `Rule` class can also express a `Fact` by having no RHS, this | ||
// is explicitly to prepare input to a Souffle program. You can think of the | ||
// difference between this `Fact` and a `Rule` fact as a difference between | ||
// data and code. | ||
template <class... RelationParameterTypes> | ||
class InputRelationFact { | ||
public: | ||
InputRelationFact(RelationParameterTypes &&...args) | ||
: relation_arguments_(std::forward<RelationParameterTypes>(args)...) {} | ||
|
||
virtual absl::string_view GetRelationName() const = 0; | ||
|
||
std::string ToDatalogString() const { | ||
return absl::StrFormat(R"(%s(%s).)", GetRelationName(), | ||
absl::StrJoin(relation_arguments_, ", ", | ||
[](std::string *str, const auto &arg) { | ||
absl::StrAppend( | ||
str, arg.ToDatalogString()); | ||
})); | ||
} | ||
|
||
private: | ||
std::tuple<RelationParameterTypes...> relation_arguments_; | ||
}; | ||
|
||
} // namespace raksha::ir::datalog | ||
|
||
#endif // SRC_IR_DATALOG_INPUT_RELATION_FACT_H_ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,80 @@ | ||
//----------------------------------------------------------------------------- | ||
// 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/ir/datalog/input_relation_fact.h" | ||
|
||
#include "absl/strings/string_view.h" | ||
#include "src/common/testing/gtest.h" | ||
#include "src/ir/datalog/value.h" | ||
|
||
namespace raksha::ir::datalog { | ||
|
||
using testing::Combine; | ||
using testing::TestWithParam; | ||
using testing::ValuesIn; | ||
|
||
class IsAccessPathFact : public InputRelationFact<Symbol> { | ||
public: | ||
using InputRelationFact::InputRelationFact; | ||
virtual ~IsAccessPathFact() {} | ||
static constexpr absl::string_view relation_name() { return "isAccessPath"; } | ||
absl::string_view GetRelationName() const override { return relation_name(); } | ||
}; | ||
|
||
class IsAccessPathFactTest : public TestWithParam<absl::string_view> {}; | ||
|
||
TEST_P(IsAccessPathFactTest, IsAccessPathFactTest) { | ||
absl::string_view symbol_string = GetParam(); | ||
EXPECT_EQ(IsAccessPathFact(Symbol(symbol_string)).ToDatalogString(), | ||
absl::StrFormat(R"(isAccessPath("%s").)", symbol_string)); | ||
} | ||
|
||
static const absl::string_view kSampleAccessPathStrings[] = {"", "P1.foo", | ||
"P2.handle1.x"}; | ||
|
||
INSTANTIATE_TEST_SUITE_P(IsAccessPathFactTest, IsAccessPathFactTest, | ||
ValuesIn(kSampleAccessPathStrings)); | ||
|
||
static const char kUnitName[] = "Unit"; | ||
|
||
class SimpleAdt : public Adt { | ||
using Adt::Adt; | ||
}; | ||
|
||
class UnitAdtBranch : public SimpleAdt { | ||
public: | ||
UnitAdtBranch() : SimpleAdt(kUnitName) {} | ||
}; | ||
|
||
class OneOfEachFact | ||
: public InputRelationFact<Number, Symbol, Record<Number, Symbol>, | ||
SimpleAdt> { | ||
public: | ||
using InputRelationFact::InputRelationFact; | ||
virtual ~OneOfEachFact() {} | ||
static constexpr absl::string_view relation_name() { return "oneOfEach"; } | ||
absl::string_view GetRelationName() const override { return relation_name(); } | ||
}; | ||
|
||
TEST(OneOfEachFactTest, OneOfEachFactTest) { | ||
EXPECT_EQ(OneOfEachFact(Number(5), Symbol("foo"), | ||
Record<Number, Symbol>(Number(3), Symbol("bar")), | ||
SimpleAdt(UnitAdtBranch())) | ||
.ToDatalogString(), | ||
R"(oneOfEach(5, "foo", [3, "bar"], $Unit{}).)"); | ||
} | ||
|
||
} // namespace raksha::ir::datalog |