Upgrading fuzz system

hevm.cabal

@@ -181,8 +181,7 @@ library
     spawn                             >= 0.3 && < 0.4,
     filepattern                       >= 0.1.2 && < 0.2,
     witch                             >= 1.1 && < 1.3,
-    unliftio-core                     >= 0.2.1.0,
-    MonadRandom                       >= 0.5.1,
+    unliftio-core                     >= 0.2.1.0
   if !os(windows)
     build-depends:
       brick                           >= 1.4 && < 2.0,

src/EVM/Effects.hs

@@ -55,6 +55,10 @@ data Config = Config
   , abstRefineMem   :: Bool
   , dumpTrace       :: Bool
   , numCexFuzz      :: Integer
+   -- Used to debug fuzzer in test.hs. It disables the SMT solver
+   -- and uses the fuzzer ONLY to try to find a counterexample.
+   -- Returns Unknown if the Cex cannot be found via fuzzing
+  , onlyCexFuzz     :: Bool
   }
   deriving (Show, Eq)
 
@@ -67,7 +71,8 @@ defaultConfig = Config
   , abstRefineArith = False
   , abstRefineMem   = False
   , dumpTrace = False
-  , numCexFuzz = 100
+  , numCexFuzz = 10
+  , onlyCexFuzz  = False
   }
 
 -- Write to the console

src/EVM/Expr.hs

@@ -836,6 +836,8 @@ simplify e = if (mapExpr go e == e)
     go (EVM.Types.GEq a b) = leq b a
     go (EVM.Types.LEq a b) = EVM.Types.IsZero (gt a b)
     go (IsZero a) = iszero a
+    go (SLT a@(Lit _) b@(Lit _)) = slt a b
+    go (SGT a b) = SLT b a
 
     -- syntactic Eq reduction
     go (Eq (Lit a) (Lit b))

src/EVM/Fuzz.hs

@@ -26,8 +26,9 @@ import Test.QuickCheck.Random (mkQCGen)
 
 -- TODO: Extract Var X = Lit Z, and set it
 tryCexFuzz :: [Prop] -> Integer -> (Maybe (SMT.SMTCex))
-tryCexFuzz ps tries = unGen (testVals tries) (mkQCGen 0) 1337
+tryCexFuzz prePs tries = unGen (testVals tries) (mkQCGen 0) 1337
   where
+    ps = Expr.simplifyProps $ Expr.concKeccakProps prePs
     vars = extractVars ps
     bufs = extractBufs ps
     stores = extractStorage ps
@@ -38,8 +39,8 @@ tryCexFuzz ps tries = unGen (testVals tries) (mkQCGen 0) 1337
       bufVals <- getBufs bufs
       storeVals <- getStores stores
       let
-        ret =  filterCorrectKeccak $ map (substituteEWord varvals . substituteBuf bufVals . substituteStores storeVals) ps
-        retSimp =  Expr.simplifyProps ret
+        ret = filterCorrectKeccak $ map (substituteEWord varvals . substituteBuf bufVals . substituteStores storeVals) ps
+        retSimp = Expr.simplifyProps $ Expr.concKeccakProps ret
       if null retSimp then pure $ Just (SMT.SMTCex {
                                     vars = varvals
                                     , addrs = mempty
@@ -103,7 +104,7 @@ findVarProp p = mapPropM go p
     go = \case
       e@(Var a) -> do
         s <- get
-        put $ s {vars = Set.insert (Var a) s.vars}
+        put s {vars = Set.insert (Var a) s.vars}
         pure e
       e@(Lit a) -> do
         s <- get
@@ -135,7 +136,7 @@ findBufProp p = mapPropM go p
     go = \case
       e@(AbstractBuf a) -> do
         s <- get
-        put $ s{bufs=Set.insert (AbstractBuf a) s.bufs}
+        put s {bufs=Set.insert (AbstractBuf a) s.bufs}
         pure e
       e -> pure e
 
@@ -146,14 +147,37 @@ data CollectStorage = CollectStorage { addrs :: Set.Set (Expr EAddr)
                                      }
   deriving (Show)
 
+instance Semigroup (CollectStorage) where
+  (CollectStorage a b c) <> (CollectStorage a2 b2 c2) = CollectStorage (a <> a2) (b <> b2) (c <> c2)
+
 initStorageState :: CollectStorage
 initStorageState = CollectStorage { addrs = Set.empty, keys = Set.empty, vals = Set.fromList [0x0, 0x1, Expr.maxLit] }
 
 extractStorage :: [Prop] -> CollectStorage
-extractStorage ps = execState (mapM_ findStorageProp ps) initStorageState
+extractStorage ps = execState (mapM_ findStoragePropInner ps) initStorageState <>
+    execState (mapM_ findStoragePropComp ps) initStorageState
+
+findStoragePropComp :: Prop -> State CollectStorage Prop
+findStoragePropComp p = go2 p
+  where
+    go2 :: Prop -> State CollectStorage (Prop)
+    go2 = \case
+      PNeg x -> go2 x
+      e@(PEq (Lit val) (SLoad {})) -> do
+        s <- get
+        put (s {vals=Set.insert val s.vals} :: CollectStorage)
+        pure e
+      e@(PLT (Lit val) (SLoad {})) -> do
+        s <- get
+        put (s {vals=Set.insert val s.vals} :: CollectStorage)
+        pure e
+      (PGT a@(Lit _) b@(SLoad {})) -> go2 (PLT a b)
+      (PGEq a@(Lit _) b@(SLoad {})) -> go2 (PLT a b)
+      (PLEq a@(Lit _) b@(SLoad {})) -> go2 (PLT a b)
+      e -> pure e
 
-findStorageProp :: Prop -> State CollectStorage Prop
-findStorageProp p = mapPropM go p
+findStoragePropInner :: Prop -> State CollectStorage Prop
+findStoragePropInner p = mapPropM go p
   where
     go :: forall a. Expr a -> State CollectStorage (Expr a)
     go = \case
@@ -163,7 +187,7 @@ findStorageProp p = mapPropM go p
         pure e
       e@(SLoad (Lit val) _) -> do
         s <- get
-        put $ s{keys=Set.insert val s.keys}
+        put s {keys=Set.insert val s.keys}
         pure e
       e@(SStore _ (Lit val) _) -> do
         s <- get

src/EVM/Solvers.hs

@@ -134,7 +134,7 @@ withSolvers solver count timeout cont = do
           then do
             when (conf.debug) $ putStrLn $ "Cex found via fuzzing:" <> (show fuzzResult)
             writeChan r (Sat $ fromJust fuzzResult)
-          else do
+          else if not conf.onlyCexFuzz then do
             when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex"
             -- reset solver and send all lines of provided script
             out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty ps)
@@ -163,6 +163,9 @@ withSolvers solver count timeout cont = do
                                       _ -> pure . Error $ T.toStrict $ "Unable to parse solver output: " <> sat2
                       _ -> pure . Error $ T.toStrict $ "Unable to parse solver output: " <> sat
                 writeChan r res
+          else do
+            when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex, not trying SMT due to onlyCexFuzz"
+            writeChan r Unknown
 
         -- put the instance back in the list of available instances
         writeChan availableInstances inst

test/test.hs

@@ -95,6 +95,9 @@ assertBoolM a b = liftIO $ assertBool a b
 test :: TestName -> ReaderT Env IO () -> TestTree
 test a b = testCase a $ runEnv testEnv b
 
+testFuzz :: TestName -> ReaderT Env IO () -> TestTree
+testFuzz a b = testCase a $ runEnv (testEnv {config = testEnv.config {numCexFuzz = 100, onlyCexFuzz = True}}) b
+
 prop :: Testable prop => ReaderT Env IO prop -> Property
 prop a = ioProperty $ runEnv testEnv a
 
@@ -2729,7 +2732,7 @@ tests = testGroup "hevm"
           putStrLnM "Expected counterexample found"
   ]
   , testGroup "concr-fuzz"
-    [ test "fuzz-complicated-mul" $ do
+    [ testFuzz "fuzz-complicated-mul" $ do
       Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -2756,7 +2759,7 @@ tests = testGroup "hevm"
       assertBoolM "Must fail" (not val)
       putStrLnM  $ "expected counterexample found, x:  " <> (show x) <> " y: " <> (show y) <> " z: " <> (show z)
       putStrLnM  $ "cex a: " <> (show a) <> " b: " <> (show b)
-    , test "fuzz-stores" $ do
+    , testFuzz "fuzz-stores" $ do
       Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -2769,7 +2772,7 @@ tests = testGroup "hevm"
       let sig = (Sig "func()" [])
       (_, [Cex (_, ctr)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
       putStrLnM  $ "expected counterexample found.  ctr: " <> (show ctr)
-    , test "fuzz-simple-fixed-value" $ do
+    , testFuzz "fuzz-simple-fixed-value" $ do
       Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -2782,7 +2785,7 @@ tests = testGroup "hevm"
       let sig = (Sig "func(uint256)" [AbiUIntType 256])
       (_, [Cex (_, ctr)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
       putStrLnM  $ "expected counterexample found.  ctr: " <> (show ctr)
-    , test "fuzz-simple-fixed-value2" $ do
+    , testFuzz "fuzz-simple-fixed-value2" $ do
       Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -2794,7 +2797,7 @@ tests = testGroup "hevm"
       let sig = (Sig "func(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
       (_, [Cex (_, ctr)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
       putStrLnM  $ "expected counterexample found.  ctr: " <> (show ctr)
-    , test "fuzz-simple-fixed-value3" $ do
+    , testFuzz "fuzz-simple-fixed-value3" $ do
       Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -2806,6 +2809,34 @@ tests = testGroup "hevm"
       let sig = (Sig "func(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
       (_, [Cex (_, ctr1), Cex (_, ctr2)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
       putStrLnM  $ "expected counterexamples found.  ctr1: " <> (show ctr1) <> " ctr2: " <> (show ctr2)
+    , testFuzz "fuzz-simple-fixed-value-store1" $ do
+      Just c <- solcRuntime "MyContract"
+        [i|
+        contract MyContract {
+          mapping(uint => uint) items;
+          function func(uint a) public {
+            uint f = items[2];
+            assert(a != f);
+          }
+        }
+        |]
+      let sig = (Sig "func(uint256)" [AbiUIntType 256, AbiUIntType 256])
+      (_, [Cex _]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+      putStrLnM  $ "expected counterexamples found"
+    , testFuzz "fuzz-simple-fixed-value-store2" $ do
+      Just c <- solcRuntime "MyContract"
+        [i|
+        contract MyContract {
+          mapping(uint => uint) items;
+          function func(uint a) public {
+            items[0] = 1337;
+            assert(a != items[0]);
+          }
+        }
+        |]
+      let sig = (Sig "func(uint256)" [AbiUIntType 256, AbiUIntType 256])
+      (_, [Cex (_, ctr1)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+      putStrLnM  $ "expected counterexamples found: " <> show ctr1
   ]
   , testGroup "simplification-working"
   [