add ExprFoldable class that doesn't rely on IO

ExprFoldableIO class falls back to the original behavior
(i.e. using ExprMappable instance)

arch/Pate/AArch32.hs

@@ -57,6 +57,7 @@ import qualified Language.ASL.Globals as ASL
 import qualified Pate.Arch as PA
 import qualified Pate.Block as PB
 import qualified Pate.Discovery.PLT as PLT
+import qualified Pate.ExprMappable as PEM
 import qualified Pate.Equivalence.Error as PEE
 import qualified Pate.Equivalence.RegisterDomain as PER
 import qualified Pate.Equivalence.EquivalenceDomain as PED
@@ -124,6 +125,12 @@ instance W4S.W4Serializable sym (ARMReg.ARMReg tp) where
 instance W4S.W4SerializableF sym ARMReg.ARMReg where
 instance (W4S.W4SerializableFC ARMReg.ARMReg) where
 
+instance PEM.ExprFoldable sym (ARMReg.ARMReg tp) where
+  foldExpr _ _ _ = return
+
+instance PEM.ExprFoldableF sym ARMReg.ARMReg where
+instance (PEM.ExprFoldableFC ARMReg.ARMReg) where
+
 instance PA.ValidArch SA.AArch32 where
   type ArchConfigOpts SA.AArch32 = AArch32Opts SA.AArch32
   -- FIXME: define these

arch/Pate/PPC.hs

@@ -69,6 +69,7 @@ import qualified Pate.Binary as PB
 import qualified Pate.Block as PBl
 import qualified Pate.Discovery as PD
 import qualified Pate.Discovery.PLT as PLT
+import qualified Pate.ExprMappable as PEM
 import qualified Pate.Equivalence.Error as PEE
 import qualified Pate.Equivalence.RegisterDomain as PER
 import qualified Pate.Equivalence.EquivalenceDomain as PED
@@ -172,6 +173,12 @@ instance forall v sym tp. SP.KnownVariant v => W4S.W4Serializable sym (PPC.PPCRe
 instance SP.KnownVariant v => W4S.W4SerializableF sym (PPC.PPCReg v) where
 instance SP.KnownVariant v => W4S.W4SerializableFC (PPC.PPCReg v) where
 
+instance SP.KnownVariant v =>  PEM.ExprFoldable sym (PPC.PPCReg v tp) where
+  foldExpr _ _ _ = return
+
+instance SP.KnownVariant v => PEM.ExprFoldableF sym (PPC.PPCReg v) where
+instance SP.KnownVariant v => (PEM.ExprFoldableFC (PPC.PPCReg v)) where
+
 instance PA.ValidArch PPC.PPC32 where
   type ArchConfigOpts PPC.PPC32 = ()
   rawBVReg r = case r of

src/Pate/Arch.hs

@@ -126,6 +126,7 @@ import qualified What4.Expr.ArrayUpdateMap as AUM
 import qualified Data.Parameterized.TraversableF as TF
 import Data.Maybe
 import Pate.Memory
+import qualified Pate.ExprMappable as PEM
 
 -- | The type of architecture-specific dedicated registers
 --
@@ -188,6 +189,7 @@ class
   , MCS.HasArchEndCase arch
   , Integral (EEP.ElfWordType (MC.ArchAddrWidth arch))
   , W4S.W4SerializableFC (MC.ArchReg arch)
+  , PEM.ExprFoldableFC (MC.ArchReg arch)
   ) => ValidArch arch where
 
   type ArchConfigOpts arch

src/Pate/Equivalence.hs

@@ -389,8 +389,7 @@ instance W4S.SerializableExprs sym => W4S.W4Serializable sym (MemoryCondition sy
 memPreCondToPred ::
   forall sym arch v.
   IsSymInterface sym =>
-  MM.RegisterInfo (MM.ArchReg arch) =>
-  Typeable arch =>
+  PA.ValidArch arch =>
   sym ->
   SimScope sym arch v ->
   MemRegionEquality sym arch ->

src/Pate/EventTrace.hs

@@ -28,6 +28,7 @@ symbolic execution.
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 
 module Pate.EventTrace
 ( MemEvent(..)
@@ -175,6 +176,11 @@ instance PEM.ExprMappable sym (MemOpCondition sym) where
     Conditional p -> Conditional <$> f p
     Unconditional -> return Unconditional
 
+instance PEM.ExprFoldable sym (MemOpCondition sym) where
+  foldExpr _sym f mc b = case mc of
+    Conditional p -> f p b
+    Unconditional -> return b
+
 data MemOpDirection =
     Read
   | Write
@@ -234,6 +240,12 @@ instance PEM.ExprMappable sym (MemOp sym w) where
       cond' <- PEM.mapExpr sym f cond
       return $ MemOp ptr' dir cond' w val' endian
 
+instance PEM.ExprFoldable sym (MemOp sym w) where
+  foldExpr sym f (MemOp ptr _dir cond _w val _endian) b0 = do
+    b1 <- PEM.foldExpr sym f (Ptr.fromLLVMPointer ptr) b0
+    b2 <- PEM.foldExpr sym f (Ptr.fromLLVMPointer val) b1
+    PEM.foldExpr sym f cond b2
+
 instance W4S.SerializableExprs sym => W4S.W4Serializable sym (MemOp sym ptrW) where
   w4Serialize (MemOp addr dir cond n val end) =
     W4S.object
@@ -272,6 +284,9 @@ instance (W4S.W4SerializableFC (ArchReg arch), W4S.SerializableExprs sym)
 instance PEM.ExprMappable sym (RegOp sym arch) where
   mapExpr sym f (RegOp m) = (RegOp . PEM.unExprMapFElems) <$> PEM.mapExpr sym f (PEM.ExprMapFElems m)
 
+instance PEM.ExprFoldableFC (ArchReg arch) => PEM.ExprFoldable sym (RegOp sym arch) where
+  foldExpr sym f (RegOp m) b = PEM.foldExpr sym f m b
+
 
 data MemEvent sym ptrW where
   MemOpEvent :: MemOp sym ptrW -> MemEvent sym ptrW
@@ -296,6 +311,11 @@ instance PEM.ExprMappable sym (ExternalCallData sym ptrW) where
     ExternalCallDataExpr e -> ExternalCallDataExpr <$> f e
     ExternalCallDataChunk c -> ExternalCallDataChunk <$> PEM.mapExpr sym f c
 
+instance PEM.ExprFoldable sym (ExternalCallData sym ptrW) where
+  foldExpr sym f ec b = case ec of
+    ExternalCallDataExpr e -> f e b
+    ExternalCallDataChunk c -> PEM.foldExpr sym f c b
+
 instance W4S.SerializableExprs sym => W4S.W4Serializable sym (ExternalCallData sym ptrW) where
   w4Serialize (ExternalCallDataExpr e) = W4S.object ["data_expr" .== e]
   w4Serialize (ExternalCallDataChunk c) = W4S.object ["mem_chunk" .= c]
@@ -412,6 +432,9 @@ instance OrdF (SymExpr sym) => Eq (MemEvent sym ptrW) where
 instance PEM.ExprMappable sym (MemChunk sym ptrW) where
   mapExpr _sym f (MemChunk a b c) = MemChunk <$> f a <*> f b <*> f c
 
+instance PEM.ExprFoldable sym (MemChunk sym ptrW) where
+  foldExpr _sym f (MemChunk a b c) s = f a s >>= f b >>= f c
+
 instance W4S.SerializableExprs sym => W4S.W4Serializable sym (MemChunk sym ptrW) where
   w4Serialize (MemChunk a b c) = W4S.object ["mem_arr" .== a, "base" .== b, "len" .== c]
 
@@ -531,8 +554,15 @@ instance PEM.ExprMappable sym (MemEvent sym w) where
     MemOpEvent op -> MemOpEvent <$> PEM.mapExpr sym f op
     SyscallEvent i arg -> SyscallEvent i <$> f arg
     -- MuxTree is unmodified since it has no symbolic expressions
+    -- FIXME: shouldn't we still check the booleans?
     ExternalCallEvent nm vs -> ExternalCallEvent nm <$> PEM.mapExpr sym f vs
 
+instance PEM.ExprFoldable sym (MemEvent sym w) where
+  foldExpr sym f ev b = case ev of
+    MemOpEvent op -> PEM.foldExpr sym f op b
+    -- FIXME: see above
+    SyscallEvent _i arg -> f arg b
+    ExternalCallEvent _nm vs -> PEM.foldExpr sym f vs b
 
 filterEvent ::
   IsExprBuilder sym =>
@@ -567,11 +597,19 @@ instance W4S.W4Serializable sym  (MemSegmentOff w) where
 instance PEM.ExprMappable sym (MemSegmentOff w) where
   mapExpr _ _ = return
 
+instance PEM.ExprFoldable sym (MemSegmentOff w) where
+  foldExpr _ _ _ = return
+
 instance PEM.ExprMappable sym (TraceEvent sym arch) where
   mapExpr sym f e = case e of
     RegOpEvent i rop -> RegOpEvent <$> PEM.mapExpr sym f i <*> PEM.mapExpr sym f rop
     TraceMemEvent i mop -> TraceMemEvent <$> PEM.mapExpr sym f i <*> PEM.mapExpr sym f mop
 
+instance PEM.ExprFoldableFC (ArchReg arch) => PEM.ExprFoldable sym (TraceEvent sym arch) where
+  foldExpr sym f te b0 = case te of
+    RegOpEvent i rop -> PEM.foldExpr sym f i b0 >>= PEM.foldExpr sym f rop
+    TraceMemEvent i mop -> PEM.foldExpr sym f i b0 >>= PEM.foldExpr sym f mop
+
 instance W4S.W4Serializable sym  (MemAddr w) where
   w4Serialize addr = do
     base_json <- return $ JSON.toJSON (addrBase addr)
@@ -595,6 +633,9 @@ data InstructionEvent arch = InstructionEvent { instrAddr :: ArchSegmentOff arch
 instance PEM.ExprMappable sym (InstructionEvent arch) where
   mapExpr _sym _f e = return e
 
+instance PEM.ExprFoldable sym (InstructionEvent arch) where
+  foldExpr _ _ _ = return
+
 instance W4S.W4Serializable sym (InstructionEvent arch) where
   w4Serialize (InstructionEvent addr dis) = W4S.object ["address" .= addr, "disassembled" .= dis]
 

src/Pate/ExprMappable.hs

@@ -15,14 +15,21 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 
 -- must come after TypeFamilies, see also https://gitlab.haskell.org/ghc/ghc/issues/18006
 {-# LANGUAGE NoMonoLocalBinds #-}
 {-# OPTIONS_GHC -fno-warn-simplifiable-class-constraints #-}
 
 module Pate.ExprMappable (
     ExprMappable(..)
+  , ExprMappableFC
   , ExprFoldable(..)
+  , ExprFoldableF(..)
+  , withExprFoldable
+  , ExprFoldableFC
+  , ExprFoldableIO(..)
   , SkipTransformation(..)
   , ToExprMappable(..)
   , SymExprMappable(..)
@@ -60,10 +67,14 @@ 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           Data.Parameterized.Map (MapF)
+import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.TraversableF as TF
 import Data.Text
-import Control.Monad (forM)
+import Control.Monad (forM, foldM)
+import Data.Kind (Type)
+import Data.Proxy
+
 
 -- Expression binding
 
@@ -101,16 +112,35 @@ class ExprMappable2 sym sym' f f' where
 
 class ExprFoldable sym f where
   foldExpr ::
+    Monad m => 
     WI.IsSymExprBuilder sym =>
-    IO.MonadIO m =>
     sym ->
     (forall tp. WI.SymExpr sym tp -> b -> m b) ->
     f ->
     b ->
     m b
 
-instance ExprMappable sym f => ExprFoldable sym f where
-  foldExpr sym f e b =
+-- Constrainted variant of 'ExprFoldable' that uses 'ExprMappable'
+-- instance by default
+class ExprFoldableIO sym f where
+  foldExprIO ::
+    IO.MonadIO m => 
+    WI.IsSymExprBuilder sym =>
+    sym ->
+    (forall tp. WI.SymExpr sym tp -> b -> m b) ->
+    f ->
+    b ->
+    m b
+  default foldExprIO :: 
+    ExprMappable sym f =>
+    IO.MonadIO m => 
+    WI.IsSymExprBuilder sym =>
+    sym ->
+    (forall tp. WI.SymExpr sym tp -> b -> m b) ->
+    f ->
+    b ->
+    m b
+  foldExprIO sym f e b = 
     CMS.execStateT (mapExpr sym (\e' -> CMS.get >>= \s -> lift (f e' s) >>= CMS.put >> return e') e) b
 
 instance (ExprMappable sym a, ExprMappable sym b) => ExprMappable sym (a, b) where
@@ -201,6 +231,12 @@ instance
 instance ExprMappable (W4B.ExprBuilder t st fs) (W4B.Expr t tp) where
   mapExpr sym f e = applyExprMappable sym f e
 
+instance ExprFoldable (W4B.ExprBuilder t st fs) (W4B.Expr t tp) where
+  foldExpr _sym f e = f e
+
+instance ExprFoldableIO (W4B.ExprBuilder t st fs) (W4B.Expr t tp) where
+  foldExprIO _sym f e = f e
+
 -- | This is a bit redundant, but it forces the function to be evaluated
 --   according to the 'ToExprMappable' instance for 'ExprMappable', which
 --   avoids the potential for conflicting instances for 'W4B.Expr' vs. 'WI.SymExpr'
@@ -363,6 +399,23 @@ instance ExprMappable sym () where
 instance ExprMappable sym Text where
   mapExpr _ _ = return
 
+class (forall sym tp. ExprMappable sym (f tp)) => ExprMappableFC f
+
+class ExprFoldableF (sym :: Type) (f :: k -> Type) where
+  withExprFoldable_ :: p sym -> q f -> r tp -> (ExprFoldable sym (f tp) => a) -> a
+
+  default withExprFoldable_ :: ExprFoldable sym (f tp) => p sym -> q f -> r tp -> (ExprFoldable sym (f tp) => a) -> a
+  withExprFoldable_ _ _ _ x = x
+
+-- instantiates proxies (assumes TypeApplications)
+withExprFoldable :: 
+  forall sym f tp a.
+   ExprFoldableF sym f =>
+  (ExprFoldable sym (f tp) => a) -> a
+withExprFoldable f = withExprFoldable_ (Proxy @sym) (Proxy @f) (Proxy @tp) f
+
+class (forall sym. ExprFoldableF sym f) => ExprFoldableFC f where
+
 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)
@@ -381,4 +434,44 @@ instance (Ord f, ExprMappable sym f) => ExprMappable sym (MT.MuxTree sym f) wher
 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
+  mapExpr sym f (ExprMapFElems m) = ExprMapFElems <$> TF.traverseF (mapExpr sym f) m
+
+
+instance forall sym a b. (ExprFoldableF sym a, ExprFoldableF sym b) => ExprFoldable sym (MapF a b) where
+  foldExpr sym f m b = 
+    MapF.foldlMWithKey (\b_ (k :: a tp) (v :: b tp) -> 
+      withExprFoldable @sym @a @tp $ withExprFoldable @sym @b @tp $
+       foldExpr sym f k b_ >>= foldExpr sym f v) b m
+
+instance ExprFoldable sym a => ExprFoldable sym [a] where
+  foldExpr sym f m b = foldM (\b_ a -> foldExpr sym f a b_) b m
+
+instance ExprFoldable sym Text where
+  foldExpr _ _ _ = return
+
+instance (ExprFoldable sym f, ExprFoldable sym g) => ExprFoldable sym (f, g) where
+  foldExpr sym f (a,b) b0 = foldExpr sym f a b0 >>= foldExpr sym f b
+
+instance ExprFoldable sym f => ExprFoldable sym (Maybe f) where
+  foldExpr sym f (Just e) b0 = foldExpr sym f e b0
+  foldExpr _ _ Nothing b0 = return b0
+
+instance (ExprFoldable sym f) => ExprFoldable sym (MT.MuxTree sym f) where
+  foldExpr sym f mt b0 | SymExprFoldable aEF <- symExprFoldable sym = aEF @WI.BaseBoolType $ foldExpr sym f (MT.viewMuxTree mt) b0
+
+newtype ToExprFoldable sym tp = ToExprFoldable { unEF :: WI.SymExpr sym tp }
+
+instance ExprFoldable sym (ToExprFoldable sym tp) where
+  foldExpr _sym f (ToExprFoldable e) b = f e b
+
+newtype SymExprFoldable sym f = SymExprFoldable (forall tp a. ((ExprFoldable sym (f tp)) => a) -> a)
+
+-- Same approach for 'symExprMappable' to create ExprFoldable instances for SymExpr
+symExprFoldable ::
+  forall sym.
+  sym ->
+  SymExprFoldable sym (WI.SymExpr sym)
+symExprFoldable _sym =
+  unsafeCoerce r
+  where r :: SymExprFoldable sym (ToExprFoldable sym)
+        r = SymExprFoldable (\a -> a)

src/Pate/Ground.hs

@@ -71,6 +71,7 @@ import qualified What4.Partial as W4P
 import qualified SemMC.Util as SU
 
 import qualified Pate.Panic as PP
+import qualified Control.Monad.IO.Class as IO
 
 -- | This module allows a model from What4 to be captured with respect to
 -- some expression-containing type. This is used to ground concrete counter-examples
@@ -216,7 +217,7 @@ integerToNat i
 ground ::
   forall sym a.
   PS.ValidSym sym =>
-  PEM.ExprMappable sym (a sym) =>
+  PEM.ExprFoldableIO sym (a sym) =>
   sym ->
   -- | stack region
   W4.SymNat sym ->
@@ -239,7 +240,7 @@ ground sym stackRegion mkinfo a = do
       Nothing -> do
         upd <- MapF.updatedValue <$> MapF.updateAtKey e (Just <$> mkinfo e) (\_ -> return $ MapF.Keep) (grndInfoMap gdata)
         return $ gdata { grndInfoMap = upd }
-  gdata <- PEM.foldExpr sym f' a initGround
+  gdata <- PEM.foldExprIO sym f' a initGround
   return $ Grounded a gdata
 
 -- trivial instance - grounded values should not be modified

src/Pate/MemCell.hs

@@ -162,7 +162,7 @@ readMemCell sym mem cell@(MemCell{}) = do
 writeMemCell ::
   forall sym arch w.
   IsSymInterface sym =>
-  MC.RegisterInfo (MC.ArchReg arch) =>
+  PMT.MemTraceValidArch arch =>
   Typeable arch =>
   sym ->
   -- | write condition