Allow limiting the amount of exploration we do

[msooseth]

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]

PR is here #674

[msooseth]

That PR now depends on the #691 PR so may take a bit of time to get merged. However, the #691 is important for future improvements and testing the CLI.

[gustavo-grieco]

I think we can close this one, the amount of exploration is needed properly limited AFAIK.

[msooseth]

Thanks, good point, closing.