From 2c521685a12f0588e2db2b6a942aa729860d4171 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 23 Jul 2024 14:24:19 +0200 Subject: [PATCH 1/7] Fixing docs, adding symbolic execution tutorial --- doc/src/SUMMARY.md | 2 +- doc/src/code_examples/contract-symb-1.sol | 9 + doc/src/code_examples/contract-symb-2.sol | 11 ++ doc/src/code_examples/contract-symb-3.sol | 8 + doc/src/equivalence-checking-tutorial.md | 6 +- doc/src/symbolic-execution-tutorial.md | 194 ++++++++++++++++++++++ 6 files changed, 226 insertions(+), 4 deletions(-) create mode 100644 doc/src/code_examples/contract-symb-1.sol create mode 100644 doc/src/code_examples/contract-symb-2.sol create mode 100644 doc/src/code_examples/contract-symb-3.sol create mode 100644 doc/src/symbolic-execution-tutorial.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index d177fc20c..1346e490c 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -6,7 +6,7 @@ - [ds-test tutorial](./ds-test-tutorial.md) - [Equivalence checking tutorial](./equivalence-checking-tutorial.md) - +- [Symbolic execution tutorial](./symbolic-execution-tutorial.md) # Reference diff --git a/doc/src/code_examples/contract-symb-1.sol b/doc/src/code_examples/contract-symb-1.sol new file mode 100644 index 000000000..51b3671ad --- /dev/null +++ b/doc/src/code_examples/contract-symb-1.sol @@ -0,0 +1,9 @@ +//SPDX-License-Identifier: MIT +pragma solidity ^0.8.19; +contract MyContract { + function simple_symb() public pure { + uint i; + i = 1; + assert(i == 2); + } +} diff --git a/doc/src/code_examples/contract-symb-2.sol b/doc/src/code_examples/contract-symb-2.sol new file mode 100644 index 000000000..434011332 --- /dev/null +++ b/doc/src/code_examples/contract-symb-2.sol @@ -0,0 +1,11 @@ +//SPDX-License-Identifier: MIT +pragma solidity ^0.8.19; +contract MyContract { + uint i; + function simple_symb1() public view { + assert(i == 2); + } + function simple_symb2() public view { + assert(i == 3); + } +} diff --git a/doc/src/code_examples/contract-symb-3.sol b/doc/src/code_examples/contract-symb-3.sol new file mode 100644 index 000000000..f9b93d411 --- /dev/null +++ b/doc/src/code_examples/contract-symb-3.sol @@ -0,0 +1,8 @@ +//SPDX-License-Identifier: MIT +pragma solidity ^0.8.19; +contract MyContract { + uint i; + function simple_symb() public view { + assert(i == 0); + } +} diff --git a/doc/src/equivalence-checking-tutorial.md b/doc/src/equivalence-checking-tutorial.md index 17fef86f9..b0a93dc81 100644 --- a/doc/src/equivalence-checking-tutorial.md +++ b/doc/src/equivalence-checking-tutorial.md @@ -7,7 +7,7 @@ checking, one can check whether the two behave the same. ## Finding Discrepancies -Let's see this toy contract, in file [contract1.sol](contract1.sol): +Let's see this toy contract, in file [contract1.sol](code_examples/contract1.sol): ```solidity //SPDX-License-Identifier: MIT @@ -21,7 +21,7 @@ contract MyContract { } ``` -And this, slightly modified one, in file [contract2.sol](contract2.sol): +And this, slightly modified one, in file [contract2.sol](code_examples/contract2.sol): ```solidity //SPDX-License-Identifier: MIT @@ -69,7 +69,7 @@ div 2 = 17` twice, which is 34, the other will add 35. ## Fixing and Proving Correctness Let's fix the above issue by incrementing the balance by 1 in case it's an odd -value. Let's call this [contract3.sol](contract3.sol): +value. Let's call this [contract3.sol](code_examples/contract3.sol): ```solidity //SPDX-License-Identifier: MIT diff --git a/doc/src/symbolic-execution-tutorial.md b/doc/src/symbolic-execution-tutorial.md new file mode 100644 index 000000000..ab646377a --- /dev/null +++ b/doc/src/symbolic-execution-tutorial.md @@ -0,0 +1,194 @@ +# Symbolic Execution Tutorial + +Symbolic execution mode of hevm checks whether any call to the contract could +result in an assertion violation. For more details on what exactly is considered an assertion violation, see +[symbolic]. + + +## Simple Example + +Let's see this toy contract, in file +[contract-symb-1.sol](contract-symb-1.sol): + +```solidity +//SPDX-License-Identifier: MIT +pragma solidity ^0.8.19; +contract MyContract { + function simple_symb() public pure { + uint i; + i = 1; + assert(i == 2); + } +} +``` + +Let's first compile it: + +```shell +$ solc --bin-runtime doc/src/code_examples/contract-symb-1.sol +======= contract-symb-1.sol:MyContract ======= +Binary: +6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f600190506002811460455760446048565b5b50565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea26469706673582212202bc2d2c44310edeba83b816dca9ef8abcc9cc1c775bae801b393bf4d5ff2d32364736f6c63430008180033 +``` + +Now let's symbolically execute it: + +```shell +$ hevm symbolic --sig "simple_symb()" --code "6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f600190506002811460455760446048565b5b50565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea26469706673582212202bc2d2c44310edeba83b816dca9ef8abcc9cc1c775bae801b393bf4d5ff2d32364736f6c63430008180033" + +Discovered the following counterexamples: + +Calldata: + 0x881fc77c5f9a8ff385b17ae4c2b3fc970010862df98bfa2f885b071e8c29c7d920e385230182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002 + +Storage: + Addr SymAddr "miner": [] + Addr SymAddr "origin": [] +``` + +## Symbolically executing a specific function + +When there are more than one functions in the code, the system will try to +symbolically execute all. Let's take the file +[contract-symb-2.sol](contract-symb-2.sol): +```solidity +//SPDX-License-Identifier: MIT +pragma solidity ^0.8.19; +contract MyContract { + uint i; + function simple_symb1() public view { + assert(i == 2); + } + function simple_symb2() public view { + assert(i == 3); + } +} +``` + +And compile it with solc: + +```shell + +$ solc --bin-runtime doc/src/code_examples/contract-symb-2.sol + +======= contract-symb-2.sol:MyContract ======= +Binary of the runtime part: +6080604052348015600e575f80fd5b50600436106030575f3560e01c806385c2fc7114603457806386ae330914603c575b5f80fd5b603a6044565b005b60426055565b005b60025f541460535760526066565b5b565b60035f541460645760636066565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220d70d3cfe85d6f0c8a34ce660d76d7f933db353e59397674009e3a3d982275d7e64736f6c63430008180033 +``` + +Now execute the bytecode symbolically with hevm: + +```shell +$ hevm symbolic --code "6080604052348015600e575f80fd5b50600436106030575f3560e01c806385c2fc7114603457806386ae330914603c575b5f80fd5b603a6044565b005b60426055565b005b60025f541460535760526066565b5b565b60035f541460645760636066565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220d70d3cfe85d6f0c8a34ce660d76d7f933db353e59397674009e3a3d982275d7e64736f6c63430008180033" + +Discovered the following counterexamples: + +Calldata: + 0x85c2fc71 + +Storage: + Addr SymAddr "entrypoint": [(0x0,0x0)] + Addr SymAddr "miner": [] + Addr SymAddr "origin": [] + +Transaction Context: + TxValue: 0x0 + + +Calldata: + 0x86ae3309 + +Storage: + Addr SymAddr "entrypoint": [(0x0,0x0)] + Addr SymAddr "miner": [] + Addr SymAddr "origin": [] + +Transaction Context: + TxValue: 0x0 +``` + +Notice that it discovered two issues. The calldata in each case is the function +signature that `cast` from `foundry` gives for the two functions: + +```shell +$ cast sig "simple_symb1()" +0x85c2fc71 + +$cast sig "simple_symb2()" +0x86ae3309 +``` + +In case you only want to execute a particular function, you tell `hevm` that you only want a particular signature executed: + +```shell +$ hevm symbolic --sig "simple_symb1()" --code "6080604052348015600e575f80fd5b50600436106030575f3560e01c806385c2fc7114603457806386ae330914603c575b5f80fd5b603a6044565b005b60426055565b005b60025f541460535760526066565b5b565b60035f541460645760636066565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220d70d3cfe85d6f0c8a34ce660d76d7f933db353e59397674009e3a3d982275d7e64736f6c63430008180033" + + +Discovered the following counterexamples: + +Calldata: + 0x85c2fc71 + +Storage: + Addr SymAddr "entrypoint": [(0x0,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)] + Addr SymAddr "miner": [] + Addr SymAddr "origin": [] +``` + + +## Abstract versus empty starting storage + +The initial store state of `hevm` is completely abstract. This means that the +functions are explored for all possible values of the state. Let's take the +following contract [contract-symb-3.sol](contract-symb-3.sol): + +```solidity +//SPDX-License-Identifier: MIT +pragma solidity ^0.8.19; +contract MyContract { + uint i; + function simple_symb() public view { + assert(i == 0); + } +} +``` + +Let's compile with solc: + +```shell +solc --bin-runtime doc/src/code_examples/contract-symb-3.sol + +======= contract-symb-3.sol:MyContract ======= +Binary of the runtime part: +6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f805414604057603f6042565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220cf838a7ff084e553805b9b56decd46ea37363e97e26405b2409d22cb905de0e664736f6c63430008180033 +``` + +With default symbolic execution, a counterexample is found: + +```shell +$ cabal hevm symbolic --initial-storage Empty --code "6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f805414604057603f6042565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220cf838a7ff084e553805b9b56decd46ea37363e97e26405b2409d22cb905de0e664736f6c63430008180033" + +Discovered the following counterexamples: + +Calldata: + 0x881fc77c + +Storage: + Addr SymAddr "entrypoint": [(0x0,0x1)] + Addr SymAddr "miner": [] + Addr SymAddr "origin": [] + +Transaction Context: + TxValue: 0x0 +``` + +However, notice that the counterexample has `1` as the value for `i` storage +variable. However, this contract can never actually assign `i` to any value. +Running this contract with `--initial-state Empty` ensures that the default +value, 0, is assigned, and the assert can never fail: + +```shell +cabal run exe:hevm -- symbolic --initial-storage Empty --code "6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f805414604057603f6042565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220cf838a7ff084e553805b9b56decd46ea37363e97e26405b2409d22cb905de0e664736f6c63430008180033" + +QED: No reachable property violations discovered +``` From b10062458bce9bc74c0e50f118da129dc7f37dc0 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 23 Jul 2024 19:02:18 +0200 Subject: [PATCH 2/7] Fixing up text --- doc/src/symbolic-execution-tutorial.md | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/doc/src/symbolic-execution-tutorial.md b/doc/src/symbolic-execution-tutorial.md index ab646377a..f9b8d8714 100644 --- a/doc/src/symbolic-execution-tutorial.md +++ b/doc/src/symbolic-execution-tutorial.md @@ -8,7 +8,7 @@ result in an assertion violation. For more details on what exactly is considered ## Simple Example Let's see this toy contract, in file -[contract-symb-1.sol](contract-symb-1.sol): +[contract-symb-1.sol](code_examples/contract-symb-1.sol): ```solidity //SPDX-License-Identifier: MIT @@ -25,14 +25,13 @@ contract MyContract { Let's first compile it: ```shell -$ solc --bin-runtime doc/src/code_examples/contract-symb-1.sol +$ solc --bin-runtime contract-symb-1.sol ======= contract-symb-1.sol:MyContract ======= Binary: 6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f600190506002811460455760446048565b5b50565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea26469706673582212202bc2d2c44310edeba83b816dca9ef8abcc9cc1c775bae801b393bf4d5ff2d32364736f6c63430008180033 ``` Now let's symbolically execute it: - ```shell $ hevm symbolic --sig "simple_symb()" --code "6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f600190506002811460455760446048565b5b50565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea26469706673582212202bc2d2c44310edeba83b816dca9ef8abcc9cc1c775bae801b393bf4d5ff2d32364736f6c63430008180033" @@ -50,7 +49,7 @@ Storage: When there are more than one functions in the code, the system will try to symbolically execute all. Let's take the file -[contract-symb-2.sol](contract-symb-2.sol): +[contract-symb-2.sol](code_examples/contract-symb-2.sol): ```solidity //SPDX-License-Identifier: MIT pragma solidity ^0.8.19; @@ -69,7 +68,7 @@ And compile it with solc: ```shell -$ solc --bin-runtime doc/src/code_examples/contract-symb-2.sol +$ solc --bin-runtime contract-symb-2.sol ======= contract-symb-2.sol:MyContract ======= Binary of the runtime part: @@ -140,7 +139,7 @@ Storage: The initial store state of `hevm` is completely abstract. This means that the functions are explored for all possible values of the state. Let's take the -following contract [contract-symb-3.sol](contract-symb-3.sol): +following contract [contract-symb-3.sol](code_examples/contract-symb-3.sol): ```solidity //SPDX-License-Identifier: MIT @@ -156,7 +155,7 @@ contract MyContract { Let's compile with solc: ```shell -solc --bin-runtime doc/src/code_examples/contract-symb-3.sol +solc --bin-runtime contract-symb-3.sol ======= contract-symb-3.sol:MyContract ======= Binary of the runtime part: From 5efc017027160c5d09879ac1cb9005174c28ba33 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 23 Jul 2024 19:07:33 +0200 Subject: [PATCH 3/7] Adding tutorial for symbolic execution --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index fca7184e6..b59770366 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -18,6 +18,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Updated Bitwuzla to newer version - New cheatcodes `startPrank()` & `stopPrank()` - ARM64 and x86_64 Mac along with Linux x86_64 static binaries for releases +- Tutorial for symbolic execution ## Fixed - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing From b7eacc2f19e6003557a413cae58da359fe3b3ad9 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 23 Jul 2024 19:17:04 +0200 Subject: [PATCH 4/7] Mini-refactor of docs --- doc/src/symbolic-execution-tutorial.md | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/doc/src/symbolic-execution-tutorial.md b/doc/src/symbolic-execution-tutorial.md index f9b8d8714..725852129 100644 --- a/doc/src/symbolic-execution-tutorial.md +++ b/doc/src/symbolic-execution-tutorial.md @@ -1,13 +1,7 @@ # Symbolic Execution Tutorial Symbolic execution mode of hevm checks whether any call to the contract could -result in an assertion violation. For more details on what exactly is considered an assertion violation, see -[symbolic]. - - -## Simple Example - -Let's see this toy contract, in file +result in an assertion violation. Let's see a simple contract, in file [contract-symb-1.sol](code_examples/contract-symb-1.sol): ```solidity @@ -22,7 +16,7 @@ contract MyContract { } ``` -Let's first compile it: +Let's first compile it with `solc`: ```shell $ solc --bin-runtime contract-symb-1.sol @@ -117,7 +111,8 @@ $cast sig "simple_symb2()" 0x86ae3309 ``` -In case you only want to execute a particular function, you tell `hevm` that you only want a particular signature executed: +In case you only want to execute only a particular function, you tell `hevm` +that you only want a particular signature executed: ```shell $ hevm symbolic --sig "simple_symb1()" --code "6080604052348015600e575f80fd5b50600436106030575f3560e01c806385c2fc7114603457806386ae330914603c575b5f80fd5b603a6044565b005b60426055565b005b60025f541460535760526066565b5b565b60035f541460645760636066565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220d70d3cfe85d6f0c8a34ce660d76d7f933db353e59397674009e3a3d982275d7e64736f6c63430008180033" From 35c833d6055db8c1de031d1817b04e52e1fa81bd Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 23 Jul 2024 19:18:23 +0200 Subject: [PATCH 5/7] More text in doc --- doc/src/symbolic-execution-tutorial.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/doc/src/symbolic-execution-tutorial.md b/doc/src/symbolic-execution-tutorial.md index 725852129..c0983e8cb 100644 --- a/doc/src/symbolic-execution-tutorial.md +++ b/doc/src/symbolic-execution-tutorial.md @@ -186,3 +186,6 @@ cabal run exe:hevm -- symbolic --initial-storage Empty --code "60806040523480156 QED: No reachable property violations discovered ``` + +Here, no counterexamples are discovered, because with empty default state, the +value of `i` is zero, and therefore `assert(i == 0)` will all never trigger. From c108cfce2798e610bdc8d50b410838385d212a65 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 24 Jul 2024 12:42:48 +0200 Subject: [PATCH 6/7] Fixing this output --- doc/src/symbolic-execution-tutorial.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/doc/src/symbolic-execution-tutorial.md b/doc/src/symbolic-execution-tutorial.md index c0983e8cb..4ed63f24c 100644 --- a/doc/src/symbolic-execution-tutorial.md +++ b/doc/src/symbolic-execution-tutorial.md @@ -32,11 +32,14 @@ $ hevm symbolic --sig "simple_symb()" --code "6080604052348015600e575f80fd5b5060 Discovered the following counterexamples: Calldata: - 0x881fc77c5f9a8ff385b17ae4c2b3fc970010862df98bfa2f885b071e8c29c7d920e385230182dad8c17bd5e89e8043a08ada90a6d5efdee4425f85cb863109783e158ba4fba908a0e6fae6c6b51002 + 0x881fc77c Storage: Addr SymAddr "miner": [] Addr SymAddr "origin": [] + +Transaction Context: + TxValue: 0x0 ``` ## Symbolically executing a specific function From fa43ad7db1d6f1da200ecd9db5871045cd89029a Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 24 Jul 2024 12:44:49 +0200 Subject: [PATCH 7/7] Updating signature explanation --- doc/src/symbolic-execution-tutorial.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/src/symbolic-execution-tutorial.md b/doc/src/symbolic-execution-tutorial.md index 4ed63f24c..a0e02a6b8 100644 --- a/doc/src/symbolic-execution-tutorial.md +++ b/doc/src/symbolic-execution-tutorial.md @@ -103,7 +103,7 @@ Transaction Context: TxValue: 0x0 ``` -Notice that it discovered two issues. The calldata in each case is the function +Notice that hevm discovered two issues. The calldata in each case is the function signature that `cast` from `foundry` gives for the two functions: ```shell @@ -114,8 +114,8 @@ $cast sig "simple_symb2()" 0x86ae3309 ``` -In case you only want to execute only a particular function, you tell `hevm` -that you only want a particular signature executed: +In case you only want to execute only a particular function, you can ask `hevm` +to only execute a particular function signature via the `--sig` option: ```shell $ hevm symbolic --sig "simple_symb1()" --code "6080604052348015600e575f80fd5b50600436106030575f3560e01c806385c2fc7114603457806386ae330914603c575b5f80fd5b603a6044565b005b60426055565b005b60025f541460535760526066565b5b565b60035f541460645760636066565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220d70d3cfe85d6f0c8a34ce660d76d7f933db353e59397674009e3a3d982275d7e64736f6c63430008180033"