Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

simulator: add counterexample minimization #623

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

simulator: add counterexample minimization #623

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2a4d461
previously, interactions plans were comprised of a flat sequence of o…
alpaylan Jan 6, 2025
daa77fe
add assumptions to the interactions, where a failing assumption stops
alpaylan Jan 6, 2025
cc56276
add execution history to the simulator, the history records
alpaylan Jan 7, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
211 changes: 150 additions & 61 deletions simulator/generation/plan.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
use std::{fmt::Display, rc::Rc};

use limbo_core::{Connection, Result, StepResult};
use rand::SeedableRng;
use rand_chacha::ChaCha8Rng;

use crate::{
model::{
Expand All @@ -19,20 +17,56 @@ use super::{pick, pick_index};
pub(crate) type ResultSet = Result<Vec<Vec<Value>>>;

pub(crate) struct InteractionPlan {
pub(crate) plan: Vec<Interaction>,
pub(crate) plan: Vec<Property>,
pub(crate) stack: Vec<ResultSet>,
pub(crate) interaction_pointer: usize,
pub(crate) secondary_pointer: usize,
}

pub(crate) struct Property {
pub(crate) name: Option<String>,
pub(crate) interactions: Vec<Interaction>,
}

impl Property {
pub(crate) fn new(name: Option<String>, interactions: Vec<Interaction>) -> Self {
Self { name, interactions }
}

pub(crate) fn anonymous(interactions: Vec<Interaction>) -> Self {
Self {
name: None,
interactions,
}
}
}

impl Display for InteractionPlan {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
for interaction in &self.plan {
match interaction {
Interaction::Query(query) => writeln!(f, "{};", query)?,
Interaction::Assertion(assertion) => {
writeln!(f, "-- ASSERT: {};", assertion.message)?
for property in &self.plan {
if let Some(name) = &property.name {
writeln!(f, "-- begin testing '{}'", name)?;
}

for interaction in &property.interactions {
if property.name.is_some() {
write!(f, "\t")?;
}
Interaction::Fault(fault) => writeln!(f, "-- FAULT: {};", fault)?,

match interaction {
Interaction::Query(query) => writeln!(f, "{};", query)?,
Interaction::Assumption(assumption) => {
writeln!(f, "-- ASSUME: {};", assumption.message)?
}
Interaction::Assertion(assertion) => {
writeln!(f, "-- ASSERT: {};", assertion.message)?
}
Interaction::Fault(fault) => writeln!(f, "-- FAULT: {};", fault)?,
}
}

if let Some(name) = &property.name {
writeln!(f, "-- end testing '{}'", name)?;
}
}

Expand Down Expand Up @@ -60,6 +94,7 @@ impl Display for InteractionStats {

pub(crate) enum Interaction {
Query(Query),
Assumption(Assertion),
Assertion(Assertion),
Fault(Fault),
}
Expand All @@ -68,13 +103,14 @@ impl Display for Interaction {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
Self::Query(query) => write!(f, "{}", query),
Self::Assumption(assumption) => write!(f, "ASSUME: {}", assumption.message),
Self::Assertion(assertion) => write!(f, "ASSERT: {}", assertion.message),
Self::Fault(fault) => write!(f, "FAULT: {}", fault),
}
}
}

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

pub(crate) struct Assertion {
pub(crate) func: Box<AssertionFunc>,
Expand All @@ -93,11 +129,9 @@ impl Display for Fault {
}
}

pub(crate) struct Interactions(Vec<Interaction>);

impl Interactions {
impl Property {
pub(crate) fn shadow(&self, env: &mut SimulatorEnv) {
for interaction in &self.0 {
for interaction in &self.interactions {
match interaction {
Interaction::Query(query) => match query {
Query::Create(create) => {
Expand All @@ -117,6 +151,7 @@ impl Interactions {
Query::Select(_) => {}
},
Interaction::Assertion(_) => {}
Interaction::Assumption(_) => {}
Interaction::Fault(_) => {}
}
}
Expand All @@ -129,29 +164,29 @@ impl InteractionPlan {
plan: Vec::new(),
stack: Vec::new(),
interaction_pointer: 0,
secondary_pointer: 0,
}
}

pub(crate) fn push(&mut self, interaction: Interaction) {
self.plan.push(interaction);
}

pub(crate) fn stats(&self) -> InteractionStats {
let mut read = 0;
let mut write = 0;
let mut delete = 0;
let mut create = 0;

for interaction in &self.plan {
match interaction {
Interaction::Query(query) => match query {
Query::Select(_) => read += 1,
Query::Insert(_) => write += 1,
Query::Delete(_) => delete += 1,
Query::Create(_) => create += 1,
},
Interaction::Assertion(_) => {}
Interaction::Fault(_) => {}
for property in &self.plan {
for interaction in &property.interactions {
match interaction {
Interaction::Query(query) => match query {
Query::Select(_) => read += 1,
Query::Insert(_) => write += 1,
Query::Delete(_) => delete += 1,
Query::Create(_) => create += 1,
},
Interaction::Assertion(_) => {}
Interaction::Assumption(_) => {}
Interaction::Fault(_) => {}
}
}
}

Expand All @@ -164,36 +199,33 @@ impl InteractionPlan {
}
}

impl ArbitraryFrom<SimulatorEnv> for InteractionPlan {
fn arbitrary_from<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Self {
impl InteractionPlan {
// todo: This is a hack to get around the fact that `ArbitraryFrom<T>` can't take a mutable
// reference of T, so instead write a bespoke function without using the trait system.
pub(crate) fn arbitrary_from<R: rand::Rng>(rng: &mut R, env: &mut SimulatorEnv) -> Self {
let mut plan = InteractionPlan::new();

let mut env = SimulatorEnv {
opts: env.opts.clone(),
tables: vec![],
connections: vec![],
io: env.io.clone(),
db: env.db.clone(),
rng: ChaCha8Rng::seed_from_u64(rng.next_u64()),
};

let num_interactions = env.opts.max_interactions;

// First create at least one table
let create_query = Create::arbitrary(rng);
env.tables.push(create_query.table.clone());
plan.push(Interaction::Query(Query::Create(create_query)));

plan.plan.push(Property {
name: Some("initial table creation".to_string()),
interactions: vec![Interaction::Query(Query::Create(create_query))],
});

while plan.plan.len() < num_interactions {
log::debug!(
"Generating interaction {}/{}",
plan.plan.len(),
num_interactions
);
let interactions = Interactions::arbitrary_from(rng, &(&env, plan.stats()));
interactions.shadow(&mut env);
let property = Property::arbitrary_from(rng, &(env, plan.stats()));
property.shadow(env);

plan.plan.extend(interactions.0.into_iter());
plan.plan.push(property);
}

log::info!("Generated plan with {} interactions", plan.plan.len());
Expand Down Expand Up @@ -251,31 +283,67 @@ impl Interaction {
Self::Assertion(_) => {
unreachable!("unexpected: this function should only be called on queries")
}
Interaction::Fault(_) => {
Self::Assumption(_) => {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Btw you can just do sth like

_ => unreachable!("unexpected: ...")

to reduce some lines-of-code noise from the pattern matching. or alternatively

if let Self::Query(query) = self {
  ...
} else {
  unreachable!(...)
}

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's a nice touch, adding it in the next commit.

unreachable!("unexpected: this function should only be called on queries")
}
Self::Fault(_) => {
unreachable!("unexpected: this function should only be called on queries")
}
}
}

pub(crate) fn execute_assertion(&self, stack: &Vec<ResultSet>) -> Result<()> {
pub(crate) fn execute_assertion(
&self,
stack: &Vec<ResultSet>,
env: &SimulatorEnv,
) -> Result<()> {
match self {
Self::Query(_) => {
unreachable!("unexpected: this function should only be called on assertions")
}
Self::Assertion(assertion) => {
if !assertion.func.as_ref()(stack) {
if !assertion.func.as_ref()(stack, env) {
return Err(limbo_core::LimboError::InternalError(
assertion.message.clone(),
));
}
Ok(())
}
Self::Assumption(_) => {
unreachable!("unexpected: this function should only be called on assertions")
}
Self::Fault(_) => {
unreachable!("unexpected: this function should only be called on assertions")
}
}
}

pub(crate) fn execute_assumption(
&self,
stack: &Vec<ResultSet>,
env: &SimulatorEnv,
) -> Result<()> {
match self {
Self::Query(_) => {
unreachable!("unexpected: this function should only be called on assumptions")
}
Self::Assertion(_) => {
unreachable!("unexpected: this function should only be called on assumptions")
}
Self::Assumption(assumption) => {
if !assumption.func.as_ref()(stack, env) {
return Err(limbo_core::LimboError::InternalError(
assumption.message.clone(),
));
}
Ok(())
}
Self::Fault(_) => {
unreachable!("unexpected: this function should only be called on assumptions")
}
}
}

pub(crate) fn execute_fault(&self, env: &mut SimulatorEnv, conn_index: usize) -> Result<()> {
match self {
Self::Query(_) => {
Expand All @@ -284,6 +352,9 @@ impl Interaction {
Self::Assertion(_) => {
unreachable!("unexpected: this function should only be called on faults")
}
Self::Assumption(_) => {
unreachable!("unexpected: this function should only be called on faults")
}
Self::Fault(fault) => {
match fault {
Fault::Disconnect => {
Expand All @@ -306,7 +377,7 @@ impl Interaction {
}
}

fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Interactions {
fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Property {
// Get a random table
let table = pick(&env.tables, rng);
// Pick a random column
Expand All @@ -324,6 +395,18 @@ fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Inte
row.push(value);
}
}

// Check that the table exists
let assumption = Interaction::Assumption(Assertion {
message: format!("table {} exists", table.name),
func: Box::new({
let table_name = table.name.clone();
move |_: &Vec<ResultSet>, env: &SimulatorEnv| {
env.tables.iter().any(|t| t.name == table_name)
}
}),
});

// Insert the row
let insert_query = Interaction::Query(Query::Insert(Insert {
table: table.name.clone(),
Expand All @@ -345,7 +428,7 @@ fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Inte
column.name,
value,
),
func: Box::new(move |stack: &Vec<ResultSet>| {
func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
let rows = stack.last().unwrap();
match rows {
Ok(rows) => rows.iter().any(|r| r == &row),
Expand All @@ -354,10 +437,13 @@ fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Inte
}),
});

Interactions(vec![insert_query, select_query, assertion])
Property::new(
Some("select contains inserted value".to_string()),
vec![assumption, insert_query, select_query, assertion],
)
}

fn property_double_create_failure<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv) -> Interactions {
fn property_double_create_failure<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv) -> Property {
let create_query = Create::arbitrary(rng);
let table_name = create_query.table.name.clone();
let cq1 = Interaction::Query(Query::Create(create_query.clone()));
Expand All @@ -367,7 +453,7 @@ fn property_double_create_failure<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv
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>| {
func: Box::new(move |stack: &Vec<ResultSet>, _: &SimulatorEnv| {
let last = stack.last().unwrap();
match last {
Ok(_) => false,
Expand All @@ -378,31 +464,34 @@ fn property_double_create_failure<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv
}),
});

Interactions(vec![cq1, cq2, assertion])
Property::new(
Some("creating the same table twice fails".to_string()),
vec![cq1, cq2, assertion],
)
}

fn create_table<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv) -> Interactions {
fn create_table<R: rand::Rng>(rng: &mut R, _env: &SimulatorEnv) -> Property {
let create_query = Interaction::Query(Query::Create(Create::arbitrary(rng)));
Interactions(vec![create_query])
Property::anonymous(vec![create_query])
}

fn random_read<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Interactions {
fn random_read<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Property {
let select_query = Interaction::Query(Query::Select(Select::arbitrary_from(rng, &env.tables)));
Interactions(vec![select_query])
Property::anonymous(vec![select_query])
}

fn random_write<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Interactions {
fn random_write<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Property {
let table = pick(&env.tables, rng);
let insert_query = Interaction::Query(Query::Insert(Insert::arbitrary_from(rng, table)));
Interactions(vec![insert_query])
Property::anonymous(vec![insert_query])
}

fn random_fault<R: rand::Rng>(_rng: &mut R, _env: &SimulatorEnv) -> Interactions {
fn random_fault<R: rand::Rng>(_rng: &mut R, _env: &SimulatorEnv) -> Property {
let fault = Interaction::Fault(Fault::Disconnect);
Interactions(vec![fault])
Property::anonymous(vec![fault])
}

impl ArbitraryFrom<(&SimulatorEnv, InteractionStats)> for Interactions {
impl ArbitraryFrom<(&SimulatorEnv, InteractionStats)> for Property {
fn arbitrary_from<R: rand::Rng>(
rng: &mut R,
(env, stats): &(&SimulatorEnv, InteractionStats),
Expand Down
Loading
Loading