Fix bigIntTDiv division by 0 condition (#209)

* Fix `bigIntTDiv` division by 0 condition * Set Version: 0.1.9 * add test and fix error message --------- Co-authored-by: devops <[email protected]>
runtimeverification · Mar 4, 2024 · 18b8d3f · 18b8d3f
1 parent cf37117
commit 18b8d3f
Show file tree

Hide file tree

Showing 5 changed files with 54 additions and 5 deletions.
diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmultiversx"
-version = "0.1.8"
+version = "0.1.9"
 description = "Python tools for Elrond semantics"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.8
+0.1.9
diff --git a/tests/basic_features.test b/tests/basic_features.test
@@ -73,4 +73,6 @@ deps/mx-sdk-rs/contracts/feature-tests/basic-features/scenarios/storage_u64.scen
 deps/mx-sdk-rs/contracts/feature-tests/basic-features/scenarios/storage_usize_bad.scen.json
 deps/mx-sdk-rs/contracts/feature-tests/basic-features/scenarios/storage_usize.scen.json
 deps/mx-sdk-rs/contracts/feature-tests/basic-features/scenarios/struct_eq.scen.json
+tests/custom-scenarios/basic-features/big_uint_div.scen.json
+tests/custom-scenarios/basic-features/mint_burn_errors.scen.json
 tests/custom-scenarios/basic-features/storage_mapper_fungible_token.scen.json
diff --git a/tests/custom-scenarios/basic-features/big_uint_div.scen.json b/tests/custom-scenarios/basic-features/big_uint_div.scen.json
@@ -0,0 +1,47 @@
+{
+    "name": "pow",
+    "gasSchedule": "v3",
+    "steps": [
+        {
+            "step": "setState",
+            "accounts": {
+                "sc:basic-features": {
+                    "nonce": "0",
+                    "balance": "0",
+                    "storage": {},
+                    "code": "file:../../../deps/mx-sdk-rs/contracts/feature-tests/basic-features/output/basic-features.wasm"
+                },
+                "address:an_account": {
+                    "nonce": "0",
+                    "balance": "0",
+                    "storage": {},
+                    "code": ""
+                }
+            }
+        },
+        {
+            "step": "scCall",
+            "id": "pow",
+            "tx": {
+                "from": "address:an_account",
+                "to": "sc:basic-features",
+                "value": "0",
+                "function": "div_big_uint",
+                "arguments": [
+                    "10",
+                    "0"
+                ],
+                "gasLimit": "50,000,000",
+                "gasPrice": "0"
+            },
+            "expect": {
+                "out": [],
+                "status": "10",
+                "message": "str:division by 0",
+                "logs": "*",
+                "gas": "*",
+                "refund": "*"
+            }
+        }
+    ]
+}
diff --git a/vmhooks/bigIntOps.md b/vmhooks/bigIntOps.md
@@ -315,7 +315,7 @@ module BIGINTOPS
          </bigIntHeap>
       requires OP1_IDX in_keys{{HEAP}}
        andBool OP2_IDX in_keys{{HEAP}}
-       andBool HEAP{{OP1_IDX}} orDefault 0 =/=Int 0
+       andBool HEAP{{OP2_IDX}} orDefault 0 =/=Int 0
       [preserves-definedness]
       // Preserving definedness:
       //  - we checked that /Int is defined
@@ -331,13 +331,13 @@ module BIGINTOPS
         orBool notBool (OP2_IDX in_keys{{HEAP}})
 
     rule <instrs> hostCall("env", "bigIntTDiv", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ])
-               => #throwException(ExecutionFailed, "bigInt division by 0") ...
+               => #throwException(ExecutionFailed, "division by 0") ...
          </instrs>
          <locals> 0 |-> <i32> _DST  1 |-> <i32> OP1_IDX  2 |-> <i32> OP2_IDX </locals>
          <bigIntHeap> HEAP </bigIntHeap>
       requires OP1_IDX in_keys{{HEAP}}
        andBool OP2_IDX in_keys{{HEAP}}
-       andBool HEAP{{OP1_IDX}} orDefault 0 ==Int 0
+       andBool HEAP{{OP2_IDX}} orDefault 0 ==Int 0
 
     // extern int32_t bigIntSign(void* context, int32_t op);
     rule <instrs> hostCall("env", "bigIntSign", [ i32 .ValTypes ] -> [ i32 .ValTypes ])