diff --git a/simulator/generation/plan.rs b/simulator/generation/plan.rs index df68a17b8..836c24780 100644 --- a/simulator/generation/plan.rs +++ b/simulator/generation/plan.rs @@ -239,6 +239,28 @@ impl InteractionPlan { env: &mut SimulatorEnv, ) -> Option> { let num_interactions = env.opts.max_interactions as usize; + // If last interaction needs to check all db tables, generate the Property to do so + if let Some(i) = self.plan.last() + && i.check_tables() + { + let check_all_tables = Interactions::new( + i.connection_index, + InteractionsType::Property(Property::AllTableHaveExpectedContent { + tables: env + .connection_context(i.connection_index) + .tables() + .iter() + .map(|t| t.name.clone()) + .collect(), + }), + ); + + let out_interactions = check_all_tables.interactions(); + + self.push(check_all_tables); + return Some(out_interactions); + } + if self.len() < num_interactions { let conn_index = env.choose_conn(rng); let interactions = if self.mvcc && !env.conn_in_transaction(conn_index) { @@ -561,6 +583,14 @@ impl Interactions { InteractionsType::Query(..) | InteractionsType::Fault(..) => None, } } + + /// Whether the interaction needs to check the database tables + pub fn check_tables(&self) -> bool { + match &self.interactions { + InteractionsType::Property(property) => property.check_tables(), + InteractionsType::Query(..) | InteractionsType::Fault(..) => false, + } + } } impl Deref for Interactions { diff --git a/simulator/generation/property.rs b/simulator/generation/property.rs index e3a2f0f8a..8d6b4cb79 100644 --- a/simulator/generation/property.rs +++ b/simulator/generation/property.rs @@ -116,6 +116,17 @@ pub enum Property { TableHasExpectedContent { table: String, }, + /// AllTablesHaveExpectedContent is a property in which the table + /// must have the expected content, i.e. all the insertions and + /// updates and deletions should have been persisted in the way + /// we think they were. + /// The execution of the property is as follows + /// SELECT * FROM + /// ASSERT + /// for each table in the simulator model + AllTableHaveExpectedContent { + tables: Vec, + }, /// 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 @@ -222,11 +233,9 @@ pub enum Property { /// FsyncNoWait { query: Query, - tables: Vec, }, FaultyQuery { query: Query, - tables: Vec, }, /// Property used to subsititute a property with its queries only Queries { @@ -249,6 +258,7 @@ impl Property { Property::InsertValuesSelect { .. } => "Insert-Values-Select", Property::ReadYourUpdatesBack { .. } => "Read-Your-Updates-Back", Property::TableHasExpectedContent { .. } => "Table-Has-Expected-Content", + Property::AllTableHaveExpectedContent { .. } => "All-Tables-Have-Expected-Content", Property::DoubleCreateFailure { .. } => "Double-Create-Failure", Property::SelectLimit { .. } => "Select-Limit", Property::DeleteSelect { .. } => "Delete-Select", @@ -262,6 +272,11 @@ impl Property { } } + /// Property Does some sort of fault injection + pub fn check_tables(&self) -> bool { + matches!(self, Property::FsyncNoWait { .. } | Property::FaultyQuery { .. }) + } + pub fn get_extensional_queries(&mut self) -> Option<&mut Vec> { match self { Property::InsertValuesSelect { queries, .. } @@ -275,7 +290,8 @@ impl Property { | Property::WhereTrueFalseNull { .. } | Property::UNIONAllPreservesCardinality { .. } | Property::ReadYourUpdatesBack { .. } - | Property::TableHasExpectedContent { .. } => None, + | Property::TableHasExpectedContent { .. } + | Property::AllTableHaveExpectedContent { .. } => None, } } @@ -455,7 +471,10 @@ impl Property { | Property::WhereTrueFalseNull { .. } | Property::UNIONAllPreservesCardinality { .. } | Property::ReadYourUpdatesBack { .. } - | Property::TableHasExpectedContent { .. } => unreachable!("No extensional queries"), + | Property::TableHasExpectedContent { .. } + | Property::AllTableHaveExpectedContent { .. } => { + unreachable!("No extensional queries") + } } } @@ -464,6 +483,9 @@ impl Property { /// and `interaction` cannot be serialized directly. pub(crate) fn interactions(&self, connection_index: usize) -> Vec { match self { + Property::AllTableHaveExpectedContent { tables } => { + assert_all_table_values(tables, connection_index).collect() + } Property::TableHasExpectedContent { table } => { let table = table.to_string(); let table_name = table.clone(); @@ -1033,18 +1055,13 @@ impl Property { Interaction::new(connection_index, assertion), ] } - Property::FsyncNoWait { query, tables } => { - let checks = assert_all_table_values(tables, connection_index); - Vec::from_iter( - std::iter::once(Interaction::new( - connection_index, - InteractionType::FsyncQuery(query.clone()), - )) - .chain(checks), - ) + Property::FsyncNoWait { query } => { + vec![Interaction::new( + connection_index, + InteractionType::FsyncQuery(query.clone()), + )] } - Property::FaultyQuery { query, tables } => { - let checks = assert_all_table_values(tables, connection_index); + Property::FaultyQuery { query } => { let query_clone = query.clone(); // A fault may not occur as we first signal we want a fault injected, // then when IO is called the fault triggers. It may happen that a fault is injected @@ -1071,13 +1088,13 @@ impl Property { } }, ); - let first = [ + [ InteractionType::FaultyQuery(query.clone()), InteractionType::Assertion(assert), ] .into_iter() - .map(|i| Interaction::new(connection_index, i)); - Vec::from_iter(first.chain(checks)) + .map(|i| Interaction::new(connection_index, i)) + .collect() } Property::WhereTrueFalseNull { select, predicate } => { let assumption = InteractionType::Assumption(Assertion::new( @@ -1534,6 +1551,17 @@ fn property_table_has_expected_content( } } +fn property_all_tables_have_expected_content( + _rng: &mut R, + _query_distr: &QueryDistribution, + ctx: &impl GenerationContext, + _mvcc: bool, +) -> Property { + Property::AllTableHaveExpectedContent { + tables: ctx.tables().iter().map(|t| t.name.clone()).collect(), + } +} + fn property_select_limit( rng: &mut R, _query_distr: &QueryDistribution, @@ -1704,7 +1732,6 @@ fn property_fsync_no_wait( ) -> Property { Property::FsyncNoWait { query: Query::arbitrary_from(rng, ctx, query_distr), - tables: ctx.tables().iter().map(|t| t.name.clone()).collect(), } } @@ -1716,7 +1743,6 @@ fn property_faulty_query( ) -> Property { Property::FaultyQuery { query: Query::arbitrary_from(rng, ctx, query_distr), - tables: ctx.tables().iter().map(|t| t.name.clone()).collect(), } } @@ -1732,6 +1758,9 @@ impl PropertyDiscriminants { PropertyDiscriminants::InsertValuesSelect => property_insert_values_select, PropertyDiscriminants::ReadYourUpdatesBack => property_read_your_updates_back, PropertyDiscriminants::TableHasExpectedContent => property_table_has_expected_content, + PropertyDiscriminants::AllTableHaveExpectedContent => { + property_all_tables_have_expected_content + } PropertyDiscriminants::DoubleCreateFailure => property_double_create_failure, PropertyDiscriminants::SelectLimit => property_select_limit, PropertyDiscriminants::DeleteSelect => property_delete_select, @@ -1774,6 +1803,8 @@ impl PropertyDiscriminants { 0 } } + // AllTableHaveExpectedContent should only be generated by Properties that inject faults + PropertyDiscriminants::AllTableHaveExpectedContent => 0, PropertyDiscriminants::DoubleCreateFailure => { if !env.opts.disable_double_create_failure { remaining.create / 2 @@ -1872,6 +1903,7 @@ impl PropertyDiscriminants { QueryCapabilities::SELECT.union(QueryCapabilities::UPDATE) } PropertyDiscriminants::TableHasExpectedContent => QueryCapabilities::SELECT, + PropertyDiscriminants::AllTableHaveExpectedContent => QueryCapabilities::SELECT, PropertyDiscriminants::DoubleCreateFailure => QueryCapabilities::CREATE, PropertyDiscriminants::SelectLimit => QueryCapabilities::SELECT, PropertyDiscriminants::DeleteSelect => { diff --git a/simulator/shrink/plan.rs b/simulator/shrink/plan.rs index 93f2f1702..6da5d93e8 100644 --- a/simulator/shrink/plan.rs +++ b/simulator/shrink/plan.rs @@ -101,12 +101,6 @@ impl InteractionPlan { // Remove all properties that do not use the failing tables self.retain_mut(|interactions| { let retain = if idx == failing_interaction_index { - if let InteractionsType::Property( - Property::FsyncNoWait { tables, .. } | Property::FaultyQuery { tables, .. }, - ) = &mut interactions.interactions - { - tables.retain(|table| depending_tables.contains(table)); - } true } else { let mut has_table = interactions @@ -128,14 +122,10 @@ impl InteractionPlan { | Property::Queries { queries } => { extensional_queries.append(queries); } - Property::FsyncNoWait { tables, query } - | Property::FaultyQuery { tables, query } => { - if !query.uses().iter().any(|t| depending_tables.contains(t)) { - tables.clear(); - } else { - tables.retain(|table| depending_tables.contains(table)); - } + Property::AllTableHaveExpectedContent { tables } => { + tables.retain(|table| depending_tables.contains(table)); } + Property::FsyncNoWait { .. } | Property::FaultyQuery { .. } => {} Property::SelectLimit { .. } | Property::SelectSelectOptimizer { .. } | Property::WhereTrueFalseNull { .. } @@ -350,7 +340,8 @@ impl InteractionPlan { | Property::FaultyQuery { .. } | Property::FsyncNoWait { .. } | Property::ReadYourUpdatesBack { .. } - | Property::TableHasExpectedContent { .. } => {} + | Property::TableHasExpectedContent { .. } + | Property::AllTableHaveExpectedContent { .. } => {} } } }