`interpret` could return the pair of program counters and contracts visited

[gustavo-grieco]

The interpret function is a key part of the symbolic execution since it computes the models for reachable parts of the code, to be solved later. The returned models lack of any detail on the program counters (PC) visited, and therefore, it is very hard to know which ones are more important or more relevant to solve.

If third party applications such as Echidna, wants to integrate the symbolic execution into a fuzzing campaign, it will be really useful to have the list of explored PCs. Tools can filter which models they want to solve, for instance to find inputs that allow deeper code lines, instead of solving path conditions from states already visited.

[msooseth]

This is something that we should definitely do and it is actually not too much work. I'd rather accumulate the visited places in some datastruct related to the Expr. By the way, the original hevm had code coverage reporting somewhere, I think. The original architecture.md used to talk about it. See https://github.com/ethereum/hevm/pull/705/files

There are many different interpreters with different features, e.g. a concrete interpreter, a symbolic interpreter, an interpreter that collects coverage information, a debug interpreter that can accept user input. Interpreters can handle Queries in different ways, for example in the symbolic inerpreter, both sides of a branch point will be explored, while in the symbolic debug interpreter, user input will be requested to determine which side of the branch point will be taken.

[gustavo-grieco]

I started to play with the hevm code to create a PR for this and wanted to request some feedback on the used approach:

type VisitedSet = Set (Int, Expr EAddr)

-- | Interpreter which explores all paths at branching points. Returns an
-- 'Expr End' representing the possible executions.
interpret
  :: forall m . App m
  => Fetch.Fetcher Symbolic m RealWorld
  -> Maybe Integer -- max iterations
  -> Integer -- ask smt iterations
  -> LoopHeuristic
  -> VM Symbolic RealWorld
  -> VisitedSet
  -> Stepper Symbolic RealWorld (Expr End, VisitedSet)
  -> m (Expr End, VisitedSet)
interpret fetcher maxIter askSmtIters heuristic vm visited =
  eval . Operational.view
  where
  eval
    :: Operational.ProgramView (Stepper.Action Symbolic RealWorld) (Expr End, VisitedSet)
    -> m (Expr End, VisitedSet)
    ....
      Stepper.Fork (PleaseRunBoth cond continue) -> do
        frozen <- liftIO $ stToIO $ freezeVM vm
        let visited' = Set.insert (vm.state.pc, vm.state.contract) visited
        let newDepth = vm.exploreDepth+1
        evalLeft <- toIO $ do
          (ra, vma) <- liftIO $ stToIO $ runStateT (continue True) frozen { result = Nothing, exploreDepth = newDepth }
          interpret fetcher maxIter askSmtIters heuristic vma visited' (k ra)
        evalRight <- toIO $ do
          (rb, vmb) <- liftIO $ stToIO $ runStateT (continue False) frozen { result = Nothing, exploreDepth = newDepth }
          interpret fetcher maxIter askSmtIters heuristic vmb visited' (k rb)
        ((a, vs1), (b, vs2)) <- liftIO $ concurrently evalLeft evalRight
        pure $ (ITE cond a b, Set.union vs1 vs2)

[msooseth]

Regarding the VisitedSet. It could work, although it might complicate things eventually. Keeping it around will mean that we need to be careful in case e.g. we want to do state merging. And it we will need to be careful of deleting unreachable branches, as that means that some parts of the code will show never to have been visited (i.e. no Expr End generated). Say:

if (x == 4) {
  a = 5;
}
if (x==4 && a == 6) {
  ... blah ...
}

We will actually delete the branch that contains ..blah.. because the SMT solver will tell us during exploration that it cannot be reached. So we won't even build an Expr End for it. Here this unreachability is "obvious" but this can be quite complicated and then the user may be confused that we never ever generated an Expr End that contained "blah" to be visited -- and then later proved it cannot be reached. Because we proved it during exploration. So our on-the-fly branch checker can cause issues with what seems to be proven to be impossible to visit. This could be fixed by collecting unreachable parts of the code while the interpreter is running. But we need to be careful about it.

In general, I like the approach, but let's make sure it adds relatively little to the overall complexity and sort of "just works" without too much hassle.

---

Side-comment:

I feel like this thing needs some cleanup:

  -> Maybe Integer -- max iterations
  -> Integer -- ask smt iterations
  -> LoopHeuristic

Should be a config struct Maybe that could be cleaned up at the same time. I am vary of having too many parameters to a function -- it gets hard to follow and easy to mix up params.

[msooseth]

Sorry, re-reading it sounds like I'm being negative :) I actually really like it!

[gustavo-grieco]

This is very valuable feedback. If I understand correctly, the main point here is that the visited set will not allow to distinguish between a branch that is always unreachable and a branch that can be unreachable under a concrete state. Is this correct?

I think in your example, the lines if (x == 4) and if (x==4 && a == 6) will be marked as visited, despite unreachability of the blah code. This will signal the user that the symbolic exploration is actually reaching that part of the code, despite it is (or can be) unreachable.

[msooseth]

Let's do this and add that test case and see what will happen :) Maybe it'll be correct actually. Sorry, maybe I was just nitpicking :S