mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-29 21:44:11 +03:00
naming only: trace, not 2
This commit is contained in:
parent
f4daaa7e81
commit
ef91508325
@ -34,7 +34,7 @@ library
|
|||||||
Data.Macaw.Symbolic.CrucGen
|
Data.Macaw.Symbolic.CrucGen
|
||||||
Data.Macaw.Symbolic.PersistentState
|
Data.Macaw.Symbolic.PersistentState
|
||||||
Data.Macaw.Symbolic.MemOps
|
Data.Macaw.Symbolic.MemOps
|
||||||
Data.Macaw.Symbolic.MemOps2
|
Data.Macaw.Symbolic.MemTraceOps
|
||||||
|
|
||||||
ghc-options: -Wall -Wcompat
|
ghc-options: -Wall -Wcompat
|
||||||
ghc-prof-options: -O2 -fprof-auto-top
|
ghc-prof-options: -O2 -fprof-auto-top
|
||||||
|
@ -14,7 +14,7 @@
|
|||||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||||
{-# LANGUAGE TypeFamilies #-}
|
{-# LANGUAGE TypeFamilies #-}
|
||||||
{-# LANGUAGE ViewPatterns #-}
|
{-# LANGUAGE ViewPatterns #-}
|
||||||
module Data.Macaw.Symbolic.MemOps2 where
|
module Data.Macaw.Symbolic.MemTraceOps where
|
||||||
|
|
||||||
import Control.Applicative
|
import Control.Applicative
|
||||||
import Control.Lens ((%~), (&), (^.))
|
import Control.Lens ((%~), (&), (^.))
|
||||||
@ -69,8 +69,8 @@ data MemOp sym ptrW where
|
|||||||
MemOp sym ptrW
|
MemOp sym ptrW
|
||||||
MergeOps ::
|
MergeOps ::
|
||||||
Pred sym ->
|
Pred sym ->
|
||||||
MemImpl2 sym ptrW ->
|
MemTraceImpl sym ptrW ->
|
||||||
MemImpl2 sym ptrW ->
|
MemTraceImpl sym ptrW ->
|
||||||
MemOp sym ptrW
|
MemOp sym ptrW
|
||||||
|
|
||||||
instance Eq (MemOpCondition (ExprBuilder t st fs)) where
|
instance Eq (MemOpCondition (ExprBuilder t st fs)) where
|
||||||
@ -86,30 +86,29 @@ instance Eq (MemOp (ExprBuilder t st fs) ptrW) where
|
|||||||
MergeOps p opsT opsF == MergeOps p' opsT' opsF' = p == p' && opsT == opsT' && opsF == opsF'
|
MergeOps p opsT opsF == MergeOps p' opsT' opsF' = p == p' && opsT == opsT' && opsF == opsF'
|
||||||
_ == _ = False
|
_ == _ = False
|
||||||
|
|
||||||
-- TODO: how about "trace memory model"-based naming instead of "2"-based naming?
|
type MemTraceImpl sym ptrW = Seq (MemOp sym ptrW)
|
||||||
type MemImpl2 sym ptrW = Seq (MemOp sym ptrW)
|
type MemTrace arch = IntrinsicType "Abstract_memory" (EmptyCtx ::> BVType (ArchAddrWidth arch))
|
||||||
type Mem2 arch = IntrinsicType "Abstract_memory" (EmptyCtx ::> BVType (ArchAddrWidth arch))
|
|
||||||
|
|
||||||
memRepr2 :: (KnownNat (ArchAddrWidth arch), 1 <= ArchAddrWidth arch) => TypeRepr (Mem2 arch)
|
memTraceRepr :: (KnownNat (ArchAddrWidth arch), 1 <= ArchAddrWidth arch) => TypeRepr (MemTrace arch)
|
||||||
memRepr2 = knownRepr
|
memTraceRepr = knownRepr
|
||||||
|
|
||||||
instance IntrinsicClass (ExprBuilder t st fs) "Abstract_memory" where
|
instance IntrinsicClass (ExprBuilder t st fs) "Abstract_memory" where
|
||||||
-- TODO: cover other cases with a TypeError
|
-- TODO: cover other cases with a TypeError
|
||||||
type Intrinsic (ExprBuilder t st fs) "Abstract_memory" (EmptyCtx ::> BVType ptrW) = MemImpl2 (ExprBuilder t st fs) ptrW
|
type Intrinsic (ExprBuilder t st fs) "Abstract_memory" (EmptyCtx ::> BVType ptrW) = MemTraceImpl (ExprBuilder t st fs) ptrW
|
||||||
muxIntrinsic _ _ _ (Empty :> BVRepr _) p l r = pure $ case Seq.spanl (uncurry (==)) (Seq.zip l r) of
|
muxIntrinsic _ _ _ (Empty :> BVRepr _) p l r = pure $ case Seq.spanl (uncurry (==)) (Seq.zip l r) of
|
||||||
(_, Seq.Empty) -> l
|
(_, Seq.Empty) -> l
|
||||||
(eqs, Seq.unzip -> (l', r')) -> (fst <$> eqs) Seq.:|> MergeOps p l' r'
|
(eqs, Seq.unzip -> (l', r')) -> (fst <$> eqs) Seq.:|> MergeOps p l' r'
|
||||||
|
|
||||||
type MacawEvalStmtFunc sym arch = EvalStmtFunc (MacawStmtExtension arch) (MacawSimulatorState sym) sym (MacawExt arch)
|
type MacawTraceEvalStmtFunc sym arch = EvalStmtFunc (MacawStmtExtension arch) (MacawSimulatorState sym) sym (MacawExt arch)
|
||||||
type GlobalMap2 sym arch = sym -> MemImpl2 sym (ArchAddrWidth arch) -> RegValue sym NatType -> RegValue sym (BVType (ArchAddrWidth arch)) -> IO (Maybe (LLVMPtr sym (ArchAddrWidth arch)))
|
type TraceGlobalMap sym arch = sym -> MemTraceImpl sym (ArchAddrWidth arch) -> RegValue sym NatType -> RegValue sym (BVType (ArchAddrWidth arch)) -> IO (Maybe (LLVMPtr sym (ArchAddrWidth arch)))
|
||||||
type MacawArchEvalFn2 sym arch = GlobalVar (Mem2 arch) -> GlobalMap2 sym arch -> EvalStmtFunc (MacawArchStmtExtension arch) (MacawSimulatorState sym) sym (MacawExt arch)
|
type MacawTraceArchEvalFn sym arch = GlobalVar (MemTrace arch) -> TraceGlobalMap sym arch -> EvalStmtFunc (MacawArchStmtExtension arch) (MacawSimulatorState sym) sym (MacawExt arch)
|
||||||
|
|
||||||
execMacawStmtExtension ::
|
execMacawStmtExtension ::
|
||||||
forall sym arch t st fs. (IsSymInterface sym, KnownNat (ArchAddrWidth arch), sym ~ ExprBuilder t st fs) =>
|
forall sym arch t st fs. (IsSymInterface sym, KnownNat (ArchAddrWidth arch), sym ~ ExprBuilder t st fs) =>
|
||||||
MacawArchEvalFn2 sym arch ->
|
MacawTraceArchEvalFn sym arch ->
|
||||||
GlobalVar (Mem2 arch) ->
|
GlobalVar (MemTrace arch) ->
|
||||||
GlobalMap2 sym arch ->
|
TraceGlobalMap sym arch ->
|
||||||
MacawEvalStmtFunc sym arch
|
MacawTraceEvalStmtFunc sym arch
|
||||||
execMacawStmtExtension archStmtFn mvar globs stmt
|
execMacawStmtExtension archStmtFn mvar globs stmt
|
||||||
= case stmt of
|
= case stmt of
|
||||||
MacawReadMem addrWidth memRepr addr
|
MacawReadMem addrWidth memRepr addr
|
||||||
@ -281,7 +280,7 @@ doReadMem ::
|
|||||||
AddrWidthRepr ptrW ->
|
AddrWidthRepr ptrW ->
|
||||||
LLVMPtr sym ptrW ->
|
LLVMPtr sym ptrW ->
|
||||||
MemRepr ty ->
|
MemRepr ty ->
|
||||||
StateT (MemImpl2 sym ptrW) IO (RegValue sym (ToCrucibleType ty))
|
StateT (MemTraceImpl sym ptrW) IO (RegValue sym (ToCrucibleType ty))
|
||||||
doReadMem sym ptrWidth ptr memRepr = do
|
doReadMem sym ptrWidth ptr memRepr = do
|
||||||
val <- liftIO $ freshRegValue sym ptr memRepr
|
val <- liftIO $ freshRegValue sym ptr memRepr
|
||||||
doMemOpInternal sym Read Unconditional ptrWidth ptr val memRepr
|
doMemOpInternal sym Read Unconditional ptrWidth ptr val memRepr
|
||||||
@ -295,7 +294,7 @@ doCondReadMem ::
|
|||||||
AddrWidthRepr ptrW ->
|
AddrWidthRepr ptrW ->
|
||||||
LLVMPtr sym ptrW ->
|
LLVMPtr sym ptrW ->
|
||||||
MemRepr ty ->
|
MemRepr ty ->
|
||||||
StateT (MemImpl2 sym ptrW) IO (RegValue sym (ToCrucibleType ty))
|
StateT (MemTraceImpl sym ptrW) IO (RegValue sym (ToCrucibleType ty))
|
||||||
doCondReadMem sym cond def ptrWidth ptr memRepr = do
|
doCondReadMem sym cond def ptrWidth ptr memRepr = do
|
||||||
val <- liftIO $ freshRegValue sym ptr memRepr
|
val <- liftIO $ freshRegValue sym ptr memRepr
|
||||||
doMemOpInternal sym Read (Conditional cond) ptrWidth ptr val memRepr
|
doMemOpInternal sym Read (Conditional cond) ptrWidth ptr val memRepr
|
||||||
@ -308,7 +307,7 @@ doWriteMem ::
|
|||||||
LLVMPtr sym ptrW ->
|
LLVMPtr sym ptrW ->
|
||||||
RegValue sym (ToCrucibleType ty) ->
|
RegValue sym (ToCrucibleType ty) ->
|
||||||
MemRepr ty ->
|
MemRepr ty ->
|
||||||
StateT (MemImpl2 sym ptrW) IO ()
|
StateT (MemTraceImpl sym ptrW) IO ()
|
||||||
doWriteMem sym = doMemOpInternal sym Write Unconditional
|
doWriteMem sym = doMemOpInternal sym Write Unconditional
|
||||||
|
|
||||||
doCondWriteMem ::
|
doCondWriteMem ::
|
||||||
@ -319,7 +318,7 @@ doCondWriteMem ::
|
|||||||
LLVMPtr sym ptrW ->
|
LLVMPtr sym ptrW ->
|
||||||
RegValue sym (ToCrucibleType ty) ->
|
RegValue sym (ToCrucibleType ty) ->
|
||||||
MemRepr ty ->
|
MemRepr ty ->
|
||||||
StateT (MemImpl2 sym ptrW) IO ()
|
StateT (MemTraceImpl sym ptrW) IO ()
|
||||||
doCondWriteMem sym cond = doMemOpInternal sym Write (Conditional cond)
|
doCondWriteMem sym cond = doMemOpInternal sym Write (Conditional cond)
|
||||||
|
|
||||||
freshRegValue :: forall sym ptrW ty.
|
freshRegValue :: forall sym ptrW ty.
|
||||||
@ -357,9 +356,9 @@ doMemOpInternal :: forall sym ptrW ty.
|
|||||||
LLVMPtr sym ptrW ->
|
LLVMPtr sym ptrW ->
|
||||||
RegValue sym (ToCrucibleType ty) ->
|
RegValue sym (ToCrucibleType ty) ->
|
||||||
MemRepr ty ->
|
MemRepr ty ->
|
||||||
StateT (MemImpl2 sym ptrW) IO ()
|
StateT (MemTraceImpl sym ptrW) IO ()
|
||||||
doMemOpInternal sym dir cond ptrWidth = go where
|
doMemOpInternal sym dir cond ptrWidth = go where
|
||||||
go :: LLVMPtr sym ptrW -> RegValue sym (ToCrucibleType ty') -> MemRepr ty' -> StateT (MemImpl2 sym ptrW) IO ()
|
go :: LLVMPtr sym ptrW -> RegValue sym (ToCrucibleType ty') -> MemRepr ty' -> StateT (MemTraceImpl sym ptrW) IO ()
|
||||||
go ptr@(LLVMPointer reg off) regVal = \case
|
go ptr@(LLVMPointer reg off) regVal = \case
|
||||||
BVMemRepr byteWidth endianness -> logOp $ MemOp ptr dir cond bitWidth regVal endianness
|
BVMemRepr byteWidth endianness -> logOp $ MemOp ptr dir cond bitWidth regVal endianness
|
||||||
where bitWidth = natMultiply (knownNat @8) byteWidth
|
where bitWidth = natMultiply (knownNat @8) byteWidth
|
||||||
@ -394,7 +393,7 @@ iteDeep sym cond t f = \case
|
|||||||
PackedVecMemRepr countRepr recRepr -> V.generateM (fromInteger (intValue countRepr)) $ \i ->
|
PackedVecMemRepr countRepr recRepr -> V.generateM (fromInteger (intValue countRepr)) $ \i ->
|
||||||
iteDeep sym cond (t V.! i) (f V.! i) recRepr
|
iteDeep sym cond (t V.! i) (f V.! i) recRepr
|
||||||
|
|
||||||
logOp :: (MonadState (MemImpl2 sym ptrW) m) => MemOp sym ptrW -> m ()
|
logOp :: (MonadState (MemTraceImpl sym ptrW) m) => MemOp sym ptrW -> m ()
|
||||||
logOp op = modify (Seq.:|> op)
|
logOp op = modify (Seq.:|> op)
|
||||||
|
|
||||||
addrWidthsArePositive :: AddrWidthRepr w -> (1 <= w => a) -> a
|
addrWidthsArePositive :: AddrWidthRepr w -> (1 <= w => a) -> a
|
Loading…
Reference in New Issue
Block a user