Merge pull request #16 from informalsystems/gabriela/small-fixes

Fix init value for List and nondet value for constructors with no params

src/boilerplate.rs

@@ -98,6 +98,10 @@ fn init_value_for_type(ctx: &Context, ty: String) -> String {
         return "Map()".to_string();
     }
 
+    if ty.starts_with("List") {
+        return "[]".to_string();
+    }
+
     if ctx.structs.contains_key(&ty) {
         // Type is a struct, initialize fields recursively
         let fields = ctx.structs.get(&ty).unwrap();
@@ -116,7 +120,6 @@ fn init_value_for_type(ctx: &Context, ty: String) -> String {
     }
 
     match ty.as_str() {
-        "List" => "List()".to_string(),
         "str" => "\"\"".to_string(),
         "int" => "0".to_string(),
         "Addr" => "\"s1\"".to_string(),

src/nondet.rs

@@ -153,7 +153,7 @@ impl NondetValue for Constructor {
     fn nondet_info(&self, ctx: &mut Context, ident: &str) -> NondetInfo {
         if self.fields.is_empty() {
             // If the constuctor has no field, it can only contain one value, and that is deterministic
-            return (vec![], self.name.clone());
+            return (vec!["".to_string()], self.name.clone());
         }
 
         let (defs, record) = self.fields.nondet_info(ctx, ident);

tests/snapshots/integration_tests__ctf01.snap

@@ -39,7 +39,8 @@ module oaksecurity_cosmwasm_ctf_01 {
   action deposit_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_Deposit.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_Deposit
     execute_message(message, max_funds)
   }
   pure def withdraw(state: ContractState, env: Env, info: MessageInfo, ids: List[int]): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)

tests/snapshots/integration_tests__ctf02.snap

@@ -43,7 +43,8 @@ module oaksecurity_cosmwasm_ctf_02 {
   action deposit_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_Deposit.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_Deposit
     execute_message(message, max_funds)
   }
   pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)

tests/snapshots/integration_tests__ctf03.snap

@@ -37,39 +37,44 @@ module flash_loan {
   action flash_loan_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: UnknownType = ConstructorForflash_loan.oneOf()
+
+    pure val message: UnknownType = ConstructorForflash_loan
     execute_message(message, max_funds)
   }
   pure def settle_loan(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
 
   action settle_loan_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: UnknownType = ConstructorForsettle_loan.oneOf()
+
+    pure val message: UnknownType = ConstructorForsettle_loan
     execute_message(message, max_funds)
   }
   pure def set_proxy_addr(state: ContractState, info: MessageInfo, proxy_addr: str): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
 
   action set_proxy_addr_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: UnknownType = ConstructorForset_proxy_addr.oneOf()
+
+    pure val message: UnknownType = ConstructorForset_proxy_addr
     execute_message(message, max_funds)
   }
   pure def withdraw_funds(state: ContractState, env: Env, info: MessageInfo, recipient: Addr): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
 
   action withdraw_funds_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: UnknownType = ConstructorForwithdraw_funds.oneOf()
+
+    pure val message: UnknownType = ConstructorForwithdraw_funds
     execute_message(message, max_funds)
   }
   pure def transfer_owner(state: ContractState, info: MessageInfo, new_owner: Addr): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
 
   action transfer_owner_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: UnknownType = ConstructorFortransfer_owner.oneOf()
+
+    pure val message: UnknownType = ConstructorFortransfer_owner
     execute_message(message, max_funds)
   }
   pure def is_trusted(sender: Addr, config: Config): bool = trusted
@@ -183,7 +188,8 @@ module mock_arb {
   action arbitrage_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: UnknownType = ConstructorForarbitrage.oneOf()
+
+    pure val message: UnknownType = ConstructorForarbitrage
     execute_message(message, max_funds)
   }
   pure val DENOM = "uawesome"
@@ -290,7 +296,8 @@ module proxy {
   action request_flash_loan_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: UnknownType = ConstructorForrequest_flash_loan.oneOf()
+
+    pure val message: UnknownType = ConstructorForrequest_flash_loan
     execute_message(message, max_funds)
   }
   pure val DENOM = "uawesome"

tests/snapshots/integration_tests__ctf04.snap

@@ -40,7 +40,8 @@ module oaksecurity_cosmwasm_ctf_04 {
   action mint_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_Mint.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_Mint
     execute_message(message, max_funds)
   }
   pure def burn(state: ContractState, env: Env, info: MessageInfo, shares: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)

tests/snapshots/integration_tests__ctf05.snap

@@ -47,7 +47,8 @@ module oaksecurity_cosmwasm_ctf_05 {
   action deposit_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_Deposit.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_Deposit
     execute_message(message, max_funds)
   }
   pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
@@ -82,15 +83,17 @@ module oaksecurity_cosmwasm_ctf_05 {
   action accept_owner_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_AcceptOwnership.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_AcceptOwnership
     execute_message(message, max_funds)
   }
   pure def drop_owner(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
 
   action drop_owner_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_DropOwnershipProposal.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_DropOwnershipProposal
     execute_message(message, max_funds)
   }
   pure def assert_owner(store: <missing-type>, sender: Addr): Result[(), ContractError] = Ok(())

tests/snapshots/integration_tests__ctf06.snap

@@ -46,23 +46,26 @@ module oaksecurity_cosmwasm_ctf_06 {
   action receive_cw20_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_Receive.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_Receive
     execute_message(message, max_funds)
   }
   pure def propose(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
 
   action propose_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_Propose.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_Propose
     execute_message(message, max_funds)
   }
   pure def resolve_proposal(state: ContractState, env: Env, _info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(response), state)
 
   action resolve_proposal_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_ResolveProposal.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_ResolveProposal
     execute_message(message, max_funds)
   }
   pure def owner_action(state: ContractState, info: MessageInfo, msg: CosmosMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)

tests/snapshots/integration_tests__ctf07.snap

@@ -43,7 +43,8 @@ module oaksecurity_cosmwasm_ctf_07 {
   action deposit_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_Deposit.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_Deposit
     execute_message(message, max_funds)
   }
   pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)

tests/snapshots/integration_tests__ctf09.snap

@@ -44,15 +44,17 @@ module oaksecurity_cosmwasm_ctf_09 {
   action increase_reward_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_IncreaseReward.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_IncreaseReward
     execute_message(message, max_funds)
   }
   pure def deposit(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
 
   action deposit_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_Deposit.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_Deposit
     execute_message(message, max_funds)
   }
   pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
@@ -69,7 +71,8 @@ module oaksecurity_cosmwasm_ctf_09 {
   action claim_rewards_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_ClaimRewards.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_ClaimRewards
     execute_message(message, max_funds)
   }
   pure val DENOM = "uawesome"

tests/snapshots/integration_tests__ctf10.snap

@@ -38,7 +38,8 @@ module oaksecurity_cosmwasm_ctf_10 {
   action mint_action = {
     // TODO: Change next line according to fund expectations
     pure val max_funds = MAX_AMOUNT
-    nondet message: ExecuteMsg = ExecuteMsg_Mint.oneOf()
+
+    pure val message: ExecuteMsg = ExecuteMsg_Mint
     execute_message(message, max_funds)
   }
   pure def reply(state: ContractState, _env: Env, reply: Reply): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state)
@@ -51,7 +52,7 @@ module oaksecurity_cosmwasm_ctf_10 {
 
   pure val init_contract_state = {
         config: { nft_contract: "s1",mint_per_user: 0,total_tokens: 0 },
-    whitelist: { users: <missing-type> }
+    whitelist: { users: [] }
   }
 
   action execute_step = all {