add "pointer" as a formal parameter to events

this makes pretty-printing ground traces easier,
as the GUI can decide how to present grounded pointers
differently depending on the region

pate_binja/pate.py

@@ -1616,6 +1616,8 @@ def pprint_mem_op(mem_op: dict, pre: str = '', out: IO = sys.stdout, prune_zero:
 def pretty_call_arg(arg):
     if isinstance(arg, dict) and 'data_expr' in arg:
         return str(arg['data_expr'])
+    elif isinstance(arg, dict) and 'pointer' in arg:
+      return (get_value_id(arg['pointer']))
     else:
         return str(arg)
 

src/Pate/Arch.hs

@@ -128,6 +128,7 @@ import Data.Maybe
 import Pate.Memory
 import qualified Pate.ExprMappable as PEM
 import Control.Monad (forM)
+import qualified Pate.Pointer as Ptr
 
 -- | The type of architecture-specific dedicated registers
 --
@@ -843,8 +844,9 @@ mkDefaultStubOverrideArg nm rArgs rOut = StubOverride $ \sym _ _ -> do
   let w = MC.memWidthNatRepr @(MC.ArchAddrWidth arch)
 
   return $ StateTransformer $ \st -> do
-    vals <- mapM (\(Some r) -> getType sym (PS.simRegs st ^. MC.boundValue r)) rArgs
-    Some vals_ctx <- return $ Ctx.fromList (concat vals)
+    datas <- concat <$> mapM (\(Some r) -> getType sym (PS.simRegs st ^. MC.boundValue r)) rArgs
+    dataExprs <- PEM.foldExpr sym (\e_ es_ -> return (Some e_:es_)) datas [] 
+    Some vals_ctx <- return $ Ctx.fromList (reverse dataExprs)
     -- globally unique function
     result_fn <- W4U.mkUninterpretedSymFn sym nm (TFC.fmapFC W4.exprType vals_ctx) (W4.BaseBVRepr w)
     fresh_bv <- W4.applySymFn sym result_fn vals_ctx
@@ -856,8 +858,8 @@ mkDefaultStubOverrideArg nm rArgs rOut = StubOverride $ \sym _ _ -> do
         -- the call was saved. Ideally there would be a formal slot in the
         -- event to store this information.
         let nm' = rOutNm ++ " <- " ++ nm
-        IO.liftIO $ PMT.addExternalCallEvent sym (T.pack nm') vals_ctx False mem0
-      Nothing -> IO.liftIO $ PMT.addExternalCallEvent sym (T.pack nm) vals_ctx False mem0
+        IO.liftIO $ PMT.addMemEvent sym (PMT.ExternalCallEventHidden (T.pack nm') datas) mem0
+      Nothing -> IO.liftIO $ PMT.addMemEvent sym (PMT.ExternalCallEventHidden (T.pack nm) datas) mem0
     val <- IO.liftIO $ PSR.bvToEntry sym fresh_bv
     updateRegister sym rOut val (st { PS.simMem = mem1 })
 
@@ -866,13 +868,12 @@ mkDefaultStubOverrideArg nm rArgs rOut = StubOverride $ \sym _ _ -> do
       W4.IsExprBuilder sym => 
       sym -> 
       PSR.MacawRegEntry sym tp -> 
-      IO [Some (W4.SymExpr sym)]
+      IO [PMT.ExternalCallData sym (MC.ArchAddrWidth arch)]
     getType _sym r = case PSR.macawRegRepr r of
-      CLM.LLVMPointerRepr{} -> do
-        let CLM.LLVMPointer reg off = PSR.macawRegValue r
-        let iRegion = W4.natToIntegerPure reg
-        return $ [Some iRegion, Some off]
-      LCT.BoolRepr -> return $ [Some $ PSR.macawRegValue r]
+      CLM.LLVMPointerRepr{} -> 
+        return $ [PMT.ExternalCallDataPointer (Ptr.fromLLVMPointer $ PSR.macawRegValue r )]
+
+      LCT.BoolRepr -> return $ [PMT.ExternalCallDataExpr $ PSR.macawRegValue r]
       LCT.StructRepr Ctx.Empty -> return []
       x -> error $ "mkDefaultStubOverrideArg: unsupported type" ++ show x
 

src/Pate/EventTrace.hs

@@ -71,7 +71,7 @@ import qualified Data.Parameterized.Context as Ctx
 
 import           What4.Interface hiding ( integerToNat )
 
-import           Lang.Crucible.LLVM.MemModel (LLVMPtr, pattern LLVMPointer, ppPtr)
+import           Lang.Crucible.LLVM.MemModel (LLVMPtr, pattern LLVMPointer, ppPtr )
 import           Lang.Crucible.Utils.MuxTree ( MuxTree, viewMuxTree )
 import           Lang.Crucible.Simulator.SymSequence ( SymSequence(..), muxSymSequence, evalWithFreshCache, nilSymSequence, consSymSequence, appendSymSequence, isNilSymSequence, traverseSymSequence )
 
@@ -315,20 +315,24 @@ pattern ExternalCallEventHidden nm args = ExternalCallEventGen nm args False
 
 data ExternalCallData sym ptrW =
     forall tp. ExternalCallDataExpr (SymExpr sym tp)
+  | forall w. 1 <= w => ExternalCallDataPointer (Ptr.Pointer sym w)
   | ExternalCallDataChunk (MemChunk sym ptrW)
 
 instance PEM.ExprMappable sym (ExternalCallData sym ptrW) where
   mapExpr sym f = \case
     ExternalCallDataExpr e -> ExternalCallDataExpr <$> f e
+    ExternalCallDataPointer ptr -> ExternalCallDataPointer <$> PEM.mapExpr sym f ptr
     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
+    ExternalCallDataPointer ptr -> PEM.foldExpr sym f ptr 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 (ExternalCallDataPointer ptr) = W4S.object ["pointer" .== ptr]
   w4Serialize (ExternalCallDataChunk c) = W4S.object ["mem_chunk" .= c]
 
 instance OrdF (SymExpr sym) => Eq (ExternalCallData sym ptrW) where
@@ -337,8 +341,18 @@ instance OrdF (SymExpr sym) => Eq (ExternalCallData sym ptrW) where
 instance OrdF (SymExpr sym) => Ord (ExternalCallData sym ptrW) where
   compare (ExternalCallDataExpr e1) (ExternalCallDataExpr e2) = toOrdering $ compareF e1 e2
   compare (ExternalCallDataChunk c1) (ExternalCallDataChunk c2) = compare c1 c2
+  compare (ExternalCallDataPointer ptr1) (ExternalCallDataPointer ptr2) = 
+    toOrdering $  compareF ptr1 ptr2
+
+  compare (ExternalCallDataExpr{}) (ExternalCallDataPointer{}) = LT
   compare (ExternalCallDataExpr{}) (ExternalCallDataChunk{}) = LT
+
+  compare (ExternalCallDataPointer{}) (ExternalCallDataExpr{}) = GT
+  compare (ExternalCallDataPointer{}) (ExternalCallDataChunk{}) = LT
+
   compare (ExternalCallDataChunk{}) (ExternalCallDataExpr{})  = GT
+  compare (ExternalCallDataChunk{}) (ExternalCallDataPointer{})  = GT
+
 
 groundExternalCallData ::
   forall sym ptrW t st fs. sym ~ W4B.ExprBuilder t st fs =>
@@ -351,6 +365,7 @@ groundExternalCallData sym evalFn = \case
   ExternalCallDataExpr e -> ExternalCallDataExpr <$> do
     e_g <- W4G.groundEval evalFn e
     PVC.symbolicFromConcrete sym e_g e
+  ExternalCallDataPointer ptr -> ExternalCallDataPointer <$> Ptr.groundPtr sym evalFn ptr
   ExternalCallDataChunk (MemChunk mem base len) -> ExternalCallDataChunk <$> do
     let ptrW = memWidthNatRepr @ptrW
     base_g <- W4G.groundEval evalFn base
@@ -381,6 +396,8 @@ compareExternalCallData ::
 compareExternalCallData sym ec1 ec2 = case (ec1, ec2) of
   (ExternalCallDataExpr e1, ExternalCallDataExpr e2) | Just Refl <- testEquality (exprType e1) (exprType e2) ->
     isEq sym e1 e2
+  (ExternalCallDataPointer ptr1, ExternalCallDataPointer ptr2) ->
+    Ptr.ptrEq sym ptr1 ptr2
   (ExternalCallDataChunk (MemChunk mem1 base1 len1), ExternalCallDataChunk (MemChunk mem2 base2 len2)) -> do
     len_eq <- isEq sym len1 len2
     let ptrW = MC.memWidthNatRepr @ptrW
@@ -419,6 +436,7 @@ printExternalCallData ::
   ExternalCallData sym ptrW ->
   Doc a
 printExternalCallData (ExternalCallDataExpr e) = printSymExpr e
+printExternalCallData (ExternalCallDataPointer ptr) = pretty ptr
 printExternalCallData (ExternalCallDataChunk (MemChunk mem1 base1 len1)) =
   "TODO print mem chunk: " <+> printSymExpr mem1 <+> printSymExpr base1 <+> printSymExpr len1
 

src/Pate/Memory/MemTrace.hs

@@ -67,6 +67,7 @@ module Pate.Memory.MemTrace
 , prettyMemTraceSeq
 , addExternalCallEvent
 , addExternalCallWrite
+, addMemEvent
 , SymBV'(..)
 , getPtrAssertion
 , PtrAssertions

src/Pate/Pointer.hs

@@ -23,6 +23,8 @@ module Pate.Pointer
   , withWidth
   , asConcrete
   , traverseAsPtr
+  , ptrEq
+  , groundPtr
   ) where
 
 import Data.UnwrapType
@@ -42,6 +44,10 @@ import qualified Lang.Crucible.LLVM.MemModel as CLM
 import qualified Data.Aeson as JSON
 import Data.Aeson ((.=))
 import qualified Pate.ExprMappable as PEM
+import qualified What4.ExprHelpers as WEH
+import qualified What4.Expr.Builder as W4B
+import qualified What4.Expr.GroundEval as W4G
+import qualified Pate.Verification.Concretize as PVC
 
 
 newtype Pointer sym w = PointerC { unPtr :: (CLM.LLVMPtr sym w) }
@@ -84,6 +90,14 @@ asConcrete (Pointer reg off) = case (W4.asNat reg, W4.asConcrete off) of
   (Just reg_c, Just (W4.ConcreteBV _ off_c)) -> Just (reg_c, off_c)
   _ -> Nothing
 
+groundPtr :: forall sym ptrW t st fs. sym ~ W4B.ExprBuilder t st fs =>
+  sym ->
+  W4G.GroundEvalFn t ->
+  Pointer sym ptrW ->
+  IO (Pointer sym ptrW)
+groundPtr sym evalFn ptr = 
+  PEM.mapExpr sym (\e -> W4G.groundEval evalFn e >>= \gv -> PVC.symbolicFromConcrete sym gv e) ptr
+
 width :: W4.IsExpr (W4.SymExpr sym) => Pointer sym w -> W4.NatRepr w
 width ptr = withWidth ptr id
 
@@ -93,6 +107,17 @@ withWidth (Pointer _ off) f | W4.BaseBVRepr w <- W4.exprType off = f w
 traverseAsPtr :: Applicative t => CLM.LLVMPtr sym w1 -> (Pointer sym w1 -> t (Pointer sym w2)) -> t (CLM.LLVMPtr sym w2)
 traverseAsPtr ptr f = unPtr <$> f (PointerC ptr)
 
+-- | True iff the pointers are the same width and have the same region/offset
+ptrEq :: W4.IsExprBuilder sym => sym -> Pointer sym w1 -> Pointer sym w2 -> IO (W4.Pred sym)
+ptrEq sym ptr1@(Pointer reg1 off1) ptr2@(Pointer reg2 off2) =
+  case testEquality (width ptr1) (width ptr2) of
+    Just Refl -> do
+      regsEq <- W4.natEq sym reg1 reg2
+      W4.BaseBVRepr{} <- return $ W4.exprType off1
+      offsEq <- W4.bvEq sym off1 off2
+      W4.andPred sym regsEq offsEq
+    Nothing -> return $ W4.falsePred sym
+
 instance TestEquality (W4.SymExpr sym) => TestEquality (Pointer sym) where
   testEquality (Pointer reg1 off1) (Pointer reg2 off2) = case (reg1 == reg2, testEquality off1 off2) of
     (True, Just Refl) -> Just Refl
@@ -115,5 +140,8 @@ instance W4S.SerializableExprs sym => W4S.W4Serializable sym (Pointer sym w) whe
 
 instance W4S.SerializableExprs sym => W4S.W4SerializableF sym (Pointer sym) where
 
+instance PEM.ExprMappable sym (Pointer sym w) where
+  mapExpr sym f (PointerC llvmptr) = PointerC <$> WEH.mapExprPtr sym f llvmptr
+
 instance PEM.ExprFoldable sym (Pointer sym w) where
   foldExpr _sym f (Pointer reg1 off1) b = f (W4.natToIntegerPure reg1) b >>= f off1