aljaz/turso
1
0
Fork 0
mirror of https://github.com/aljazceru/turso.git synced 2026-02-06 08:44:23 +01:00
Code Issues Packages Projects Releases Wiki Activity

add assumptions to the interactions, where a failing assumption stops

Browse Source 
the execution of the current property and switches to the next one.
This commit is contained in:
alpaylan
2025-01-06 19:04:29 +03:00
parent 2a4d461627
commit daa77feea1
2 changed files with 108 additions and 18 deletions
Download Patch File Download Diff File Expand all files Collapse all files

72
simulator/generation/plan.rs
View File

@@ -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,

54
simulator/main.rs
View File

@@ -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>]) {