Skip to content

Commit 6911864

Browse files
Add Soufflé backend
1 parent 84f3992 commit 6911864

File tree

20 files changed

+1632
-73
lines changed

20 files changed

+1632
-73
lines changed

Cargo.toml

Lines changed: 14 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,21 +3,25 @@ name = "polonius"
33
version = "0.7.0"
44
authors = ["The Rust Project Developers", "Polonius Developers"]
55
description = "Core definition for the Rust borrow checker"
6-
license = "Apache-2.0/MIT"
7-
repository = "https://github.com/rust-lang/polonius"
8-
readme = "README.md"
9-
keywords = ["compiler", "borrowck", "datalog"]
10-
edition = "2018"
6+
license = "Apache-2.0/MIT"
7+
repository = "https://github.com/rust-lang-nursery/polonius"
8+
readme = "README.md"
9+
keywords = ["compiler", "borrowck", "datalog"]
10+
edition = "2018"
1111

1212
[dev-dependencies]
1313
diff = "0.1.0"
1414
polonius-parser = { path = "./polonius-parser" }
1515

1616
[dependencies]
17-
rustc-hash = "1.0.0"
18-
polonius-engine = { path = "./polonius-engine" }
19-
log = "0.4"
20-
petgraph = "0.4.13"
21-
pico-args = "0.2"
17+
rustc-hash = "1.0.0"
18+
polonius-engine = { path = "polonius-engine" }
19+
polonius-souffle = { path = "polonius-souffle" }
20+
log = "0.4"
21+
petgraph = "0.4.13"
22+
pico-args = "0.2"
23+
24+
[build-dependencies]
25+
glob = "0.3.0"
2226

2327
[workspace]

build.rs

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
use glob::glob;
2+
3+
fn main() {
4+
// See `polonius-souffle/build.rs` for background.
5+
//
6+
// FIXME: We should expose these symbols in a single location instead of globbing.
7+
for ruleset in glob("rules/*.dl").unwrap() {
8+
let stem = ruleset.unwrap();
9+
let stem = stem.file_stem().unwrap().to_str().unwrap();
10+
println!("cargo:rustc-link-arg=-u__factory_Sf_{}_instance", stem);
11+
}
12+
}

polonius-engine/src/output/mod.rs

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,24 @@ impl Algorithm {
5555
"Hybrid",
5656
]
5757
}
58+
59+
pub fn engine(&self) -> Engine {
60+
match *self {
61+
Self::Naive(eng) | Self::DatafrogOpt(eng) => eng,
62+
Self::LocationInsensitive | Self::Compare | Self::Hybrid => Engine::Datafrog,
63+
}
64+
}
65+
66+
pub fn souffle_name(&self) -> Option<&'static str> {
67+
let ret = match self {
68+
Self::Naive(Engine::Souffle) => "naive",
69+
Self::DatafrogOpt(Engine::Souffle) => "opt",
70+
71+
_ => return None,
72+
};
73+
74+
Some(ret)
75+
}
5876
}
5977

6078
impl ::std::str::FromStr for Algorithm {

polonius-souffle/Cargo.toml

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
[package]
2+
name = "polonius-souffle"
3+
version = "0.1.0"
4+
edition = "2018"
5+
authors = ["The Rust Project Developers", "Polonius Developers"]
6+
description = "Core definition for the Rust borrow checker"
7+
license = "Apache-2.0/MIT"
8+
repository = "https://github.com/rust-lang-nursery/polonius"
9+
readme = "README.md"
10+
keywords = ["compiler", "borrowck", "datalog"]
11+
build = "build.rs"
12+
13+
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
14+
15+
[dependencies]
16+
cxx = "1.0.50"
17+
log = "0.4"
18+
polonius-engine = { path = "../polonius-engine" }
19+
20+
[build-dependencies]
21+
cc = "1.0.69"
22+
cxx-build = "1.0.50"
23+
glob = "0.3.0"
24+
is_executable = "1.0.1"
25+
which = "4.2.1"

polonius-souffle/build.rs

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
use std::collections::HashSet;
2+
use std::error::Error;
3+
use std::fs;
4+
use std::io::{BufWriter, Write};
5+
use std::path::{Path, PathBuf};
6+
use std::process::Command;
7+
8+
use glob::glob;
9+
use which::which;
10+
11+
const RULES_DIR: &str = "../rules";
12+
const CXX_BRIDGE: &str = "src/ffi.rs";
13+
14+
type Result<T> = ::std::result::Result<T, Box<dyn Error>>;
15+
16+
/// Gets the filename for each "top-level" rulest
17+
fn get_rulesets() -> Vec<PathBuf> {
18+
let result: std::result::Result<Vec<_>, _> =
19+
glob(&format!("{}/*.dl", RULES_DIR)).unwrap().collect();
20+
result.unwrap()
21+
}
22+
fn print_rerun_if_changed() {
23+
// Rerun if any C++ file changes
24+
for file in glob("shims/*").unwrap() {
25+
println!("cargo:rerun-if-changed={}", file.unwrap().to_string_lossy());
26+
}
27+
28+
// Rerun if any datalog file changes.
29+
for file in glob(&format!("{}/**/*.dl", RULES_DIR)).unwrap() {
30+
println!("cargo:rerun-if-changed={}", file.unwrap().to_string_lossy());
31+
}
32+
33+
// Rerun if our CXX bindings change.
34+
println!("cargo:rerun-if-changed={}", CXX_BRIDGE);
35+
}
36+
37+
fn main() -> Result<()> {
38+
print_rerun_if_changed();
39+
40+
if which("souffle").is_err() {
41+
eprintln!("`souffle` not in PATH. Is it installed?");
42+
return Err("missing `souffle`".into());
43+
}
44+
45+
let mut cpp_filenames = vec![];
46+
let mut known_stems = HashSet::new();
47+
for ruleset in get_rulesets() {
48+
// Get the common name for this ruleset.
49+
let stem = ruleset.file_stem().unwrap().to_str().unwrap();
50+
51+
// Check that name for duplicates
52+
//
53+
// Souffle uses a single, global registry for datalog programs, indexed by string.
54+
if !known_stems.insert(stem.to_owned()) {
55+
eprintln!("Multiple datalog files named `{}`", stem);
56+
return Err("Duplicate filenames".into());
57+
}
58+
59+
let cpp_filename = souffle_generate(&ruleset)?;
60+
cpp_filenames.push(cpp_filename);
61+
}
62+
63+
for stem in known_stems {
64+
// HACK: Souffle adds datalog programs to the registry in the initializer of a global
65+
// variable (whose name begins with `__factory_Sf`). Since that global variable is never used
66+
// by the Rust program, it is occasionally removed by the linker, its initializer is never
67+
// run (!!!), and the program is never registered.
68+
//
69+
// `-u` marks the symbol as undefined, so that it will not be optimized out.
70+
let prog_symbol = format!("__factory_Sf_{}_instance", stem);
71+
println!("cargo:rustc-link-arg=-u{}", prog_symbol);
72+
}
73+
74+
let mut cc = cxx_build::bridge(CXX_BRIDGE);
75+
76+
for file in cpp_filenames {
77+
cc.file(&file);
78+
}
79+
80+
cc.cpp(true)
81+
.define("__EMBEDDED_SOUFFLE__", None)
82+
.include("./shims")
83+
.flag("-std=c++17")
84+
.flag("-Wno-unused-parameter")
85+
.flag("-Wno-parentheses")
86+
.try_compile("souffle")?;
87+
88+
Ok(())
89+
}
90+
91+
/// Uses Souffle to generate a C++ file for evaluating the given datalog program.
92+
fn souffle_generate(datalog_filename: &Path) -> Result<PathBuf> {
93+
let mut cpp_filename = PathBuf::from(std::env::var("OUT_DIR").unwrap());
94+
cpp_filename.push(datalog_filename.with_extension("cpp").file_name().unwrap());
95+
96+
eprintln!("Generating code for {:?}...", &datalog_filename);
97+
98+
let result = Command::new("souffle")
99+
.arg("--generate")
100+
.arg(&cpp_filename)
101+
.arg(&datalog_filename)
102+
.status()?;
103+
104+
if !result.success() {
105+
return Err("Invalid datalog".into());
106+
}
107+
108+
Ok(cpp_filename)
109+
}

polonius-souffle/shims/shims.hpp

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
#pragma once
2+
3+
#include <cstdint>
4+
#include <memory>
5+
#include <string>
6+
7+
#include <souffle/SouffleInterface.h>
8+
9+
#include "polonius-souffle/src/ffi.rs.h"
10+
#include "rust/cxx.h"
11+
12+
#ifndef __EMBEDDED_SOUFFLE__
13+
#error "Build script must define __EMBEDDED_SOUFFLE__"
14+
#endif
15+
16+
/*
17+
* Wrappers around generated souffle functions. From Rust, we cannot safely
18+
* call functions that accept or return things with move constructors by-value
19+
* (e.g. `std::string`). The usual fix is to move them into a `unique_ptr`
20+
* first, or to pass a borrowed version (e.g. `cxx::Str`) from the Rust side
21+
* and copy it here.
22+
*/
23+
24+
namespace souffle {
25+
26+
std::unique_ptr<SouffleProgram>
27+
ProgramFactory_newInstance(const std::string &name) {
28+
std::unique_ptr<SouffleProgram> prog(ProgramFactory::newInstance(name));
29+
return prog;
30+
}
31+
32+
void load_all(SouffleProgram &foo, const std::string &name) {
33+
foo.loadAll(name);
34+
}
35+
36+
void print_all(SouffleProgram &foo, const std::string &name) {
37+
foo.printAll(name);
38+
}
39+
40+
void get_output_relations(const SouffleProgram &prog, rust::Vec<RelationPtr> &out) {
41+
auto relations = prog.getOutputRelations();
42+
for (auto rel : relations) {
43+
RelationPtr ptr{};
44+
ptr.ptr = rel;
45+
out.push_back(ptr);
46+
}
47+
}
48+
49+
void get_all_relations(const SouffleProgram &prog, rust::Vec<RelationPtr> &out) {
50+
auto relations = prog.getAllRelations();
51+
for (auto rel : relations) {
52+
RelationPtr ptr{};
53+
ptr.ptr = rel;
54+
out.push_back(ptr);
55+
}
56+
}
57+
58+
std::unique_ptr<std::string> get_name(const Relation& rel) {
59+
return std::make_unique<std::string>(rel.getName());
60+
}
61+
62+
// Fact loading
63+
64+
// This function is copied from the member function on `Program`.
65+
//
66+
// We cannot use the original because it requires a reference to both a
67+
// `Program` and a `Relation`, which have the same lifetime on the Rust side.
68+
template <typename... Args>
69+
void insert(const std::tuple<Args...> &t, Relation *rel) {
70+
souffle::tuple t1(rel);
71+
SouffleProgram::tuple_insert<decltype(t), sizeof...(Args)>::add(t, t1);
72+
rel->insert(t1);
73+
}
74+
75+
void insert_tuple1(Relation &rel, Tuple1 r) {
76+
insert(std::make_tuple(r.a), &rel);
77+
}
78+
79+
void insert_tuple2(Relation &rel, Tuple2 r) {
80+
insert(std::make_tuple(r.a, r.b), &rel);
81+
}
82+
83+
void insert_tuple3(Relation &rel, Tuple3 r) {
84+
insert(std::make_tuple(r.a, r.b, r.c), &rel);
85+
}
86+
87+
void insert_tuple4(Relation &rel, Tuple4 r) {
88+
insert(std::make_tuple(r.a, r.b, r.c, r.d), &rel);
89+
}
90+
91+
DynTuples dump_tuples(const Relation &rel) {
92+
DynTuples out{};
93+
out.arity = rel.getArity();
94+
95+
for (auto tuple : rel) {
96+
for (unsigned i = 0; i < out.arity; ++i) {
97+
out.data.push_back(tuple[i]);
98+
}
99+
}
100+
101+
return out;
102+
}
103+
104+
} // namespace bridge

polonius-souffle/src/facts.rs

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
use std::convert::TryInto;
2+
use std::pin::Pin;
3+
4+
use log::warn;
5+
use polonius_engine::{AllFacts, FactTypes};
6+
7+
use crate::ffi::{self, InsertIntoRelation};
8+
9+
fn insert_facts<T>(mut rel: Pin<&mut ffi::Relation>, name: &str, facts: &[T])
10+
where
11+
T: Copy + InsertIntoRelation,
12+
{
13+
debug_assert_eq!(std::mem::size_of::<T>() % std::mem::size_of::<u32>(), 0);
14+
let datafrog_arity = std::mem::size_of::<T>() / std::mem::size_of::<u32>();
15+
16+
let souffle_arity: usize = rel.getArity().try_into().unwrap();
17+
18+
if souffle_arity != datafrog_arity {
19+
panic!(
20+
r#"Arity mismatch for "{}". souffle={}, datafrog={}"#,
21+
name, souffle_arity, datafrog_arity
22+
);
23+
}
24+
25+
for &fact in facts {
26+
fact.insert_into_relation(rel.as_mut());
27+
}
28+
}
29+
30+
macro_rules! load_facts {
31+
($prog:ident, $facts:ident; $( $f:ident ),* $(,)?) => {
32+
// Exhaustive matching, since new facts must be reflected below as well.
33+
let AllFacts {
34+
$( ref $f ),*
35+
} = $facts;
36+
$(
37+
let name = stringify!($f);
38+
let rel = $prog.as_mut().relation_mut(name);
39+
if let Some(rel) = rel {
40+
insert_facts(rel, name, $f);
41+
} else {
42+
warn!("Relation named `{}` not found. Skipping...", name);
43+
}
44+
)*
45+
}
46+
}
47+
48+
pub fn insert_all_facts<T>(mut prog: Pin<&mut ffi::Program>, facts: &AllFacts<T>)
49+
where
50+
T: FactTypes,
51+
T::Origin: Into<u32>,
52+
T::Loan: Into<u32>,
53+
T::Point: Into<u32>,
54+
T::Variable: Into<u32>,
55+
T::Path: Into<u32>,
56+
{
57+
load_facts!(prog, facts;
58+
loan_issued_at,
59+
universal_region,
60+
cfg_edge,
61+
loan_killed_at,
62+
subset_base,
63+
loan_invalidated_at,
64+
var_used_at,
65+
var_defined_at,
66+
var_dropped_at,
67+
use_of_var_derefs_origin,
68+
drop_of_var_derefs_origin,
69+
child_path,
70+
path_is_var,
71+
path_assigned_at_base,
72+
path_moved_at_base,
73+
path_accessed_at_base,
74+
known_placeholder_subset,
75+
placeholder,
76+
);
77+
}

0 commit comments

Comments
 (0)