Also add abstraction-refinement

cli/cli.hs

@@ -191,7 +191,10 @@ mainEnv = Env { config = defaultConfig }
 main :: IO ()
 main = do
   cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"
-  let env = Env { config = defaultConfig { dumpQueries = cmd.smtdebug} }
+  let env = Env { config = defaultConfig {
+    dumpQueries = cmd.smtdebug
+    , abstRefineMem = cmd.abstractMemory
+    , abstRefineArith = cmd.abstractArithmetic} }
   case cmd of
     Version {} ->putStrLn getFullVersion
     Symbolic {} -> do
@@ -226,7 +229,6 @@ equivalence cmd = do
                           , maxIter = cmd.maxIterations
                           , askSmtIters = cmd.askSmtIterations
                           , loopHeuristic = cmd.loopDetectionHeuristic
-                          , abstRefineConfig = AbstRefineConfig cmd.abstractArithmetic cmd.abstractMemory
                           , rpcInfo = Nothing
                           }
   calldata <- liftIO $ buildCalldata cmd
@@ -312,13 +314,12 @@ assert cmd = do
                         , maxIter = cmd.maxIterations
                         , askSmtIters = cmd.askSmtIterations
                         , loopHeuristic = cmd.loopDetectionHeuristic
-                        , abstRefineConfig = AbstRefineConfig cmd.abstractArithmetic cmd.abstractMemory
                         , rpcInfo = rpcinfo
     }
     (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes)
     case res of
-      [Qed _] -> liftIO $ do
-        putStrLn "\nQED: No reachable property violations discovered\n"
+      [Qed _] -> do
+        liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"
         showExtras solvers cmd calldata expr
       _ -> do
         let cexs = snd <$> mapMaybe getCex res
@@ -337,26 +338,28 @@ assert cmd = do
                  , "Could not determine reachability of the following end states:"
                  , ""
                  ] <> fmap (formatExpr) timeouts
-        liftIO $ do
-          T.putStrLn $ T.unlines (counterexamples <> unknowns)
-          showExtras solvers cmd calldata expr
-          exitFailure
+        liftIO $ T.putStrLn $ T.unlines (counterexamples <> unknowns)
+        showExtras solvers cmd calldata expr
+        liftIO $ exitFailure
 
-showExtras :: SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> IO ()
+showExtras
+  :: (MonadUnliftIO m, ReadConfig m)
+  => SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> m ()
 showExtras solvers cmd calldata expr = do
-  when cmd.showTree $ do
+  when cmd.showTree $ liftIO $ do
     putStrLn "=== Expression ===\n"
     T.putStrLn $ formatExpr expr
     putStrLn ""
   when cmd.showReachableTree $ do
     reached <- reachable solvers expr
-    putStrLn "=== Reachable Expression ===\n"
-    T.putStrLn (formatExpr . snd $ reached)
-    putStrLn ""
+    liftIO $ do
+      putStrLn "=== Reachable Expression ===\n"
+      T.putStrLn (formatExpr . snd $ reached)
+      putStrLn ""
   when cmd.getModels $ do
-    putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ===\n"
+    liftIO $ putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ===\n"
     ms <- produceModels solvers expr
-    forM_ ms (showModel (fst calldata))
+    liftIO $ forM_ ms (showModel (fst calldata))
 
 isTestOrLib :: Text -> Bool
 isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "src/tests/", "lib/"] file

src/EVM/Effects.hs

@@ -20,14 +20,19 @@ data Config = Config
   , dumpExprs :: Bool
   , dumpEndStates :: Bool
   , verbose :: Bool
+  , abstRefineArith :: Bool
+  , abstRefineMem   :: Bool
   }
+  deriving (Show, Eq)
 
 defaultConfig :: Config
 defaultConfig = Config {
   dumpQueries = False
   , dumpExprs = False
   , dumpEndStates = False
   , verbose = False
+  , abstRefineArith = False
+  , abstRefineMem   = False
   }
 
 

src/EVM/Fetch.hs

@@ -240,14 +240,15 @@ type Fetcher m s = (ReadConfig m, MonadUnliftIO m) => Query s -> m (EVM s ())
 -- but for normal execution paths with inconsistent pathconditions
 -- will be pruned anyway.
 checkBranch :: (MonadUnliftIO m, ReadConfig m) => SolverGroup -> Prop -> Prop -> m BranchCondition
-checkBranch solvers branchcondition pathconditions = liftIO $ do
-  checkSat solvers (assertProps abstRefineDefault [(branchcondition .&& pathconditions)]) >>= \case
+checkBranch solvers branchcondition pathconditions = do
+  conf <- readConfig
+  liftIO $ checkSat solvers (assertProps conf [(branchcondition .&& pathconditions)]) >>= \case
     -- the condition is unsatisfiable
     Unsat -> -- if pathconditions are consistent then the condition must be false
       pure $ Case False
     -- Sat means its possible for condition to hold
-    Sat _ -> -- is its negation also possible?
-      checkSat solvers (assertProps abstRefineDefault [(pathconditions .&& (PNeg branchcondition))]) >>= \case
+    Sat _ -> do -- is its negation also possible?
+      checkSat solvers (assertProps conf [(pathconditions .&& (PNeg branchcondition))]) >>= \case
         -- No. The condition must hold
         Unsat -> pure $ Case True
         -- Yes. Both branches possible

src/EVM/SMT.hs

@@ -31,7 +31,7 @@ import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg)
 import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..))
 import Numeric (readHex, readBin)
 import Witch (into, unsafeInto)
-import Control.Monad.State
+import Control.Monad.State (State, runState, get, put)
 import EVM.Format (formatProp)
 
 import EVM.CSE
@@ -40,6 +40,7 @@ import EVM.Expr qualified as Expr
 import EVM.Keccak (keccakAssumptions, keccakCompute)
 import EVM.Traversals
 import EVM.Types
+import EVM.Effects
 
 
 -- ** Encoding ** ----------------------------------------------------------------------------------
@@ -171,21 +172,21 @@ data AbstState = AbstState
   }
   deriving (Show)
 
-abstractAwayProps :: AbstRefineConfig -> [Prop] -> ([Prop], AbstState)
-abstractAwayProps abstRefineConfig ps = runState (mapM abstrAway ps) (AbstState mempty 0)
+abstractAwayProps :: Config -> [Prop] -> ([Prop], AbstState)
+abstractAwayProps conf ps = runState (mapM abstrAway ps) (AbstState mempty 0)
   where
     abstrAway :: Prop -> State AbstState Prop
     abstrAway prop = mapPropM go prop
     go :: Expr a -> State AbstState (Expr a)
     go x = case x of
-        e@(Mod{})       | abstRefineConfig.arith  -> abstrExpr e
-        e@(SMod{})      | abstRefineConfig.arith  -> abstrExpr e
-        e@(MulMod{})    | abstRefineConfig.arith  -> abstrExpr e
-        e@(AddMod{})    | abstRefineConfig.arith  -> abstrExpr e
-        e@(Mul{})       | abstRefineConfig.arith  -> abstrExpr e
-        e@(Div{})       | abstRefineConfig.arith  -> abstrExpr e
-        e@(SDiv {})     | abstRefineConfig.arith  -> abstrExpr e
-        e@(ReadWord {}) | abstRefineConfig.mem -> abstrExpr e
+        e@(Mod{})       | conf.abstRefineArith  -> abstrExpr e
+        e@(SMod{})      | conf.abstRefineArith  -> abstrExpr e
+        e@(MulMod{})    | conf.abstRefineArith  -> abstrExpr e
+        e@(AddMod{})    | conf.abstRefineArith  -> abstrExpr e
+        e@(Mul{})       | conf.abstRefineArith  -> abstrExpr e
+        e@(Div{})       | conf.abstRefineArith  -> abstrExpr e
+        e@(SDiv {})     | conf.abstRefineArith  -> abstrExpr e
+        e@(ReadWord {}) | conf.abstRefineMem -> abstrExpr e
         e -> pure e
         where
             abstrExpr e = do
@@ -203,13 +204,15 @@ smt2Line :: Builder -> SMT2
 smt2Line txt = SMT2 [txt] mempty mempty mempty
 
 assertProps :: AbstRefineConfig -> [Prop] -> SMT2
+assertProps :: Config -> [Prop] -> SMT2
+-- first simplify to rewrite sload/sstore combos, then concretize&simplify
 assertProps conf ps = assertPropsNoSimp conf (Expr.simplifyProps ps)
 
 -- Note: we need a version that does NOT call simplify or simplifyProps,
 -- because we make use of it to verify the correctness of our simplification
 -- passes through property-based testing.
-assertPropsNoSimp :: AbstRefineConfig -> [Prop] -> SMT2
-assertPropsNoSimp abstRefineConfig ps =
+assertPropsNoSimp :: Config -> [Prop] -> SMT2
+assertPropsNoSimp config psPreConc =
   let encs = map propToSMT psElimAbst
       abstSMT = map propToSMT abstProps
       intermediates = declareIntermediates bufs stores in
@@ -238,8 +241,8 @@ assertPropsNoSimp abstRefineConfig ps =
 
   where
     (psElim, bufs, stores) = eliminateProps ps
-    (psElimAbst, abst@(AbstState abstExprToInt _)) = if abstRefineConfig.arith || abstRefineConfig.mem
-      then abstractAwayProps abstRefineConfig psElim
+    (psElimAbst, abst@(AbstState abstExprToInt _)) = if config.abstRefineArith || config.abstRefineMem
+      then abstractAwayProps config psElim
       else (psElim, AbstState mempty 0)
 
     abstProps = map toProp (Map.toList abstExprToInt)

src/EVM/SymExec.hs

@@ -77,7 +77,6 @@ data VeriOpts = VeriOpts
   , maxIter :: Maybe Integer
   , askSmtIters :: Integer
   , loopHeuristic :: LoopHeuristic
-  , abstRefineConfig :: AbstRefineConfig
   , rpcInfo :: Fetch.RpcInfo
   }
   deriving (Eq, Show)
@@ -88,16 +87,12 @@ defaultVeriOpts = VeriOpts
   , maxIter = Nothing
   , askSmtIters = 1
   , loopHeuristic = StackBased
-  , abstRefineConfig = abstRefineDefault
   , rpcInfo = Nothing
   }
 
 rpcVeriOpts :: (Fetch.BlockNumber, Text) -> VeriOpts
 rpcVeriOpts info = defaultVeriOpts { rpcInfo = Just info }
 
-debugAbstVeriOpts :: VeriOpts
-debugAbstVeriOpts = defaultVeriOpts { abstRefineConfig = AbstRefineConfig True True }
-
 extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
 extractCex (Cex c) = Just c
 extractCex _ = Nothing
@@ -486,9 +481,12 @@ flattenExpr = go []
 -- the incremental nature of the task at hand. Introducing support for
 -- incremental queries might let us go even faster here.
 -- TODO: handle errors properly
-reachable :: SolverGroup -> Expr End -> IO ([SMT2], Expr End)
+reachable
+  :: (MonadUnliftIO m, ReadConfig m)
+  => SolverGroup -> Expr End -> m ([SMT2], Expr End)
 reachable solvers e = do
-  res <- go [] e
+  conf <- readConfig
+  res <- liftIO $ go conf [] e
   pure $ second (fromMaybe (internalError "no reachable paths found")) res
   where
     {-
@@ -497,20 +495,20 @@ reachable solvers e = do
        If reachable return the expr wrapped in a Just. If not return Nothing.
        When walking back up the tree drop unreachable subbranches.
     -}
-    go :: [Prop] -> Expr End -> IO ([SMT2], Maybe (Expr End))
-    go pcs = \case
+    go :: Config -> [Prop] -> Expr End -> IO ([SMT2], Maybe (Expr End))
+    go conf pcs = \case
       ITE c t f -> do
         (tres, fres) <- concurrently
-          (go (PEq (Lit 1) c : pcs) t)
-          (go (PEq (Lit 0) c : pcs) f)
+          (go conf (PEq (Lit 1) c : pcs) t)
+          (go conf (PEq (Lit 0) c : pcs) f)
         let subexpr = case (snd tres, snd fres) of
               (Just t', Just f') -> Just $ ITE c t' f'
               (Just t', Nothing) -> Just t'
               (Nothing, Just f') -> Just f'
               (Nothing, Nothing) -> Nothing
         pure (fst tres <> fst fres, subexpr)
       leaf -> do
-        let query = assertProps abstRefineDefault pcs
+        let query = assertProps conf pcs
         res <- checkSat solvers query
         case res of
           Sat _ -> pure ([query], Just leaf)
@@ -578,7 +576,7 @@ verify solvers opts preState maybepost = do
               _ -> True
           assumes = preState.constraints
           withQueries = canViolate <&> \leaf ->
-            (assertProps opts.abstRefineConfig (PNeg (post preState leaf) : assumes <> extractProps leaf), leaf)
+            (assertProps conf (PNeg (post preState leaf) : assumes <> extractProps leaf), leaf)
         putStrLn $ "Checking for reachability of "
                      <> show (length withQueries)
                      <> " potential property violation(s)"
@@ -633,7 +631,7 @@ equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do
     False -> do
       branchesA <- getBranches bytecodeA
       branchesB <- getBranches bytecodeB
-      equivalenceCheck' solvers branchesA branchesB opts
+      equivalenceCheck' solvers branchesA branchesB
   where
     -- decompiles the given bytecode into a list of branches
     getBranches :: ByteString -> m [Expr End]
@@ -647,8 +645,8 @@ equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do
 
 equivalenceCheck'
   :: forall m . (MonadUnliftIO m, ReadConfig m)
-  => SolverGroup -> [Expr End] -> [Expr End] -> VeriOpts -> m [EquivResult]
-equivalenceCheck' solvers branchesA branchesB opts = do
+  => SolverGroup -> [Expr End] -> [Expr End] -> m [EquivResult]
+equivalenceCheck' solvers branchesA branchesB = do
       when (any isPartial branchesA || any isPartial branchesB) $ liftIO $ do
         putStrLn ""
         putStrLn "WARNING: hevm was only able to partially explore the given contract due to the following issues:"
@@ -669,8 +667,8 @@ equivalenceCheck' solvers branchesA branchesB opts = do
         liftIO $ T.writeFile ("prop-checked-" <> show i <> ".prop") (T.pack $ show x))
 
       knownUnsat <- liftIO $ newTVarIO []
-      procs <- liftIO $ getNumProcessors
-      results <- liftIO $ checkAll differingEndStates knownUnsat procs
+      procs <- liftIO getNumProcessors
+      results <- checkAll differingEndStates knownUnsat procs
 
       let useful = foldr (\(_, b) n -> if b then n+1 else n) (0::Integer) results
       liftIO $ putStrLn $ "Reuse of previous queries was Useful in " <> (show useful) <> " cases"
@@ -691,9 +689,9 @@ equivalenceCheck' solvers branchesA branchesB opts = do
     -- the solver if we can determine unsatisfiability from the cache already
     -- the last element of the returned tuple indicates whether the cache was
     -- used or not
-    check :: UnsatCache -> (Set Prop) -> IO (EquivResult, Bool)
-    check knownUnsat props = do
-      let smt = assertProps opts.abstRefineConfig (Set.toList props)
+    check :: Config -> UnsatCache -> (Set Prop) -> IO (EquivResult, Bool)
+    check conf knownUnsat props = do
+      let smt = assertProps conf (Set.toList props)
       ku <- readTVarIO knownUnsat
       res <- if subsetAny props ku
              then pure (True, Unsat)
@@ -715,10 +713,13 @@ equivalenceCheck' solvers branchesA branchesB opts = do
     -- from left-to-right, and with a max of K threads. This is in contrast to
     -- mapConcurrently which would spawn as many threads as there are jobs, and
     -- run them in a random order. We ordered them correctly, though so that'd be bad
-    checkAll :: [(Set Prop)] -> UnsatCache -> Int -> IO [(EquivResult, Bool)]
+    checkAll
+      :: (MonadUnliftIO m, ReadConfig m)
+      => [(Set Prop)] -> UnsatCache -> Int -> m [(EquivResult, Bool)]
     checkAll input cache numproc = do
-       wrap <- pool numproc
-       parMapIO (wrap . (check cache)) input
+       conf <- readConfig
+       wrap <- liftIO $ pool numproc
+       liftIO $ parMapIO (wrap . (check conf cache)) input
 
 
     -- Takes two branches and returns a set of props that will need to be
@@ -785,11 +786,14 @@ equivalenceCheck' solvers branchesA branchesB opts = do
 both' :: (a -> b) -> (a, a) -> (b, b)
 both' f (x, y) = (f x, f y)
 
-produceModels :: SolverGroup -> Expr End -> IO [(Expr End, CheckSatResult)]
+produceModels
+  :: (MonadUnliftIO m, ReadConfig m)
+  => SolverGroup -> Expr End -> m [(Expr End, CheckSatResult)]
 produceModels solvers expr = do
   let flattened = flattenExpr expr
-      withQueries = fmap (\e -> ((assertProps abstRefineDefault) . extractProps $ e, e)) flattened
-  results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
+      withQueries conf = fmap (\e -> ((assertProps conf) . extractProps $ e, e)) flattened
+  conf <- readConfig
+  results <- liftIO $ (flip mapConcurrently) (withQueries conf) $ \(query, leaf) -> do
     res <- checkSat solvers query
     pure (res, leaf)
   pure $ fmap swap $ filter (\(res, _) -> not . isUnsat $ res) results

src/EVM/Types.hs

@@ -621,15 +621,6 @@ data RuntimeConfig = RuntimeConfig
   }
   deriving (Show)
 
-abstRefineDefault :: AbstRefineConfig
-abstRefineDefault = AbstRefineConfig False False
-
-data AbstRefineConfig = AbstRefineConfig
-  { arith :: Bool
-  , mem   :: Bool
-  }
-  deriving (Show, Eq)
-
 -- | An entry in the VM's "call/create stack"
 data Frame s = Frame
   { context :: FrameContext