From 597ac4157a2da76a0cfbf9650547f5384b662336 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Mon, 3 Feb 2025 15:33:32 -0800 Subject: [PATCH] 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 | 2 ++ src/Pate/Arch.hs | 21 +++++++++++---------- src/Pate/EventTrace.hs | 20 +++++++++++++++++++- src/Pate/Memory/MemTrace.hs | 1 + src/Pate/Pointer.hs | 28 ++++++++++++++++++++++++++++ 5 files changed, 61 insertions(+), 11 deletions(-) diff --git a/pate_binja/pate.py b/pate_binja/pate.py index 4a53a5ca..bec7e13d 100644 --- a/pate_binja/pate.py +++ b/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) diff --git a/src/Pate/Arch.hs b/src/Pate/Arch.hs index a9b05f02..1675855a 100644 --- a/src/Pate/Arch.hs +++ b/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 diff --git a/src/Pate/EventTrace.hs b/src/Pate/EventTrace.hs index 8f91ffa6..c52dc4c8 100644 --- a/src/Pate/EventTrace.hs +++ b/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 diff --git a/src/Pate/Memory/MemTrace.hs b/src/Pate/Memory/MemTrace.hs index 933186c9..5d08d950 100644 --- a/src/Pate/Memory/MemTrace.hs +++ b/src/Pate/Memory/MemTrace.hs @@ -67,6 +67,7 @@ module Pate.Memory.MemTrace , prettyMemTraceSeq , addExternalCallEvent , addExternalCallWrite +, addMemEvent , SymBV'(..) , getPtrAssertion , PtrAssertions diff --git a/src/Pate/Pointer.hs b/src/Pate/Pointer.hs index 064c34e5..4e5cffae 100644 --- a/src/Pate/Pointer.hs +++ b/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 \ No newline at end of file