add assumptions to the interactions, where a failing assumption stops

the execution of the current property and switches to the next one.

Author: alpaylan

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<ResultSet>) -> bool;
+type AssertionFunc = dyn Fn(&Vec<ResultSet>, &SimulatorEnv) -> bool;
 
 pub(crate) struct Assertion {
     pub(crate) func: Box<AssertionFunc>,
@@ -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<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(_) => {
@@ -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<R: rand::Rng>(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<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(),
@@ -379,7 +437,7 @@ fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Prop
             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),
@@ -390,7 +448,7 @@ fn property_insert_select<R: rand::Rng>(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<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,

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<ResultSet>,
-) -> Result<()> {
+) -> Result<ExecutionContinuation> {
     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<Value>], b: &[Vec<Value>]) {