A cleaner implementation

ethereum · Sep 5, 2023 · c3ea1b4 · c3ea1b4
1 parent 02ea2e4
commit c3ea1b4
Show file tree

Hide file tree

Showing 6 changed files with 41 additions and 37 deletions.
diff --git a/cli/cli.hs b/cli/cli.hs
@@ -216,8 +216,7 @@ equivalence cmd = do
                           , maxIter = cmd.maxIterations
                           , askSmtIters = cmd.askSmtIterations
                           , loopHeuristic = cmd.loopDetectionHeuristic
-                          , abstRefineArith = cmd.abstractArithmetic
-                          , abstRefineMem = cmd.abstractMemory
+                          , abstRefineConfig = AbstRefineConfig cmd.abstractArithmetic cmd.abstractMemory
                           , rpcInfo = Nothing
                           }
   calldata <- buildCalldata cmd
@@ -297,15 +296,13 @@ assert cmd = do
   let solverCount = fromMaybe cores cmd.numSolvers
   solver <- getSolver cmd
   withSolvers solver solverCount cmd.smttimeout $ \solvers -> do
-    let opts = VeriOpts {
-      simp = True,
-      debug = cmd.smtdebug,
-      maxIter = cmd.maxIterations,
-      askSmtIters = cmd.askSmtIterations,
-      loopHeuristic = cmd.loopDetectionHeuristic,
-      abstRefineArith = cmd.abstractArithmetic,
-      abstRefineMem = cmd.abstractMemory,
-      rpcInfo = rpcinfo
+    let opts = VeriOpts { simp = True
+                        , debug = cmd.smtdebug
+                        , 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

diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
@@ -238,13 +238,13 @@ type Fetcher s = Query s -> IO (EVM s ())
 -- will be pruned anyway.
 checkBranch :: SolverGroup -> Prop -> Prop -> IO BranchCondition
 checkBranch solvers branchcondition pathconditions = do
-  checkSat solvers (assertProps False False [(branchcondition .&& pathconditions)]) >>= \case
+  checkSat solvers (assertProps abstRefineDefault [(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 False False [(pathconditions .&& (PNeg branchcondition))]) >>= \case
+      checkSat solvers (assertProps abstRefineDefault [(pathconditions .&& (PNeg branchcondition))]) >>= \case
         -- No. The condition must hold
         Unsat -> pure $ Case True
         -- Yes. Both branches possible

diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
@@ -162,21 +162,21 @@ data AbstState = AbstState
   }
   deriving (Show)
 
-abstractAwayProps :: Bool -> Bool -> [Prop] -> ([Prop], AbstState)
-abstractAwayProps abstRefineArith abstRefineMem ps = runState (mapM abstrAway ps) (AbstState mempty 0)
+abstractAwayProps :: AbstRefineConfig -> [Prop] -> ([Prop], AbstState)
+abstractAwayProps abstRefineConfig 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{})       | abstRefineArith  -> abstrExpr e
-        e@(SMod{})      | abstRefineArith  -> abstrExpr e
-        e@(MulMod{})    | abstRefineArith  -> abstrExpr e
-        e@(AddMod{})    | abstRefineArith  -> abstrExpr e
-        e@(Mul{})       | abstRefineArith  -> abstrExpr e
-        e@(Div{})       | abstRefineArith  -> abstrExpr e
-        e@(SDiv {})     | abstRefineArith  -> abstrExpr e
-        e@(ReadWord {}) | abstRefineMem -> abstrExpr e
+        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 -> pure e
         where
             abstrExpr e = do
@@ -193,8 +193,8 @@ abstractAwayProps abstRefineArith abstRefineMem ps = runState (mapM abstrAway ps
 smt2Line :: Builder -> SMT2
 smt2Line txt = SMT2 [txt] mempty mempty
 
-assertProps :: Bool -> Bool -> [Prop] -> SMT2
-assertProps abstRefineArith abstRefineMem ps =
+assertProps :: AbstRefineConfig -> [Prop] -> SMT2
+assertProps abstRefineConfig ps =
   let encs = map propToSMT psElimAbst
       abstSMT = map propToSMT abstProps
       intermediates = declareIntermediates bufs stores in
@@ -222,8 +222,8 @@ assertProps abstRefineArith abstRefineMem ps =
 
   where
     (psElim, bufs, stores) = eliminateProps ps
-    (psElimAbst, abst@(AbstState abstExprToInt _)) = if abstRefineArith || abstRefineMem
-      then abstractAwayProps abstRefineArith abstRefineMem psElim
+    (psElimAbst, abst@(AbstState abstExprToInt _)) = if abstRefineConfig.arith || abstRefineConfig.mem
+      then abstractAwayProps abstRefineConfig psElim
       else (psElim, AbstState mempty 0)
 
     abstProps = map toProp (Map.toList abstExprToInt)

diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
@@ -77,8 +77,7 @@ data VeriOpts = VeriOpts
   , maxIter :: Maybe Integer
   , askSmtIters :: Integer
   , loopHeuristic :: LoopHeuristic
-  , abstRefineArith :: Bool
-  , abstRefineMem :: Bool
+  , abstRefineConfig :: AbstRefineConfig
   , rpcInfo :: Fetch.RpcInfo
   }
   deriving (Eq, Show)
@@ -90,8 +89,7 @@ defaultVeriOpts = VeriOpts
   , maxIter = Nothing
   , askSmtIters = 1
   , loopHeuristic = StackBased
-  , abstRefineArith = False
-  , abstRefineMem = False
+  , abstRefineConfig = abstRefineDefault
   , rpcInfo = Nothing
   }
 
@@ -102,7 +100,7 @@ debugVeriOpts :: VeriOpts
 debugVeriOpts = defaultVeriOpts { debug = True }
 
 debugAbstVeriOpts :: VeriOpts
-debugAbstVeriOpts = defaultVeriOpts { abstRefineMem = True, abstRefineArith = True }
+debugAbstVeriOpts = defaultVeriOpts { abstRefineConfig = AbstRefineConfig True True }
 
 extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
 extractCex (Cex c) = Just c
@@ -496,7 +494,7 @@ reachable solvers e = do
               (Nothing, Nothing) -> Nothing
         pure (fst tres <> fst fres, subexpr)
       leaf -> do
-        let query = assertProps False False pcs
+        let query = assertProps abstRefineDefault pcs
         res <- checkSat solvers query
         case res of
           Sat _ -> pure ([query], Just leaf)
@@ -562,7 +560,7 @@ verify solvers opts preState maybepost = do
             _ -> True
         assumes = preState.constraints
         withQueries = canViolate <&> \leaf ->
-          (assertProps opts.abstRefineArith opts.abstRefineMem (PNeg (post preState leaf) : assumes <> extractProps leaf), leaf)
+          (assertProps opts.abstRefineConfig (PNeg (post preState leaf) : assumes <> extractProps leaf), leaf)
       putStrLn $ "Checking for reachability of "
                    <> show (length withQueries)
                    <> " potential property violation(s)"
@@ -674,7 +672,7 @@ equivalenceCheck' solvers branchesA branchesB opts = do
     -- used or not
     check :: UnsatCache -> (Set Prop) -> Int -> IO (EquivResult, Bool)
     check knownUnsat props idx = do
-      let smt = assertProps opts.abstRefineArith opts.abstRefineMem (Set.toList props)
+      let smt = assertProps opts.abstRefineConfig (Set.toList props)
       -- if debug is on, write the query to a file
       let filename = "equiv-query-" <> show idx <> ".smt2"
       when opts.debug $ TL.writeFile filename (formatSMT2 smt <> "\n\n(check-sat)")
@@ -773,7 +771,7 @@ both' f (x, y) = (f x, f y)
 produceModels :: SolverGroup -> Expr End -> IO [(Expr End, CheckSatResult)]
 produceModels solvers expr = do
   let flattened = flattenExpr expr
-      withQueries = fmap (\e -> ((assertProps False False) . extractProps $ e, e)) flattened
+      withQueries = fmap (\e -> ((assertProps abstRefineDefault) . extractProps $ e, e)) flattened
   results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
     res <- checkSat solvers query
     pure (res, leaf)

diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
@@ -620,6 +620,15 @@ 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

diff --git a/test/test.hs b/test/test.hs
@@ -2727,7 +2727,7 @@ checkEquivBase mkprop l r = withSolvers Z3 1 (Just 1) $ \solvers -> do
        putStrLn "skip"
        pure True
      else do
-       let smt = assertProps False False [mkprop l r]
+       let smt = assertProps abstRefineDefault [mkprop l r]
        res <- checkSat solvers smt
        print res
        pure $ case res of