Merge branch 'main' into simplified-copyslice

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
@@ -41,6 +47,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Contract code can now be fully abstract. Calls into contracts with unknown code will fail with `UnexpectedSymbolicArg`.
 - Run expression simplification on branch conditions
 - CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases
+- Better simplification of Eq IR elements
 
 ## API Changes
 

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`.
 

flake.nix

@@ -3,7 +3,7 @@
 
   inputs = {
     flake-utils.url = "github:numtide/flake-utils";
-    nixpkgs.url = "github:nixos/nixpkgs/haskell-updates";
+    nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
     foundry.url = "github:shazow/foundry.nix/monthly";
     flake-compat = {
       url = "github:edolstra/flake-compat";
@@ -49,7 +49,7 @@
             Cabal-syntax = dontCheck (self.callCabal2nix "Cabal-syntax" "${cabal-head}/Cabal-syntax" {});
             Cabal = dontCheck (self.callCabal2nix "Cabal" "${cabal-head}/Cabal" {});
             unix = dontCheck (doJailbreak super.unix_2_8_1_1);
-            filepath = dontCheck (doJailbreak super.filepath_1_4_100_3);
+            filepath = dontCheck (doJailbreak super.filepath_1_4_100_4);
             process = dontCheck (doJailbreak super.process_1_6_17_0);
             directory = dontCheck (doJailbreak (super.directory_1_3_7_1));
             tasty = dontCheck (doJailbreak super.tasty);

hevm.cabal

@@ -131,7 +131,6 @@ library
     text                              >= 1.2.3 && < 2.1,
     unordered-containers              >= 0.2.10 && < 0.3,
     vector                            >= 0.12.1 && < 0.14,
-    ansi-wl-pprint                    >= 0.6.9 && < 0.7,
     base16                            >= 0.3.2.0 && < 0.3.3.0,
     megaparsec                        >= 9.0.0 && < 10.0,
     mtl                               >= 2.2.2 && < 2.3,
@@ -195,7 +194,6 @@ executable hevm
   build-depends:
     QuickCheck,
     aeson,
-    ansi-wl-pprint,
     async,
     base,
     base16,

src/EVM.hs

@@ -1258,14 +1258,14 @@ query = assign #result . Just . HandleEffect . Query
 choose :: Choose s -> EVM s ()
 choose = assign #result . Just . HandleEffect . Choose
 
-branch :: Expr EWord -> (Bool -> EVM s ()) -> EVM s ()
+branch :: forall s. Expr EWord -> (Bool -> EVM s ()) -> EVM s ()
 branch cond continue = do
   loc <- codeloc
   pathconds <- use #constraints
   query $ PleaseAskSMT cond pathconds (choosePath loc)
   where
     condSimp = Expr.simplify cond
-    -- choosePath :: CodeLocation -> BranchCondition -> EVM s ()
+    choosePath :: CodeLocation -> BranchCondition -> EVM s ()
     choosePath loc (Case v) = do
       assign #result Nothing
       pushTo #constraints $ if v then Expr.evalProp (condSimp ./= Lit 0) else Expr.evalProp (condSimp .== Lit 0)
@@ -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))

src/EVM/Expr.hs

@@ -623,7 +623,7 @@ getAddr :: Expr Storage -> Maybe (Expr EAddr)
 getAddr (SStore _ _ p) = getAddr p
 getAddr (AbstractStore a) = Just a
 getAddr (ConcreteStore _) = Nothing
-getAddr (GVar _) = error "cannot determine addr of a GVar"
+getAddr (GVar _) = internalError "cannot determine addr of a GVar"
 
 
 -- ** Whole Expression Simplification ** -----------------------------------------------------------
@@ -685,20 +685,19 @@ simplify e = if (mapExpr go e == e)
     go (EVM.Types.LT _ (Lit 0)) = Lit 0
 
     -- normalize all comparisons in terms of LT
-    go (EVM.Types.GT a b) = EVM.Types.LT b a
-    go (EVM.Types.GEq a b) = EVM.Types.LEq b a
-    go (EVM.Types.LEq a b) = EVM.Types.IsZero (EVM.Types.GT a b)
-
+    go (EVM.Types.GT a b) = lt b a
+    go (EVM.Types.GEq a b) = leq b a
+    go (EVM.Types.LEq a b) = EVM.Types.IsZero (gt a b)
     go (IsZero a) = iszero a
 
     -- syntactic Eq reduction
     go (Eq (Lit a) (Lit b))
       | a == b = Lit 1
       | otherwise = Lit 0
-    go (Eq (Lit 0) (Sub a b)) = Eq a b
-    go o@(Eq a b)
+    go (Eq (Lit 0) (Sub a b)) = eq a b
+    go (Eq a b)
       | a == b = Lit 1
-      | otherwise = o
+      | otherwise = eq a b
 
     -- redundant ITE
     go (ITE (Lit x) a b)
@@ -734,28 +733,28 @@ simplify e = if (mapExpr go e == e)
     go (Add (Sub orig (Lit x)) (Lit y)) = Add orig (Lit (y-x))
 
     -- redundant add / sub
-    go o@(Sub (Add a b) c)
+    go (Sub (Add a b) c)
       | a == c = b
       | b == c = a
-      | otherwise = o
+      | otherwise = sub (add a b) c
 
     -- add / sub identities
-    go o@(Add a b)
+    go (Add a b)
       | b == (Lit 0) = a
       | a == (Lit 0) = b
-      | otherwise = o
-    go o@(Sub a b)
+      | otherwise = add a b
+    go (Sub a b)
       | a == b = Lit 0
       | b == (Lit 0) = a
-      | otherwise = o
+      | otherwise = sub a b
 
     -- SHL / SHR by 0
-    go o@(SHL a v)
+    go (SHL a v)
       | a == (Lit 0) = v
-      | otherwise = o
-    go o@(SHR a v)
+      | otherwise = shl a v
+    go (SHR a v)
       | a == (Lit 0) = v
-      | otherwise = o
+      | otherwise = shr a v
 
     -- doubled And
     go o@(And a (And b c))
@@ -798,8 +797,21 @@ simplify e = if (mapExpr go e == e)
     go (EVM.Types.Not (EVM.Types.Not a)) = a
 
     -- Some trivial min / max eliminations
-    go (Max (Lit 0) a) = a
-    go (Min (Lit 0) _) = Lit 0
+    go (Max a b) = case (a, b) of
+                    (Lit 0, _) -> b
+                    _ -> EVM.Expr.max a b
+    go (Min a b) = case (a, b) of
+                     (Lit 0, _) -> Lit 0
+                     _ -> EVM.Expr.min a b
+
+    -- Some trivial mul eliminations
+    go (Mul a b) = case (a, b) of
+                     (Lit 0, _) -> Lit 0
+                     (Lit 1, _) -> b
+                     _ -> mul a b
+    -- Some trivial div eliminations
+    go (Div (Lit 0) _) = Lit 0 -- divide 0 by anything (including 0) is zero in EVM
+    go (Div _ (Lit 0)) = Lit 0 -- divide anything by 0 is zero in EVM
 
     -- If a >= b then the value of the `Max` expression can never be < b
     go o@(LT (Max (Lit a) _) (Lit b))

src/EVM/Format.hs

@@ -649,13 +649,13 @@ formatExpr = go
         ]
 
       -- Stores
-      SLoad slot store -> T.unlines
+      SLoad slot storage -> T.unlines
         [ "(SLoad"
         , indent 2 $ T.unlines
           [ "slot:"
           , indent 2 $ formatExpr slot
-          , "store:"
-          , indent 2 $ formatExpr store
+          , "storage:"
+          , indent 2 $ formatExpr storage
           ]
         , ")"
         ]

src/EVM/SMT.hs

@@ -1023,7 +1023,7 @@ getStore getVal abstractReads =
                 (TermQualIdentifier (Unqualified (IdSymbol symbol)), term) ->
                   if symbol == (T.toStrict name)
                   then interpret1DArray Map.empty term
-                  else error "Internal Error: solver did not return model for requested value"
+                  else internalError "solver did not return model for requested value"
                 r -> parseErr r
 
     -- then create a map by adding only the locations that are read by the program

src/EVM/SymExec.hs

@@ -28,7 +28,7 @@ import Data.Text.Lazy qualified as TL
 import Data.Text.Lazy.IO qualified as TL
 import Data.Tree.Zipper qualified as Zipper
 import Data.Tuple (swap)
-import EVM (makeVm, abstractContract, getCodeLocation, isValidJumpDest)
+import EVM (makeVm, abstractContract, initialContract, getCodeLocation, isValidJumpDest)
 import EVM.Exec
 import EVM.Fetch qualified as Fetch
 import EVM.ABI
@@ -207,7 +207,7 @@ loadSymVM
   -> ST s (VM s)
 loadSymVM x callvalue cd create =
   (makeVm $ VMOpts
-    { contract = abstractContract x (SymAddr "entrypoint")
+    { contract = if create then initialContract x else abstractContract x (SymAddr "entrypoint")
     , calldata = cd
     , value = callvalue
     , baseState = AbstractBase