Write tests to a tests/ folder to avoid handling modules

README.md

@@ -26,3 +26,13 @@ rustup target add wasm32-unknown-unknown
 ``` bash
 cargo clean && cargo cosmwasm-to-quint
 ```
+
+4. In order to run the generated tests, you'll need to add some dependencies:
+```bash
+cargo add itf@0.2.4 --dev
+cargo add anyhow@1.0.83 --dev
+cargo add num-bigint@0.4.4 --dev
+cargo add num-traits@0.2.17 --dev
+```
+
+5. TODO: Add instructions on how to produce traces for the test

src/lib.rs

@@ -134,6 +134,7 @@ fn translate_all_items(tcx: TyCtxt) {
 fn translate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>) {
     let mut ctx = Context {
         tcx,
+        crate_name,
         message_type_for_action: HashMap::from([(
             "instantiate".to_string(),
             "InstantiateMsg".to_string(),
@@ -190,8 +191,8 @@ fn translate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>)
         .expect("Unable to write file");
 
     // write tests to file
-    std::fs::create_dir_all("src/mbt").expect("Unable to create directory");
-    std::fs::write(format!("src/mbt/{}.rs", crate_name), tests).expect("Unable to write file");
+    std::fs::create_dir_all("tests").expect("Unable to create directory");
+    std::fs::write(format!("tests/mbt_{}.rs", crate_name), tests).expect("Unable to write file");
 }
 
 // This is the main entry point for the plugin. It prints the generated quint code to STDOUT.

src/quint-lib-files/basicSpells.qnt

@@ -171,15 +171,4 @@ module basicSpells {
 
   pure def listFilter(l: List[a], f: (a) => bool): List[a] =
     l.foldl([], (acc, e) => if (f(e)) acc.append(e) else acc)
-
-  pure def listMap(l: List[a], f: (a) => b): List[b] =
-    l.foldl([], (acc, e) => acc.append(f(e)))
-
-  //// Returns a set of the elements in the list.
-  ////
-  //// - @param __list a list
-  //// - @returns a set of the elements in __list
-  pure def toSet(__list: List[a]): Set[a] = {
-      __list.foldl(Set(), (__s, __e) => __s.union(Set(__e)))
-  }
 }

src/test_generation/boilerplate.rs

@@ -1,10 +1,18 @@
-pub const TEST_HEADER: &str = "
+pub fn test_header(crate_name: &str) -> String {
+    format!(
+        "
 #[cfg(test)]
-pub mod tests {
-    use crate::{
-        mbt::state_structs::*,
-        msg::{ExecuteMsg, InstantiateMsg, QueryMsg},
-    };
+pub mod tests {{
+    use {crate_name}::contract;
+    use {crate_name}::msg::{{ExecuteMsg, InstantiateMsg, QueryMsg}};
+
+{TEST_AUX}
+"
+    )
+}
+
+const TEST_AUX: &str = "
+    use crate::state_structs::*;
     use cosmwasm_std::{coin, Addr, Uint128};
     use cw_multi_test::{App, AppResponse, ContractWrapper, Executor};
     use itf::trace_from_str;
@@ -90,11 +98,7 @@ pub mod tests {
     #[test]
     fn model_test() {
         let mut app = App::default();
-        let code = ContractWrapper::new(
-            crate::contract::execute,
-            crate::contract::instantiate,
-            crate::contract::query,
-        );
+        let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query);
         let code_id = app.store_code(Box::new(code));
 
         // create test state

src/test_generation/mod.rs

@@ -8,7 +8,7 @@ pub fn generate_tests(ctx: Context) -> String {
     format!(
         "{}{}{}{}",
         structs::translate_structs(ctx.clone()),
-        boilerplate::TEST_HEADER,
+        boilerplate::test_header(ctx.crate_name),
         actions::translate_actions(ctx),
         boilerplate::TEST_FOOTER
     )

src/translate.rs

@@ -485,9 +485,6 @@ impl Translatable for rustc_hir::Item<'_> {
           || name.starts_with("ContractError")
           // skip items from proto files
           || format!("{:?}", self.span).contains("protos")
-          // skip items from generated test file
-          // TODO: use parameterized name instead of hardcoded
-          || format!("{:?}", self.span).contains("src/mbt.rs")
         {
             // skip irrelevant items
             return "".to_string();

src/types.rs

@@ -28,8 +28,9 @@ pub struct Function<'f> {
 }
 
 #[derive(Clone)]
-pub struct Context<'tcx> {
+pub struct Context<'tcx, 'c> {
     // global
+    pub crate_name: &'c str,
     pub message_type_for_action: HashMap<String, String>,
     pub constructors: HashMap<String, Constructor>,
     pub structs: HashMap<String, Vec<Field>>,

tests/integration_tests.rs

@@ -64,7 +64,7 @@ fn run(dir: &str, f: impl FnOnce(&mut Command)) -> Result<String> {
         .collect::<Vec<String>>()
         .join("\n\n");
 
-    let mut mbt_entries = fs::read_dir(ws.join("src/mbt"))?
+    let mut mbt_entries = fs::read_dir(ws.join("tests"))?
         .map(|res| res.map(|e| e.path()))
         .collect::<Result<Vec<_>, io::Error>>()?;
     mbt_entries.sort();

tests/snapshots/integration_tests__ctf01.snap

@@ -155,7 +155,7 @@ module oaksecurity_cosmwasm_ctf_01 {
 
 
 mbt:
-oaksecurity_cosmwasm_ctf_01.rs:
+mbt_oaksecurity_cosmwasm_ctf_01.rs:
 
 pub mod state_structs {
     use num_bigint::BigInt;
@@ -220,10 +220,11 @@ pub mod state_structs {
 }
 #[cfg(test)]
 pub mod tests {
-    use crate::{
-        mbt::state_structs::*,
-        msg::{ExecuteMsg, InstantiateMsg, QueryMsg},
-    };
+    use oaksecurity_cosmwasm_ctf_01::contract;
+    use oaksecurity_cosmwasm_ctf_01::msg::{ExecuteMsg, InstantiateMsg, QueryMsg};
+
+
+    use crate::state_structs::*;
     use cosmwasm_std::{coin, Addr, Uint128};
     use cw_multi_test::{App, AppResponse, ContractWrapper, Executor};
     use itf::trace_from_str;
@@ -309,11 +310,7 @@ pub mod tests {
     #[test]
     fn model_test() {
         let mut app = App::default();
-        let code = ContractWrapper::new(
-            crate::contract::execute,
-            crate::contract::instantiate,
-            crate::contract::query,
-        );
+        let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query);
         let code_id = app.store_code(Box::new(code));
 
         // create test state
@@ -342,47 +339,35 @@ pub mod tests {
 
             match action_taken.as_str() {
 
-               "q::init" => {
-                    println!("Initializing contract.");
 
+               "withdraw_action" => {
                     let sender = Addr::unchecked(sender.unwrap());
                     let funds = funds_from_trace(amount, denom);
 
-
-                    let msg = InstantiateMsg { count: 0 };
+                   let message_ids = nondet_picks.message_ids.clone().unwrap().iter().map(|x| x.to_u64().unwrap().into()).collect();
+                    let msg = ExecuteMsg::Withdraw { ids: message_ids };
                     println!("Message: {:?}", msg);
                     println!("Sender: {:?}", sender);
                     println!("Funds: {:?}", funds);
 
-                    test_state.contract_addr = app.instantiate_contract(
-                        code_id,
+                    let res = app.execute_contract(
                         sender,
+                        test_state.contract_addr.clone(),
                         &msg,
                         &funds,
-                        "test",
-                        None,
-                    ).unwrap();
+                    );
 
-                    for (addr, coins) in s.value.bank.clone().iter() {
-                        for (denom, amount) in coins.iter() {
-                            app = mint_tokens(
-                                app,
-                                addr.clone(),
-                                denom.to_string(),
-                                Uint128::new(amount.to_u128().unwrap()),
-                            );
-                        }
-                    }
+                    compare_result(s.value.result.clone(), res)
                 }
 
 
 
-               "withdraw_action" => {
+               "deposit_action" => {
                     let sender = Addr::unchecked(sender.unwrap());
                     let funds = funds_from_trace(amount, denom);
 
-                   let message_ids = nondet_picks.message_ids.clone().unwrap().iter().map(|x| x.to_u64().unwrap().into()).collect();
-                    let msg = ExecuteMsg::Withdraw { ids: message_ids };
+
+                    let msg = ExecuteMsg::Deposit {  };
                     println!("Message: {:?}", msg);
                     println!("Sender: {:?}", sender);
                     println!("Funds: {:?}", funds);
@@ -399,24 +384,37 @@ pub mod tests {
 
 
 
-               "deposit_action" => {
+               "q::init" => {
+                    println!("Initializing contract.");
+
                     let sender = Addr::unchecked(sender.unwrap());
                     let funds = funds_from_trace(amount, denom);
 
 
-                    let msg = ExecuteMsg::Deposit {  };
+                    let msg = InstantiateMsg { count: 0 };
                     println!("Message: {:?}", msg);
                     println!("Sender: {:?}", sender);
                     println!("Funds: {:?}", funds);
 
-                    let res = app.execute_contract(
+                    test_state.contract_addr = app.instantiate_contract(
+                        code_id,
                         sender,
-                        test_state.contract_addr.clone(),
                         &msg,
                         &funds,
-                    );
+                        "test",
+                        None,
+                    ).unwrap();
 
-                    compare_result(s.value.result.clone(), res)
+                    for (addr, coins) in s.value.bank.clone().iter() {
+                        for (denom, amount) in coins.iter() {
+                            app = mint_tokens(
+                                app,
+                                addr.clone(),
+                                denom.to_string(),
+                                Uint128::new(amount.to_u128().unwrap()),
+                            );
+                        }
+                    }
                 }
 
 

tests/snapshots/integration_tests__ctf02.snap

@@ -176,7 +176,7 @@ module oaksecurity_cosmwasm_ctf_02 {
 
 
 mbt:
-oaksecurity_cosmwasm_ctf_02.rs:
+mbt_oaksecurity_cosmwasm_ctf_02.rs:
 
 pub mod state_structs {
     use num_bigint::BigInt;
@@ -245,10 +245,11 @@ pub mod state_structs {
 }
 #[cfg(test)]
 pub mod tests {
-    use crate::{
-        mbt::state_structs::*,
-        msg::{ExecuteMsg, InstantiateMsg, QueryMsg},
-    };
+    use oaksecurity_cosmwasm_ctf_02::contract;
+    use oaksecurity_cosmwasm_ctf_02::msg::{ExecuteMsg, InstantiateMsg, QueryMsg};
+
+
+    use crate::state_structs::*;
     use cosmwasm_std::{coin, Addr, Uint128};
     use cw_multi_test::{App, AppResponse, ContractWrapper, Executor};
     use itf::trace_from_str;
@@ -334,11 +335,7 @@ pub mod tests {
     #[test]
     fn model_test() {
         let mut app = App::default();
-        let code = ContractWrapper::new(
-            crate::contract::execute,
-            crate::contract::instantiate,
-            crate::contract::query,
-        );
+        let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query);
         let code_id = app.store_code(Box::new(code));
 
         // create test state
@@ -367,12 +364,35 @@ pub mod tests {
 
             match action_taken.as_str() {
 
-               "withdraw_action" => {
+
+               "unstake_action" => {
                     let sender = Addr::unchecked(sender.unwrap());
                     let funds = funds_from_trace(amount, denom);
 
-                   let message_amount = nondet_picks.message_amount.clone().unwrap().to_u64().unwrap().into();
-                    let msg = ExecuteMsg::Withdraw { amount: message_amount };
+                   let message_unlock_amount = nondet_picks.message_unlock_amount.clone().unwrap().to_u64().unwrap().into();
+                    let msg = ExecuteMsg::Unstake { unlock_amount: message_unlock_amount };
+                    println!("Message: {:?}", msg);
+                    println!("Sender: {:?}", sender);
+                    println!("Funds: {:?}", funds);
+
+                    let res = app.execute_contract(
+                        sender,
+                        test_state.contract_addr.clone(),
+                        &msg,
+                        &funds,
+                    );
+
+                    compare_result(s.value.result.clone(), res)
+                }
+
+
+
+               "deposit_action" => {
+                    let sender = Addr::unchecked(sender.unwrap());
+                    let funds = funds_from_trace(amount, denom);
+
+
+                    let msg = ExecuteMsg::Deposit {  };
                     println!("Message: {:?}", msg);
                     println!("Sender: {:?}", sender);
                     println!("Funds: {:?}", funds);
@@ -424,34 +444,12 @@ pub mod tests {
 
 
 
-               "unstake_action" => {
-                    let sender = Addr::unchecked(sender.unwrap());
-                    let funds = funds_from_trace(amount, denom);
-
-                   let message_unlock_amount = nondet_picks.message_unlock_amount.clone().unwrap().to_u64().unwrap().into();
-                    let msg = ExecuteMsg::Unstake { unlock_amount: message_unlock_amount };
-                    println!("Message: {:?}", msg);
-                    println!("Sender: {:?}", sender);
-                    println!("Funds: {:?}", funds);
-
-                    let res = app.execute_contract(
-                        sender,
-                        test_state.contract_addr.clone(),
-                        &msg,
-                        &funds,
-                    );
-
-                    compare_result(s.value.result.clone(), res)
-                }
-
-
-
-               "deposit_action" => {
+               "stake_action" => {
                     let sender = Addr::unchecked(sender.unwrap());
                     let funds = funds_from_trace(amount, denom);
 
-
-                    let msg = ExecuteMsg::Deposit {  };
+                   let message_lock_amount = nondet_picks.message_lock_amount.clone().unwrap().to_u64().unwrap().into();
+                    let msg = ExecuteMsg::Stake { lock_amount: message_lock_amount };
                     println!("Message: {:?}", msg);
                     println!("Sender: {:?}", sender);
                     println!("Funds: {:?}", funds);
@@ -468,12 +466,12 @@ pub mod tests {
 
 
 
-               "stake_action" => {
+               "withdraw_action" => {
                     let sender = Addr::unchecked(sender.unwrap());
                     let funds = funds_from_trace(amount, denom);
 
-                   let message_lock_amount = nondet_picks.message_lock_amount.clone().unwrap().to_u64().unwrap().into();
-                    let msg = ExecuteMsg::Stake { lock_amount: message_lock_amount };
+                   let message_amount = nondet_picks.message_amount.clone().unwrap().to_u64().unwrap().into();
+                    let msg = ExecuteMsg::Withdraw { amount: message_amount };
                     println!("Message: {:?}", msg);
                     println!("Sender: {:?}", sender);
                     println!("Funds: {:?}", funds);