diff --git a/src/dapp-tests/bytes.sol b/src/dapp-tests/bytes.sol new file mode 100644 index 000000000..dbec0336c --- /dev/null +++ b/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]); + } +} diff --git a/src/dapp-tests/integration/tests.sh b/src/dapp-tests/integration/tests.sh index 5296a50fa..05a82427a 100755 --- a/src/dapp-tests/integration/tests.sh +++ b/src/dapp-tests/integration/tests.sh @@ -66,6 +66,10 @@ test_hevm_symbolic() { solc --bin-runtime -o . --overwrite AB.sol hevm equivalence --code-a $( "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 diff --git a/src/hevm/src/EVM.hs b/src/hevm/src/EVM.hs index 9102c2db6..1def10018 100644 --- a/src/hevm/src/EVM.hs +++ b/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 diff --git a/src/hevm/src/EVM/Fetch.hs b/src/hevm/src/EVM/Fetch.hs index c59912ac1..4050a3d14 100644 --- a/src/hevm/src/EVM/Fetch.hs +++ b/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 diff --git a/src/hevm/src/EVM/SymExec.hs b/src/hevm/src/EVM/SymExec.hs index 66febd08e..67b75d163 100644 --- a/src/hevm/src/EVM/SymExec.hs +++ b/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) diff --git a/src/hevm/src/EVM/Symbolic.hs b/src/hevm/src/EVM/Symbolic.hs index 0f7192373..684759537 100644 --- a/src/hevm/src/EVM/Symbolic.hs +++ b/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 = diff --git a/src/hevm/test/test.hs b/src/hevm/test/test.hs index c22174945..7dda52a8c 100644 --- a/src/hevm/test/test.hs +++ b/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" [