vm.fail
an intermediate symbolic execution engine for EVM bytecode
1module Main where
2
3import SymbolicExpression
4import SymbolicState
5import Executor
6import qualified Data.ByteString as BS
7import qualified Data.Map.Strict as Map
8
9main :: IO ()
10main = do
11 let bytecode = BS.pack
12 [ 0x33
13 , 0x61, 0x12, 0x34
14 , 0x14
15 , 0x60, 0x0b
16 , 0x57
17 , 0x60, 0xc8
18 , 0x60, 0x0f
19 , 0x56
20 , 0x5b
21 , 0x60, 0x64
22 , 0x5b
23 , 0x00
24 ]
25
26 let results = explore bytecode (initState BS.empty) 50
27
28 putStrLn $ "Paths: " ++ show (length results)
29 mapM_ printResult results
30
31printResult :: ExecState -> IO ()
32printResult state = do
33 putStrLn ""
34 putStrLn $ "PC: " ++ show (pc state)
35 putStrLn $ "Halted: " ++ show (halted state)
36 putStrLn $ "Reverted: " ++ show (reverted state)
37
38 let SymStack stackItems = stack state
39 when (not $ null stackItems) $ do
40 putStrLn "Stack:"
41 mapM_ (\(i, expr) -> putStrLn $ " [" ++ show i ++ "] " ++ prettyExpr expr)
42 (zip [0..] stackItems)
43
44 let SymStorage stor = storage state
45 when (not $ null $ Map.toList stor) $ do
46 putStrLn "Storage:"
47 mapM_ (\(k, v) -> putStrLn $ " " ++ prettyExpr k ++ " => " ++ prettyExpr v)
48 (Map.toList stor)
49
50 when (not $ null $ constraints state) $ do
51 putStrLn "Constraints:"
52 mapM_ (\c -> putStrLn $ " " ++ prettyConstraint c) (reverse $ constraints state)
53
54 case returnData state of
55 Just val -> putStrLn $ "Return: " ++ prettyExpr val
56 Nothing -> return ()
57
58when :: Bool -> IO () -> IO ()
59when True action = action
60when False _ = return ()