diff --git a/Cargo.lock b/Cargo.lock index d26da84a6..986baa6fe 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1735,6 +1735,8 @@ dependencies = [ "notify", "rand 0.8.5", "rand_chacha 0.3.1", + "regex", + "regex-syntax", "serde", "serde_json", "tempfile", diff --git a/simulator/generation/plan.rs b/simulator/generation/plan.rs index 4717d7309..d06cdfff3 100644 --- a/simulator/generation/plan.rs +++ b/simulator/generation/plan.rs @@ -5,7 +5,7 @@ use serde::{Deserialize, Serialize}; use crate::{ model::{ - query::{Create, Insert, Query, Select}, + query::{Create, Delete, Distinctness, Insert, Query, Select}, table::Value, }, runner::env::SimConnection, @@ -282,6 +282,29 @@ impl Interactions { Property::SelectLimit { select } => { select.shadow(env); } + Property::DeleteSelect { + table, + predicate, + queries, + } => { + let delete = Query::Delete(Delete { + table: table.clone(), + predicate: predicate.clone(), + }); + + let select = Query::Select(Select { + table: table.clone(), + predicate: predicate.clone(), + distinct: Distinctness::All, + limit: None, + }); + + delete.shadow(env); + for query in queries { + query.shadow(env); + } + select.shadow(env); + } } for interaction in property.interactions() { match interaction { @@ -303,7 +326,15 @@ impl Interactions { .unwrap(); table.rows.extend(values); } - Query::Delete(_) => todo!(), + Query::Delete(delete) => { + let table = env + .tables + .iter_mut() + .find(|t| t.name == delete.table) + .unwrap(); + let t2 = &table.clone(); + table.rows.retain_mut(|r| delete.predicate.test(r, t2)); + } Query::Select(_) => {} }, Interaction::Assertion(_) => {} diff --git a/simulator/generation/property.rs b/simulator/generation/property.rs index 3d4b9b4ce..fe454e9fd 100644 --- a/simulator/generation/property.rs +++ b/simulator/generation/property.rs @@ -65,7 +65,7 @@ pub(crate) enum Property { /// Select Limit is a property in which the select query /// has a limit clause that is respected by the query. /// The execution of the property is as follows - /// SELECT * FROM WHERE LIMIT + /// SELECT * FROM WHERE LIMIT /// This property is a single-interaction property. /// The interaction has the following constraints; /// - The select query will respect the limit clause. @@ -73,6 +73,27 @@ pub(crate) enum Property { /// The select query select: Select, }, + /// Delete-Select is a property in which the deleted row + /// must not be in the resulting rows of a select query that has a + /// where clause that matches the deleted row. In practice, `p1` of + /// the delete query will be used as the predicate for the select query, + /// hence the select should return NO ROWS. + /// The execution of the property is as follows + /// DELETE FROM WHERE + /// I_0 + /// I_1 + /// ... + /// I_n + /// SELECT * FROM WHERE + /// The interactions in the middle has the following constraints; + /// - There will be no errors in the middle interactions. + /// - A row that holds for the predicate will not be inserted. + /// - The table `t` will not be renamed, dropped, or altered. + DeleteSelect { + table: String, + predicate: Predicate, + queries: Vec, + }, } impl Property { @@ -81,6 +102,7 @@ impl Property { Property::InsertValuesSelect { .. } => "Insert-Values-Select".to_string(), Property::DoubleCreateFailure { .. } => "Double-Create-Failure".to_string(), Property::SelectLimit { .. } => "Select-Limit".to_string(), + Property::DeleteSelect { .. } => "Delete-Select".to_string(), } } /// interactions construct a list of interactions, which is an executable representation of the property. @@ -217,6 +239,56 @@ impl Property { assertion, ] } + Property::DeleteSelect { + table, + predicate, + queries, + } => { + let assumption = Interaction::Assumption(Assertion { + message: format!("table {} exists", table), + func: Box::new({ + let table = table.clone(); + move |_: &Vec, env: &SimulatorEnv| { + Ok(env.tables.iter().any(|t| t.name == table)) + } + }), + }); + + let assertion = Interaction::Assertion(Assertion { + message: format!( + "select '{}' should return no values for table '{}'", + predicate, table, + ), + func: Box::new(move |stack: &Vec, _: &SimulatorEnv| { + let rows = stack.last().unwrap(); + match rows { + Ok(rows) => Ok(rows.is_empty()), + Err(err) => Err(LimboError::InternalError(err.to_string())), + } + }), + }); + + let delete = Interaction::Query(Query::Delete(Delete { + table: table.clone(), + predicate: predicate.clone(), + })); + + let select = Interaction::Query(Query::Select(Select { + table: table.clone(), + predicate: predicate.clone(), + limit: None, + distinct: Distinctness::All, + })); + + let mut interactions = Vec::new(); + interactions.push(assumption); + interactions.push(delete); + interactions.extend(queries.clone().into_iter().map(Interaction::Query)); + interactions.push(select); + interactions.push(assertion); + + interactions + } } } } @@ -365,6 +437,48 @@ fn property_double_create_failure( } } +fn property_delete_select( + rng: &mut R, + env: &SimulatorEnv, + remaining: &Remaining, +) -> Property { + // Get a random table + let table = pick(&env.tables, rng); + // Generate a random predicate + let predicate = Predicate::arbitrary_from(rng, table); + + // Create random queries respecting the constraints + let mut queries = Vec::new(); + // - [x] There will be no errors in the middle interactions. (this constraint is impossible to check, so this is just best effort) + // - [x] A row that holds for the predicate will not be inserted. + // - [ ] The table `t` will not be renamed, dropped, or altered. (todo: add this constraint once ALTER or DROP is implemented) + for _ in 0..rng.gen_range(0..3) { + let query = Query::arbitrary_from(rng, (env, remaining)); + match &query { + Query::Insert(Insert::Values { table: t, values }) => { + // A row that holds for the predicate will not be inserted. + if t == &table.name && values.iter().any(|v| predicate.test(v, table)) { + continue; + } + } + Query::Create(Create { table: t }) => { + // There will be no errors in the middle interactions. + // - Creating the same table is an error + if t.name == table.name { + continue; + } + } + _ => (), + } + queries.push(query); + } + + Property::DeleteSelect { + table: table.name.clone(), + predicate, + queries, + } +} impl ArbitraryFrom<(&SimulatorEnv, &InteractionStats)> for Property { fn arbitrary_from( rng: &mut R, @@ -385,6 +499,10 @@ impl ArbitraryFrom<(&SimulatorEnv, &InteractionStats)> for Property { remaining_.read, Box::new(|rng: &mut R| property_select_limit(rng, env)), ), + ( + f64::min(remaining_.read, remaining_.write), + Box::new(|rng: &mut R| property_delete_select(rng, env, &remaining_)), + ), ], rng, ) diff --git a/simulator/generation/query.rs b/simulator/generation/query.rs index efafa6c05..7624367a5 100644 --- a/simulator/generation/query.rs +++ b/simulator/generation/query.rs @@ -113,7 +113,7 @@ impl ArbitraryFrom<(&SimulatorEnv, &Remaining)> for Query { Box::new(|rng| Self::Insert(Insert::arbitrary_from(rng, env))), ), ( - 0.0, + remaining.write, Box::new(|rng| Self::Delete(Delete::arbitrary_from(rng, env))), ), ], diff --git a/simulator/model/query.rs b/simulator/model/query.rs index 474a54f1e..9d3b3d404 100644 --- a/simulator/model/query.rs +++ b/simulator/model/query.rs @@ -288,7 +288,7 @@ pub(crate) struct Delete { impl Delete { pub(crate) fn shadow(&self, _env: &mut SimulatorEnv) -> Vec> { - todo!() + vec![] } } diff --git a/simulator/shrink/plan.rs b/simulator/shrink/plan.rs index eed4fbd0f..0ce978ab4 100644 --- a/simulator/shrink/plan.rs +++ b/simulator/shrink/plan.rs @@ -31,7 +31,8 @@ impl InteractionPlan { if let Interactions::Property(p) = interaction { match p { Property::InsertValuesSelect { queries, .. } - | Property::DoubleCreateFailure { queries, .. } => { + | Property::DoubleCreateFailure { queries, .. } + | Property::DeleteSelect { queries, .. } => { queries.clear(); } Property::SelectLimit { .. } => {}