Merge pull request #83 from trailofbits/dev-perprop-exe

Dev perprop exe

lib/Echidna/Exec.hs

@@ -20,6 +20,7 @@ module Echidna.Exec (
   , execCallCoverage
   , getCover
   , ppHashes
+  , printResults
   , module Echidna.Internal.Runner
   ) where
 
@@ -37,7 +38,7 @@ import Data.List                  (intercalate, foldl')
 import Data.Map.Strict            (Map, insertWith, toAscList)
 import Data.Maybe                 (fromMaybe)
 import Data.Ord                   (comparing)
-import Data.Set                   (Set, insert, singleton)
+import Data.Set                   (Set, insert, singleton, size)
 import Data.Text                  (Text)
 import Data.Typeable              (Typeable)
 import Data.Vector                (Vector, fromList)
@@ -59,7 +60,7 @@ import EVM.Exec     (exec)
 import EVM.Types    (W256)
 
 import Echidna.ABI (SolCall, SolSignature, displayAbiCall, encodeSig, genInteractions, mutateCall)
-import Echidna.Config (Config(..), testLimit, shrinkLimit, range)
+import Echidna.Config (Config(..), testLimit, printCoverage, range, shrinkLimit)
 import Echidna.Internal.Runner
 import Echidna.Property (PropertyType(..))
 
@@ -78,6 +79,11 @@ type CoverageRef  = IORef CoverageInfo
 byHashes :: (Foldable t, Monoid (t CoveragePoint)) => t CoveragePoint -> Map W256 (Set (Int, Int))
 byHashes = foldr (\(C i w) -> insertWith mappend w $ singleton i) mempty . toList
 
+printResults :: (MonadIO m, MonadReader Config m) => Set CoveragePoint -> m ()
+printResults ci = do liftIO (putStrLn $ "Coverage: " ++ show (size ci) ++ " unique arcs")
+                     view printCoverage >>= \case True  -> liftIO . print . ppHashes $ byHashes ci
+                                                  False -> pure ()
+
 data ContractCov = ContractCov { hash :: String, arcs :: [(Int, Int)] } deriving (Show, Generic)
 newtype CoverageReport = CoverageReport { coverage :: [ContractCov] } deriving (Show, Generic)
 

package.yaml

@@ -56,3 +56,7 @@ executables:
     main: StateMachine.hs
     source-dirs: examples/state-machine
     dependencies: echidna
+  perprop-exe:
+    main: Main.hs
+    source-dirs: perprop
+    dependencies: echidna

perprop/Main.hs

@@ -0,0 +1,117 @@
+{-# LANGUAGE LambdaCase, FlexibleContexts, TemplateHaskell, TupleSections #-}
+
+module Main where
+
+import Control.Concurrent.MVar (MVar, newMVar, readMVar, swapMVar)
+import Control.Lens
+import Control.Monad           (forM, replicateM_)
+import Control.Monad.Identity  (Identity(..))
+import Control.Monad.Reader    (runReaderT)
+import Data.List               (foldl')
+import Data.Set                (unions)
+import Data.Text               (Text)
+import Data.Yaml
+import EVM                     (VM)
+import EVM.Types               (Addr)
+import System.Environment     (getArgs)
+
+import qualified Data.ByteString as BS
+
+import Hedgehog hiding (checkParallel, Property)
+import Hedgehog.Internal.Property (GroupName(..), PropertyName(..))
+
+import Echidna.ABI
+import Echidna.Config
+import Echidna.Exec
+import Echidna.Property
+import Echidna.Solidity
+
+
+-- }}}
+-- Types & instances
+-- {{{
+
+data Sender = Sender {
+    _address   :: Addr
+  , _name      :: String
+  } deriving Show
+
+data Property = Property {
+    _function :: Text
+  , _return   :: PropertyType
+  } deriving Show
+
+data PerPropConf = PerPropConf {
+    _testLimit' :: TestLimit
+  , _sender     :: [Sender]
+  , _properties :: [Property]
+  } deriving Show
+
+makeLenses ''Sender
+makeLenses ''Property
+makeLenses ''PerPropConf
+
+instance FromJSON Sender where
+  parseJSON (Object v) = Sender <$> v .: "address" <*> v.: "name"
+  parseJSON _ = mempty
+
+instance FromJSON Property where
+  parseJSON (Object v) = Property <$> v .: "name" <*> v .: "return"
+  parseJSON _ = mempty
+
+instance FromJSON PerPropConf where
+  parseJSON (Object v) = PerPropConf
+    <$> ((v .: "testLimit" :: Data.Yaml.Parser Int) <&> fromIntegral)
+    <*> v .: "sender"
+    <*> v .: "properties"
+  parseJSON _ = mempty
+
+-- }}}
+-- Parsing a config
+-- {{{
+
+readConf :: FilePath -> IO (Maybe (Config, [Property]))
+readConf f = decodeEither <$> BS.readFile f >>= \case
+  Left e -> putStrLn ("couldn't parse config, " ++ e) >> pure Nothing
+  Right (PerPropConf t s p) -> pure . Just . (,p) $
+    defaultConfig & addrList .~ Just (view address <$> s) & testLimit .~ t & epochs .~ 1
+
+group :: String
+      -> Config
+      -> [SolSignature]
+      -> VM
+      -> [(Property, [SolCall], MVar [CoverageInfo])]
+      -> Group
+group n c a v ps = Group (GroupName n) $ map prop ps where
+  prop ((Property f r),cov,mvar) = ( PropertyName $ show f
+                                   , useConfig (ePropertySeqCoverage cov mvar (flip (checkTest r) f) a v))
+
+  useConfig = runIdentity . (`runReaderT` c)
+
+-- }}}
+-- Main
+-- {{{
+
+main :: IO ()
+main = getArgs >>= \case
+  [cf,sf] -> readConf cf >>= \case
+    Nothing       -> pure ()
+    (Just (c, ps)) -> do
+      (v,a,_) <- runReaderT (loadSolidity sf Nothing) c
+      tests <- mapM (\p -> fmap (p,) (newMVar [])) ps
+      replicateM_ (c ^. epochs) $ do
+        xs <- forM tests $ \(p,mvar) -> do
+          cov     <- readMVar mvar
+          lastGen <- getCover cov
+          _       <- swapMVar mvar []
+          pure (p,lastGen,mvar)
+
+        checkParallel $ group sf c a v xs
+
+      ls <- mapM (readMVar . snd) tests
+      let ci = foldl' (\acc xs -> unions (acc : map snd xs)) mempty ls
+      putStrLn $ ppHashes (byHashes ci)
+
+  _ -> putStrLn "USAGE: ./perprop-exe config.yaml contract.sol"
+  
+-- }}}

src/Main.hs

@@ -8,7 +8,7 @@ import Control.Monad           (forM, replicateM_)
 import Control.Monad.IO.Class  (liftIO)
 import Control.Monad.Reader    (runReaderT)
 import Data.List               (foldl')
-import Data.Set                (size, unions)
+import Data.Set                (unions)
 import Data.Text               (pack)
 import Data.Semigroup          ((<>))
 
@@ -84,5 +84,4 @@ main = do
         
       ls <- liftIO $ mapM (readMVar . snd) tests
       let ci = foldl' (\acc xs -> unions (acc : map snd xs)) mempty ls
-      liftIO $ putStrLn $ "Coverage: " ++ show (size ci) ++ " unique arcs"
-      if config ^. printCoverage then liftIO $ print $ ppHashes $ byHashes ci else pure ()
+      printResults ci