Skip to content

Commit

Permalink
Merge 'simulator: --differential mode against SQLite' from Alperen …
Browse files Browse the repository at this point in the history 
…Keleş

Closes #987
  • Loading branch information
@penberg
penberg committed Feb 12, 2025
2 parents e48c50f + babf33b commit 11970d9
Show file tree
Hide file tree
Showing 10 changed files with 433 additions and 44 deletions.
1 change: 1 addition & 0 deletions Cargo.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions simulator/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,3 +28,4 @@ clap = { version = "4.5", features = ["derive"] }
serde = { version = "1.0", features = ["derive"] }
serde_json = { version = "1.0" }
notify = "8.0.0"
rusqlite = { version = "0.29", features = ["bundled"] }
8 changes: 4 additions & 4 deletions simulator/generation/plan.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use crate::{
},
table::Value,
},
runner::env::SimConnection,
runner::env::{SimConnection, SimulatorEnvTrait},
SimulatorEnv,
};

Expand Down Expand Up @@ -239,7 +239,7 @@ impl Display for Interaction {
}
}

type AssertionFunc = dyn Fn(&Vec<ResultSet>, &SimulatorEnv) -> Result<bool>;
type AssertionFunc = dyn Fn(&Vec<ResultSet>, &dyn SimulatorEnvTrait) -> Result<bool>;

enum AssertionAST {
Pick(),
Expand Down Expand Up @@ -523,7 +523,7 @@ impl Interaction {
pub(crate) fn execute_assertion(
&self,
stack: &Vec<ResultSet>,
env: &SimulatorEnv,
env: &impl SimulatorEnvTrait,
) -> Result<()> {
match self {
Self::Query(_) => {
Expand Down Expand Up @@ -554,7 +554,7 @@ impl Interaction {
pub(crate) fn execute_assumption(
&self,
stack: &Vec<ResultSet>,
env: &SimulatorEnv,
env: &dyn SimulatorEnvTrait,
) -> Result<()> {
match self {
Self::Query(_) => {
Expand Down
38 changes: 19 additions & 19 deletions simulator/generation/property.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use crate::{
},
table::Value,
},
runner::env::SimulatorEnv,
runner::env::{SimulatorEnv, SimulatorEnvTrait},
};

use super::{
Expand Down Expand Up @@ -170,8 +170,8 @@ impl Property {
message: format!("table {} exists", insert.table()),
func: Box::new({
let table_name = table.clone();
move |_: &Vec<ResultSet>, env: &SimulatorEnv| {
Ok(env.tables.iter().any(|t| t.name == table_name))
move |_: &Vec<ResultSet>, env: &dyn SimulatorEnvTrait| {
Ok(env.tables().iter().any(|t| t.name == table_name))
}
}),
});
Expand All @@ -182,7 +182,7 @@ impl Property {
row.iter().map(|v| v.to_string()).collect::<Vec<String>>(),
insert.table(),
),
func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
func: Box::new(move |stack: &Vec<ResultSet>, _: &dyn SimulatorEnvTrait| {
let rows = stack.last().unwrap();
match rows {
Ok(rows) => Ok(rows.iter().any(|r| r == &row)),
Expand All @@ -206,8 +206,8 @@ impl Property {
let assumption = Interaction::Assumption(Assertion {
message: "Double-Create-Failure should not be called on an existing table"
.to_string(),
func: Box::new(move |_: &Vec<ResultSet>, env: &SimulatorEnv| {
Ok(!env.tables.iter().any(|t| t.name == table_name))
func: Box::new(move |_: &Vec<ResultSet>, env: &dyn SimulatorEnvTrait| {
Ok(!env.tables().iter().any(|t| t.name == table_name))
}),
});

Expand All @@ -220,7 +220,7 @@ impl Property {
message:
"creating two tables with the name should result in a failure for the second query"
.to_string(),
func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
func: Box::new(move |stack: &Vec<ResultSet>, _: &dyn SimulatorEnvTrait| {
let last = stack.last().unwrap();
match last {
Ok(_) => Ok(false),
Expand All @@ -245,8 +245,8 @@ impl Property {
message: format!("table {} exists", table_name),
func: Box::new({
let table_name = table_name.clone();
move |_: &Vec<ResultSet>, env: &SimulatorEnv| {
Ok(env.tables.iter().any(|t| t.name == table_name))
move |_: &Vec<ResultSet>, env: &dyn SimulatorEnvTrait| {
Ok(env.tables().iter().any(|t| t.name == table_name))
}
}),
});
Expand All @@ -257,7 +257,7 @@ impl Property {

let assertion = Interaction::Assertion(Assertion {
message: "select query should respect the limit clause".to_string(),
func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
func: Box::new(move |stack: &Vec<ResultSet>, _: &dyn SimulatorEnvTrait| {
let last = stack.last().unwrap();
match last {
Ok(rows) => Ok(limit >= rows.len()),
Expand All @@ -281,8 +281,8 @@ impl Property {
message: format!("table {} exists", table),
func: Box::new({
let table = table.clone();
move |_: &Vec<ResultSet>, env: &SimulatorEnv| {
Ok(env.tables.iter().any(|t| t.name == table))
move |_: &Vec<ResultSet>, env: &dyn SimulatorEnvTrait| {
Ok(env.tables().iter().any(|t| t.name == table))
}
}),
});
Expand All @@ -292,7 +292,7 @@ impl Property {
"select '{}' should return no values for table '{}'",
predicate, table,
),
func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
func: Box::new(move |stack: &Vec<ResultSet>, _: &dyn SimulatorEnvTrait| {
let rows = stack.last().unwrap();
match rows {
Ok(rows) => Ok(rows.is_empty()),
Expand Down Expand Up @@ -332,8 +332,8 @@ impl Property {
message: format!("table {} exists", table),
func: Box::new({
let table = table.clone();
move |_: &Vec<ResultSet>, env: &SimulatorEnv| {
Ok(env.tables.iter().any(|t| t.name == table))
move |_: &Vec<ResultSet>, env: &dyn SimulatorEnvTrait| {
Ok(env.tables().iter().any(|t| t.name == table))
}
}),
});
Expand All @@ -345,7 +345,7 @@ impl Property {
"select query should result in an error for table '{}'",
table
),
func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
func: Box::new(move |stack: &Vec<ResultSet>, _: &dyn SimulatorEnvTrait| {
let last = stack.last().unwrap();
match last {
Ok(_) => Ok(false),
Expand Down Expand Up @@ -377,8 +377,8 @@ impl Property {
message: format!("table {} exists", table),
func: Box::new({
let table = table.clone();
move |_: &Vec<ResultSet>, env: &SimulatorEnv| {
Ok(env.tables.iter().any(|t| t.name == table))
move |_: &Vec<ResultSet>, env: &dyn SimulatorEnvTrait| {
Ok(env.tables().iter().any(|t| t.name == table))
}
}),
});
Expand All @@ -401,7 +401,7 @@ impl Property {

let assertion = Interaction::Assertion(Assertion {
message: "select queries should return the same amount of results".to_string(),
func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
func: Box::new(move |stack: &Vec<ResultSet>, _: &dyn SimulatorEnvTrait| {
let select_star = stack.last().unwrap();
let select_predicate = stack.get(stack.len() - 2).unwrap();
match (select_predicate, select_star) {
Expand Down
66 changes: 45 additions & 21 deletions simulator/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use rand::prelude::*;
use runner::cli::SimulatorCLI;
use runner::env::SimulatorEnv;
use runner::execution::{execute_plans, Execution, ExecutionHistory, ExecutionResult};
use runner::watch;
use runner::{differential, watch};
use std::any::Any;
use std::backtrace::Backtrace;
use std::io::Write;
Expand Down Expand Up @@ -85,10 +85,30 @@ fn main() -> Result<(), String> {

if cli_opts.watch {
watch_mode(seed, &cli_opts, &paths, last_execution.clone()).unwrap();
} else if cli_opts.differential {
differential_testing(env, plans, last_execution.clone())
} else {
run_simulator(seed, &cli_opts, &paths, env, plans, last_execution.clone());
run_simulator(&cli_opts, &paths, env, plans, last_execution.clone());
}

// Print the seed, the locations of the database and the plan file at the end again for easily accessing them.
println!("database path: {:?}", paths.db);
if cli_opts.doublecheck {
println!("doublecheck database path: {:?}", paths.doublecheck_db);
} else if cli_opts.shrink {
println!("shrunk database path: {:?}", paths.shrunk_db);
}
println!("simulator plan path: {:?}", paths.plan);
println!(
"simulator plan serialized path: {:?}",
paths.plan.with_extension("plan.json")
);
if cli_opts.shrink {
println!("shrunk plan path: {:?}", paths.shrunk_plan);
}
println!("simulator history path: {:?}", paths.history);
println!("seed: {}", seed);

Ok(())
}

Expand Down Expand Up @@ -153,7 +173,6 @@ fn watch_mode(
}

fn run_simulator(
seed: u64,
cli_opts: &SimulatorCLI,
paths: &Paths,
env: SimulatorEnv,
Expand Down Expand Up @@ -278,24 +297,6 @@ fn run_simulator(
}
}
}

// Print the seed, the locations of the database and the plan file at the end again for easily accessing them.
println!("database path: {:?}", paths.db);
if cli_opts.doublecheck {
println!("doublecheck database path: {:?}", paths.doublecheck_db);
} else if cli_opts.shrink {
println!("shrunk database path: {:?}", paths.shrunk_db);
}
println!("simulator plan path: {:?}", paths.plan);
println!(
"simulator plan serialized path: {:?}",
paths.plan.with_extension("plan.json")
);
if cli_opts.shrink {
println!("shrunk plan path: {:?}", paths.shrunk_plan);
}
println!("simulator history path: {:?}", paths.history);
println!("seed: {}", seed);
}

fn doublecheck(
Expand Down Expand Up @@ -361,6 +362,29 @@ fn doublecheck(
}
}

fn differential_testing(
env: SimulatorEnv,
plans: Vec<InteractionPlan>,
last_execution: Arc<Mutex<Execution>>,
) {
let env = Arc::new(Mutex::new(env));
let result = SandboxedResult::from(
std::panic::catch_unwind(|| {
let plan = plans[0].clone();
differential::run_simulation(env, &mut [plan], last_execution.clone())
}),
last_execution.clone(),
);

if let SandboxedResult::Correct = result {
log::info!("simulation succeeded");
println!("simulation succeeded");
} else {
log::error!("simulation failed");
println!("simulation failed");
}
}

#[derive(Debug)]
enum SandboxedResult {
Panicked {
Expand Down
2 changes: 2 additions & 0 deletions simulator/runner/cli.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,8 @@ pub struct SimulatorCLI {
help = "enable watch mode that reruns the simulation on file changes"
)]
pub watch: bool,
#[clap(long, help = "run differential testing between sqlite and Limbo")]
pub differential: bool,
}

impl SimulatorCLI {
Expand Down
Loading

0 comments on commit 11970d9

Please sign in to comment.