Test generation

README.md

@@ -26,3 +26,14 @@ 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 cw-multi-test@0.16.2 --dev
+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/boilerplate.rs

@@ -3,42 +3,30 @@ use itertools::Itertools;
 use crate::types::Context;
 
 pub const IMPORTS: &str = "
-  import basicSpells.* from \"../lib/basicSpells\"
-  import cw_types.* from \"../lib/cw_types\"
-  import messaging.* from \"../lib/messaging\"
-  import bank from \"../lib/bank\"
+  import basicSpells.* from \"./lib/basicSpells\"
+  import cw_types.* from \"./lib/cw_types\"
+  import cw_utils.* from \"./lib/cw_utils\"
+  import messaging.* from \"./lib/messaging\"
+  import bank from \"./lib/bank\"
 ";
 
 pub const VARS: &str = "
   var contract_state: ContractState
-  var return: Result
+  var result: Result
   var bank: bank::Bank
   var time: int
 ";
 
 pub const CONTRACT_ADDRESS: &str = "
-  pure val CONTRACT_ADDRESS = \"<contract>\"
+  pure val CONTRACT_ADDRESS = \"contract0\"
 ";
 
 pub const VALUES: &str = "
-  pure val ADDRESSES = Set(\"s1\", \"s2\", \"s3\", CONTRACT_ADDRESS)
+  pure val ADDRESSES = Set(\"sender1\", \"sender2\", \"sender3\", CONTRACT_ADDRESS)
   pure val DENOMS = Set(\"d1\", \"uawesome\")
   pure val MAX_AMOUNT = 200
 ";
 
-pub const INITIALIZERS: &str = "
-  pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT))
-
-  val env_val = { block: { time: time } }
-
-  action init = all {
-    contract_state' = init_contract_state,
-    bank' = init_bank_state,
-    return' = Err(\"No previous request\"),
-    time' = 0,
-  }
-";
-
 pub const ACTIONS: &str = "
   action execute_message(message, max_funds) = {
     nondet sender = ADDRESSES.oneOf()
@@ -50,26 +38,29 @@ pub const ACTIONS: &str = "
     val r = execute(contract_state, env_val, info, message)
     all {
       bank.get(sender).get(denom) >= amount,
-      bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount))
-                  .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)),
-      return' = r._1,
+      match r._1 {
+        | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount))
+                               .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount))
+        | Err(_) => bank' = bank
+      },
+      result' = r._1,
       contract_state' = r._2,
     }
   }
 
   action advance_time = time' = time + 1
 
   action step = {
-    val message_getting = get_message(return)
-    val new_return = message_getting._1
+    val message_getting = get_message(result)
+    val new_result = message_getting._1
     val opt_message = message_getting._2
     match opt_message {
       | Some(submsg) => {
-          val current_state = { bank: bank, return: new_return, contract_state: contract_state }
+          val current_state = { bank: bank, result: new_result, contract_state: contract_state }
           val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply)
           all {
             bank' = new_state.bank,
-            return' = new_state.return,
+            result' = new_state.result,
             contract_state' = new_state.contract_state,
             advance_time,
           }
@@ -90,10 +81,43 @@ pub fn pre_items(crate_name: &str) -> String {
     )
 }
 
+pub fn initializers(ctx: &Context) -> String {
+    let instatiate_msg = ctx.message_type_for_action.get("instantiate").unwrap();
+    format!(
+        "
+  pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT))
+
+  val env_val = {{ block: {{ time: time }} }}
+
+  action init = {{
+    // TODO: Change next line according to fund expectations
+    pure val max_funds = 0
+
+    nondet sender = Set(\"admin\").oneOf()
+    nondet denom = DENOMS.oneOf()
+    nondet amount = 0.to(max_funds).oneOf()
+    val funds = [{{ denom: denom, amount: amount }}]
+    val info = {{ sender: sender, funds: funds }}
+
+    pure val message: InstantiateMsg = {}
+    pure val r = instantiate(init_contract_state, {{ block: {{ time: 0 }} }}, info, message)
+
+    all {{
+      contract_state' = r._2,
+      bank' = init_bank_state,
+      result' = r._1,
+      time' = 0,
+    }}
+  }}
+",
+        init_value_for_type(ctx, instatiate_msg.clone())
+    )
+}
+
 // TODO: This doesn't belong here, but I'm not sure where to put it
 /// Generates a default value for a given type, used to initialize values of all
 /// contract state fields
-fn init_value_for_type(ctx: &Context, ty: String) -> String {
+pub fn init_value_for_type(ctx: &Context, ty: String) -> String {
     if ty.contains("->") {
         return "Map()".to_string();
     }
@@ -137,29 +161,21 @@ pub fn post_items(ctx: &Context) -> String {
         .iter()
         .map(|x| format!("{}: {}", x.0, x.1))
         .collect_vec()
-        .join(",\n  ");
+        .join(",\n    ");
 
     // After all items were visited, we can produce the complete contract state initializer
     let initializer = ctx
         .contract_state
         .iter()
-        .map(|field| {
-            format!(
-                "    {}: {}",
-                field.0,
-                init_value_for_type(ctx, field.1.clone())
-            )
-        })
+        .map(|field| format!("{}: {}", field.0, init_value_for_type(ctx, field.1.clone())))
         .collect_vec()
-        .join(",\n");
+        .join(",\n    ");
 
     let special_actions = ["execute", "instantiate", "reply"];
     let reply = if !ctx.ops_with_mutability.contains(&"reply".to_string()) {
         // Generate default reply to be given for the message handler
         "
-
   pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state)
-
 "
     } else {
         "\n"
@@ -190,8 +206,9 @@ pub fn post_items(ctx: &Context) -> String {
     advance_time,
   }}
 {reply}
-{INITIALIZERS}
+{}
 {ACTIONS}
-}}"
+}}",
+        initializers(ctx)
     )
 }

src/lib.rs

@@ -5,6 +5,7 @@
 pub mod boilerplate;
 pub mod nondet;
 pub mod state_extraction;
+pub mod test_generation;
 pub mod translate;
 pub mod types;
 
@@ -30,6 +31,7 @@ use translate::Translatable;
 use crate::types::{Constructor, Context};
 
 use crate::boilerplate::{post_items, pre_items};
+use crate::test_generation::generate_tests;
 
 // This struct is the plugin provided to the rustc_plugin framework,
 // and it must be exported for use by the CLI/driver binaries.
@@ -125,13 +127,14 @@ fn translate_all_items(tcx: TyCtxt) {
 
     items_by_crate.into_iter().for_each(|(crate_id, items)| {
         let crate_name = tcx.crate_name(crate_id);
-        traslate_items(tcx, crate_name.as_str(), items.collect_vec())
+        translate_items(tcx, crate_name.as_str(), items.collect_vec())
     });
 }
 
-fn traslate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>) {
+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(),
@@ -147,6 +150,11 @@ fn traslate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>) {
         structs: HashMap::new(),
         ops_with_mutability: vec![],
         contract_state: vec![],
+        nondet_picks: vec![
+            ("sender".to_string(), "Addr".to_string()),
+            ("denom".to_string(), "str".to_string()),
+            ("amount".to_string(), "int".to_string()),
+        ],
         // scoped
         record_fields: vec![],
         struct_fields: vec![],
@@ -170,12 +178,46 @@ fn traslate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>) {
         return;
     }
 
-    println!("{}", pre_items(crate_name));
-    println!("{}", translated_items);
-    println!("{}", post_items(&ctx));
+    let module = format!(
+        "{}\n{}\n{}\n",
+        pre_items(crate_name),
+        translated_items,
+        post_items(&ctx)
+    );
+    let tests = generate_tests(ctx.clone());
+
+    // write module to file
+    std::fs::write(format!("quint/{}_stubs.qnt", crate_name), module)
+        .expect("Unable to write file");
+
+    // write tests to file
+    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.
 fn cosmwasm_to_quint(tcx: TyCtxt, _args: &CosmwasmToQuintPluginArgs) {
+    // create directories for the output files (if they don't already exist)
+    std::fs::create_dir_all("quint/lib").expect("Unable to create directory");
+    std::fs::create_dir_all("tests").expect("Unable to create directory");
+
+    // Read quint lib files. `include_str!` makes it so they are read at
+    // compilation time, and therefore get embeded in the cosmwasm-to-quint executable
+    let bank = include_str!("./quint-lib-files/bank.qnt");
+    let basic_spells = include_str!("./quint-lib-files/basicSpells.qnt");
+    let bounded_uint = include_str!("./quint-lib-files/BoundedUInt.qnt");
+    let cw_types = include_str!("./quint-lib-files/cw_types.qnt");
+    let cw_utils = include_str!("./quint-lib-files/cw_utils.qnt");
+    let messaging = include_str!("./quint-lib-files/messaging.qnt");
+
+    // Write the lib files in runtime
+    std::fs::write("quint/lib/bank.qnt", bank).expect("Unable to write file");
+    std::fs::write("quint/lib/basicSpells.qnt", basic_spells).expect("Unable to write file");
+    std::fs::write("quint/lib/BoundedUInt.qnt", bounded_uint).expect("Unable to write file");
+    std::fs::write("quint/lib/cw_types.qnt", cw_types).expect("Unable to write file");
+    std::fs::write("quint/lib/cw_utils.qnt", cw_utils).expect("Unable to write file");
+    std::fs::write("quint/lib/messaging.qnt", messaging).expect("Unable to write file");
+
     translate_all_items(tcx);
+
+    println!("Sucessfully generated files. Quint files are inside quint/ and test files are inside tests/.")
 }

src/nondet.rs

@@ -17,15 +17,16 @@ pub trait NondetValue: Translatable {
     fn nondet_definition(&self, ctx: &mut Context, ident: &str) -> String {
         let info = self.nondet_info(ctx, ident);
         let ty = self.translate(ctx);
-        nondet_info_to_def(info, &ty, ident)
+        nondet_info_to_def(ctx, info, &ty, ident)
     }
 }
 
 /// Converts a NondetInfo to a definition for a nondeterministic value with the
 /// given identifier, ready to be printed.
-fn nondet_info_to_def(info: NondetInfo, ty: &str, ident: &str) -> String {
+fn nondet_info_to_def(ctx: &mut Context, info: NondetInfo, ty: &str, ident: &str) -> String {
     let (auxiliary_defs, value) = info;
     if auxiliary_defs.is_empty() {
+        ctx.nondet_picks.push((ident.to_string(), ty.to_string()));
         format!("nondet {}: {} = {}.oneOf()", ident, ty, value)
     } else {
         format!(
@@ -82,25 +83,9 @@ fn nondet_value_for_list(ty: &rustc_hir::Ty<'_>, ctx: &mut Context, ident: &str)
         return (element_defs, format!("[{element_value}]"));
     }
 
-    let defs = vec![
-        format!(
-            "val possibilities = {}.map(i => Some(i)).union(Set(None))",
-            element_value
-        ),
-        "nondet v1 = possibilities.oneOf()".to_string(),
-        "nondet v2 = possibilities.oneOf()".to_string(),
-        "nondet v3 = possibilities.oneOf()".to_string(),
-    ];
-
-    let value = "
-    [v1, v2, v3].foldl([], (acc, v) => match v {
-      | Some(i) => acc.append(i)
-      | None => acc
-    })
-"
-    .to_string();
+    let value = format!("{element_value}.allListsUpTo(2)");
 
-    (defs, value)
+    (vec![], value)
 }
 
 fn nondet_value_for_option(ty: &rustc_hir::Ty<'_>, ctx: &mut Context, ident: &str) -> NondetInfo {
@@ -122,13 +107,14 @@ fn nondet_value_for_option(ty: &rustc_hir::Ty<'_>, ctx: &mut Context, ident: &st
 }
 
 impl NondetValue for Vec<Field> {
-    fn nondet_info(&self, _ctx: &mut Context, ident: &str) -> NondetInfo {
+    fn nondet_info(&self, ctx: &mut Context, ident: &str) -> NondetInfo {
         // Each field needs its own named nondet value, in the form of
         // `nondet ident_field_name: field_type = something.oneOf()`
         let defs = self
             .iter()
             .map(|field| {
                 nondet_info_to_def(
+                    ctx,
                     field.nondet_info.clone(),
                     &field.ty,
                     format!("{}_{}", ident, field.name).as_str(),

src/quint-lib-files/basicSpells.qnt

@@ -171,4 +171,15 @@ 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 l a list
+  //// - @returns a set of the elements in l
+  pure def toSet(l: List[a]): Set[a] = {
+      l.foldl(Set(), (s, e) => s.union(Set(e)))
+  }
 }

src/quint-lib-files/cw_utils.qnt

@@ -10,7 +10,7 @@ module cw_utils {
     } else if (info.funds.indices().size() == 1) {
       val coin = info.funds[0]
       if (coin.amount == 0) {
-        Err("No funds")
+        Err("Zero funds")
       } else {
         Ok(coin)
       }
@@ -24,7 +24,7 @@ module cw_utils {
       | Err(err) => Err(err)
       | Ok(coin) => {
         if (coin.denom != denom) {
-          Err("Missing Denom")
+          Err("Wrong Denom")
         } else {
           Ok(coin.amount)
         }