WIP

src/Pate/Equivalence/Error.hs

@@ -27,7 +27,9 @@ module Pate.Equivalence.Error (
   , isRecoverable
   , isTracedWhenWarning
   , loaderError
-  , someExpr) where
+  , someExpr
+  , PairGraphErr(..)
+  ) where
 
 import qualified Control.Exception as X
 import           Data.Maybe ( catMaybes )
@@ -160,6 +162,10 @@ data InnerEquivalenceError arch
   | forall tp. FailedToGroundExpr (SomeExpr tp)
   | OrphanedSingletonAnalysis (PB.FunPair arch)
   | RequiresInvalidPointerOps
+  | PairGraphError PairGraphErr
+
+data PairGraphErr = PairGraphErr String
+  deriving Show
 
 data SomeExpr tp = forall sym. W4.IsExpr (W4.SymExpr sym) => SomeExpr (W4.SymExpr sym tp)
 

src/Pate/Monad.hs

@@ -1319,7 +1319,12 @@ traceBundle bundle msg = do
   let bp = TF.fmapF (Const . PB.concreteAddress . simInBlock) (simIn bundle)
   emitEvent (PE.ProofTraceEvent callStack bp (T.pack msg))
 
-fnTrace :: String -> EquivM_ sym arch a -> EquivM_ sym arch a
+fnTrace :: 
+  forall k e m a.
+  IsTreeBuilder k e m =>
+  TraceNodeType k "function_name" ->
+  m a ->
+  m a
 fnTrace nm f = withTracing @"function_name" nm f
 
 --------------------------------------

src/Pate/PatchPair.hs

@@ -48,6 +48,7 @@ module Pate.PatchPair (
   , view
   , asTuple
   , fromTuple
+  , fromMaybes
   , ppEq
   , LiftF(..)
   , PatchPairF
@@ -96,6 +97,8 @@ import Control.Monad.Identity
 import Pate.TraceTree
 import qualified What4.JSON as W4S
 import What4.JSON
+import Control.Monad.State.Strict (StateT (..), put)
+import qualified Control.Monad.State.Strict as CMS
 
 -- | A pair of values indexed based on which binary they are associated with (either the
 --   original binary or the patched binary).
@@ -172,6 +175,14 @@ instance Monad m => PatchPairM (MaybeT m) where
     Just ra -> return $ Just ra
     Nothing -> b
 
+instance PatchPairM m => PatchPairM (StateT s m) where
+  throwPairErr = lift $ throwPairErr
+  catchPairErr a b = do
+    s <- CMS.get
+    (x, s') <- lift $ catchPairErr (runStateT a s) (runStateT b s)
+    put s'
+    return x
+
 liftPairErr :: PatchPairM m => Maybe a -> m a
 liftPairErr (Just a) = return a
 liftPairErr Nothing = throwPairErr
@@ -204,6 +215,15 @@ asTuple pPair = case pPair of
 fromTuple :: (tp PB.Original, tp PB.Patched) -> PatchPair tp
 fromTuple (vO,vP) = PatchPair vO vP
 
+fromMaybes :: PatchPairM m => (Maybe (tp PB.Original), Maybe (tp PB.Patched)) -> m (PatchPair tp)
+fromMaybes = \case
+  (Just vO,Just vP) -> return $ PatchPair vO vP
+  (Just vO, Nothing) -> return $ PatchPairSingle PB.OriginalRepr vO
+  (Nothing, Just vP) -> return $ PatchPairSingle PB.PatchedRepr vP
+  (Nothing, Nothing) -> throwPairErr
+
+
+
 -- | Set the value in the given 'PatchPair' according to the given 'PB.WhichBinaryRepr'
 --   Raises 'pairErr' if the given 'PatchPair' does not contain a value for the given binary.
 set :: HasCallStack => PatchPairM m => PB.WhichBinaryRepr bin -> (forall tp. PatchPair tp -> tp bin -> m (PatchPair tp))

src/Pate/TraceTree.hs

@@ -151,6 +151,7 @@ import qualified Control.Concurrent as IO
 import qualified System.IO as IO
 import Data.Maybe (catMaybes)
 import Control.Concurrent (threadDelay)
+import Control.Monad.State.Strict (StateT (..), MonadState (..))
 
 data TraceTag =
     Summary
@@ -1023,6 +1024,14 @@ instance Monad m => MonadTreeBuilder k (NoTreeBuilder k m) where
   getTreeBuilder = return $ noTreeBuilder
   withTreeBuilder _ = id
 
+instance MonadTreeBuilder k m => MonadTreeBuilder k (StateT s m) where
+  getTreeBuilder = lift $ getTreeBuilder
+  withTreeBuilder tb f = do
+    s <- get
+    (a,s') <- lift $ withTreeBuilder tb (runStateT f s)
+    put s'
+    return a
+
 noTracing :: NoTreeBuilder k m a -> m a
 noTracing (NoTreeBuilder f) = f