add witness traces to more phases of the analysis

src/Pate/Equivalence.hs

@@ -87,6 +87,7 @@ import qualified What4.PredMap as WPM
 import qualified Pate.ExprMappable as PEM
 
 import           Pate.TraceTree
+import Data.Data (Typeable)
 
 data EquivalenceStatus =
     Equivalent
@@ -384,6 +385,7 @@ memPreCondToPred ::
   forall sym arch v.
   IsSymInterface sym =>
   MM.RegisterInfo (MM.ArchReg arch) =>
+  Typeable arch =>
   sym ->
   SimScope sym arch v ->
   MemRegionEquality sym arch ->

src/Pate/Equivalence/Error.hs

@@ -158,6 +158,7 @@ data InnerEquivalenceError arch
   | FailedToResolveAddress (MM.MemWord (MM.ArchAddrWidth arch))
   | forall tp. FailedToGroundExpr (SomeExpr tp)
   | OrphanedSingletonAnalysis (PB.FunPair arch)
+  | RequiresInvalidPointerOps
 
 data SomeExpr tp = forall sym. W4.IsExpr (W4.SymExpr sym) => SomeExpr (W4.SymExpr sym tp)
 

src/Pate/ExprMappable.hs

@@ -32,6 +32,8 @@ module Pate.ExprMappable (
   , PartialF(..)
   , toPartialSeq
   , updateFilterSeq
+  , ExprMapFElems(..)
+
   ) where
 
 import qualified Control.Monad.IO.Class as IO
@@ -57,6 +59,11 @@ import qualified Pate.Parallel as Par
 import Unsafe.Coerce(unsafeCoerce)
 import Lang.Crucible.Simulator.SymSequence
 import Data.Maybe (fromMaybe)
+import qualified Lang.Crucible.Utils.MuxTree as MT
+import Data.Parameterized.Map (MapF)
+import qualified Data.Parameterized.TraversableF as TF
+import Data.Text
+import Control.Monad (forM)
 
 -- Expression binding
 
@@ -351,4 +358,27 @@ updateFilterSeq sym f_ s_ = evalWithFreshCache f s_
 
 
 instance ExprMappable sym () where
-  mapExpr _sym _f _e = pure ()
+  mapExpr _sym _f _e = pure ()
+
+instance ExprMappable sym Text where
+  mapExpr _ _ = return
+
+instance (Ord f, ExprMappable sym f) => ExprMappable sym (MT.MuxTree sym f) where
+  mapExpr sym (f :: forall tp. WI.SymExpr sym tp -> m (WI.SymExpr sym tp)) mt = do
+    go (MT.viewMuxTree @sym mt)
+    where
+      go :: WI.IsExprBuilder sym => [(f, WI.Pred sym)] -> m (MT.MuxTree sym f)
+      go [] = error "Unexpected empty Mux Tree"
+      go [(a,_p)] = MT.toMuxTree sym <$> mapExpr sym f a
+      go ((a, p):xs) = do
+        a' <- MT.toMuxTree sym <$> mapExpr sym f a
+        x <- go xs
+        p' <- f p
+        IO.liftIO $ MT.mergeMuxTree sym p' a' x
+
+-- | Wrapper for 'MapF' indicating that only the elements of the map should be
+--   traversed with 'mapExpr'
+newtype ExprMapFElems a b = ExprMapFElems { unExprMapFElems :: (MapF a b) }
+
+instance (forall tp. ExprMappable sym (f tp)) => ExprMappable sym (ExprMapFElems a f) where
+  mapExpr sym f (ExprMapFElems m) = ExprMapFElems <$> TF.traverseF (mapExpr sym f) m

src/Pate/MemCell.hs

@@ -40,6 +40,7 @@ import qualified Pate.ExprMappable as PEM
 import qualified Pate.Memory.MemTrace as PMT
 import qualified What4.ExprHelpers as WEH
 import qualified What4.PredMap as WPM
+import Data.Data (Typeable)
 
 -- | A pointer with an attached width, representing the size of the "cell" in bytes.
 -- It represents a discrete read or write, used as the key when forming a 'Pate.Equivalence.MemPred'
@@ -144,8 +145,10 @@ readMemCell sym mem cell@(MemCell{}) = do
 
 -- FIXME: this currently drops the region due to weaknesses in the memory model
 writeMemCell ::
+  forall sym arch w.
   IsSymInterface sym =>
   MC.RegisterInfo (MC.ArchReg arch) =>
+  Typeable arch =>
   sym ->
   -- | write condition
   WI.Pred sym ->
@@ -155,7 +158,7 @@ writeMemCell ::
   IO (PMT.MemTraceState sym (MC.ArchAddrWidth arch))
 writeMemCell sym cond mem cell@(MemCell{}) valPtr = do
   let repr = MC.BVMemRepr (cellWidth cell) (cellEndian cell)
-  PMT.writeMemState sym cond mem (cellPtr cell) repr valPtr
+  PMT.writeMemState @_ @arch sym cond mem (cellPtr cell) repr valPtr
 
 instance PEM.ExprMappable sym (MemCell sym arch w) where
   mapExpr sym f (MemCell ptr w end) = do