[DRAFT] Preliminary dynamic ABI types

src/EVM/SymExec.hs

@@ -125,6 +125,10 @@ symAbiArg name = \case
     Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg (name <> "-a-" <> i) tp) $ (V.replicate sz tps)
   AbiTupleType tps ->
     Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg (name <> "-t-" <> i) tp) $ tps
+  AbiBytesDynamicType -> do
+    let arr = (AbstractBuf ("db-" <> name))
+        sz = BufLength arr
+    Dy [PEq (Expr.eq (Lit 1) (Lit 1)) (Lit 0x1)] sz arr
   t -> internalError $ "TODO: symbolic abi encoding for " <> show t
   where
     v = Var name
@@ -168,6 +172,7 @@ cdLen = go (Lit 4)
       (hd:tl) -> case hd of
                    St _ _ -> go (Expr.add acc (Lit 32)) tl
                    Comp xs | all isSt xs -> go acc (xs <> tl)
+                   Dy _ sz _ -> go (Expr.add acc sz) tl
                    _ -> internalError "unsupported"
 
 writeSelector :: Expr Buf -> Text -> Expr Buf
@@ -186,9 +191,9 @@ combineFragments fragments base = go (Lit 4) fragments (base, [])
       case f of
         -- static fragments get written as a word in place
         St p w -> go (Expr.add idx (Lit 32)) rest (Expr.writeWord idx w buf, p <> ps)
+        Dy p sz buf2 -> go (Expr.add idx sz) rest (Expr.copySlice (Lit 0) idx sz buf buf2, p <> ps)
         -- compound fragments that contain only static fragments get written in place
         Comp xs | all isSt xs -> go idx (xs <> rest) (buf,ps)
-        -- dynamic fragments are not yet supported... :/
         s -> internalError $ "unsupported cd fragment: " <> show s
 
 isSt :: CalldataFragment -> Bool

test/test.hs

@@ -2994,6 +2994,22 @@ tests = testGroup "hevm"
           let sig = (Just (Sig "stuff(address)" [AbiAddressType]))
           (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
           putStrLnM $ "Basic tstore check passed"
+        , test "dynamic-calldata" $ do
+          Just c <- solcRuntime "C"
+            [i|
+            contract C {
+              uint x;
+              uint y;
+              function fun(bytes calldata a) external{
+                require(x != 0);
+                require(y != 0);
+                assert (x == y);
+              }
+            }
+            |]
+          let sig = (Just (Sig "fun(bytes)" [AbiBytesDynamicType]))
+          (_, [(Cex _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c sig [] defaultVeriOpts
+          putStrLnM "Expected counterexample found"
   ]
   , testGroup "concr-fuzz"
     [ testFuzz "fuzz-complicated-mul" $ do