Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow limiting the amount of exploration we do #670

Open
msooseth opened this issue Feb 19, 2025 · 1 comment
Open

Allow limiting the amount of exploration we do #670

msooseth opened this issue Feb 19, 2025 · 1 comment

Comments

@msooseth
Copy link
Collaborator

Currently, things can get really out of hand, with a nested if-then-else creating 2^20 threads via:

      Stepper.Fork (PleaseRunBoth cond continue) -> do
        frozen <- liftIO $ stToIO $ freezeVM vm
        evalLeft <- toIO $ do
          (ra, vma) <- liftIO $ stToIO $ runStateT (continue True) frozen { result = Nothing }
          interpret fetcher maxIter askSmtIters heuristic vma (k ra)
        evalRight <- toIO $ do
          (rb, vmb) <- liftIO $ stToIO $ runStateT (continue False) frozen { result = Nothing }
          interpret fetcher maxIter askSmtIters heuristic vmb (k rb)
        (a, b) <- liftIO $ concurrently evalLeft evalRight

This can lead to actual issues not being found because the system keeps exploring more and more paths. We could try to limit the number of explored paths, with a command line option of limitExplore = Maybe Int that would be in Config. Then, if the above code has launched more than limitExplore threads, it would return a Partial with the a PartialExec, that's a new entry here, for example TooManyBranches:

data PartialExec
  = UnexpectedSymbolicArg { pc :: Int, opcode :: String, msg  :: String, args  :: [SomeExpr] }
  | MaxIterationsReached  { pc :: Int, addr :: Expr EAddr }
  | JumpIntoSymbolicCode  { pc :: Int, jumpDst :: Int }
  | CheatCodeMissing      { pc :: Int, selector :: FunctionSelector }

Then we can indicate to the user that some branches were left unexplored, due to the limit.

This would not change our default behaviour.

As requested by @ggrieco-tob

@msooseth
Copy link
Collaborator Author

msooseth commented Mar 4, 2025

PR is here #674

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant