Use Slither for constant extraction

.github/scripts/install-crytic-compile.sh

@@ -1,4 +1,3 @@
 if [ "$(uname)" != "Darwin" ]; then
-    pip3 install crytic-compile --user
     pip3 install slither-analyzer --user
 fi

README.md

@@ -10,7 +10,7 @@ More seriously, Echidna is a Haskell program designed for fuzzing/property-based
 
 * Generates inputs tailored to your actual code
 * Optional corpus collection, mutation and coverage guidance to find deeper bugs
-* Optional [Slither](https://github.com/crytic/slither) integration to extract useful information before the fuzzing campaign
+* Powered by [Slither](https://github.com/crytic/slither) to extract useful information before the fuzzing campaign
 * Curses-based retro UI, text-only or JSON output
 * Automatic testcase minimization for quick triage
 * Seamless integration into the development workflow
@@ -129,9 +129,12 @@ will either be `property` or `assertion`, and `status` always takes on either
 
 ## Installation
 
+
+
 ### Precompiled binaries
 
-If you want to quickly test Echidna in Linux or MacOS, we provide statically linked Linux binaries built on Ubuntu and mostly static MacOS binaries on our [releases page](https://github.com/crytic/echidna/releases). You can also grab the same type of binaries from our [CI pipeline](https://github.com/crytic/echidna/actions?query=workflow%3ACI+branch%3Amaster+event%3Apush), just click the commit to find binaries for Linux or MacOS. Make sure you have the latest release of [crytic-compile](https://github.com/crytic/crytic-compile) and [slither](https://github.com/crytic/slither) installed before starting to use Echidna.
+Before starting, make sure Slither is [installed](https://github.com/crytic/slither) (`pip3 install slither-analyzer --user`).
+If you want to quickly test Echidna in Linux or MacOS, we provide statically linked Linux binaries built on Ubuntu and mostly static MacOS binaries on our [releases page](https://github.com/crytic/echidna/releases). You can also grab the same type of binaries from our [CI pipeline](https://github.com/crytic/echidna/actions?query=workflow%3ACI+branch%3Amaster+event%3Apush), just click the commit to find binaries for Linux or MacOS.
 
 ### Docker container
 

examples/solidity/basic/constants.sol

@@ -1,12 +1,19 @@
 contract Constants {
   bool found = false;
+  bool found_large = false;
 
   function find(int i) public {
-    if (i == 1447) {found = true;}
-    if (i == 133700000000) {found = false;}
+    if (i == 1447) { found = true; }
+    if (i == 133700000000) { found = false; }
+    if (i == 11234567890123456789012345678901234560) { found_large = true; }
   }
 
   function echidna_found() public view returns (bool) {
     return(!found);
   }
+
+  function echidna_found_large() public view returns (bool) {
+    return(!found_large);
+  }
+
 }

examples/solidity/basic/darray-mutation.sol

@@ -1,9 +1,9 @@
 contract C { 
-  bytes example = "abcdef123";
+  bytes e = "abcdef123";
   bool state;
 
   function f(bytes memory bs) public {
-    if (bs[0] == "a" && bs[1] == "b" && bs[2] == "c" && bs.length > 16)
+    if (bs[0] == e[0] && bs[1] == e[1] && bs[2] == e[2] && bs.length > 16)
         state = true;
   }
 

lib/Echidna.hs

@@ -53,10 +53,13 @@ prepareContract cfg fs c g = do
   ca <- view (hasLens . cryticArgs)
   si <- runSlither (NE.head fs) ca
 
+  -- filter extracted constants
+  let extractedConstants = filterConstantValue si
+
   -- load tests
   (v, w, ts) <- prepareForTest p c si
   let ads' = AbiAddress <$> v ^. env . EVM.contracts . to keys
   -- start ui and run tests
-  return (v, w, ts, Just $ mkGenDict df (extractConstants cs ++ timeConstants ++ largeConstants ++ NE.toList ads ++ ads') [] g (returnTypes cs), txs)
+  return (v, w, ts, Just $ mkGenDict df (extractedConstants ++ timeConstants ++ largeConstants ++ NE.toList ads ++ ads') [] g (returnTypes cs), txs)
   where cd = cfg ^. cConf . corpusDir
         df = cfg ^. cConf . dictFreq

lib/Echidna/ABI.hs

@@ -22,11 +22,12 @@ import Data.Hashable (Hashable(..))
 import Data.HashMap.Strict (HashMap)
 import Data.HashSet (HashSet, fromList, union)
 import Data.List (intercalate)
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, catMaybes)
 import Data.Text (Text)
 import Data.Vector (Vector)
 import Data.Vector.Instances ()
 import Data.Word8 (Word8)
+import Data.DoubleWord (Int256, Word256)
 import Numeric (showHex)
 
 import EVM.ABI hiding (genAbiValue)
@@ -49,6 +50,23 @@ import Echidna.Types.Signature
 fallback :: SolSignature
 fallback = ("",[])
 
+commonTypeSizes :: [Int]
+commonTypeSizes = [8,16..256]
+
+mkValidAbiInt :: Int -> Int256 -> Maybe AbiValue
+mkValidAbiInt i x = if abs x <= 2 ^ (i - 1) - 1 then Just $ AbiInt i x else Nothing
+
+mkValidAbiUInt :: Int -> Word256 -> Maybe AbiValue
+mkValidAbiUInt i x = if x <= 2 ^ i - 1 then Just $ AbiUInt i x else Nothing
+
+makeNumAbiValues :: Integer -> [AbiValue]
+makeNumAbiValues i = let l f = f <$> commonTypeSizes <*> fmap fromIntegral [i-1..i+1] in
+    catMaybes (l mkValidAbiInt ++ l mkValidAbiUInt) 
+
+makeArrayAbiValues :: BS.ByteString -> [AbiValue]
+makeArrayAbiValues b = let size = BS.length b in [AbiString b, AbiBytesDynamic b] ++
+ fmap (\n -> AbiBytes n . BS.append b $ BS.replicate (n - size) 0) [size..32]
+
 -- | Pretty-print some 'AbiValue'.
 ppAbiValue :: AbiValue -> String
 ppAbiValue (AbiUInt _ n)         = show n

lib/Echidna/Processor.hs

@@ -11,25 +11,31 @@ import Control.Exception          (Exception)
 import Control.Monad.Catch        (MonadThrow(..))
 import Data.Aeson                 (decode, Value(..))
 import Data.Text                  (Text, pack, unpack)
+import Data.List                  (nub)
+import Text.Read                  (readMaybe)
 import System.Directory           (findExecutable)
 import System.Process             (StdStream(..), readCreateProcessWithExitCode, proc, std_err)
 import System.Exit                (ExitCode(..))
+import Numeric                    (showHex)
 
 import qualified Data.ByteString.Lazy.Char8 as BSL
+import qualified Data.ByteString.UTF8 as BSU
 import qualified Data.HashMap.Strict as M
 
 import Echidna.Types.Signature (ContractName, FunctionName, FunctionHash)
-import Echidna.ABI (hashSig)
+import EVM.ABI (AbiValue(..))
+import Echidna.ABI (hashSig, makeNumAbiValues, makeArrayAbiValues)
+
 
 -- | Things that can go wrong trying to run a processor. Read the 'Show'
 -- instance for more detailed explanations.
 data ProcException = ProcessorFailure String String
-                   | ProcessorNotFound String
+                   | ProcessorNotFound String String
 
 instance Show ProcException where
   show = \case
-    ProcessorFailure p e -> "Error running " ++ p ++ ": " ++ e
-    ProcessorNotFound p  -> "Cannot find processor " ++ p
+    ProcessorFailure p e -> "Error running " ++ p ++ ":\n" ++ e
+    ProcessorNotFound p e -> "Cannot find " ++ p ++ "in PATH.\n" ++ e
 
 instance Exception ProcException
 
@@ -46,7 +52,7 @@ filterResults Nothing rs = concatMap (fmap hashSig . snd) rs
 data SlitherInfo = PayableInfo (ContractName, [FunctionName])
                  | ConstantFunctionInfo (ContractName, [FunctionName])
                  | AssertFunction (ContractName, [FunctionName])
-                 | ConstantValue (ContractName, Text) -- Not used right now, it will change soon
+                 | ConstantValue AbiValue
                  | GenerationGraph (ContractName, FunctionName, [FunctionName])
   deriving (Show)
 makePrisms ''SlitherInfo
@@ -66,17 +72,20 @@ filterConstantFunction = slitherFilter _ConstantFunctionInfo
 filterGenerationGraph :: [SlitherInfo] -> [(ContractName, FunctionName, [FunctionName])]
 filterGenerationGraph = slitherFilter _GenerationGraph
 
+filterConstantValue :: [SlitherInfo] -> [AbiValue]
+filterConstantValue = slitherFilter _ConstantValue
+
 -- Slither processing
 runSlither :: (MonadIO m, MonadThrow m) => FilePath -> [String] -> m [SlitherInfo]
 runSlither fp args = let args' = ["--ignore-compile", "--print", "echidna", "--json", "-"] ++ args in do
   mp <- liftIO $ findExecutable "slither"
   case mp of
-    Nothing -> return []
+    Nothing -> throwM $ ProcessorNotFound "slither" "You should install it using 'pip3 install slither-analyzer --user'"
     Just path -> liftIO $ do
-      (ec, out, _) <- readCreateProcessWithExitCode (proc path $ args' |> fp) {std_err = Inherit} ""
+      (ec, out, err) <- readCreateProcessWithExitCode (proc path $ args' |> fp) {std_err = Inherit} ""
       case ec of
         ExitSuccess -> return $ procSlither out
-        ExitFailure _ -> return [] --we can make slither mandatory using: throwM $ ProcessorFailure "slither" err
+        ExitFailure _ -> throwM $ ProcessorFailure "slither" err
 
 procSlither :: String -> [SlitherInfo]
 procSlither r =
@@ -139,13 +148,30 @@ mconsts _  _         = []
 
 mconsts' :: Text -> Value -> [SlitherInfo]
 mconsts' _ (Object o) = case (M.lookup "value" o, M.lookup "type" o) of
-                         (Just v, Just (String t)) -> [ConstantValue (pack $ show v, t)]
-                         (Nothing, Nothing)        -> concatMap (uncurry mconsts') $ M.toList o
-                         _                         -> error "invalid JSON formatting parsing constants"
+                         (Just (String s), Just (String t)) -> map ConstantValue $ nub $ parseAbiValue (unpack s, unpack t)
+                         (Nothing, Nothing)                 -> concatMap (uncurry mconsts') $ M.toList o
+                         _                                  -> error "invalid JSON formatting parsing constants"
 
 mconsts' _ (Array  a) = concatMap (mconsts' "") a
 mconsts' _  _         = []
 
+parseAbiValue :: (String, String) -> [AbiValue]
+parseAbiValue (v, 'u':'i':'n':'t':_) = case readMaybe v of 
+                                               Just m -> makeNumAbiValues m
+                                               _      -> []
+
+parseAbiValue (v, 'i':'n':'t':_)     = case readMaybe v of 
+                                               Just m -> makeNumAbiValues m
+                                               _      -> []
+
+parseAbiValue (v, "string")          = makeArrayAbiValues $ BSU.fromString v
+parseAbiValue (v, "address")         = case readMaybe v :: Maybe Int of
+                                                          Just n -> case readMaybe ("0x" ++ showHex n "") of
+                                                                      Just a  -> [AbiAddress a]
+                                                                      Nothing -> []
+                                                          _      -> []
+parseAbiValue _                      = []
+
 
 -- parse actual generation graph
 mggraph :: Text -> Value -> [SlitherInfo]

lib/Echidna/Solidity.hs

@@ -15,24 +15,19 @@ import Control.Monad.IO.Class     (MonadIO(..))
 import Control.Monad.Fail         (MonadFail)
 import Control.Monad.Reader       (MonadReader)
 import Control.Monad.State.Strict (execStateT)
-import Data.Aeson                 (Value(..))
-import Data.ByteString.Lens       (packedChars)
-import Data.DoubleWord            (Int256, Word256)
 import Data.Foldable              (toList)
 import Data.Has                   (Has(..))
-import Data.List                  (find, nub, partition)
-import Data.List.Lens             (prefixed, suffixed)
+import Data.List                  (find, partition)
 import Data.Map                   (elems)
 import Data.Maybe                 (isJust, isNothing, catMaybes)
 import Data.Monoid                ((<>))
 import Data.Text                  (Text, isPrefixOf, isSuffixOf, append)
 import Data.Text.Lens             (unpacked)
-import Data.Text.Read             (decimal)
 import System.Process             (StdStream(..), readCreateProcessWithExitCode, proc, std_err)
 import System.IO                  (openFile, IOMode(..))
 import System.Exit                (ExitCode(..))
 import System.Directory           (findExecutable)
-import Echidna.ABI                (encodeSig, hashSig, fallback)
+import Echidna.ABI                (encodeSig, hashSig, fallback, commonTypeSizes, mkValidAbiInt, mkValidAbiUInt)
 import Echidna.Exec               (execTx, initialVM)
 import Echidna.RPC                (loadEthenoBatch)
 import Echidna.Types.Signature    (FunctionHash, SolSignature, SignatureMap)
@@ -47,7 +42,6 @@ import EVM.Solidity
 import EVM.Types    (Addr)
 import EVM.Concrete (w256)
 
-import qualified Data.ByteString     as BS
 import qualified Data.List.NonEmpty  as NE
 import qualified Data.List.NonEmpty.Extra as NEE
 import qualified Data.HashMap.Strict as M
@@ -293,21 +287,12 @@ loadSolTests :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x, Has Tx
              => NE.NonEmpty FilePath -> Maybe Text -> m (VM, World, [SolTest])
 loadSolTests fp name = loadWithCryticCompile fp name >>= (\t -> prepareForTest t Nothing [])
 
-commonTypeSizes :: [Int]
-commonTypeSizes = [8,16..256]
-
-mkValidAbiInt :: Int -> Int256 -> Maybe AbiValue
-mkValidAbiInt i x = if abs x <= 2 ^ (i - 1) - 1 then Just $ AbiInt i x else Nothing
-
 mkLargeAbiInt :: Int -> AbiValue
 mkLargeAbiInt i = AbiInt i $ 2 ^ (i - 1) - 1
 
 mkLargeAbiUInt :: Int -> AbiValue
 mkLargeAbiUInt i = AbiUInt i $ 2 ^ i - 1
 
-mkValidAbiUInt :: Int -> Word256 -> Maybe AbiValue
-mkValidAbiUInt i x = if x <= 2 ^ i - 1 then Just $ AbiUInt i x else Nothing
-
 timeConstants :: [AbiValue]
 timeConstants = concatMap dec [initialTimestamp, initialBlockNumber]
   where dec i = let l f = f <$> commonTypeSizes <*> fmap fromIntegral [i-1..i+1] in
@@ -316,36 +301,6 @@ timeConstants = concatMap dec [initialTimestamp, initialBlockNumber]
 largeConstants :: [AbiValue]
 largeConstants = concatMap (\i -> [mkLargeAbiInt i, mkLargeAbiUInt i]) commonTypeSizes
 
--- | Given a list of 'SolcContract's, try to parse out string and integer literals
-extractConstants :: [SolcContract] -> [AbiValue]
-extractConstants = nub . concatMap (constants "" . view contractAst) where
-  -- Tools for parsing numbers and quoted strings from 'Text'
-  asDecimal = preview $ to decimal . _Right . _1
-  asQuoted  = preview $ unpacked . prefixed "\"" . suffixed "\"" . packedChars
-  -- We need this because sometimes @solc@ emits a json string with a type, then a string
-  -- representation of some value of that type. Why is this? Unclear. Anyway, this lets us match
-  -- those cases like regular strings
-  literal t f (String (T.words -> ((^? only t) -> m) : y : _)) = m *> f y
-  literal _ _ _                                                = Nothing
-  -- When we get a number, it could be an address, uint, or int. We'll try everything.
-  dec i = let l f = f <$> commonTypeSizes <*> fmap fromIntegral [i-1..i+1] in
-    AbiAddress i : catMaybes (l mkValidAbiInt ++ l mkValidAbiUInt)
-  -- 'constants' takes a property name and its 'Value', then tries to find solidity literals
-  -- CASE ONE: we're looking at a big object with a bunch of little objects, recurse
-  constants _ (Object o) = concatMap (uncurry constants) $ M.toList o
-  constants _ (Array  a) = concatMap (constants "")        a
-  -- CASE TWO: we're looking at a @type@, try to parse it
-  -- 2.1: We're looking at a @int_const@ with a decimal number inside, could be an address, int, or uint
-  --      @type: "int_const 0x12"@ ==> @[AbiAddress 18, AbiUInt 8 18,..., AbiUInt 256 18, AbiInt 8 18,...]@
-  constants "typeString" (literal "int_const" asDecimal -> Just i) = dec i
-  -- 2.2: We're looking at something of the form @type: literal_string "[...]"@, a string literal
-  --      @type: "literal_string \"123\""@ ==> @[AbiString "123", AbiBytes 3 "123"...]@
-  constants "typeString" (literal "literal_string" asQuoted -> Just b) =
-    let size = BS.length b in [AbiString b, AbiBytesDynamic b] ++
-      fmap (\n -> AbiBytes n . BS.append b $ BS.replicate (n - size) 0) [size..32]
-  -- CASE THREE: we're at a leaf node with no constants
-  constants _  _ = []
-
 returnTypes :: [SolcContract] -> Text -> Maybe AbiType
 returnTypes cs t = preview (_Just . methodOutput . _Just . _2) .
   find ((== t) . view methodName) $ concatMap (toList . view abiMap) cs

package.yaml

@@ -42,6 +42,7 @@ dependencies:
   - unix
   - unliftio
   - unliftio-core
+  - utf8-string
   - unordered-containers
   - vector
   - vector-instances

src/test/Tests/Integration.hs

@@ -62,7 +62,8 @@ integrationTests = testGroup "Solidity Integration Testing"
   , testContract "basic/contractAddr.sol" (Just "basic/contractAddr.yaml")
       [ ("echidna_address failed",                 passed      "echidna_address") ]
   , testContract "basic/constants.sol"    Nothing
-      [ ("echidna_found failed",                   solved      "echidna_found") ]
+      [ ("echidna_found failed",                   solved      "echidna_found")
+      , ("echidna_found_large failed",             solved      "echidna_found_large") ]
   , testContract "basic/constants2.sol"   Nothing
       [ ("echidna_found32 failed",                 solved      "echidna_found32") ]
   , testContract "basic/constants3.sol"   Nothing