Merge pull request #354 from ethereum/vm-assume

EVM: Add `deal` and `assume` cheatcodes

CHANGELOG.md

@@ -7,6 +7,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+## Added
+
+- `vm.prank` now handles symbolic addresses
+- added `vm.deal` cheatcode
+- added `vm.assume` cheatcode
+
 ## Fixed
 
 - CopySlice wraparound issue especially during CopyCallBytesToMemory
@@ -17,6 +23,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - No more false positives when keccak is called with inputs of different sizes
 - `test` now falls back to displaying an unecoded bytestring for calldata when the model returned by the solver has a different length the length of the arguments in the test signature.
 - we now generate correct counterexamples for branches where only a subset of input variables are referenced by the path conditions
+- `vm.prank` now works correctly when passed a symbolic address
 
 ## Changed
 
@@ -26,7 +33,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - `check` prefix now recognized for symbolic tests
 - solidity tests no longer consider reverts to be a failure, and check only for the ds-test failed bit or unser defined assertion failures (i.e. `Panic(0x01)`). A positive (i.e. non `proveFail`) test with no rechable assertion violations that does not have any succesful branches will still be considered a failure.
-- `vm.prank` now works correctly when passed a symbolic address
 - `test` now takes a `--number` argument to specify which block should be used when making rpc queries
 - The `--initial-storage` flag no longer accepts a concrete prestore (valid values are now `Empty` or `Abstract`)
 - The visual debugger has been removed

doc/src/controlling-the-unit-testing-environment.md

@@ -12,6 +12,13 @@ These can be accessed by calling into a contract (typically called `Vm`) at addr
 - `function roll(uint x) public`
   Sets the block number to `x`.
 
+- `function assume(bool b) public`
+  Add the condition `b` to the assumption base for the current branch. This functions almost identically to `require`.
+
+- `function deal(uint usr, uint amt) public`
+  Sets the eth balance of `usr` to `amt`. Note that if `usr` is a symbolic address, then it must be the address of a contract that has already been deployed.
+  This restriction is in place to ensure soundness of our symbolic address encoding with respect to potential aliasing of symbolic addresses.
+
 - `function store(address c, bytes32 loc, bytes32 val) public`
   Sets the slot `loc` of contract `c` to `val`.
 

src/EVM.hs

@@ -1648,6 +1648,19 @@ cheatActions =
           [x]  -> assign (#block % #timestamp) x
           _ -> vmError (BadCheatCode sig),
 
+      action "deal(address,uint256)" $
+        \sig _ _ input -> case decodeStaticArgs 0 2 input of
+          [a, amt] ->
+            forceAddr a "vm.deal: cannot decode target into an address" $ \usr ->
+              fetchAccount usr $ \_ -> do
+                assign (#env % #contracts % ix usr % #balance) amt
+          _ -> vmError (BadCheatCode sig),
+
+      action "assume(bool)" $
+        \sig _ _ input -> case decodeStaticArgs 0 1 input of
+          [c] -> modifying #constraints ((:) (PEq c (Lit 1)))
+          _ -> vmError (BadCheatCode sig),
+
       action "roll(uint256)" $
         \sig _ _ input -> case decodeStaticArgs 0 1 input of
           [x] -> forceConcrete x "cannot roll to a symbolic block number" (assign (#block % #number))

test/contracts/pass/cheatCodes.sol

@@ -4,6 +4,8 @@ import "ds-test/test.sol";
 
 interface Hevm {
     function warp(uint256) external;
+    function deal(address,uint256) external;
+    function assume(bool) external;
     function roll(uint256) external;
     function load(address,bytes32) external returns (bytes32);
     function store(address,bytes32,bytes32) external;
@@ -27,6 +29,8 @@ contract Payable {
     function hi() public payable {}
 }
 
+contract Empty {}
+
 contract CheatCodes is DSTest {
     address store = address(new HasStorage());
     Hevm hevm = Hevm(HEVM_ADDRESS);
@@ -123,7 +127,56 @@ contract CheatCodes is DSTest {
         assertEq(prankster.prankme(), address(this));
     }
 
-    function test_prank_val() public {
+    // this is not supported yet due to restrictions around symbolic address aliasing...
+    function proveFail_deal_unknown_address(address e, uint val) public {
+        hevm.deal(e, val);
+        assert(e.balance == val);
+    }
+
+    function prove_deal_simple(uint val) public {
+        address e = address(new Empty());
+        assert(e.balance == 0);
+        hevm.deal(e, val);
+        assert(e.balance == val);
+    }
+
+    function prove_deal_no_underflow(uint val) public {
+        require(address(this).balance < val);
+        prove_deal_simple(val);
+    }
+
+    function prove_deal_multiple(uint val1, uint val2) public {
+        address e = address(new Empty());
+
+        assert(e.balance == 0);
+        hevm.deal(e, val1);
+        assert(e.balance == val1);
+
+        hevm.deal(e, val2);
+        assert(e.balance == val2);
+    }
+
+    function prove_assume(bool b) public {
+        hevm.assume(b);
+        assert(b);
+    }
+
+    function prove_assume(uint v) public {
+        hevm.assume(v > 10);
+        assert(v > 10);
+    }
+
+    function proveFail_assume(uint v) public {
+        hevm.assume(v > 10);
+        assert(v <= 10);
+    }
+
+    function proveFail_assume(bool b) public {
+        hevm.assume(b);
+        assert(!b);
+    }
+
+    function prove_prank_val() public {
         address from = address(0x1312);
         uint amt = 10;
 

test/test.hs

@@ -576,6 +576,24 @@ tests = testGroup "hevm"
           checkAssert s [0x41] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
         putStrLn "expected counterexample found"
       ,
+      testCase "vm.deal unknown address" $ do
+        Just c <- solcRuntime "C"
+          [i|
+            interface Vm {
+              function deal(address,uint256) external;
+            }
+            contract C {
+              // this is not supported yet due to restrictions around symbolic address aliasing...
+              function f(address e, uint val) external {
+                  Vm vm = Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
+                  vm.deal(e, val);
+                  assert(e.balance == val);
+              }
+            }
+          |]
+        Right e <- reachableUserAsserts c (Just $ Sig "f(address,uint256)" [AbiAddressType, AbiUIntType 256])
+        assertBool "The expression is not partial" $ Expr.containsNode isPartial e
+      ,
       testCase "vm.prank underflow" $ do
         Just c <- solcRuntime "C"
             [i|