diff --git a/CHANGELOG.md b/CHANGELOG.md index a7e89cbe9..728bd7cc5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -52,6 +52,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases - Better simplification of Eq IR elements - Run a toplevel constant folding reasoning system on branch conditions +- `evalProp` is renamed to `simplifyProp` for consistency - Mem explosion in `writeWord` function was possible in case `offset` was close to 2^256. Fixed. ## API Changes diff --git a/src/EVM.hs b/src/EVM.hs index e9e2a79c2..12a2c0e4f 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -1266,7 +1266,7 @@ branch cond continue = do choosePath :: CodeLocation -> BranchCondition -> EVM s () choosePath loc (Case v) = do assign #result Nothing - pushTo #constraints $ if v then Expr.evalProp (condSimp ./= Lit 0) else Expr.evalProp (condSimp .== Lit 0) + pushTo #constraints $ if v then Expr.simplifyProp (condSimp ./= Lit 0) else Expr.simplifyProp (condSimp .== Lit 0) (iteration, _) <- use (#iterations % at loc % non (0,[])) stack <- use (#state % #stack) assign (#cache % #path % at (loc, iteration)) (Just v) diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 340cc9a0b..f3176f20e 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -978,14 +978,14 @@ simplify e = if (mapExpr go e == e) simplifyProps :: [Prop] -> [Prop] simplifyProps ps = if canBeSat then simplified else [PBool False] where - simplified = remRedundantProps . map evalProp . flattenProps $ ps + simplified = remRedundantProps . map simplifyProp . flattenProps $ ps canBeSat = constFoldProp simplified -- | Evaluate the provided proposition down to its most concrete result -evalProp :: Prop -> Prop -evalProp prop = +simplifyProp :: Prop -> Prop +simplifyProp prop = let new = mapProp' go (simpInnerExpr prop) - in if (new == prop) then prop else evalProp new + in if (new == prop) then prop else simplifyProp new where go :: Prop -> Prop @@ -1305,7 +1305,7 @@ data ConstState = ConstState constFoldProp :: [Prop] -> Bool constFoldProp ps = oneRun ps (ConstState mempty True) where - oneRun ps2 startState = (execState (mapM (go . evalProp) ps2) startState).canBeSat + oneRun ps2 startState = (execState (mapM (go . simplifyProp) ps2) startState).canBeSat go :: Prop -> State ConstState () go x = case x of PEq (Lit l) a -> do diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 4203ad509..bf72308e2 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -573,7 +573,7 @@ verify solvers opts preState maybepost = do let -- Filter out any leaves that can be statically shown to be safe canViolate = flip filter flattened $ - \leaf -> case Expr.evalProp (post preState leaf) of + \leaf -> case Expr.simplifyProp (post preState leaf) of PBool True -> False _ -> True assumes = preState.constraints diff --git a/test/test.hs b/test/test.hs index c40d314c1..7dc1a888e 100644 --- a/test/test.hs +++ b/test/test.hs @@ -397,14 +397,14 @@ tests = testGroup "hevm" Just asList -> do let asBuf = Expr.fromList asList checkEquiv asBuf input - , testProperty "evalProp-equivalence-lit" $ \(LitProp p) -> ioProperty $ do + , testProperty "simplifyProp-equivalence-lit" $ \(LitProp p) -> ioProperty $ do let simplified = Expr.simplifyProps [p] case simplified of [] -> checkEquivProp (PBool True) p [val@(PBool _)] -> checkEquivProp val p _ -> assertFailure "must evaluate down to a literal bool" - , testProperty "evalProp-equivalence-sym" $ \(p) -> ioProperty $ do - let simplified = Expr.evalProp p + , testProperty "simplifyProp-equivalence-sym" $ \(p) -> ioProperty $ do + let simplified = Expr.simplifyProp p checkEquivProp simplified p , testProperty "simpProp-equivalence-sym" $ \(ps :: [Prop]) -> ioProperty $ do let simplified = pand (Expr.simplifyProps ps)