Skip to content

Commit

Permalink
Add byods data structure providers under byods/rels-ascent
Browse files Browse the repository at this point in the history
  • Loading branch information
s-arash committed Dec 27, 2023
1 parent 72ed150 commit 8830a56
Show file tree
Hide file tree
Showing 36 changed files with 54,260 additions and 1 deletion.
13 changes: 13 additions & 0 deletions .github/workflows/rust.yml
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,19 @@ jobs:
working-directory: ./ascent_macro
run: cargo test test

byods-rels:
runs-on: ubuntu-latest

steps:
- uses: actions/checkout@v2

- name: Install Rust
uses: actions-rs/toolchain@v1

- name: cargo test
working-directory: ./byods/rels-ascent
run: cargo test

dependency-check:
runs-on: ubuntu-latest

Expand Down
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[workspace]
members = ["ascent", "ascent_base", "ascent_macro"]
exclude = ["ascent_tests", "wasm-tests"]
exclude = ["ascent_tests", "wasm-tests", "byods"]
3 changes: 3 additions & 0 deletions byods/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
This directory contains custom data structure providers for Ascent's ["Bring Your Own Data Strcutures"](https://dl.acm.org/doi/10.1145/3622840) feature.

To get started with custom data structures in Ascent, see the example in `./rels-ascent/examples/steensgaard`.
23 changes: 23 additions & 0 deletions byods/rels-ascent/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
[package]
name = "rels-ascent"
version = "0.1.0"
edition = "2021"

[dev-dependencies]
proptest = "1"
rand = "0.8"
serde = "1.0.193"
csv = "1"
separator = "0.4.1"


[dependencies]
ascent = { path = "../../ascent", version = "0.5.0" }
itertools = "0.12"
rustc-hash = "1.1"
derive_more = "0.99"
paste = "1.0"
hashbrown = { version = "0.14", features = ["raw", "rayon"] }

[features]
compact = []
146 changes: 146 additions & 0 deletions byods/rels-ascent/examples/steensgaard/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,146 @@
use std::alloc::System;

use ascent::ascent;
use ascent::internal::Instant;
use itertools::Itertools;

use rels_ascent::tracking_alloc::{self, TrackingAllocator};

#[global_allocator]
static GLOBAL: TrackingAllocator<System> = TrackingAllocator(System);

type Symbol = &'static str;

ascent! {
#![measure_rule_times]
/// Steensgaard analysis using `eqrel`
struct Steensgaard;

relation alloc(Symbol, Symbol);
// x := y;
relation assign(Symbol, Symbol);
// x := y.f;
relation load(Symbol, Symbol, Symbol);
// x.f := y;
relation store(Symbol, Symbol, Symbol);

#[ds(rels_ascent::eqrel)]
relation vpt(Symbol, Symbol);

// assignments
vpt(x,y) <--
assign(x,y);

// allocation sites
vpt(x,y) <--
alloc(x,y);

// load/store pairs
vpt(y,p) <--
store(x,f, y),
load(p,q,f),
vpt(x,q);
}

ascent! {
#![measure_rule_times]
/// Explicit Steensgaard analysis
struct SteensgaardExplicit;

relation alloc(Symbol, Symbol);
// x := y;
relation assign(Symbol, Symbol);
// x := y.f;
relation load(Symbol, Symbol, Symbol);
// x.f := y;
relation store(Symbol, Symbol, Symbol);

relation vpt(Symbol, Symbol);

vpt(y, x), vpt(x, x) <-- vpt(x, y);
vpt(x, z) <-- vpt(x, y), vpt(y, z);

// assignments
vpt(x,y) <--
assign(x,y);

// allocation sites
vpt(x,y) <--
alloc(x,y);

// load/store pairs
vpt(y,p) <--
store(x,f, y),
load(p,q,f),
vpt(x,q);
}

fn read_csv<T>(path: &str) -> impl Iterator<Item = T>
where
for<'de> T: serde::de::Deserialize<'de>,
{
csv::ReaderBuilder::new()
.delimiter(b'\t')
.has_headers(false)
.double_quote(false)
.quoting(false)
.from_path(path)
.unwrap()
.into_deserialize()
.map(|x| x.unwrap())
}

fn main() {
let path = "./examples/steensgaard/openjdk_javalang_steensgaard/";
let get_path = |x: &str| format!("{path}{x}");

println!("Running eqrel version.");
let mem_use_before = tracking_alloc::current_alloc();
let start_time = Instant::now();
let mut prog = Steensgaard::default();

prog.alloc =
read_csv::<(String, String)>(&get_path("alloc.facts")).map(|(x, y)| (x.leak() as _, y.leak() as _)).collect_vec();
prog.assign = read_csv::<(String, String)>(&get_path("assign.facts"))
.map(|(x, y)| (x.leak() as _, y.leak() as _))
.collect_vec();
prog.load = read_csv::<(String, String, String)>(&get_path("load.facts"))
.map(|(x, y, z)| (x.leak() as _, y.leak() as _, z.leak() as _))
.collect_vec();
prog.store = read_csv::<(String, String, String)>(&get_path("store.facts"))
.map(|(x, y, z)| (x.leak() as _, y.leak() as _, z.leak() as _))
.collect_vec();

prog.run();

println!("mem use: {:.2} Mib", (tracking_alloc::max_alloc() - mem_use_before) as f64 / 2f64.powi(20));
println!("everything took: {:?}", start_time.elapsed());
println!("vpt size: {}", prog.__vpt_ind_common.count_exact());

tracking_alloc::reset_max_alloc();

// Explicit version:
println!("");
println!("Running Explicit version. This will take FOREVER!");
let mem_use_before = tracking_alloc::current_alloc();
let start_time = Instant::now();
let mut prog = SteensgaardExplicit::default();

prog.alloc =
read_csv::<(String, String)>(&get_path("alloc.facts")).map(|(x, y)| (x.leak() as _, y.leak() as _)).collect_vec();
prog.assign = read_csv::<(String, String)>(&get_path("assign.facts"))
.map(|(x, y)| (x.leak() as _, y.leak() as _))
.collect_vec();
prog.load = read_csv::<(String, String, String)>(&get_path("load.facts"))
.map(|(x, y, z)| (x.leak() as _, y.leak() as _, z.leak() as _))
.collect_vec();
prog.store = read_csv::<(String, String, String)>(&get_path("store.facts"))
.map(|(x, y, z)| (x.leak() as _, y.leak() as _, z.leak() as _))
.collect_vec();

prog.run();

println!("mem use: {:.2} Mib", (tracking_alloc::max_alloc() - mem_use_before) as f64 / 2f64.powi(20));
println!("everything took: {:?}", start_time.elapsed());
println!("vpt size: {}", prog.vpt.len());
}
Loading

0 comments on commit 8830a56

Please sign in to comment.