symexec rebase and symbolic VM from concrete

flake.nix

@@ -15,10 +15,10 @@
   outputs = { self, nixpkgs, flake-utils, nix-bundle-exe, ... }:
     flake-utils.lib.eachDefaultSystem (system:
       let
-        pkgs = nixpkgs.legacyPackages.${system};
+        systemPkgs = nixpkgs.legacyPackages.${system};
         # prefer musl on Linux, static glibc + threading does not work properly
         # TODO: maybe only override it for echidna-redistributable?
-        pkgsStatic = if pkgs.stdenv.hostPlatform.isLinux then pkgs.pkgsMusl else pkgs;
+        pkgs = if systemPkgs.stdenv.hostPlatform.isLinux then systemPkgs.pkgsMusl else systemPkgs;
         # this is not perfect for development as it hardcodes solc to 0.5.7, test suite runs fine though
         # would be great to integrate solc-select to be more flexible, improve this in future
         solc = pkgs.stdenv.mkDerivation {
@@ -41,13 +41,13 @@
           '';
         };
 
-        secp256k1-static = pkgsStatic.secp256k1.overrideAttrs (attrs: {
+        secp256k1-static = pkgs.secp256k1.overrideAttrs (attrs: {
           configureFlags = attrs.configureFlags ++ [ "--enable-static" ];
         });
 
-        ncurses-static = pkgsStatic.ncurses.override { enableStatic = true; };
+        ncurses-static = pkgs.ncurses.override { enableStatic = true; };
 
-        hevm = pkgs: pkgs.haskell.lib.dontCheck (
+        hevm = pkgs.haskell.lib.dontCheck (
           pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "ethereum";
             repo = "hevm";
@@ -57,16 +57,16 @@
 
         # FIXME: figure out solc situation, it conflicts with the one from
         # solc-select that is installed with slither, disable tests in the meantime
-        echidna = pkgs: pkgs.haskell.lib.dontCheck (
+        echidna = pkgs.haskell.lib.dontCheck (
           with pkgs; lib.pipe
-          (haskellPackages.callCabal2nix "echidna" ./. { inherit (hevm pkgs); })
+          (haskellPackages.callCabal2nix "echidna" ./. { inherit hevm; })
           [
             (haskell.lib.compose.addTestToolDepends [ haskellPackages.hpack slither-analyzer solc ])
             (haskell.lib.compose.disableCabalFlag "static")
           ]);
 
-        echidna-static = with pkgsStatic; lib.pipe
-          (echidna pkgsStatic)
+        echidna-static = with pkgs; lib.pipe
+          echidna
           [
             (haskell.lib.compose.appendConfigureFlags
               ([
@@ -78,7 +78,6 @@
                 "--extra-lib-dirs=${stripDylib (ncurses-static)}/lib"
               ] ++ (if stdenv.hostPlatform.isDarwin then [
                 "--extra-lib-dirs=${stripDylib (libiconv.override { enableStatic = true; })}/lib"
-                "--extra-lib-dirs=${stripDylib (libcxxabi)}/lib"
               ] else [])))
             (haskell.lib.compose.enableCabalFlag "static")
           ];
@@ -98,28 +97,22 @@
         in if pkgs.stdenv.isLinux
         then pkgs.runCommand "echidna-stripNixRefs" {} ''
           mkdir -p $out/bin
-          cp ${pkgsStatic.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
+          cp ${pkgs.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
           # fix TERMINFO path in ncurses
           ${perl} -i -pe 's#(${ncurses-static}/share/terminfo)#"/usr/share/terminfo" . "\x0" x (length($1) - 19)#e' $out/bin/echidna
           chmod 555 $out/bin/echidna
         '' else pkgs.runCommand "echidna-stripNixRefs" {} ''
           mkdir -p $out/bin
-          cp ${pkgsStatic.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
+          cp ${pkgs.haskell.lib.dontCheck echidna-static}/bin/echidna $out/bin/
           # get the list of dynamic libs from otool and tidy the output
           libs=$(${otool} -L $out/bin/echidna | tail -n +2 | sed 's/^[[:space:]]*//' | cut -d' ' -f1)
           # get the path for libcxx
-          cxx=$(echo "$libs" | ${grep} '^/nix/store/.*-libcxx-')
+          cxx=$(echo "$libs" | ${grep} '^/nix/store/.*-libcxx')
           # rewrite /nix/... library paths to point to /usr/lib
           chmod 777 $out/bin/echidna
           ${install_name_tool} -change "$cxx" /usr/lib/libc++.1.dylib $out/bin/echidna
           # fix TERMINFO path in ncurses
           ${perl} -i -pe 's#(${ncurses-static}/share/terminfo)#"/usr/share/terminfo" . "\x0" x (length($1) - 19)#e' $out/bin/echidna
-          # check that no nix deps remain
-          nixdeps=$(${otool} -L $out/bin/echidna | tail -n +2 | { ${grep} /nix/store -c || test $? = 1; })
-          if [ ! "$nixdeps" = "0" ]; then
-            echo "Nix deps remain in redistributable binary!"
-            exit 255
-          fi
           # re-sign binary
           CODESIGN_ALLOCATE=${codesign_allocate} ${codesign} -f -s - $out/bin/echidna
           chmod 555 $out/bin/echidna
@@ -137,14 +130,14 @@
         '';
 
       in rec {
-        packages.echidna = echidna pkgs;
-        packages.default = echidna pkgs;
+        packages.echidna = echidna;
+        packages.default = echidna;
 
         packages.echidna-redistributable = echidnaRedistributable;
 
         devShell = with pkgs;
           haskellPackages.shellFor {
-            packages = _: [ (echidna pkgs) ];
+            packages = _: [ echidna ];
             shellHook = "hpack";
             buildInputs = [
               solc

lib/Echidna.hs

@@ -47,12 +47,15 @@ prepareContract
   -> NonEmpty FilePath
   -> Maybe ContractName
   -> Seed
-  -> IO (VM RealWorld, World, GenDict)
+  -> IO (VM RealWorld, World, GenDict, [Tx])
 prepareContract env contracts solFiles specifiedContract seed = do
   let solConf = env.cfg.solConf
 
   -- compile and load contracts
-  (vm, funs, testNames, signatureMap) <- loadSpecified env specifiedContract contracts
+  (vm, funs, testNames, signatureMap) <-
+    loadSpecified env specifiedContract contracts
+
+  symTxs <- createSymTx env specifiedContract contracts vm
 
   -- run processors
   slitherInfo <- runSlither (NE.head solFiles) solConf
@@ -87,7 +90,7 @@ prepareContract env contracts solFiles specifiedContract seed = do
                      (returnTypes contracts)
 
   writeIORef env.testsRef echidnaTests
-  pure (vm, world, dict)
+  pure (vm, world, dict, symTxs)
 
 loadInitialCorpus :: Env -> World -> IO [[Tx]]
 loadInitialCorpus env world = do

lib/Echidna/Config.hs

@@ -119,6 +119,7 @@ instance FromJSON EConfigWithUsage where
         <*> v ..:? "testDestruction" ..!= False
         <*> v ..:? "allowFFI"        ..!= False
         <*> fnFilter
+        <*> v ..:? "symExec"         ..!= False
         where
         mode = v ..:? "testMode" >>= \case
           Just s  -> pure $ validateTestMode s

lib/Echidna/Solidity.hs

@@ -40,6 +40,7 @@ import Echidna.Events (EventMap, extractEvents)
 import Echidna.Exec (execTx, initialVM)
 import Echidna.Processor
 import Echidna.Symbolic (forceAddr)
+import Echidna.SymExec qualified
 import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isDapptestMode)
 import Echidna.Types.Config (EConfig(..), Env(..))
 import Echidna.Types.Signature
@@ -48,7 +49,7 @@ import Echidna.Types.Solidity
 import Echidna.Types.Test (EchidnaTest(..))
 import Echidna.Types.Tx
   ( basicTx, createTxWithValue, unlimitedGasPerBlock, initialTimestamp
-  , initialBlockNumber )
+  , initialBlockNumber, Tx )
 import Echidna.Types.World (World(..))
 import Echidna.Utility (measureIO)
 
@@ -179,6 +180,25 @@ abiOf pref solcContract =
     filter (not . isPrefixOf pref . fst)
            (Map.elems solcContract.abiMap <&> \method -> (method.name, snd <$> method.inputs))
 
+createSymTx :: Env -> Maybe Text -> [SolcContract] -> VM RealWorld -> IO [Tx]
+createSymTx env name cs vm = do
+    mainContract <- choose cs name
+    Echidna.SymExec.exploreContract solConf.contractAddr mainContract vm
+  where
+    -- copied from loadSpecified
+    solConf = env.cfg.solConf
+    choose [] _ = throwM NoContracts
+    choose (c:_) Nothing = pure c
+    choose _ (Just n) =
+      maybe (throwM $ ContractNotFound n) pure $
+        find (Data.Text.isSuffixOf (contractId n) . (.contractName)) cs
+    contractId n
+      | T.any (== ':') n =
+        let (splitPath, splitName) = T.breakOn ":" n
+        in rewritePathSeparators splitPath `T.append` splitName
+      | otherwise = ":" `append` n
+    rewritePathSeparators = T.pack . joinPath . splitDirectories . T.unpack
+
 -- | Given an optional contract name and a list of 'SolcContract's, try to load the specified
 -- contract, or, if not provided, the first contract in the list, into a 'VM' usable for Echidna
 -- testing and extract an ABI and list of tests. Throws exceptions if anything returned doesn't look
@@ -368,8 +388,8 @@ loadSolTests
   -> IO (VM RealWorld, World, [EchidnaTest])
 loadSolTests env fp name = do
   let solConf = env.cfg.solConf
-  buildOutputs <- compileContracts solConf fp
-  let contracts = Map.elems . Map.unions $ (\(BuildOutput (Contracts c) _) -> c) <$> buildOutputs
+  foo <- compileContracts solConf fp
+  let contracts = Map.elems . Map.unions $ (\(BuildOutput (Contracts c) _) -> c) <$> foo
   (vm, funs, testNames, _signatureMap) <- loadSpecified env name contracts
   let
     eventMap = Map.unions $ map (.eventMap) contracts

lib/Echidna/SymExec.hs

@@ -0,0 +1,95 @@
+{-# LANGUAGE DataKinds #-}
+
+module Echidna.SymExec where
+
+import Control.Monad (forM)
+import Data.ByteString qualified as BS
+import Data.ByteString.Lazy qualified as BS
+import Data.Functor ((<&>))
+import Data.Map qualified as Map
+import Data.Maybe (fromMaybe, mapMaybe)
+import Data.Text qualified as T
+import Optics.State.Operators
+import Optics.Core
+import EVM.ABI
+import EVM.Expr (simplify)
+import EVM.Fetch qualified as Fetch
+import EVM.SMT
+import EVM (loadContract)
+import EVM.Solidity (SolcContract(..), Method(..))
+import EVM.Solvers (withSolvers, Solver(Z3), CheckSatResult(Sat))
+import EVM.SymExec (interpret, runExpr, abstractVM, mkCalldata, produceModels, LoopHeuristic (Naive))
+import EVM.Types
+import Control.Monad.ST (stToIO, RealWorld)
+import Control.Monad.State.Strict (execState)
+import Echidna.Types.Tx
+import Data.Vector.Unboxed qualified as VUnboxed
+import Data.Vector.Unboxed.Mutable qualified as VUnboxed.Mutable
+
+
+-- test with applying multiple state modifying transactions before
+-- running exploreContract
+-- use execTxWithCov
+exploreContract :: Addr -> SolcContract -> VM RealWorld -> IO [Tx]
+exploreContract dst contract vm = do
+  let methods = Map.elems contract.abiMap
+      timeout = Just 30 -- seconds
+
+  res <- withSolvers Z3 2 timeout $ \solvers -> do
+    forM methods $ \method -> do
+      let
+        calldata@(cd, constraints) = mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+        vmSym' = abstractVM calldata contract.runtimeCode Nothing False
+        maxIter = Just 10
+        askSmtIters = 5
+        rpcInfo = Nothing
+      memory <- stToIO (ConcreteMemory <$> VUnboxed.Mutable.new 0)
+      vmSym <- stToIO vmSym'
+      let vm2 = execState (loadContract (LitAddr dst)) vm
+      let vm' = vm2 -- & #state .~ vmSym.state
+                   & #frames .~ []
+                   & #constraints .~ constraints
+                   -- & #state % #contract .~ SymAddr "entrypoint"
+                   -- & #state % #codeContract .~ SymAddr "entrypoint"
+                   & #state % #callvalue .~ TxValue
+                   & #state % #caller .~ SymAddr "caller"
+                   & #state % #calldata .~ cd
+                   & #state % #pc .~ 0
+                   & #state % #stack .~ []
+                   & #result .~ Nothing
+                   & #config % #baseState .~ AbstractBase
+                   & #env % #contracts .~ (Map.union vmSym.env.contracts vm.env.contracts)
+      -- print $ vmSym.state
+      -- print $ vm'.state
+      exprInter <- interpret (Fetch.oracle solvers rpcInfo) maxIter askSmtIters Naive vm' runExpr
+      models <- produceModels solvers (simplify exprInter)
+      print (mapMaybe (modelToTx dst method) models)
+      pure $ mapMaybe (modelToTx dst method) models
+
+  pure $ mconcat res
+
+modelToTx :: Addr -> Method -> (Expr 'End, CheckSatResult) -> Maybe Tx
+modelToTx dst method (_end, result) =
+  case result of
+    Sat cex ->
+      let
+        args = (zip [1..] method.inputs) <&> \(i::Int, (_argName, argType)) ->
+          case Map.lookup (Var ("arg" <> T.pack (show i))) cex.vars of
+            Just w ->
+              decodeAbiValue argType (BS.fromStrict (word256Bytes w))
+            Nothing -> -- put a placeholder
+              decodeAbiValue argType (BS.repeat 0)
+
+        value = fromMaybe 0 $ Map.lookup TxValue cex.txContext
+
+      in Just Tx
+        { call = SolCall (method.name, args)
+        , src = 0
+        , dst = dst
+        , gasprice = 0
+        , gas = maxGasPerBlock
+        , value = value
+        , delay = (0, 0)
+        }
+
+    _ -> Nothing

lib/Echidna/Types/Solidity.hs

@@ -78,6 +78,7 @@ data SolConf = SolConf
   , testDestruction :: Bool             -- ^ Whether or not to add a property to detect contract destruction
   , allowFFI        :: Bool             -- ^ Whether or not to allow FFI hevm cheatcode
   , methodFilter    :: Filter           -- ^ List of methods to avoid or include calling during a campaign
+  , symExec         :: Bool
   }
 
 defaultContractAddr :: Addr

src/Main.hs

@@ -114,12 +114,13 @@ main = withUtf8 $ withCP65001 $ do
 
   -- take the seed from config, otherwise generate a new one
   seed <- maybe (getRandomR (0, maxBound)) pure cfg.campaignConf.seed
-  (vm, world, dict) <-
+  (vm, world, dict, symTxs) <-
     prepareContract env contracts cliFilePath cliSelectedContract seed
 
   initialCorpus <- loadInitialCorpus env world
+  let corpus = initialCorpus <> (pure <$> symTxs)
   -- start ui and run tests
-  _campaign <- runReaderT (ui vm world dict initialCorpus) env
+  _campaign <- runReaderT (ui vm world dict corpus) env
 
   contractsCache <- readIORef cacheContractsRef
   slotsCache <- readIORef cacheSlotsRef
@@ -144,8 +145,8 @@ main = withUtf8 $ withCP65001 $ do
       measureIO cfg.solConf.quiet "Saving test reproducers" $
         saveTxs (dir </> "reproducers") (filter (not . null) $ (.reproducer) <$> tests)
       measureIO cfg.solConf.quiet "Saving corpus" $ do
-        corpus <- readIORef corpusRef
-        saveTxs (dir </> "coverage") (snd <$> Set.toList corpus)
+        finalCorpus <- readIORef corpusRef
+        saveTxs (dir </> "coverage") (snd <$> Set.toList finalCorpus)
 
       -- TODO: We use the corpus dir to save coverage reports which is confusing.
       -- Add config option to pass dir for saving coverage report and decouple it

src/test/Common.hs

@@ -114,9 +114,8 @@ runContract f selectedContract cfg = do
                 , eventQueue
                 , testsRef
                 , chainId = Nothing }
-  (vm, world, dict) <- prepareContract env contracts (f :| []) selectedContract seed
-
-  let corpus = []
+  (vm, world, dict, symTxs) <- prepareContract env contracts (f :| []) selectedContract seed
+  let corpus = pure <$> symTxs
   (_stopReason, finalState) <- flip runReaderT env $
     runWorker (pure ()) vm world dict 0 corpus cfg.campaignConf.testLimit
 

src/test/Spec.hs

@@ -32,4 +32,5 @@ main = withCurrentDirectory "./tests/solidity" . defaultMain $
            , dapptestTests
            , encodingJSONTests
            , cheatTests
+           -- , symbolicTests
            ]

src/test/Tests/Symbolic.hs

@@ -0,0 +1,13 @@
+module Tests.Symbolic (symbolicTests) where
+
+import Test.Tasty (TestTree, testGroup)
+
+import Common (testContract, solved)
+
+symbolicTests :: TestTree
+symbolicTests = testGroup "Symbolic tests"
+  [
+    testContract "symbolic/sym.sol" (Just "symbolic/sym.yaml")
+      [ ("func_one passed", solved "func_one")
+      , ("func_two passed", solved "func_two") ]
+  ]

tests/solidity/basic/default.yaml

@@ -89,3 +89,4 @@ rpcUrl: null
 rpcBlock: null
 # number of workers
 workers: 1
+symExec: false

tests/solidity/symbolic/sym.sol

@@ -0,0 +1,15 @@
+contract VulnerableContract {
+    mapping (uint256 => uint256) a;
+    function func_one(uint256 x) public payable {
+        a[12323] = ((x >> 5) / 7);
+        if (a[12323] == 2) {
+            assert(false); // BUG
+        }
+    }
+
+    function func_two(uint256 x) public payable {
+        if ((x >> 5) / 7 == 2) {
+            assert(false); // BUG
+        }
+    }
+}

tests/solidity/symbolic/sym.yaml

@@ -0,0 +1,2 @@
+testMode: assertion
+symExec: true