Merge pull request #282 from crytic/dev-temporal

Add support for time

examples/solidity/basic/default.yaml

@@ -34,3 +34,7 @@ quiet: False
 #dashboard determines if output is just text or an AFL-like display
 dashboard: true
 #seed not defined by default, is the random seed
+maxTimeDelay: 0
+#maximum time between generated txs
+maxBlockDelay: 0
+#maximum number of blocks elapsed between generated txs

examples/solidity/basic/time.sol

@@ -0,0 +1,17 @@
+contract Time {
+  uint start;
+  uint marked;
+
+  constructor() public {
+    start  = now;
+    marked = now;
+  }
+
+  function mark() public {
+    marked = now;
+  }
+
+  function echidna_timepassed() public returns (bool) {
+    return(start == marked);
+  }
+}

examples/solidity/basic/time.yaml

@@ -0,0 +1,2 @@
+maxTimeDelay: 1000
+maxBlockDelay: 5

lib/Echidna/Config.hs

@@ -8,7 +8,7 @@
 module Echidna.Config where
 
 import Control.Lens
-import Control.Monad (liftM2)
+import Control.Monad (liftM2, liftM4)
 import Control.Monad.Catch (MonadThrow)
 import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.Reader (Reader, ReaderT(..), runReader)
@@ -65,9 +65,9 @@ instance FromJSON EConfig where
                 let goal fname = if (fprefix <> "revert_") `isPrefixOf` fname then ResRevert else ResTrue
                 return $ TestConf (\fname -> (== goal fname)  . maybe ResOther classifyRes . view result)
                                   (const psender)
-        xc = liftM2 TxConf
-               (C Dull . fromIntegral <$> v .:? "propMaxGas"  .!= (8000030 :: Integer))
-               (C Dull . fromIntegral <$> v .:? "testMaxGas"  .!= (0xffffffff :: Integer))
+        getWord s d = C Dull . fromIntegral <$> v .:? s .!= (d :: Integer)
+        xc = liftM4 TxConf (getWord "propMaxGas" 8000030) (getWord "testMaxGas" 0xffffffff)
+                           (getWord "maxTimeDelay" 0)     (getWord "maxBlockDelay" 0)
         cc = CampaignConf <$> v .:? "testLimit"   .!= 50000
                           <*> v .:? "seqLen"      .!= 100
                           <*> v .:? "shrinkLimit" .!= 5000

lib/Echidna/Solidity.hs

@@ -124,7 +124,7 @@ loadLibraries :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x)
               => [SolcContract] -> Addr -> Addr -> VM -> m VM
 loadLibraries []     _  _ vm = return vm
 loadLibraries (l:ls) la d vm = loadLibraries ls (la + 1) d =<< loadRest
-  where loadRest = execStateT (execTx $ Tx (Right $ l ^. creationCode) d la 0xffffffff 0) vm
+  where loadRest = execStateT (execTx $ Tx (Right $ l ^. creationCode) d la 0xffffffff 0 (0,0)) vm
 
 -- | Generate a string to use as argument in solc to link libraries starting from addrLibrary
 linkLibraries :: [String] -> String
@@ -165,7 +165,7 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
   case find (not . null . snd) tests of
     Just (t,_) -> throwM $ TestArgsFound t                       -- Test args check
     Nothing    -> loadLibraries ls addrLibrary d blank >>= fmap (, fallback : funs, fst <$> tests) .
-      execStateT (execTx $ Tx (Right bc) d ca 0xffffffff (w256 $ fromInteger balc))
+      execStateT (execTx $ Tx (Right bc) d ca 0xffffffff (w256 $ fromInteger balc) (0,0))
 
 
   where choose []    _        = throwM NoContracts

lib/Echidna/Test.hs

@@ -60,7 +60,7 @@ checkETest t = asks getter >>= \(TestConf p s) -> view (hasLens . propGas) >>= \
       matchC sig = not . (BS.isPrefixOf . BS.take 4 $ abiCalldata (encodeSig sig) mempty)
   res <- case t of
     -- If our test is a regular user-defined test, we exec it and check the result
-    Left  (f, a) -> execTx (Tx (Left (f, [])) (s a) a g 0) >> gets (p f . getter)
+    Left  (f, a) -> execTx (Tx (Left (f, [])) (s a) a g 0 (0,0)) >> gets (p f . getter)
     -- If our test is an auto-generated assertion test, we check if we failed an assert on that fn
     Right sig    -> (||) <$> fmap matchR       (use $ hasLens . result)
                          <*> fmap (matchC sig) (use $ hasLens . state . calldata)

lib/Echidna/Transaction.hs

@@ -2,7 +2,10 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Echidna.Transaction where
 
@@ -13,7 +16,7 @@ import Control.Monad (join, liftM2, liftM3, liftM5)
 import Control.Monad.Catch (MonadThrow)
 import Control.Monad.Random.Strict (MonadRandom, getRandomR)
 import Control.Monad.Reader.Class (MonadReader)
-import Control.Monad.State.Strict (MonadState, State, runState)
+import Control.Monad.State.Strict (MonadState, State, evalStateT, runState)
 import Data.Aeson (ToJSON(..), object)
 import Data.ByteString (ByteString)
 import Data.Either (either, lefts)
@@ -39,14 +42,19 @@ data Tx = Tx { _call  :: Either SolCall ByteString -- | Either a call or code fo
              , _dst   :: Addr                      -- | Destination
              , _gas'  :: Word                      -- | Gas
              , _value :: Word                      -- | Value
+             , _delay :: (Word, Word)              -- | (Time, # of blocks since last call)
              } deriving (Eq, Ord, Show)
 
 makeLenses ''Tx
 
-data TxConf = TxConf { _propGas :: Word
+data TxConf = TxConf { _propGas       :: Word
                      -- ^ Gas to use evaluating echidna properties
-                     , _txGas   :: Word
+                     , _txGas         :: Word
                      -- ^ Gas to use in generated transactions
+                     , _maxTimeDelay  :: Word
+                     -- ^ Maximum time delay between transactions (seconds)
+                     , _maxBlockDelay :: Word
+                     -- ^ Maximum block delay between transactions
                      }
 
 makeLenses 'TxConf
@@ -55,14 +63,22 @@ makeLenses 'TxConf
 ppSolCall :: SolCall -> String
 ppSolCall (t, vs) = (if t == "" then T.unpack "*fallback*" else T.unpack t) ++ "(" ++ intercalate "," (ppAbiValue <$> vs) ++ ")"
 
+-- | If half a tuple is zero, make both halves zero. Useful for generating delays, since block number
+-- only goes up with timestamp
+level :: (Num a, Eq a) => (a, a) -> (a, a)
+level (elemOf each 0 -> True) = (0,0)
+level x                       = x
+
 instance ToJSON Tx where
-  toJSON (Tx c s d g v) = object [ ("call",  toJSON $ either ppSolCall (const "<CREATE>") c)
-                                 -- from/to are Strings, since JSON doesn't support hexadecimal notation
-                                 , ("from",  toJSON $ show s)
-                                 , ("to",    toJSON $ show d)
-                                 , ("value", toJSON $ show v)
-                                 , ("gas",   toJSON $ show g)
-                                 ]
+  toJSON (Tx c s d g v (t,b)) = object [ ("call",        toJSON $ either ppSolCall (const "<CREATE>") c)
+                                       -- from/to are Strings, since JSON doesn't support hexadecimal notation
+                                       , ("from",        toJSON $ show s)
+                                       , ("to",          toJSON $ show d)
+                                       , ("value",       toJSON $ show v)
+                                       , ("gas",         toJSON $ show g)
+                                       , ("time delay",  toJSON $ show t)
+                                       , ("block delay", toJSON $ show b)
+                                       ]
 
 -- | A contract is just an address with an ABI (for our purposes).
 type ContractA = (Addr, [SolSignature])
@@ -82,41 +98,47 @@ genTxWith :: (MonadRandom m, MonadState x m, Has World x, MonadThrow m)
           -> (Addr -> ContractA -> m SolCall)         -- ^ Call generator
           -> m Word                                   -- ^ Gas generator
           -> (Addr -> ContractA -> SolCall -> m Word) -- ^ Value generator
+          -> m (Word, Word)                           -- ^ Delay generator
           -> m Tx
-genTxWith s r c g v = use hasLens >>=
-  \case (World ss rs) -> let s' = s ss; r' = r rs; c' = join $ liftM2 c s' r' in
-                           liftM5 Tx (Left <$> c') s' (fst <$> r') g =<< liftM3 v s' r' c'
+genTxWith s r c g v t = use hasLens >>= \(World ss rs) ->
+  let s' = s ss; r' = r rs; c' = join $ liftM2 c s' r' in
+    (liftM5 Tx (Left <$> c') s' (fst <$> r') g =<< liftM3 v s' r' c') <*> t
 
 -- | Synthesize a random 'Transaction', not using a dictionary.
-genTx :: (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has World y, MonadThrow m) => m Tx
-genTx = view (hasLens . txGas) >>= \g -> genTxWith (rElem "sender list") (rElem "recipient list")
-                                                   (const $ genInteractions . snd) (pure g) (\_ _ _ -> pure 0)
+genTx :: forall m x y. (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has World y, MonadThrow m) => m Tx
+genTx = use (hasLens :: Lens' y World) >>= evalStateT genTxM . (defaultDict,)
 
 -- | Generate a random 'Transaction' with either synthesis or mutation of dictionary entries.
 genTxM :: (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has GenDict y, Has World y, MonadThrow m) => m Tx
-genTxM = view (hasLens . txGas) >>= \g -> genTxWith (rElem "sender list") (rElem "recipient list")
-                                                    (const $ genInteractionsM . snd) (pure g) (\_ _ _ -> pure 0)
+genTxM = view hasLens >>= \(TxConf _ g t b) -> genTxWith
+  (rElem "sender list") (rElem "recipient list")                             -- src and dst
+  (const $ genInteractionsM . snd)                                           -- call itself
+  (pure g) (\_ _ _ -> pure 0) (level <$> liftM2 (,) (inRange t) (inRange b)) -- gas, value, delay
+     where inRange hi = w256 . fromIntegral <$> getRandomR (0 :: Integer, fromIntegral hi)
 
 -- | Check if a 'Transaction' is as \"small\" (simple) as possible (using ad-hoc heuristics).
 canShrinkTx :: Tx -> Bool
-canShrinkTx (Tx (Right _) _ _ _ 0)    = False
-canShrinkTx (Tx (Left (_,l)) _ _ _ 0) = any canShrinkAbiValue l
-canShrinkTx _                         = True
+canShrinkTx (Tx (Right _) _ _ _ 0 (0,0))    = False
+canShrinkTx (Tx (Left (_,l)) _ _ _ 0 (0,0)) = any canShrinkAbiValue l
+canShrinkTx _                               = True
 
 -- | Given a 'Transaction', generate a random \"smaller\" 'Transaction', preserving origin,
 -- destination, value, and call signature.
 shrinkTx :: MonadRandom m => Tx -> m Tx
-shrinkTx (Tx c s d g (C _ v)) = let c' = either (fmap Left . shrinkAbiCall) (fmap Right . pure) c in
-  liftM5 Tx c' (pure s) (pure d) (pure g) $ w256 . fromIntegral <$> getRandomR (0 :: Integer, fromIntegral v)
+shrinkTx (Tx c s d g (C _ v) (C _ t, C _ b)) = let
+  c' = either (fmap Left . shrinkAbiCall) (fmap Right . pure) c
+  lower x = w256 . fromIntegral <$> getRandomR (0 :: Integer, fromIntegral x) in
+    liftM5 Tx c' (pure s) (pure d) (pure g) (lower v) <*> fmap level (liftM2 (,) (lower t) (lower b))
 
 -- | Given a 'Set' of 'Transaction's, generate a similar 'Transaction' at random.
 spliceTxs :: (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has World y, MonadThrow m) => Set Tx -> m Tx
-spliceTxs ts = let l = S.toList ts; (cs, ss) = unzip $ (\(Tx c s _ _ _) -> (c,s)) <$> l in
+spliceTxs ts = let l = S.toList ts; (cs, ss) = unzip $ (\(Tx c s _ _ _ _) -> (c,s)) <$> l in
   view (hasLens . txGas) >>= \g ->
     genTxWith (const . rElem "sender list" $ ss) (rElem "recipient list")
               (\_ _ -> mutateAbiCall =<< rElem "past calls" (lefts cs)) (pure g)
-              (\ _ _ (n,_) -> let valOf (Tx c _ _ _ v) = if elem n $ c ^? _Left . _1 then v else 0
+              (\ _ _ (n,_) -> let valOf (Tx c _ _ _ v _) = if elem n $ c ^? _Left . _1 then v else 0
                               in rElem "values" $ valOf <$> l)
+              (pure (0,0))
 
 -- | Lift an action in the context of a component of some 'MonadState' to an action in the
 -- 'MonadState' itself.
@@ -126,9 +148,10 @@ liftSH = S.state . runState . zoom hasLens
 -- | Given a 'Transaction', set up some 'VM' so it can be executed. Effectively, this just brings
 -- 'Transaction's \"on-chain\".
 setupTx :: (MonadState x m, Has VM x) => Tx -> m ()
-setupTx (Tx c s r g v) = liftSH . sequence_ $
+setupTx (Tx c s r g v (t, b)) = liftSH . sequence_ $
   [ result .= Nothing, state . pc .= 0, state . stack .= mempty, state . memory .= mempty, state . gas .= g
-  , tx . origin .= s, state . caller .= s, state . callvalue .= v, setup] where
+  , tx . origin .= s, state . caller .= s, state . callvalue .= v
+  , block . timestamp += t, block . number += b, setup] where
     setup = case c of
       Left cd  -> loadContract r >> state . calldata .= encode cd
       Right bc -> assign (env . contracts . at r) (Just $ initialContract (RuntimeCode bc) & set balance v) >> loadContract r

lib/Echidna/UI.hs

@@ -54,12 +54,14 @@ type Names = Role -> Addr -> String
 
 -- | Given rules for pretty-printing associated address, and whether to print them, pretty-print a 'Transaction'.
 ppTx :: (MonadReader x m, Has Names x, Has TxConf x) => Bool -> Tx -> m String
-ppTx b (Tx c s r g v) = let sOf = either ppSolCall (const "<CREATE>") in do
+ppTx pn (Tx c s r g v (t, b)) = let sOf = either ppSolCall (const "<CREATE>") in do
   names <- view hasLens
   tGas  <- view $ hasLens . txGas
-  return $ sOf c ++ (if not b     then "" else names Sender s ++ names Receiver r)
-                 ++ (if g == tGas then "" else " Gas: "   ++ show g)
-                 ++ (if v == 0    then "" else " Value: " ++ show v)
+  return $ sOf c ++ (if not pn    then "" else names Sender s ++ names Receiver r)
+                 ++ (if g == tGas then "" else " Gas: "         ++ show g)
+                 ++ (if v == 0    then "" else " Value: "       ++ show v)
+                 ++ (if t == 0    then "" else " Time delay: "  ++ show t)
+                 ++ (if b == 0    then "" else " Block delay: " ++ show b)
 
 -- | Given a number of boxes checked and a number of total boxes, pretty-print progress in box-checking.
 progress :: Int -> Int -> String

src/test/Spec.hs

@@ -73,7 +73,7 @@ seedTests =
     , testCase "same seeds" $ assertBool "results differ" =<< same 0 0
     ]
     where cfg s = defaultConfig & sConf . quiet .~ True
-                                & cConf .~ CampaignConf 600 5 0 Nothing (Just s)
+                                & cConf .~ CampaignConf 600 20 0 Nothing (Just s)
           gen s = view tests <$> runContract "basic/flags.sol" (cfg s)
           same s t = liftM2 (==) (gen s) (gen t)
 
@@ -146,6 +146,8 @@ integrationTests = testGroup "Solidity Integration Testing"
   , testContract "basic/assert.sol"       (Just "basic/assert.yaml") 
       [ ("echidna_set0 passed",                    solved      "ASSERTION set0")
       , ("echidna_set1 failed",                    passed      "ASSERTION set1") ]
+  , testContract "basic/time.sol"         (Just "basic/time.yaml")
+      [ ("echidna_timepassed passed",              solved      "echidna_timepassed") ]
   ]
 
 testContract :: FilePath -> Maybe FilePath -> [(String, Campaign -> Bool)] -> TestTree