Merge pull request #435 from ethereum/symbolic-encoder-static-array

Symbolic ABI encoder for static array types

CHANGELOG.md

@@ -6,10 +6,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
 ## Changed
+
 - Minimum distance requirements are now asserted for Keccak function calls. They assert that it's hard to generate two Keccak's that are less than 256 afar.
 - Keccak concretization is now done only after all simplifications are performed. This helps with simplification pre-concretization
 
 ## Added
+
+- Symbolic tests now support statically sized arrays as parameters
+- `hevm test` now has a `num-solvers` parameter that controls how many solver instances to spawn
 - New solc-specific simplification rules that should make the final Props a lot more readable
 - Prop is now correctly ordered, better BufLength and Max simplifications of Expr,
   and further solc-specific simplifications of Expr

cli/cli.hs

@@ -151,6 +151,7 @@ data Command w
       , coverage      :: w ::: Bool                     <?> "Coverage analysis"
       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
       , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc5"
+      , numSolvers    :: w ::: Maybe Natural            <?> "Number of solver instances to use (default: number of cpu cores)"
       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"
       , debug         :: w ::: Bool                     <?> "Debug printing of internal behaviour"
       , trace         :: w ::: Bool                     <?> "Dump trace"
@@ -215,9 +216,10 @@ main = do
     Test {} -> do
       root <- getRoot cmd
       withCurrentDirectory root $ do
-        cores <- unsafeInto <$> getNumProcessors
         solver <- getSolver cmd
-        runEnv env $ withSolvers solver cores cmd.smttimeout $ \solvers -> do
+        cores <- liftIO $ unsafeInto <$> getNumProcessors
+        let solverCount = fromMaybe cores cmd.numSolvers
+        runEnv env $ withSolvers solver solverCount cmd.smttimeout $ \solvers -> do
           buildOut <- liftIO $ readBuildOutput root (getProjectType cmd)
           case buildOut of
             Left e -> liftIO $ do

doc/src/test.md

@@ -19,6 +19,7 @@ Available options:
   --coverage               Coverage analysis
   --match STRING           Test case filter - only run methods matching regex
   --solver TEXT            Used SMT solver: z3 (default) or cvc5
+  --num-solvers NATURAL    Number of solver instances to use (default: number of cpu cores)
   --smtdebug               Print smt queries sent to the solver
   --ffi                    Allow the usage of the hevm.ffi() cheatcode (WARNING:
                            this allows test authors to execute arbitrary code on

src/EVM/SymExec.hs

@@ -160,6 +160,7 @@ cdLen = go (Lit 4)
       [] -> acc
       (hd:tl) -> case hd of
                    St _ _ -> go (Expr.add acc (Lit 32)) tl
+                   Comp xs | all isSt xs -> go acc (xs <> tl)
                    _ -> internalError "unsupported"
 
 writeSelector :: Expr Buf -> Text -> Expr Buf
@@ -176,9 +177,17 @@ combineFragments fragments base = go (Lit 4) fragments (base, [])
     go _ [] acc = acc
     go idx (f:rest) (buf, ps) =
       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)
+        -- 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
+isSt (St {}) = True
+isSt _ = False
+
 
 abstractVM
   :: (Expr Buf, [Prop])