From 0b9d07db4cd9b22a209e12e78bef3bf2d49c350f Mon Sep 17 00:00:00 2001 From: Jussi Saurio Date: Thu, 14 Aug 2025 18:55:34 +0300 Subject: [PATCH 1/2] sim: restrict Update::arbitrary_from() to SET each column max once --- simulator/generation/query.rs | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/simulator/generation/query.rs b/simulator/generation/query.rs index d55a47c50..fa02858bf 100644 --- a/simulator/generation/query.rs +++ b/simulator/generation/query.rs @@ -300,13 +300,32 @@ impl ArbitraryFrom<(&SimulatorEnv, &Remaining)> for Query { } } +fn pick_unique( + items: &[T], + count: usize, + rng: &mut impl rand::Rng, +) -> Vec +where + ::Owned: PartialEq, +{ + let mut picked: Vec = Vec::new(); + while picked.len() < count { + let item = pick(items, rng); + if !picked.contains(&item.to_owned()) { + picked.push(item.to_owned()); + } + } + picked +} + impl ArbitraryFrom<&SimulatorEnv> for Update { fn arbitrary_from(rng: &mut R, env: &SimulatorEnv) -> Self { let table = pick(&env.tables, rng); let num_cols = rng.gen_range(1..=table.columns.len()); - let set_values: Vec<(String, SimValue)> = (0..num_cols) - .map(|_| { - let column = pick(&table.columns, rng); + let columns = pick_unique(&table.columns, num_cols, rng); + let set_values: Vec<(String, SimValue)> = columns + .iter() + .map(|column| { ( column.name.clone(), SimValue::arbitrary_from(rng, &column.column_type), From 1a1164897491cbf72dc89cbfd96d7a71fe2441ad Mon Sep 17 00:00:00 2001 From: Jussi Saurio Date: Thu, 14 Aug 2025 18:56:53 +0300 Subject: [PATCH 2/2] sim: add Property::ReadYourUpdatesBack --- simulator/generation/property.rs | 86 ++++++++++++++++++++++++++++++++ simulator/model/query/update.rs | 6 +++ simulator/shrink/plan.rs | 4 +- 3 files changed, 95 insertions(+), 1 deletion(-) diff --git a/simulator/generation/property.rs b/simulator/generation/property.rs index d83a60fd1..a3142f3b0 100644 --- a/simulator/generation/property.rs +++ b/simulator/generation/property.rs @@ -58,6 +58,19 @@ pub(crate) enum Property { /// Interactive query information if any interactive: Option, }, + /// ReadYourUpdatesBack is a property in which the updated rows + /// must be in the resulting rows of a select query that has a + /// where clause that matches the updated row. + /// The execution of the property is as follows + /// UPDATE SET WHERE + /// SELECT FROM WHERE + /// These interactions are executed in immediate succession + /// just to verify the property that our updates did what they + /// were supposed to do. + ReadYourUpdatesBack { + update: Update, + select: Select, + }, /// Double Create Failure is a property in which creating /// the same table twice leads to an error. /// The execution of the property is as follows @@ -182,6 +195,7 @@ impl Property { pub(crate) fn name(&self) -> &str { match self { Property::InsertValuesSelect { .. } => "Insert-Values-Select", + Property::ReadYourUpdatesBack { .. } => "Read-Your-Updates-Back", Property::DoubleCreateFailure { .. } => "Double-Create-Failure", Property::SelectLimit { .. } => "Select-Limit", Property::DeleteSelect { .. } => "Delete-Select", @@ -198,6 +212,56 @@ impl Property { /// and `interaction` cannot be serialized directly. pub(crate) fn interactions(&self) -> Vec { match self { + Property::ReadYourUpdatesBack { update, select } => { + let table = update.table().to_string(); + let assumption = Interaction::Assumption(Assertion { + name: format!("table {} exists", table.clone()), + func: Box::new(move |_: &Vec, env: &mut SimulatorEnv| { + if env.tables.iter().any(|t| t.name == table.clone()) { + Ok(Ok(())) + } else { + Ok(Err(format!("table {} does not exist", table.clone()))) + } + }), + }); + + let update_interaction = Interaction::Query(Query::Update(update.clone())); + let select_interaction = Interaction::Query(Query::Select(select.clone())); + + let update = update.clone(); + + let table = update.table().to_string(); + + let assertion = Interaction::Assertion(Assertion { + name: format!( + "updated rows should be found and have the updated values for table {}", + table.clone() + ), + func: Box::new(move |stack: &Vec, _| { + let rows = stack.last().unwrap(); + match rows { + Ok(rows) => { + for row in rows { + for (i, (col, val)) in update.set_values.iter().enumerate() { + if &row[i] != val { + return Ok(Err(format!("updated row {} has incorrect value for column {col}: expected {val}, got {}", i, row[i]))); + } + } + } + Ok(Ok(())) + } + Err(err) => Err(LimboError::InternalError(err.to_string())), + } + }), + }); + + vec![ + assumption, + update_interaction, + select_interaction, + assertion, + ] + } Property::InsertValuesSelect { insert, row_index, @@ -1037,6 +1101,24 @@ fn property_insert_values_select( } } +fn property_read_your_updates_back(rng: &mut R, env: &SimulatorEnv) -> Property { + // e.g. UPDATE t SET a=1, b=2 WHERE c=1; + let update = Update::arbitrary_from(rng, env); + // e.g. SELECT a, b FROM t WHERE c=1; + let select = Select::single( + update.table().to_string(), + update + .set_values + .iter() + .map(|(col, _)| ResultColumn::Column(col.clone())) + .collect(), + update.predicate.clone(), + None, + Distinctness::All, + ); + + Property::ReadYourUpdatesBack { update, select } +} fn property_select_limit(rng: &mut R, env: &SimulatorEnv) -> Property { // Get a random table let table = pick(&env.tables, rng); @@ -1274,6 +1356,10 @@ impl ArbitraryFrom<(&SimulatorEnv, &InteractionStats)> for Property { }, Box::new(|rng: &mut R| property_insert_values_select(rng, env, &remaining_)), ), + ( + f64::min(remaining_.read, remaining_.write), + Box::new(|rng: &mut R| property_read_your_updates_back(rng, env)), + ), ( if !env.opts.disable_double_create_failure { remaining_.create / 2.0 diff --git a/simulator/model/query/update.rs b/simulator/model/query/update.rs index 175ef36f2..a4cc13fa8 100644 --- a/simulator/model/query/update.rs +++ b/simulator/model/query/update.rs @@ -13,6 +13,12 @@ pub(crate) struct Update { pub(crate) predicate: Predicate, } +impl Update { + pub fn table(&self) -> &str { + &self.table + } +} + impl Shadow for Update { type Result = anyhow::Result>>; diff --git a/simulator/shrink/plan.rs b/simulator/shrink/plan.rs index 29ea1b697..0fe329748 100644 --- a/simulator/shrink/plan.rs +++ b/simulator/shrink/plan.rs @@ -78,6 +78,7 @@ impl InteractionPlan { | Property::WhereTrueFalseNull { .. } | Property::UNIONAllPreservesCardinality { .. } | Property::FsyncNoWait { .. } + | Property::ReadYourUpdatesBack { .. } | Property::FaultyQuery { .. } => {} } } @@ -199,7 +200,8 @@ impl InteractionPlan { | Property::SelectLimit { .. } | Property::SelectSelectOptimizer { .. } | Property::FaultyQuery { .. } - | Property::FsyncNoWait { .. } => {} + | Property::FsyncNoWait { .. } + | Property::ReadYourUpdatesBack { .. } => {} } } }