Skip to content

Commit

Permalink
Update src/Act/Decompile.hs
Browse files Browse the repository at this point in the history
Co-authored-by: dxo  <[email protected]>
  • Loading branch information
zoep and d-xo authored Jul 30, 2024
1 parent 9b2b7a8 commit 95f3a90
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/Act/Decompile.hs
Original file line number Diff line number Diff line change
Expand Up @@ -149,6 +149,8 @@ summarize solvers contract = do
makeIntSafe :: forall m a. App m => SolverGroup -> EVM.Expr a -> m (EVM.Expr a)
makeIntSafe solvers expr = evalStateT (mapExprM go expr) mempty
where
-- Walks the expression bottom up and checks (using an smt solver) if overflow is possible for any
-- arithmetic operations it encounters. Results from child nodes are stored and reused as we move up the tree
go :: forall b. EVM.Expr b -> StateT (Map (EVM.Expr EVM.EWord) EVM.Prop) m (EVM.Expr b)
go = \case
e@(EVM.Add a b) -> binop (EVM.Add a b .>= a) a b e
Expand Down

0 comments on commit 95f3a90

Please sign in to comment.