put dynamic buffer test in dapp-test instead of hevm

src/dapp-tests/bytes.sol

@@ -0,0 +1,7 @@
+contract Bytes
+{
+    function f(bytes memory b1, bytes memory b2) public pure {
+        b1 = b2;
+        assert(b1[1] == b2[1]);
+    }
+}

src/dapp-tests/integration/tests.sh

@@ -66,6 +66,10 @@ test_hevm_symbolic() {
     solc --bin-runtime -o . --overwrite AB.sol
     hevm equivalence --code-a $(<A.bin-runtime) --code-b $(<B.bin-runtime) --solver cvc4
     rm -rf A.bin-runtime B.bin-runtime
+
+    # simple dynamic calldata example
+    solc --bin-runtime -o . --overwrite bytes.sol
+    timeout 2m hevm symbolic --code $(<Bytes.bin-runtime) --calldata-model DynamicCD
 }
 
 test_hevm_symbolic

src/dapp-tests/shell.nix

@@ -5,5 +5,5 @@
 pkgs.mkShell {
   name = "dapp-tests";
 
-  buildInputs = with pkgs; [ killall cacert bashInteractive curl dapp gnumake hevm procps seth solc ];
+  buildInputs = with pkgs; [ coreutils killall cacert bashInteractive curl dapp gnumake hevm procps seth solc ];
 }

src/hevm/hevm-cli/hevm-cli.hs

@@ -12,10 +12,10 @@
 
 module Main where
 
-import EVM (StorageModel(..))
+import EVM (StorageModel(..), CalldataModel(..))
 import qualified EVM
 import EVM.Concrete (createAddress, w256)
-import EVM.Symbolic (forceLitBytes, litBytes, litAddr, w256lit, sw256, SymWord(..), Buffer(..), len)
+import EVM.Symbolic (forceLitBytes, litBytes, litAddr, w256lit, sw256, SymWord(..), Buffer(..), len, Calldata(..))
 import qualified EVM.FeeSchedule as FeeSchedule
 import qualified EVM.Fetch
 import qualified EVM.Flatten
@@ -57,6 +57,7 @@ import Data.Text.IO               (hPutStr)
 import Data.Maybe                 (fromMaybe, fromJust)
 import Data.Version               (showVersion)
 import Data.SBV hiding (Word, solver, verbose, name)
+import qualified Data.SBV.List as SList
 import qualified Data.SBV as SBV
 import Data.SBV.Control hiding (Version, timeout, create)
 import System.IO                  (hFlush, hPrint, stdout, stderr)
@@ -110,17 +111,18 @@ data Command w
       , block       :: w ::: Maybe W256       <?> "Block state is be fetched from"
 
   -- symbolic execution opts
-      , jsonFile      :: w ::: Maybe String       <?> "Filename or path to dapp build output (default: out/*.solc.json)"
-      , dappRoot      :: w ::: Maybe String       <?> "Path to dapp project root directory (default: . )"
-      , storageModel  :: w ::: Maybe StorageModel <?> "Select storage model: ConcreteS, SymbolicS (default) or InitialS"
-      , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"
-      , arg           :: w ::: [String]           <?> "Values to encode"
-      , debug         :: w ::: Bool               <?> "Run interactively"
-      , getModels     :: w ::: Bool               <?> "Print example testcase for each execution path"
-      , smttimeout    :: w ::: Maybe Integer      <?> "Timeout given to SMT solver in milliseconds (default: 20000)"
-      , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"
-      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc4"
-      , smtoutput     :: w ::: Bool               <?> "Print verbose smt output"
+      , jsonFile      :: w ::: Maybe String        <?> "Filename or path to dapp build output (default: out/*.solc.json)"
+      , dappRoot      :: w ::: Maybe String        <?> "Path to dapp project root directory (default: . )"
+      , storageModel  :: w ::: Maybe StorageModel  <?> "Select storage model: ConcreteS, SymbolicS (default) or InitialS"
+      , calldataModel :: w ::: Maybe CalldataModel <?> "Select calldata model: BoundedCD (default), or DynamicCD"
+      , sig           :: w ::: Maybe Text          <?> "Signature of types to decode / encode"
+      , arg           :: w ::: [String]            <?> "Values to encode"
+      , debug         :: w ::: Bool                <?> "Run interactively"
+      , getModels     :: w ::: Bool                <?> "Print example testcase for each execution path"
+      , smttimeout    :: w ::: Maybe Integer       <?> "Timeout given to SMT solver in milliseconds (default: 20000)"
+      , maxIterations :: w ::: Maybe Integer       <?> "Number of times we may revisit a particular branching point"
+      , solver        :: w ::: Maybe Text          <?> "Used SMT solver: z3 (default) or cvc4"
+      , smtoutput     :: w ::: Bool                <?> "Print verbose smt output"
       }
   | Equivalence -- prove equivalence between two programs
       { codeA         :: w ::: ByteString    <?> "Bytecode of the first program"
@@ -681,7 +683,7 @@ vmFromCommand cmd = do
         value'   = word value 0
         caller'  = addr caller 0
         origin'  = addr origin 0
-        calldata' = ConcreteBuffer $ bytes calldata ""
+        calldata' = CalldataBuffer $ ConcreteBuffer $ bytes calldata ""
         codeType = if create cmd then EVM.InitCode else EVM.RuntimeCode
         address' = if create cmd
               then createAddress origin' (word nonce 0)
@@ -716,18 +718,29 @@ symvmFromCommand :: Command Options.Unwrapped -> Query EVM.VM
 symvmFromCommand cmd = do
   caller' <- maybe (SAddr <$> freshVar_) (return . litAddr) (caller cmd)
   callvalue' <- maybe (sw256 <$> freshVar_) (return . w256lit) (value cmd)
-  calldata' <- case (calldata cmd, sig cmd) of
-    -- static calldata (up to 256 bytes)
-    (Nothing, Nothing) -> do
-      StaticSymBuffer <$> sbytes256
+  (calldata', preCond) <- case (calldata cmd, sig cmd, calldataModel cmd) of
+    -- dynamic calldata via smt lists
+    (Nothing, Nothing, Just DynamicCD) -> do
+      cd <- freshVar_
+      return (CalldataBuffer (DynamicSymBuffer cd),
+              SList.length cd .< 1000 .&&
+               sw256 (sFromIntegral (SList.length cd)) .< sw256 1000)
+
+    -- dynamic calldata via (bounded) haskell list
+    (Nothing, Nothing, _) -> do
+      cd <- sbytes256
+      len <- freshVar_
+      return (CalldataDynamic (cd, len), len .<= 256)
+
     -- fully concrete calldata
-    (Just c, Nothing) ->
-      return $ ConcreteBuffer $ decipher c
+    (Just c, Nothing, _) ->
+      return (CalldataBuffer (ConcreteBuffer $ decipher c), sTrue)
     -- calldata according to given abi with possible specializations from the `arg` list
-    (Nothing, Just sig') -> do
+    (Nothing, Just sig', _) -> do
       method' <- io $ functionAbi sig'
       let typs = snd <$> view methodInputs method'
-      StaticSymBuffer <$> staticCalldata (view methodSignature method') typs (arg cmd)
+      cd <- staticCalldata (view methodSignature method') typs (arg cmd)
+      return (CalldataBuffer (StaticSymBuffer cd), sTrue)
 
     _ -> error "incompatible options: calldata and abi"
 
@@ -773,7 +786,7 @@ symvmFromCommand cmd = do
     (_, _, Nothing) ->
       error $ "must provide at least (rpc + address) or code"
 
-  return vm
+  return $ vm & over EVM.pathConditions (<> [preCond])
 
   where
     decipher = hexByteString "bytes" . strip0x

src/hevm/src/EVM.hs

@@ -315,7 +315,7 @@ instance ParseField StorageModel
 
 -- | Calldata can either by a normal buffer, or a custom "pseudo dynamic" encoding. See EVM.Symbolic for details
 data CalldataModel
-  = BufferCD
+  = DynamicCD
   | BoundedCD
   deriving (Read, Show)
 
@@ -2213,7 +2213,7 @@ copyCalldataToMemory (CalldataBuffer bf) size xOffset yOffset =
 copyCalldataToMemory (CalldataDynamic (b, l)) size xOffset yOffset =
   case (maybeLitWord size, maybeLitWord xOffset, maybeLitWord yOffset) of
     (Just size', Just xOffset', Just yOffset') ->
-      copyBytesToMemory (StaticSymBuffer [ite (i .<= l) x 0 | (x, i) <- zip b [1..]]) size' xOffset' yOffset'
+      copyBytesToMemory (StaticSymBuffer [ite (i .<= l) x 0 | (x, i) <- zip b [1..]]) (litWord size') (litWord xOffset') (litWord yOffset')
     _ ->
       copyBytesToMemory (DynamicSymBuffer (subList (implode b) 0 (sFromIntegral l))) size xOffset yOffset
 

src/hevm/src/EVM/Fetch.hs

@@ -187,7 +187,7 @@ checksat b = do push 1
                 b <- getInfo Name
                 m <- case b of
                        -- some custom strategies for z3 which have proven to be quite useful (can still be tweaked)
-                       Resp_Name "Z3" -> checkSatUsing "(check-sat-using (then (using-params simplify :cache-all true) smt))"
+                       Resp_Name "Z3" -> checkSatUsing "(check-sat-using (then (using-params simplify :push_ite_bv true :ite_extra_rules true) smt))"
                        _ -> checkSat
                 pop 1
                 return m

src/hevm/src/EVM/SymExec.hs

@@ -99,7 +99,7 @@ abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel
 abstractVM typesignature concreteArgs x storagemodel calldatamodel = do
   (cd',pathCond) <- case typesignature of
            Nothing -> case calldatamodel of
-                        BufferCD -> do
+                        DynamicCD -> do
                           list <- freshVar_
                           return (CalldataBuffer (DynamicSymBuffer list),
                             -- due to some current z3 shenanegans (possibly related to: https://github.com/Z3Prover/z3/issues/4635)
@@ -205,8 +205,8 @@ maxIterationsReached vm (Just maxIter) =
 type Precondition = VM -> SBool
 type Postcondition = (VM, VM) -> SBool
 
-checkAssertBuffer :: ByteString -> Query (Either (VM, [VM]) VM)
-checkAssertBuffer c = verifyContract c Nothing [] SymbolicS BufferCD (const sTrue) (Just checkAssertions)
+checkAssertDynamic :: ByteString -> Query (Either (VM, [VM]) VM)
+checkAssertDynamic c = verifyContract c Nothing [] SymbolicS DynamicCD (const sTrue) (Just checkAssertions)
 
 
 checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM)

src/hevm/src/EVM/Symbolic.hs

@@ -65,7 +65,10 @@ forceLitBytes = BS.pack . fmap (fromSized . fromJust . unliteral)
 
 forceBuffer :: Buffer -> ByteString
 forceBuffer (ConcreteBuffer b) = b
-forceBuffer (SymbolicBuffer b) = forceLitBytes b
+forceBuffer (StaticSymBuffer b) = forceLitBytes b
+forceBuffer (DynamicSymBuffer b) = case unliteral b of
+  Just b' -> BS.pack $ fmap fromSized b'
+  Nothing -> error "unexpected symbolic argument"
 
 -- | Arithmetic operations on SymWord
 
@@ -346,13 +349,13 @@ readByteOrZero i (StaticSymBuffer bs) = readByteOrZero' i bs
 readByteOrZero i (ConcreteBuffer bs) = num $ Concrete.readByteOrZero i bs
 readByteOrZero i (DynamicSymBuffer bs) = readByteOrZero'' (literal $ num i) bs
 
--- pad up to 10000 bytes in the dynamic case
+-- pad up to 1000 bytes in the dynamic case
 sliceWithZero :: SymWord -> SymWord -> Buffer -> Buffer
 sliceWithZero (S _ o) (S _ s) bf = case (unliteral o, unliteral s, bf) of
   (Just o', Just s', StaticSymBuffer m) -> StaticSymBuffer (sliceWithZero' (num o') (num s') m)
   (Just o', Just s', ConcreteBuffer m)  -> ConcreteBuffer (Concrete.byteStringSliceWithDefaultZeroes (num o') (num s') m)
   (Just o', Just s', m)                 -> truncpad' (num s') (ditch (num o') m)
-  _                                     -> DynamicSymBuffer $ SL.subList (dynamize bf .++ literal (replicate 10000 0)) (sFromIntegral o) (sFromIntegral s)
+  _                                     -> DynamicSymBuffer $ SL.subList (dynamize bf .++ literal (replicate 1000 0)) (sFromIntegral o) (sFromIntegral s)
 
 writeMemory :: Buffer -> SymWord -> SymWord -> SymWord -> Buffer -> Buffer
 writeMemory bs1 n src dst bs0 =

src/hevm/test/test.hs

@@ -558,9 +558,9 @@ main = defaultMain $ testGroup "hevm"
           Right counterexample <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
           putStrLn $ "found counterexample:"
 
+       ,
 
-      ,
-         testCase "multiple contracts" $ do
+        testCase "multiple contracts" $ do
           let code =
                 [i|
                   contract C {
@@ -589,46 +589,28 @@ main = defaultMain $ testGroup "hevm"
                                            set EVM.storage (Symbolic store)))
             verify vm Nothing Nothing (Just checkAssertions)
           putStrLn $ "found counterexample:"
-    -- ,
-    --      testCase "dynamic bytes (calldataload)" $ do
-    --       Just c <- solcRuntime "C"
-    --         [i|
-    --           contract C
-    --           {
-    --           function f() public pure {
-    --             uint y;
-    --             uint z;
-    --             assembly {
-    --               y := calldataload(12)
-    --               z := calldataload(31)
-    --             }
-    --             assert(y == z);
-    --           }
-    --           }
-    --         |]
-    --       -- should find a counterexample
-    --       Right cex <- runSMTWith z3 $ do
-    --         query $ checkAssert c Nothing []
-    --       putStrLn $ "found counterexample"
-
-
-    --  ,
-         testCase "dynamic bytes (abi decoding)" $ do
+    ,
+         testCase "dynamic bytes (calldataload)" $ do
           Just c <- solcRuntime "C"
             [i|
               contract C
               {
-               function f(bytes memory b1, bytes memory b2) public pure {
-                  b1 = b2;
-                  assert(b1[1] == b2[1]);
+              function f() public pure {
+                uint y;
+                uint z;
+                assembly {
+                  y := calldataload(12)
+                  z := calldataload(31)
                 }
+                assert(y == z);
+              }
               }
             |]
           -- should find a counterexample
-          Left (_, res) <- runSMTWith z3{verbose=True} $ do
---            setTimeOut 20000
-            query $ checkAssertBuffer c
-          putStrLn $ "successfully explored: " <> show (length res) <> " paths"
+          Right cex <- runSMTWith z3 $ do
+            query $ checkAssert c Nothing []
+          putStrLn $ "found counterexample"
+
     ]
   , testGroup "Equivalence checking"
     [