diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs index bb42c3e1..2f913fc5 100644 --- a/crates/formality-check/src/fns.rs +++ b/crates/formality-check/src/fns.rs @@ -5,18 +5,19 @@ use formality_rust::{ }; use formality_types::grammar::{Fallible, Wcs}; -use crate::{mini_rust_check, Check}; +use crate::Check; +use crate::CrateItem; impl Check<'_> { /// A "free function" is a free-standing function that is not part of an impl. - pub(crate) fn check_free_fn(&self, f: &Fn) -> Fallible<()> { - self.check_fn(&Env::default(), Wcs::t(), f) + pub(crate) fn check_free_fn(&self, f: &Fn, all_fn: &Vec) -> Fallible<()> { + self.check_fn(&Env::default(), Wcs::t(), f, all_fn) } /// Invoked for both free functions and methods. - /// + /// /// # Parameters - /// + /// /// * `in_env` -- the environment from the enclosing impl (if any) /// * `in_assumptions` -- where-clauses from the enclosing impl (if any) /// * `f` -- the function definition @@ -25,6 +26,7 @@ impl Check<'_> { in_env: &Env, in_assumptions: impl ToWcs, f: &Fn, + all_fn: &Vec, ) -> Fallible<()> { let in_assumptions = in_assumptions.to_wcs(); @@ -59,7 +61,7 @@ impl Check<'_> { for input_ty in &input_tys { self.prove_goal(&env, &fn_assumptions, input_ty.well_formed())?; } - self.prove_goal(&env, &fn_assumptions, output_ty.well_formed())?; + self.prove_goal(&env, &fn_assumptions, &output_ty.well_formed())?; // Type-check the function body, if present. match body { @@ -71,9 +73,9 @@ impl Check<'_> { // A trusted function body is assumed to be valid, all set. } formality_rust::grammar::FnBody::MiniRust(body) => { - mini_rust_check::check_body(&env, &fn_assumptions, body)?; + self.check_body(&env, &output_ty, &fn_assumptions, body, all_fn, input_tys)?; } - } + }, } Ok(()) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index a6241140..c2beff5f 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -1,5 +1,6 @@ use anyhow::bail; +use crate::CrateItem; use fn_error_context::context; use formality_core::Downcasted; use formality_prove::{Env, Safety}; @@ -18,7 +19,11 @@ use formality_types::{ impl super::Check<'_> { #[context("check_trait_impl({trait_impl:?})")] - pub(super) fn check_trait_impl(&self, trait_impl: &TraitImpl) -> Fallible<()> { + pub(super) fn check_trait_impl( + &self, + trait_impl: &TraitImpl, + all_fn: &Vec, + ) -> Fallible<()> { let TraitImpl { binder, safety: _ } = trait_impl; let mut env = Env::default(); @@ -48,7 +53,7 @@ impl super::Check<'_> { self.check_safety_matches(trait_decl, trait_impl)?; for impl_item in &impl_items { - self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?; + self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item, all_fn)?; } Ok(()) @@ -101,6 +106,7 @@ impl super::Check<'_> { assumptions: impl ToWcs, trait_items: &[TraitItem], impl_item: &ImplItem, + all_fn: &Vec, ) -> Fallible<()> { let assumptions: Wcs = assumptions.to_wcs(); assert!( @@ -108,7 +114,7 @@ impl super::Check<'_> { ); match impl_item { - ImplItem::Fn(v) => self.check_fn_in_impl(env, &assumptions, trait_items, v), + ImplItem::Fn(v) => self.check_fn_in_impl(env, &assumptions, trait_items, v, all_fn), ImplItem::AssociatedTyValue(v) => { self.check_associated_ty_value(env, assumptions, trait_items, v) } @@ -121,6 +127,7 @@ impl super::Check<'_> { impl_assumptions: impl ToWcs, trait_items: &[TraitItem], ii_fn: &Fn, + all_fn: &Vec, ) -> Fallible<()> { let impl_assumptions: Wcs = impl_assumptions.to_wcs(); assert!( @@ -139,7 +146,7 @@ impl super::Check<'_> { tracing::debug!(?ti_fn); - self.check_fn(env, &impl_assumptions, ii_fn)?; + self.check_fn(env, &impl_assumptions, ii_fn, all_fn)?; let mut env = env.clone(); let ( diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs index cee76cef..adf52257 100644 --- a/crates/formality-check/src/lib.rs +++ b/crates/formality-check/src/lib.rs @@ -1,7 +1,5 @@ #![allow(dead_code)] -use formality_types::rust::FormalityLang; - use std::{collections::VecDeque, fmt::Debug}; use anyhow::bail; @@ -13,7 +11,7 @@ use formality_rust::{ }; use formality_types::grammar::{Fallible, Wcs}; -mod mini_rust_check;; +mod mini_rust_check; /// Check all crates in the program. The crates must be in dependency order /// such that any prefix of the crates is a complete program. @@ -63,11 +61,18 @@ impl Check<'_> { fn check_current_crate(&self, c: &Crate) -> Fallible<()> { let Crate { id: _, items } = c; + // Collect all fn informatiion from current crate. + let all_fn: Vec = c + .items + .clone() + .into_iter() + .filter(|item| matches!(item, CrateItem::Fn(_))) + .collect(); self.check_for_duplicate_items()?; for item in items { - self.check_crate_item(item)?; + self.check_crate_item(item, &all_fn)?; } self.check_coherence(c)?; @@ -111,13 +116,13 @@ impl Check<'_> { Ok(()) } - fn check_crate_item(&self, c: &CrateItem) -> Fallible<()> { + fn check_crate_item(&self, c: &CrateItem, all_fn: &Vec) -> Fallible<()> { match c { - CrateItem::Trait(v) => self.check_trait(v), - CrateItem::TraitImpl(v) => self.check_trait_impl(v), + CrateItem::Trait(v) => self.check_trait(v, all_fn), + CrateItem::TraitImpl(v) => self.check_trait_impl(v, all_fn), CrateItem::Struct(s) => self.check_adt(&s.to_adt()), CrateItem::Enum(e) => self.check_adt(&e.to_adt()), - CrateItem::Fn(f) => self.check_free_fn(f), + CrateItem::Fn(f) => self.check_free_fn(f, all_fn), CrateItem::NegTraitImpl(i) => self.check_neg_trait_impl(i), CrateItem::Test(t) => self.check_test(t), } diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index d3d6075c..6256dec4 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -1,9 +1,20 @@ -use formality_core::{term, Fallible, Map, Upcast}; +use std::iter::zip; + +use formality_core::{Fallible, Map, Upcast}; use formality_prove::Env; -use formality_rust::grammar::minirust::{self, LocalId}; -use formality_types::grammar::{Ty, Wcs, Relation}; +use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace}; +use formality_rust::grammar::minirust::PlaceExpression::Local; +use formality_rust::grammar::minirust::ValueExpression::{Fn, Load}; +use formality_rust::grammar::minirust::{ + self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression, +}; +use formality_rust::grammar::FnBoundData; +use formality_types::grammar::FnId; +use formality_types::grammar::{Relation, Ty, Wcs}; use crate::Check; +use crate::CrateItem; +use anyhow::bail; impl Check<'_> { pub(crate) fn check_body( @@ -12,12 +23,15 @@ impl Check<'_> { output_ty: impl Upcast, fn_assumptions: &Wcs, body: minirust::Body, + declared_fn: &Vec, + declared_input_tys: Vec, ) -> Fallible<()> { // Type-check: // // (1) Check that all the types declared for each local variable are well-formed - // (2) Check that the type of the returned local is compatible with the declared return type - // (3) Check that the statements in the body are valid + // (2) Check whether the number of declared function parameters matches the number of arguments provided. + // (3) Check that the type of the returned local is compatible with the declared return type + // (4) Check that the statements in the body are valid let output_ty: Ty = output_ty.upcast(); @@ -25,75 +39,264 @@ impl Check<'_> { for lv in &body.locals { self.prove_goal(&env, &fn_assumptions, lv.ty.well_formed())?; } + + // Check if the local_id in function arguments are declared. + for function_arg_id in &body.args { + if body + .locals + .iter() + .find(|declared_decl| declared_decl.id == *function_arg_id) + .is_none() + { + bail!("Function argument {:?} is not declared, consider declaring them with `let {:?}: type;`", function_arg_id, function_arg_id); + } + } + + // Check if the local_id in the return place are declared. + if body + .locals + .iter() + .find(|declared_decl| declared_decl.id == body.ret) + .is_none() + { + bail!("Function return place {:?} is not declared, consider declaring them with `let {:?}: type;`", body.ret, body.ret); + } let local_variables: Map = body .locals .iter() .map(|lv| (lv.id.clone(), lv.ty.clone())) .collect(); - // (2) Check if the actual return type is the subtype of the declared return type. + // (2) Check whether the number of declared function parameters matches the number of arguments provided. + if declared_input_tys.len() != body.args.len() { + bail!( + "Function argument number mismatch: expected {} arguments, but found {}", + declared_input_tys.len(), + body.args.len() + ); + } + + // (3) Check if the actual return type is the subtype of the declared return type. self.prove_goal( &env, fn_assumptions, Relation::sub(&local_variables[&body.ret], &output_ty), )?; - let env = TypeckEnv { - env, + let mut env = TypeckEnv { + env: env.clone(), output_ty, local_variables, + blocks: body.blocks.clone(), + ret_id: body.ret, + ret_place_is_initialised: false, + declared_input_tys, + declared_fn: declared_fn.to_vec(), + callee_input_tys: Map::new(), }; - // (3) Check statements in body are valid - for block in &body.blocks { - self.check_block(&env, block)?; + // (4) Check statements in body are valid + for block in body.blocks { + self.check_block(&mut env, fn_assumptions, &block)?; } Ok(()) } - - fn check_block(&self, env: &TypeckEnv, block: &minirust::BasicBlock) -> Fallible<()> { - for statement in &block.statements { - self.check_statement(env, statement)?; + + fn check_block( + &self, + env: &mut TypeckEnv, + fn_assumptions: &Wcs, + block: &minirust::BasicBlock, + ) -> Fallible<()> { + for statement in &block.statements { + self.check_statement(env, fn_assumptions, statement)?; } - self.check_terminator(&block.terminator)?; + self.check_terminator(env, fn_assumptions, &block.terminator)?; Ok(()) } - fn check_statement(&self, env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> { + fn check_statement( + &self, + typeck_env: &mut TypeckEnv, + fn_assumptions: &Wcs, + statement: &minirust::Statement, + ) -> Fallible<()> { match statement { minirust::Statement::Assign(place_expression, value_expression) => { - // FIXME: check that the place and value are well-formed - // FIXME: check that the type of the value is a subtype of the place's type + // Check if the place expression is well-formed. + let place_ty = self.check_place(typeck_env, place_expression)?; + // Check if the value expression is well-formed. + let value_ty = self.check_value(typeck_env, value_expression)?; + // Check that the type of the value is a subtype of the place's type + self.prove_goal( + &typeck_env.env, + fn_assumptions, + Relation::sub(value_ty, place_ty), + )?; + // Record if the return place has been initialised. + if *place_expression == PlaceExpression::Local(typeck_env.ret_id.clone()) { + typeck_env.ret_place_is_initialised = true; + } } minirust::Statement::PlaceMention(place_expression) => { - // FIXME: check that the place is well-formed + // Check if the place expression is well-formed. + self.check_place(typeck_env, place_expression)?; // FIXME: check that access the place is allowed per borrowck rules } } + Ok(()) } - fn check_terminator(&self, env: &TypeckEnv, terminator: &minirust::Terminator) -> Fallible<()> { + fn check_terminator( + &self, + typeck_env: &mut TypeckEnv, + fn_assumptions: &Wcs, + terminator: &minirust::Terminator, + ) -> Fallible<()> { match terminator { minirust::Terminator::Goto(bb_id) => { - // FIXME: Check that the basic block `bb_id` exists + // Check that the basic block `bb_id` exists. + self.check_block_exist(typeck_env, bb_id)?; } - minirust::Terminator::Call { callee, arguments, ret, next_block } => { - // FIXME: check that the callee is something callable - // FIXME: check that the arguments are well formed and their types are subtypes of the expected argument types - // FIXME: check that the next block is valid - // FIXME: check that the fn's declared return type is a subtype of the type of the local variable `ret` + minirust::Terminator::Call { + callee, + generic_arguments: _, + arguments: actual_arguments, + ret, + next_block, + } => { + // Function is part of the value expression, so we will check if the function exists in check_value. + self.check_value(typeck_env, callee)?; + // Get argument information from the callee. + let Fn(callee_fn_id) = callee else { + unreachable!("Callee must exists in Terminator::Call"); + }; + let callee_fn_bound_data = typeck_env.callee_input_tys.get(callee_fn_id).unwrap(); + let callee_declared_input_tys = callee_fn_bound_data.input_tys.clone(); + // Check if the numbers of arguments passed equals to number of arguments declared. + let arguments = zip(callee_declared_input_tys, actual_arguments); + for (declared_ty, actual_argument) in arguments { + // Check if the arguments are well formed. + let actual_ty = self.check_argument_expression(typeck_env, actual_argument)?; + // Check if the actual argument type passed in is the subtype of expect argument type. + self.prove_goal( + &typeck_env.env, + fn_assumptions, + Relation::sub(&actual_ty, &declared_ty), + )?; + } + // Check if ret is well-formed. + let actual_return_ty = self.check_place(typeck_env, ret)?; + // Check that the fn's declared return type is a subtype of the type of the local variable `ret` + self.prove_goal( + &typeck_env.env, + fn_assumptions, + Relation::sub(&typeck_env.output_ty, &actual_return_ty), + )?; + + // Check that the next block is valid. + if let Some(bb_id) = next_block { + self.check_block_exist(typeck_env, bb_id)?; + }; } minirust::Terminator::Return => { - // FIXME: Check that the return local variable has been initialized + // Check that the return local variable has been initialized + if !typeck_env.ret_place_is_initialised { + bail!("The return local variable has not been initialized.") + } + } + } + Ok(()) + } + + // Check if the place expression is well-formed, and return the type of the place expression. + fn check_place(&self, env: &TypeckEnv, place: &PlaceExpression) -> Fallible { + let place_ty; + match place { + Local(local_id) => { + // Check if place id is a valid local id. + let Some((_, ty)) = env + .local_variables + .iter() + .find(|(declared_local_id, _)| *declared_local_id == local_id) + else { + bail!( + "PlaceExpression::Local: unknown local name `{:?}`", + local_id + ) + }; + place_ty = ty; + } + } + Ok(place_ty.clone()) + } + + // Check if the value expression is well-formed, and return the type of the value expression. + fn check_value(&self, typeck_env: &mut TypeckEnv, value: &ValueExpression) -> Fallible { + let value_ty; + match value { + Load(place_expression) => { + value_ty = self.check_place(typeck_env, place_expression)?; + Ok(value_ty) + } + Fn(fn_id) => { + // Check if the function called is in declared in current crate. + let item = typeck_env.declared_fn.iter().find(|&item| { + match item { + CrateItem::Fn(fn_declared) => { + if fn_declared.id == *fn_id { + let fn_bound_data = + typeck_env.env.instantiate_universally(&fn_declared.binder); + // Store the callee information in typeck_env, we will need this when type checking Terminator::Call. + typeck_env + .callee_input_tys + .insert(fn_declared.id.clone(), fn_bound_data); + return true; + } + false + } + _ => false, + } + }); + if item == None { + bail!("The function called is not declared in current crate") + } + value_ty = typeck_env.output_ty.clone(); + Ok(value_ty) + } + } + } + + fn check_argument_expression( + &self, + env: &mut TypeckEnv, + arg_expr: &ArgumentExpression, + ) -> Fallible { + let ty; + match arg_expr { + ByValue(val_expr) => { + ty = self.check_value(env, val_expr)?; + } + InPlace(place_expr) => { + ty = self.check_place(env, place_expr)?; + } + } + Ok(ty) + } + + fn check_block_exist(&self, env: &TypeckEnv, id: &BbId) -> Fallible<()> { + for block in env.blocks.iter() { + if *id == block.id { + return Ok(()); } } + bail!("Basic block {:?} does not exist", id) } } -#[term] struct TypeckEnv { env: Env, @@ -102,4 +305,22 @@ struct TypeckEnv { /// Type of each local variable, as declared. local_variables: Map, + + /// All basic blocks of current body. + blocks: Vec, + + /// local_id of return place, + ret_id: LocalId, + + /// Record if the return place has been initialised. + ret_place_is_initialised: bool, + + /// All declared argument type of current function. + declared_input_tys: Vec, + + /// All declared fn in current crate. + declared_fn: Vec, + + /// All information of callee. + callee_input_tys: Map, } diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs index d319f652..9a9a49d6 100644 --- a/crates/formality-check/src/traits.rs +++ b/crates/formality-check/src/traits.rs @@ -1,3 +1,4 @@ +use crate::CrateItem; use anyhow::bail; use fn_error_context::context; use formality_core::Set; @@ -9,7 +10,7 @@ use formality_types::grammar::Fallible; impl super::Check<'_> { #[context("check_trait({:?})", t.id)] - pub(super) fn check_trait(&self, t: &Trait) -> Fallible<()> { + pub(super) fn check_trait(&self, t: &Trait, all_fn: &Vec) -> Fallible<()> { let Trait { safety: _, id: _, @@ -27,7 +28,7 @@ impl super::Check<'_> { self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?; for trait_item in &trait_items { - self.check_trait_item(&env, &where_clauses, trait_item)?; + self.check_trait_item(&env, &where_clauses, trait_item, all_fn)?; } Ok(()) @@ -62,15 +63,22 @@ impl super::Check<'_> { env: &Env, where_clauses: &[WhereClause], trait_item: &TraitItem, + all_fn: &Vec, ) -> Fallible<()> { match trait_item { - TraitItem::Fn(v) => self.check_fn_in_trait(env, where_clauses, v), + TraitItem::Fn(v) => self.check_fn_in_trait(env, where_clauses, v, all_fn), TraitItem::AssociatedTy(v) => self.check_associated_ty(env, where_clauses, v), } } - fn check_fn_in_trait(&self, env: &Env, where_clauses: &[WhereClause], f: &Fn) -> Fallible<()> { - self.check_fn(env, where_clauses, f) + fn check_fn_in_trait( + &self, + env: &Env, + where_clauses: &[WhereClause], + f: &Fn, + all_fn: &Vec, + ) -> Fallible<()> { + self.check_fn(env, where_clauses, f, all_fn) } fn check_associated_ty( diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 1f4f8f25..3fac7ccc 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -16,6 +16,7 @@ use crate::{ }; use super::constraints::Constraints; +use formality_types::grammar::Parameter::Ty; judgment_fn! { pub fn prove_wc( @@ -53,6 +54,14 @@ judgment_fn! { (prove_wc(decls, env, assumptions, WcData::Relation(goal)) => c) ) + ( + (if let Ty(_) = param1.clone())! + (if let Ty(_) = param2.clone())! + (if param1 == param2)! + ----------------------------- ("subtype - reflexive") + (prove_wc(_decls, env, _assumptions, WcData::Relation(Relation::Sub(param1, param2))) => Constraints::none(env)) + ) + ( (decls.impl_decls(&trait_ref.trait_id) => i)! (let (env, subst) = env.existential_substitution(&i.binder)) diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs index 69ff1cfe..191b9ec9 100644 --- a/crates/formality-rust/src/grammar/minirust.rs +++ b/crates/formality-rust/src/grammar/minirust.rs @@ -1,8 +1,9 @@ - use formality_core::id; use formality_macros::term; use formality_types::grammar::{Parameter, Ty}; +use crate::grammar::FnId; + // This definition is based on [MiniRust](https://github.com/minirust/minirust/blob/master/spec/lang/syntax.md). id!(BbId); @@ -50,7 +51,7 @@ pub struct LocalDecl { } /// Based on [MiniRust statements](https://github.com/minirust/minirust/blob/9ae11cc202d040f08bc13ec5254d3d41d5f3cc25/spec/lang/syntax.md#statements-terminators). -#[term($id: ${statements} $terminator;)] +#[term($id: {statements {$*statements} $terminator;})] pub struct BasicBlock { pub id: BbId, pub statements: Vec, @@ -63,9 +64,9 @@ pub enum Statement { #[grammar($v0 = $v1;)] Assign(PlaceExpression, ValueExpression), - #[grammar($v0;)] + // Represent let _ = place; + #[grammar(place_mention($v0);)] PlaceMention(PlaceExpression), - // SetDiscriminant // Validate // Deinit @@ -87,29 +88,40 @@ pub enum Terminator { // // call foo(x, y) // call foo.add(x, y) + // FIXME: allow not having next block for goto, and add a comment for it. #[grammar(call $callee $ $(arguments) -> $ret $:goto $next_block)] Call { + /// What function or method to call. callee: ValueExpression, // cc: CallingConvention, generic_arguments: Vec, + /// The function arguments to pass. arguments: Vec, + /// The place to put the return value into. ret: PlaceExpression, + /// The block to jump to when this call returns. + /// In minirust, if this is None, then UB will be raised when the function returns. + /// FIXME(tiif): should we have the same behaviour as minirust? next_block: Option, }, + /// Return from the current function. #[grammar(return)] Return, } #[term] pub enum ArgumentExpression { + #[grammar(Copy($v0))] ByValue(ValueExpression), + #[grammar(Move($v0))] InPlace(PlaceExpression), } #[term] pub enum ValueExpression { - // Const + #[grammar(fn_id $v0)] + Fn(FnId), // #[grammar($(v0) as $v1)] // Tuple(Vec, Ty), // Union @@ -117,6 +129,7 @@ pub enum ValueExpression { // GetDiscriminant #[grammar(load($v0))] Load(PlaceExpression), + // TODO: literals // AddrOf // UnOp // BinOp @@ -124,11 +137,11 @@ pub enum ValueExpression { #[term] pub enum PlaceExpression { + // FIXME(tiif): if we remove the local keyword, call bar () -> v1 goto bb1; won't work + #[grammar(local($v0))] Local(LocalId), // Deref(Arc), // Field(Arc, FieldId), // Index // Downcast } - - diff --git a/src/lib.rs b/src/lib.rs index c71cfac1..1442d53b 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,5 +1,3 @@ -#![feature(control_flow_enum)] - use std::{path::PathBuf, sync::Arc}; use clap::Parser; diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs new file mode 100644 index 00000000..d4c79c3f --- /dev/null +++ b/src/test/mir_fn_bodies.rs @@ -0,0 +1,504 @@ +/// Test valid assign statement. +#[test] +fn test_assign_statement() { + crate::assert_ok!( + [ + crate Foo { + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + return; + } + + }; + } + ] + expect_test::expect![["()"]] + ) +} + +/// Test valid goto terminator. +#[test] +fn test_goto_terminator() { + crate::assert_ok!( + [ + crate Foo { + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements {} + goto bb1; + } + + bb1: { + statements { + local(v0) = load(local(v1)); + } + return; + } + + }; + } + ] + expect_test::expect![["()"]] + ) +} + +/// Test valid call terminator. +/// This is equivalent to: +/// ``` +/// fn foo(v1: u32) -> u32 { +/// let v0: u32; +/// v0 = v1; +/// return v0; +/// } +/// +/// fn bar(v1: u32) -> u32 { +/// v0 = v1; +/// let v0 = foo(v0); +/// return v0; +/// } +/// ``` +#[test] +fn test_call_terminator() { + crate::assert_ok!( + [ + crate Foo { + fn foo(u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + return; + } + }; + + fn bar(u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + call fn_id foo (Move(local(v0))) -> local(v0) goto bb1; + } + + bb1: { + statements {} + return; + } + }; + } + ] + expect_test::expect![["()"]] + ) +} + +/// Test valid place mention statement. +/// This is equivalent to: +/// ``` +/// fn foo(v1: u32) -> u32 { +/// let v0: u32; +/// v0; +/// v0 = v1; +/// return v0; +/// } +/// +/// ``` +#[test] +fn test_place_mention_statement() { + crate::assert_ok!( + [ + crate Foo { + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + place_mention(local(v0)); + local(v0) = load(local(v1)); + } + return; + } + + }; + } + ] + expect_test::expect![["()"]] + ) +} + +// Test what will happen if the next block does not exist for Terminator::Call. +#[test] +fn test_no_next_bb_for_call_terminator() { + crate::assert_ok!( + [ + crate Foo { + fn foo(u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + return; + } + }; + + fn bar() -> u32 = minirust() -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + call fn_id foo (Move(local(v1))) -> local(v0); + } + + }; + } + ] + expect_test::expect![["()"]] + ) +} + +/// Test the behaviour of assigning value that is not subtype of the place. +/// This is equivalent to: +/// ``` +/// fn foo(v1: u32) -> () { +/// let v0: (); +/// v0 = v1; +/// return v0; +/// } +/// +/// ``` +#[test] +fn test_invalid_assign_statement() { + crate::assert_err!( + [ + crate Foo { + fn foo (u32) -> () = minirust(v1) -> v0 { + let v0: (); + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + return; + } + + }; + } + ] + [] + expect_test::expect![[r#" + judgment `prove { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {u32 <: ()}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_wc { goal: u32 <: (), assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]] + ) +} + +// Test the behaviour of having invalid local name in place mention. +#[test] +fn test_invalid_local_in_place_mention() { + crate::assert_err!( + [ + crate Foo { + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + place_mention(local(v2)); + } + return; + } + + }; + } + ] + [] + expect_test::expect!["PlaceExpression::Local: unknown local name `v2`"] + ) +} + +// Test the behavior of having undeclared local_id in function argument. +#[test] +fn test_undeclared_local_in_function_arg() { + crate::assert_err!( + [ + crate Foo { + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + + bb0: { + statements { + } + return; + } + + }; + } + ] + [] + expect_test::expect!["Function argument v1 is not declared, consider declaring them with `let v1: type;`"] + ) +} + +// Test the behavior of having undeclared local_id in return place. +#[test] +fn test_undeclared_local_in_return_place() { + crate::assert_err!( + [ + crate Foo { + fn foo () -> u32 = minirust() -> v0 { + + bb0: { + statements { + } + return; + } + + }; + } + ] + [] + expect_test::expect!["Function return place v0 is not declared, consider declaring them with `let v0: type;`"] + ) +} + +// Test the behaviour of having invalid bb_id in goto terminator. +#[test] +fn test_invalid_goto_bbid() { + crate::assert_err!( + [ + crate Foo { + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements {} + goto bb1; + } + + }; + } + ] + [] + expect_test::expect![[r#" + Basic block bb1 does not exist"#]] + ) +} + +// Test the behaviour of calling a function that does not exist . +#[test] +fn test_call_invalid_fn() { + crate::assert_err!( + [ + crate Foo { + fn bar() -> u32 = minirust() -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + call fn_id foo (Move(local(v1))) -> local(v0); + } + + }; + } + ] + [] + expect_test::expect![[r#" + The function called is not declared in current crate"#]] + ) +} + +#[test] +// Test what will happen if the type of arguments passed in is not subtype of what is expected. +fn test_pass_non_subtype_arg() { + crate::assert_err!( + [ + crate Foo { + fn foo(u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + return; + } + }; + + fn bar(()) -> () = minirust(v1) -> v0 { + let v0: (); + let v1: (); + + bb0: { + statements { + local(v0) = load(local(v1)); + } + call fn_id foo (Move(local(v1))) -> local(v0) goto bb1; + } + + bb1: { + statements {} + return; + } + + }; + } + ] + [] + expect_test::expect![[r#" + judgment `prove { goal: {() <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {() <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_wc { goal: () <: u32, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]] + ) +} + +// Test the behaviour of having invalid next bbid Terminator::Call. +#[test] +fn test_invalid_next_bbid_for_call_terminator() { + crate::assert_err!( + [ + crate Foo { + fn foo(u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + return; + } + }; + + fn bar() -> u32 = minirust() -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + } + call fn_id foo (Move(local(v1))) -> local(v0) goto bb1; + } + + }; + } + ] + [] + expect_test::expect!["Basic block bb1 does not exist"] + ) +} + +/// Test what will happen if the declared and actual return type are not compatible. +/// This is equivalent to: +/// ``` +/// fn foo(v1: ()) -> u32 { +/// let v0: (); +/// v0 = v1; +/// return v0; +/// } +/// ``` +#[test] +fn test_incompatible_return_type() { + crate::assert_err!( + [ + crate Foo { + fn foo (()) -> u32 = minirust(v1) -> v0 { + let v0: (); + let v1: (); + + bb0: { + statements { + local(v0) = load(local(v1)); + } + return; + } + + }; + } + ] + + [] + + expect_test::expect![[r#" + judgment `prove { goal: {() <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {() <: u32}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_wc { goal: () <: u32, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]] + ) +} + +#[test] +fn test_function_arg_number_mismatch() { + crate::assert_err!( + [ + crate Foo { + fn foo () -> () = minirust(v1) -> v0 { + let v0: (); + let v1: (); + }; + } + ] + + [] + + expect_test::expect!["Function argument number mismatch: expected 0 arguments, but found 1"] + ) +} + +// Test the behaviour of having unitialised return local variable. +#[test] +fn test_uninitialised_return_type() { + crate::assert_err!( + [ + crate Foo { + fn foo () -> u32 = minirust() -> v0 { + let v0: u32; + + bb0: { + statements { + } + return; + } + + }; + } + ] + + [] + + expect_test::expect![[r#" + The return local variable has not been initialized."#]] + ) +} diff --git a/src/test/mod.rs b/src/test/mod.rs index 327f7d0a..ced577b2 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -5,6 +5,7 @@ mod coherence_overlap; mod consts; mod decl_safety; mod functions; +mod mir_fn_bodies; mod well_formed_trait_ref; #[test]