Add support for interactive debugging of verifier traces

[danmatichuk]

Motivation

Log files from the verifier are becoming extremely verbose and hard to navigate. We want to flip the interaction model with the tool to instead be able to query for additional detail about individual verification steps, rather than attempting to configure the tool up-front to produce the desired level of logging detail.

Requirements

To view the behavior of the verifier from different levels of detail, with the ability to select various verification steps and "drill down" to get more information about the individual steps taken.

The basic interface will simply be selecting an option to drill down into from a list of possible options. For example, a list of graph nodes will be presented, and selecting one will then present the list of block exits that were found from that node, etc.

The interface needs to be extensible so that more in-depth analysis can be done as necessary. For example, we may wish to take some intermediate term and view the result after applying some additional simplification step.

The tracing tree structure needs to be extensible as well so that adding additional tracing information is easy.

Approach

Initially we can build a collection of functions that are intended to be invoked from ghci that will provide a clean interface for interacting with the verifier. At a minimum it should support invoking the verifier with some subset of the configuration parameters available when calling from the command line tool. This will return a trace tree representing the various intermediate datatypes produced during verification. The toplevel then consists of a collection of tools dedicated to querying this tree.

Example

> let cfg = RunConfig "test.original.exe" "test.patched.exe" "test.toml"
> let (pGraph, treeTrace) = runVerifier cfg
> print (getBlockExits treeTrace (0x000100d8, 000100d8))
[ Call (0x000100f0, 000100f0), Return ]
> print (getPostdomain treeTrace (0x000100d8, 000100d8) (Call (0x000100f0, 000100f0)))
    == Equivalence Domain ==
    == Registers ==
    _PC

    == Stack ==
    1+bvSum cstack_base@244228:bv 0xfffffffc:[32]
    == Globals ==
    0+0x30058:[32]

Potentially there can be some implicit state used to set a “cursor” indicating the current proof node being inspected, so it doesn’t need to be quoted back each time.

> let (pGraph, treeTrace) = runVerifier cfg
> setTree treeTrace
> goToNode (0x000100d8, 000100d8)
	At Node: (0x000100d8, 000100d8)
> showExits
	1: Call (0x000100f0, 000100f0)
     2: Return
> goToExit 1
	At Node: (0x000100d8, 000100d8)
	At Exit: Call (0x000100f0, 000100f0)
> showCurrentAssumptions
	== Predicate Assumptions ==
    { let -- 0x1184c
          v241018 = select cInitMemBytes@240617:a 1
          -- 0x1184c
          v241020 = select cInitMemRegions@240618:a 1
          -- 0x1184c
          v241022 = eq (select cInitMemRegions@240514:a 1) v241020
     …
== Bindings ==
    [ let -- 0x1183c
          v240868 = bvSum cstack_base@240515:bv 0xfffffff8:[32]
     in select (select cInitMemRegions@240514:a 1) v240868 --> { 1 }

Implementation

The top-level implementation is straightforward, since we are relying on ghci for most of the repl functionality (with some additional state management for convenience). Most of the change will involve adding this information to the PairGraph with sufficient structure that it can be retrieved easily. Currently most of the desired data is thrown away when a widening pass has finished for a node.

The approach will be to augment the EquivM environment to contain the current traversal path (e.g. which node is being inspected, which verification phase is happening, which block exit is being considered, etc).

EquivM will be defined as a MonadWriter which produces a PairGraph (or something similar that can be more easily defined as a Monoid and is specialized to collecting the desired debugging information). There are some details to get right here, since there is not an obvious way to define a MonadWriter instance for a monad that is also UnliftIO.

Trace Tree

To avoid defining too much of the proof structure statically, we can define a general “trace tree” structure where the nodes of the tree can be defined ad-hoc using type classes.

The general structure of the tree will be:

Each node of a tree contains a list of key/value pairs where the key is determined by the type of the node (as determined by the type class instance) and the value is a subtree of any type.

The shape of the tree will be determined ad-hoc by the use of combinators defined in the EquivM monad, which assemble the emitted trace tree elements.

For example, the above tree shape could be generated as follows:

handleNodes nodes = withSubTree $ do
   forM (\node -> withTrace @"graphNode" node $ visitNode node) nodes

visitNode (GraphReturn x) = do
   emitTrace @"nodeRet" x
   …
visitNode (GraphEntry x) = do
  emitTrace @"nodeEntry x
  …

Notably it is up to the consumer of this trace graph (i.e. the interactive debugger) to pattern match on the tags in order to determine the type of the node, and to decide how to interpret the subtrees of the node.