Symexec tutorial

src/dapp-tests/default.nix

@@ -163,6 +163,7 @@ in
       invariant-first = fail "invariantFirst";
       invariant-test-usr-bal = fail "invariantTestUserBal";
       invariant-test-initial-inv-call = fail "invariantCount";
+      withdraw = fail "proveFail_withdraw";
     };
 
     dss = pkgs.buildDappPackage {

src/dapp-tests/fail/dsProveFail.sol

@@ -4,11 +4,23 @@ import "ds-test/test.sol";
 import "ds-token/token.sol";
 import "ds-math/math.sol";
 
+contract Withdraw {
+    receive() external payable {}
+
+    function withdraw(uint password) public {
+        require(password == 42, "Access denied!");
+        payable(msg.sender).transfer(address(this).balance);
+    }
+}
+
+
 contract SolidityTest is DSTest, DSMath {
     DSToken token;
+    Withdraw withdraw;
 
     function setUp() public {
         token = new DSToken("TKN");
+        withdraw = new Withdraw();
     }
 
     function prove_add(uint x, uint y) public {
@@ -59,5 +71,16 @@ contract SolidityTest is DSTest, DSMath {
                         : amt; // otherwise `amt` has been transfered to `usr`
         assertEq(expected, postbal - prebal);
     }
+
+    function proveFail_withdraw(uint guess) public {
+        payable(address(withdraw)).transfer(1 ether);
+        uint preBalance = address(this).balance;
+        withdraw.withdraw(guess);
+        uint postBalance = address(this).balance;
+        assertEq(preBalance + 1 ether, postBalance);
+    }
+
+    // allow sending eth to the test contract
+    receive() external payable {}
 }
 

src/dapp/README.md

@@ -50,6 +50,7 @@ Let's create a new `dapp` project. We make a new directory and initialize the `d
 
 ```sh
 mkdir dapptutorial
+cd dapptutorial
 dapp init
 ```
 
@@ -87,6 +88,9 @@ Compile the contract by running `dapp build`. If you didn't make any mistakes, y
 Let's write some tests for our vault. Change `Dapptutorial.t.sol` to the following. We'll go over whats going on in the next paragraph.
 
 ```solidity
+import {DSTest} from "ds-test/test.sol";
+import {Dapptutorial} from "./Dapptutorial.sol";
+
 contract DapptutorialTest is DSTest {
     Dapptutorial dapptutorial;
 
@@ -110,8 +114,8 @@ contract DapptutorialTest is DSTest {
         assertEq(preBalance + 1 ether, postBalance);
     }
 
-    receive() external payable {
-    }
+    // allow sending eth to the test contract
+    receive() external payable {}
 }
 ```
 

src/hevm/CHANGELOG.md

@@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Support for solc 0.8.12
 - Support for solc 0.8.13
 
+### Fixed
+
+- Correctly handle concrete returndata when checking the result of a symbolic test
+
 ## [0.49.0] - 2021-11-12
 
 ### Added

src/hevm/src/EVM/UnitTest.hs

@@ -694,9 +694,11 @@ symRun opts@UnitTestOptions{..} concreteVm testName types = do
         SBV.resetAssertions
         constrain $ sAnd (fst <$> view EVM.constraints vm')
         unless bailed $
-          case view result vm' of
-            Just (VMSuccess (SymbolicBuffer buf)) ->
-              constrain $ litBytes (encodeAbiValue $ AbiBool $ not shouldFail) .== buf
+          let
+            checkResult buf = constrain $ litBytes (encodeAbiValue $ AbiBool $ not shouldFail) .== buf
+          in case view result vm' of
+            Just (VMSuccess (SymbolicBuffer buf)) -> checkResult buf
+            Just (VMSuccess (ConcreteBuffer buf)) -> checkResult (litBytes buf)
             r -> error $ "unexpected return value: " ++ show r
         checkSat >>= \case
           Sat -> do