Fuzz tx.gasprice

examples/solidity/basic/gasprice.sol

@@ -0,0 +1,12 @@
+contract C {
+  bool state = true;
+
+  function f() public {
+    if (tx.gasprice > 0)
+      state = false;
+  }
+
+  function echidna_state() public returns (bool) {
+    return state;
+  }
+}

lib/Echidna/Config.hs

@@ -8,7 +8,7 @@
 module Echidna.Config where
 
 import Control.Lens
-import Control.Monad (liftM2, liftM4)
+import Control.Monad (liftM2)
 import Control.Monad.Catch (MonadThrow)
 import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.Reader (Reader, ReaderT(..), runReader)
@@ -67,8 +67,11 @@ instance FromJSON EConfig where
                 return $ TestConf (\fname -> (== goal fname)  . maybe ResOther classifyRes . view result)
                                   (const psender)
         getWord s d = C Dull . fromIntegral <$> v .:? s .!= (d :: Integer)
-        xc = liftM4 TxConf (getWord "propMaxGas" 8000030) (getWord "testMaxGas" 0xffffffff)
-                           (getWord "maxTimeDelay" 604800)     (getWord "maxBlockDelay" 60480)
+        xc = TxConf <$> getWord "propMaxGas" 8000030
+                    <*> getWord "testMaxGas" 0xffffffff
+                    <*> getWord "maxGasprice" 100000000000
+                    <*> getWord "maxTimeDelay" 604800
+                    <*> getWord "maxBlockDelay" 60480
         cov = v .:? "coverage" <&> \case Just True -> Just mempty
                                          _         -> Nothing
         cc = CampaignConf <$> v .:? "testLimit"   .!= 50000

lib/Echidna/Solidity.hs

@@ -123,7 +123,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 (0,0)) vm
+  where loadRest = execStateT (execTx $ Tx (Right $ l ^. creationCode) d la 0xffffffff 0 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) (0, 0))
+      execStateT (execTx $ Tx (Right bc) d ca 0xffffffff 0 (w256 $ fromInteger balc) (0, 0))
 
   where choose []    _        = throwM NoContracts
         choose (c:_) Nothing  = return c

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 (0, 0)) >> gets (p f . getter)
+    Left  (f, a) -> execTx (Tx (Left (f, [])) (s a) a g 0 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

@@ -12,7 +12,7 @@ module Echidna.Transaction where
 import Prelude hiding (Word)
 
 import Control.Lens
-import Control.Monad (join, liftM2, liftM3, liftM5)
+import Control.Monad (join, liftM2, liftM3)
 import Control.Monad.Catch (MonadThrow)
 import Control.Monad.Random.Strict (MonadRandom, getRandomR)
 import Control.Monad.Reader.Class (MonadReader)
@@ -37,12 +37,13 @@ import Echidna.ABIv2
 
 -- | A transaction is either a @CREATE@ or a regular call with an origin, destination, and value.
 -- Note: I currently don't model nonces or signatures here.
-data Tx = Tx { _call  :: Either SolCall ByteString -- | Either a call or code for a @CREATE@
-             , _src   :: Addr                      -- | Origin
-             , _dst   :: Addr                      -- | Destination
-             , _gas'  :: Word                      -- | Gas
-             , _value :: Word                      -- | Value
-             , _delay :: (Word, Word)              -- | (Time, # of blocks since last call)
+data Tx = Tx { _call      :: Either SolCall ByteString -- | Either a call or code for a @CREATE@
+             , _src       :: Addr                      -- | Origin
+             , _dst       :: Addr                      -- | Destination
+             , _gas'      :: Word                      -- | Gas
+             , _gasprice' :: Word                      -- | Gas price
+             , _value     :: Word                      -- | Value
+             , _delay     :: (Word, Word)              -- | (Time, # of blocks since last call)
              } deriving (Eq, Ord, Show)
 
 makeLenses ''Tx
@@ -51,6 +52,8 @@ data TxConf = TxConf { _propGas       :: Word
                      -- ^ Gas to use evaluating echidna properties
                      , _txGas         :: Word
                      -- ^ Gas to use in generated transactions
+                     , _maxGasprice   :: Word
+                     -- ^ Maximum gasprice to be checked for a trancation
                      , _maxTimeDelay  :: Word
                      -- ^ Maximum time delay between transactions (seconds)
                      , _maxBlockDelay :: Word
@@ -64,15 +67,17 @@ ppSolCall :: SolCall -> String
 ppSolCall (t, vs) = (if t == "" then T.unpack "*fallback*" else T.unpack t) ++ "(" ++ intercalate "," (ppAbiValue <$> vs) ++ ")"
 
 instance ToJSON Tx where
-  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)
-                                        ]
+  toJSON (Tx c s d g gp 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)
+           , ("gasprice",    toJSON $ show gp)
+           , ("time delay",  toJSON $ show t)
+           , ("block delay", toJSON $ show b)
+           ]
 
 -- | If half a tuple is zero, make both halves zero. Useful for generating delays, since block number
 -- only goes up with timestamp
@@ -96,12 +101,16 @@ genTxWith :: (MonadRandom m, MonadState x m, Has World x, MonadThrow m)
           -> ([ContractA] -> m ContractA)             -- ^ Receiver generator
           -> (Addr -> ContractA -> m SolCall)         -- ^ Call generator
           -> m Word                                   -- ^ Gas generator
+          -> m Word                                   -- ^ Gas price generator
           -> (Addr -> ContractA -> SolCall -> m Word) -- ^ Value generator
           -> m (Word, Word)                           -- ^ Delay generator
           -> m Tx
-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
+genTxWith s r c g gp v t = use hasLens >>= \(World ss rs) ->
+  let s' = s ss
+      r' = r rs
+      c' = join $ liftM2 c s' r'
+  in Tx <$> (Left <$> c') <*> s' <*> (fst <$> r') <*> g <*> gp
+        <*> join (liftM3 v s' r' c') <*> t
 
 -- | Synthesize a random 'Transaction', not using a dictionary.
 genTx :: forall m x y. (MonadRandom m, MonadReader x m, Has TxConf x, MonadState y m, Has World y, MonadThrow m) => m Tx
@@ -109,33 +118,35 @@ 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 >>= \(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
+genTxM = view hasLens >>= \(TxConf _ g maxGp t b) -> genTxWith
+  (rElem "sender list") (rElem "recipient list") -- src and dst
+  (const $ genInteractionsM . snd)               -- call itself
+  (pure g) (inRange maxGp) (\_ _ _ -> pure 0)    -- gas, gasprice, value
+  (level <$> liftM2 (,) (inRange t) (inRange b)) -- 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 (0, 0))    = False
-canShrinkTx (Tx (Left (_,l)) _ _ _ 0 (0, 0)) = any canShrinkAbiValue l
-canShrinkTx _                                = True
+canShrinkTx (Tx (Right _) _ _ _ 0 0 (0, 0))    = False
+canShrinkTx (Tx (Left (_,l)) _ _ _ 0 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) (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))
+shrinkTx (Tx c s d g gp (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 Tx <$> c' <*> pure s <*> pure d <*> pure g <*> lower gp
+        <*> 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
+              (\_ _ -> mutateAbiCall =<< rElem "past calls" (lefts cs)) (pure g) (pure 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))
 
@@ -147,10 +158,21 @@ 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 (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
-  , block . timestamp += t, block . number += b, setup] where
+setupTx (Tx c s r g gp v (t, b)) = liftSH . sequence_ $
+  [ result .= Nothing
+  , state . pc .= 0
+  , state . stack .= mempty
+  , state . memory .= mempty
+  , state . gas .= g
+  , tx . gasprice .= gp
+  , 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,11 +54,12 @@ 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 pn (Tx c s r g v (t, b)) = let sOf = either ppSolCall (const "<CREATE>") in do
+ppTx pn (Tx c s r g gp v (t, b)) = let sOf = either ppSolCall (const "<CREATE>") in do
   names <- view hasLens
   tGas  <- view $ hasLens . txGas
   return $ sOf c ++ (if not pn    then "" else names Sender s ++ names Receiver r)
                  ++ (if g == tGas then "" else " Gas: "         ++ show g)
+                 ++ (if gp == 0   then "" else " Gas price: "   ++ show gp)
                  ++ (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)

src/test/Spec.hs

@@ -218,6 +218,8 @@ integrationTests = testGroup "Solidity Integration Testing"
       [ ("echidna_timepassed passed",              solved      "echidna_timepassed") ]
   , testContract "basic/construct.sol"    Nothing
       [ ("echidna_construct passed",               solved      "echidna_construct") ]
+  , testContract "basic/gasprice.sol"     Nothing
+      [ ("echidna_state passed",                   solved      "echidna_state") ]
   , testContract "abiv2/Ballot.sol"       Nothing
       [ ("echidna_test passed",                    solved      "echidna_test") ]
   , testContract "abiv2/Dynamic.sol"      Nothing