From daa77feea13feaf2c48622d4650da9f6af8b18d7 Mon Sep 17 00:00:00 2001 From: alpaylan Date: Mon, 6 Jan 2025 19:04:29 +0300 Subject: [PATCH] add assumptions to the interactions, where a failing assumption stops the execution of the current property and switches to the next one. --- simulator/generation/plan.rs | 72 ++++++++++++++++++++++++++++++++---- simulator/main.rs | 54 +++++++++++++++++++++------ 2 files changed, 108 insertions(+), 18 deletions(-) diff --git a/simulator/generation/plan.rs b/simulator/generation/plan.rs index fafd3741b..ca3a6d503 100644 --- a/simulator/generation/plan.rs +++ b/simulator/generation/plan.rs @@ -57,6 +57,9 @@ impl Display for InteractionPlan { match interaction { Interaction::Query(query) => writeln!(f, "{};", query)?, + Interaction::Assumption(assumption) => { + writeln!(f, "-- ASSUME: {};", assumption.message)? + } Interaction::Assertion(assertion) => { writeln!(f, "-- ASSERT: {};", assertion.message)? } @@ -93,6 +96,7 @@ impl Display for InteractionStats { pub(crate) enum Interaction { Query(Query), + Assumption(Assertion), Assertion(Assertion), Fault(Fault), } @@ -101,13 +105,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) -> bool; +type AssertionFunc = dyn Fn(&Vec, &SimulatorEnv) -> bool; pub(crate) struct Assertion { pub(crate) func: Box, @@ -148,6 +153,7 @@ impl Property { Query::Select(_) => {} }, Interaction::Assertion(_) => {} + Interaction::Assumption(_) => {} Interaction::Fault(_) => {} } } @@ -180,6 +186,7 @@ impl InteractionPlan { Query::Create(_) => create += 1, }, Interaction::Assertion(_) => {} + Interaction::Assumption(_) => {} Interaction::Fault(_) => {} } } @@ -285,31 +292,67 @@ impl Interaction { Self::Assertion(_) => { unreachable!("unexpected: this function should only be called on queries") } - Interaction::Fault(_) => { + Self::Assumption(_) => { + 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) -> Result<()> { + pub(crate) fn execute_assertion( + &self, + stack: &Vec, + 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, + 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(_) => { @@ -318,6 +361,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 => { @@ -358,6 +404,18 @@ fn property_insert_select(rng: &mut R, env: &SimulatorEnv) -> Prop 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, 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(), @@ -379,7 +437,7 @@ fn property_insert_select(rng: &mut R, env: &SimulatorEnv) -> Prop column.name, value, ), - func: Box::new(move |stack: &Vec| { + func: Box::new(move |stack: &Vec, _: &SimulatorEnv| { let rows = stack.last().unwrap(); match rows { Ok(rows) => rows.iter().any(|r| r == &row), @@ -390,7 +448,7 @@ fn property_insert_select(rng: &mut R, env: &SimulatorEnv) -> Prop Property::new( Some("select contains inserted value".to_string()), - vec![insert_query, select_query, assertion], + vec![assumption, insert_query, select_query, assertion], ) } @@ -404,7 +462,7 @@ fn property_double_create_failure(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| { + func: Box::new(move |stack: &Vec, _: &SimulatorEnv| { let last = stack.last().unwrap(); match last { Ok(_) => false, diff --git a/simulator/main.rs b/simulator/main.rs index 794c9c041..ec65e228f 100644 --- a/simulator/main.rs +++ b/simulator/main.rs @@ -273,15 +273,27 @@ fn execute_plan( env.connections[connection_index] = SimConnection::Connected(env.db.connect()); } else { match execute_interaction(env, connection_index, interaction, &mut plan.stack) { - Ok(_) => { + Ok(next_execution) => { log::debug!("connection {} processed", connection_index); - if plan.secondary_pointer + 1 - >= plan.plan[plan.interaction_pointer].interactions.len() - { - plan.interaction_pointer += 1; - plan.secondary_pointer = 0; - } else { - plan.secondary_pointer += 1; + // Move to the next interaction or property + match next_execution { + ExecutionContinuation::NextInteraction => { + if plan.secondary_pointer + 1 + >= plan.plan[plan.interaction_pointer].interactions.len() + { + // If we have reached the end of the interactions for this property, move to the next property + plan.interaction_pointer += 1; + plan.secondary_pointer = 0; + } else { + // Otherwise, move to the next interaction + plan.secondary_pointer += 1; + } + } + ExecutionContinuation::NextProperty => { + // Skip to the next property + plan.interaction_pointer += 1; + plan.secondary_pointer = 0; + } } } Err(err) => { @@ -294,12 +306,23 @@ fn execute_plan( Ok(()) } +/// The next point of control flow after executing an interaction. +/// `execute_interaction` uses this type in conjunction with a result, where +/// the `Err` case indicates a full-stop due to a bug, and the `Ok` case +/// indicates the next step in the plan. +enum ExecutionContinuation { + /// Default continuation, execute the next interaction. + NextInteraction, + /// Typically used in the case of preconditions failures, skip to the next property. + NextProperty, +} + fn execute_interaction( env: &mut SimulatorEnv, connection_index: usize, interaction: &Interaction, stack: &mut Vec, -) -> Result<()> { +) -> Result { log::info!("executing: {}", interaction); match interaction { generation::plan::Interaction::Query(_) => { @@ -314,15 +337,24 @@ fn execute_interaction( stack.push(results); } generation::plan::Interaction::Assertion(_) => { - interaction.execute_assertion(stack)?; + interaction.execute_assertion(stack, env)?; stack.clear(); } + generation::plan::Interaction::Assumption(_) => { + let assumption_result = interaction.execute_assumption(stack, env); + stack.clear(); + + if assumption_result.is_err() { + log::warn!("assumption failed: {:?}", assumption_result); + return Ok(ExecutionContinuation::NextProperty); + } + } Interaction::Fault(_) => { interaction.execute_fault(env, connection_index)?; } } - Ok(()) + Ok(ExecutionContinuation::NextInteraction) } fn compare_equal_rows(a: &[Vec], b: &[Vec]) {