From 128be94dc8ded47f03b0e409279378c80052ba4e Mon Sep 17 00:00:00 2001 From: Gustavo Grieco <31542053+gustavo-grieco@users.noreply.github.com> Date: Fri, 9 May 2025 17:47:23 +0200 Subject: [PATCH 1/2] Increase exploration depth when exploring both side of branches with symbolic conditions --- src/EVM/SymExec.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 5e6e1d9e5..fb9454684 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -409,7 +409,7 @@ interpret fetcher iterConf vm = -- if we can statically determine unsatisfiability then we skip exploring the jump [PBool False] -> liftIO $ stToIO $ runStateT (continue (Case False)) vm -- otherwise we explore both branches - _ -> liftIO $ stToIO $ runStateT (continue UnknownBranch) vm + _ -> liftIO $ stToIO $ runStateT (continue UnknownBranch) vm {exploreDepth = vm.exploreDepth+1} interpret fetcher iterConf vm' (k r) _ -> performQuery From 276b0d41aa79aa24765ced1a405073ea0083b14a Mon Sep 17 00:00:00 2001 From: Gustavo Grieco <31542053+gustavo-grieco@users.noreply.github.com> Date: Thu, 15 May 2025 14:49:21 +0200 Subject: [PATCH 2/2] Update src/EVM/SymExec.hs Co-authored-by: Mate Soos @ Argot --- src/EVM/SymExec.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index fb9454684..f1c0a11ef 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -408,6 +408,7 @@ interpret fetcher iterConf vm = (r, vm') <- case simpProps of -- if we can statically determine unsatisfiability then we skip exploring the jump [PBool False] -> liftIO $ stToIO $ runStateT (continue (Case False)) vm + [] -> liftIO $ stToIO $ runStateT (continue (Case True)) vm -- otherwise we explore both branches _ -> liftIO $ stToIO $ runStateT (continue UnknownBranch) vm {exploreDepth = vm.exploreDepth+1} interpret fetcher iterConf vm' (k r)