From 80de5d94e546d94db83e803329f1756ffb5df739 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 19 Jul 2019 00:13:00 -0700 Subject: [PATCH 1/5] [symbolic] update for use of safe Nonce in crucible. Update for compatibility with Crucible changes in https://github.com/GaloisInc/crucible/pull/285. --- symbolic/src/Data/Macaw/Symbolic.hs | 65 ++++---- symbolic/src/Data/Macaw/Symbolic/CrucGen.hs | 155 +++++++++--------- .../Data/Macaw/Symbolic/PersistentState.hs | 9 +- 3 files changed, 113 insertions(+), 116 deletions(-) diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs index 55688ea1..2285d1f4 100644 --- a/symbolic/src/Data/Macaw/Symbolic.hs +++ b/symbolic/src/Data/Macaw/Symbolic.hs @@ -20,7 +20,7 @@ -- library. There are two main portions of the API: -- -- 1. Translation of Macaw IR into Crucible CFGs --- 2. Symbolic execution of Crucible CFGs generated from MAcaw +-- 2. Symbolic execution of Crucible CFGs generated from Macaw -- -- There are examples of each use case in the relevant sections of the haddocks. -- @@ -109,13 +109,12 @@ import GHC.TypeLits import Control.Lens ((^.)) import Control.Monad import Control.Monad.IO.Class -import Control.Monad.ST (ST, RealWorld, stToIO) import Data.Foldable import qualified Data.Map.Strict as Map import Data.Maybe import Data.Parameterized.Context (EmptyCtx, (::>), pattern Empty, pattern (:>)) import qualified Data.Parameterized.Context as Ctx -import Data.Parameterized.Nonce ( NonceGenerator, newSTNonceGenerator ) +import Data.Parameterized.Nonce ( NonceGenerator, newIONonceGenerator ) import Data.Parameterized.Some ( Some(Some) ) import qualified Data.Parameterized.TraversableFC as FC import qualified Data.Vector as V @@ -255,7 +254,7 @@ mkCrucRegCFG archFns halloc nm action = do pure $ CR.SomeCFG rg -- | Create a Crucible CFG from a list of blocks -addBlocksCFG :: forall h s arch ids +addBlocksCFG :: forall s arch ids . MacawSymbolicArchFunctions arch -- ^ Crucible specific functions. -> MemSegmentMap (M.ArchAddrWidth arch) @@ -266,7 +265,7 @@ addBlocksCFG :: forall h s arch ids -- ^ Function that maps offsets from start of block to Crucible position. -> M.Block arch ids -- ^ Macaw block for this region. - -> MacawMonad arch ids h s (CR.Label s, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]) + -> MacawMonad arch ids s (CR.Label s, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]) addBlocksCFG archFns baseAddrMap addr posFn macawBlock = do crucGenArchConstraints archFns $ do -- Map block map to Crucible CFG @@ -283,10 +282,10 @@ addBlocksCFG archFns baseAddrMap addr posFn macawBlock = do -- -- Also note that any 'M.FetchAndExecute' terminators are turned into Crucible -- return statements. -mkBlocksRegCFG :: forall s arch ids +mkBlocksRegCFG :: forall arch ids . MacawSymbolicArchFunctions arch -- ^ Crucible specific functions. - -> C.HandleAllocator s + -> C.HandleAllocator -- ^ Handle allocator to make the blocks -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Map from region indices to their address @@ -298,7 +297,7 @@ mkBlocksRegCFG :: forall s arch ids -- ^ Function that maps offsets from start of block to Crucible position. -> M.Block arch ids -- ^ List of blocks for this region. - -> ST s (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) + -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock = do mkCrucRegCFG archFns halloc nm $ do addBlocksCFG archFns memBaseVarMap addr posFn macawBlock @@ -312,10 +311,10 @@ mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock = do -- -- Also note that any 'M.FetchAndExecute' terminators are turned into Crucible -- return statements. -mkBlocksCFG :: forall s arch ids +mkBlocksCFG :: forall arch ids . MacawSymbolicArchFunctions arch -- ^ Crucible specific functions. - -> C.HandleAllocator s + -> C.HandleAllocator -- ^ Handle allocator to make the blocks -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Map from region indices to their address @@ -327,15 +326,15 @@ mkBlocksCFG :: forall s arch ids -- ^ Function that maps offsets from start of block to Crucible position. -> M.Block arch ids -- ^ List of blocks for this region. - -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) + -> IO (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) mkBlocksCFG archFns halloc memBaseVarMap nm addr posFn macawBlock = toCoreCFG archFns <$> mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock -- | Create a map from Macaw @(address, index)@ pairs to Crucible labels -mkBlockLabelMap :: [M.ParsedBlock arch ids] -> MacawMonad arch ids h s (BlockLabelMap arch s) +mkBlockLabelMap :: [M.ParsedBlock arch ids] -> MacawMonad arch ids s (BlockLabelMap arch s) mkBlockLabelMap blks = foldM insBlock Map.empty blks - where insBlock :: BlockLabelMap arch s -> M.ParsedBlock arch ids -> MacawMonad arch ids h s (BlockLabelMap arch s) + where insBlock :: BlockLabelMap arch s -> M.ParsedBlock arch ids -> MacawMonad arch ids s (BlockLabelMap arch s) insBlock m b = do let base = M.pblockAddr b n <- mmFreshNonce @@ -386,10 +385,10 @@ termStmtToJump tm0 addr = -- This is useful as an alternative to 'mkParsedBlockCFG' if post-processing is -- desired (as this is easier on the registerized form). Use 'toCoreCFG' to -- finish by translating the registerized CFG to SSA. -mkParsedBlockRegCFG :: forall h arch ids +mkParsedBlockRegCFG :: forall arch ids . MacawSymbolicArchFunctions arch -- ^ Architecture specific functions. - -> C.HandleAllocator h + -> C.HandleAllocator -- ^ Handle allocator to make the blocks -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Map from region indices to their address @@ -397,7 +396,7 @@ mkParsedBlockRegCFG :: forall h arch ids -- ^ Function that maps function address to Crucible position -> M.ParsedBlock arch ids -- ^ Block to translate - -> ST h (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) + -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraints archFns $ do mkCrucRegCFG archFns halloc "" $ do let strippedBlock = b { M.pblockTermStmt = termStmtToReturn (M.pblockTermStmt b) } @@ -452,10 +451,10 @@ mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraint -- -- Note that this function takes 'M.ParsedBlock's, which are the blocks -- available in the 'M.DiscoveryFunInfo'. -mkParsedBlockCFG :: forall s arch ids +mkParsedBlockCFG :: forall arch ids . MacawSymbolicArchFunctions arch -- ^ Architecture specific functions. - -> C.HandleAllocator s + -> C.HandleAllocator -- ^ Handle allocator to make the blocks -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Map from region indices to their address @@ -463,15 +462,15 @@ mkParsedBlockCFG :: forall s arch ids -- ^ Function that maps function address to Crucible position -> M.ParsedBlock arch ids -- ^ Block to translate - -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) + -> IO (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) mkParsedBlockCFG archFns halloc memBaseVarMap posFn b = toCoreCFG archFns <$> mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b mkBlockPathRegCFG - :: forall h arch ids + :: forall arch ids . MacawSymbolicArchFunctions arch -- ^ Architecture specific functions. - -> C.HandleAllocator h + -> C.HandleAllocator -- ^ Handle allocator to make the blocks -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Map from region indices to their address @@ -479,7 +478,7 @@ mkBlockPathRegCFG -- ^ Function that maps function address to Crucible position -> [M.ParsedBlock arch ids] -- ^ Bloc path to translate - -> ST h (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) + -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks = crucGenArchConstraints arch_fns $ mkCrucRegCFG arch_fns halloc "" $ do let entry_addr = M.pblockAddr $ head blocks @@ -553,10 +552,10 @@ mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks = init_extra_crucible_blocks ++ concat crucible_blocks) mkBlockPathCFG - :: forall s arch ids + :: forall arch ids . MacawSymbolicArchFunctions arch -- ^ Architecture specific functions. - -> C.HandleAllocator s + -> C.HandleAllocator -- ^ Handle allocator to make the blocks -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Map from region indices to their address @@ -564,7 +563,7 @@ mkBlockPathCFG -- ^ Function that maps function address to Crucible position -> [M.ParsedBlock arch ids] -- ^ Block to translate - -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) + -> IO (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) mkBlockPathCFG arch_fns halloc mem_base_var_map pos_fn blocks = toCoreCFG arch_fns <$> mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks @@ -575,10 +574,10 @@ mkBlockPathCFG arch_fns halloc mem_base_var_map pos_fn blocks = -- This is provided as an alternative to 'mkFunCFG' to allow for post-processing -- of the CFG (e.g., instrumentation) prior to the SSA conversion (which can be -- done using 'toCoreCFG'). -mkFunRegCFG :: forall h arch ids +mkFunRegCFG :: forall arch ids . MacawSymbolicArchFunctions arch -- ^ Architecture specific functions. - -> C.HandleAllocator h + -> C.HandleAllocator -- ^ Handle allocator to make the blocks -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Map from region indices to their address @@ -588,7 +587,7 @@ mkFunRegCFG :: forall h arch ids -- ^ Function that maps function address to Crucible position -> M.DiscoveryFunInfo arch ids -- ^ List of blocks for this region. - -> ST h (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) + -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn = crucGenArchConstraints archFns $ do mkCrucRegCFG archFns halloc nm $ do -- Get entry point address for function @@ -634,10 +633,10 @@ mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn = crucGenArchConstraints ar initExtraCrucibleBlocks ++ concat restCrucibleBlocks) -- | Translate a macaw function (passed as a 'M.DiscoveryFunInfo') into a Crucible 'C.CFG' (in SSA form) -mkFunCFG :: forall s arch ids +mkFunCFG :: forall arch ids . MacawSymbolicArchFunctions arch -- ^ Architecture specific functions. - -> C.HandleAllocator s + -> C.HandleAllocator -- ^ Handle allocator to make the blocks -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Map from region indices to their address @@ -647,7 +646,7 @@ mkFunCFG :: forall s arch ids -- ^ Function that maps function address to Crucible position -> M.DiscoveryFunInfo arch ids -- ^ List of blocks for this region. - -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) + -> IO (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) mkFunCFG archFns halloc memBaseVarMap nm posFn fn = toCoreCFG archFns <$> mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn @@ -877,7 +876,7 @@ runCodeBlock -> MacawSymbolicArchFunctions arch -- ^ Translation functions -> SB.MacawArchEvalFn sym arch - -> C.HandleAllocator RealWorld + -> C.HandleAllocator -> (MM.MemImpl sym, GlobalMap sym (M.ArchAddrWidth arch)) -> LookupFunctionHandle sym arch -> C.CFG (MacawExt arch) blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch) @@ -890,7 +889,7 @@ runCodeBlock (MacawExt arch) (C.RegEntry sym (ArchRegStruct arch))) runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH g regStruct = do - mvar <- stToIO (MM.mkMemVar halloc) + mvar <- MM.mkMemVar halloc let crucRegTypes = crucArchRegTypes archFns let macawStructRepr = C.StructRepr crucRegTypes diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs index f658317d..d59b7ba9 100644 --- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs +++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs @@ -80,7 +80,6 @@ module Data.Macaw.Symbolic.CrucGen import Control.Lens hiding (Empty, (:>)) import Control.Monad ( foldM ) import Control.Monad.Except -import Control.Monad.ST import Control.Monad.State.Strict import Data.Bits import qualified Data.Kind as K @@ -194,17 +193,17 @@ data MacawSymbolicArchFunctions arch -- LOT of memory---TypeReprs were dominating the heap). , crucGenArchRegName :: !(forall tp . M.ArchReg arch tp -> C.SolverSymbol) -- ^ Provides a solver name to use for referring to register. - , crucGenArchFn :: !(forall ids h s tp + , crucGenArchFn :: !(forall ids s tp . M.ArchFn arch (M.Value arch ids) tp - -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp))) + -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))) -- ^ Generate crucible for architecture-specific function. , crucGenArchStmt - :: !(forall ids h s . M.ArchStmt arch (M.Value arch ids) -> CrucGen arch ids h s ()) + :: !(forall ids s . M.ArchStmt arch (M.Value arch ids) -> CrucGen arch ids s ()) -- ^ Generate crucible for architecture-specific statement. - , crucGenArchTermStmt :: !(forall ids h s + , crucGenArchTermStmt :: !(forall ids s . M.ArchTermStmt arch ids -> M.RegState (M.ArchReg arch) (M.Value arch ids) - -> CrucGen arch ids h s ()) + -> CrucGen arch ids s ()) -- ^ Generate crucible for architecture-specific terminal statement. } @@ -570,14 +569,14 @@ instance MacawArchConstraints arch type MemSegmentMap w = Map M.RegionIndex (CR.GlobalVar (C.BVType w)) -- | State used for generating blocks -data CrucGenState arch ids h s +data CrucGenState arch ids s = CrucGenState { translateFns :: !(MacawSymbolicArchFunctions arch) , crucMemBaseAddrMap :: !(MemSegmentMap (M.ArchAddrWidth arch)) -- ^ Map from memory region to base address , crucRegIndexMap :: !(RegIndexMap arch) -- ^ Map from architecture register to Crucible/Macaw index pair. - , crucPState :: !(CrucPersistentState ids h s) + , crucPState :: !(CrucPersistentState ids s) -- ^ State that persists across blocks. , crucRegisterReg :: !(CR.Reg s (ArchRegStruct arch)) , macawPositionFn :: !(M.ArchAddrWord arch -> C.Position) @@ -623,43 +622,43 @@ instance OrdF (BVAtom s) where GTF -> GTF crucPStateLens :: - Simple Lens (CrucGenState arch ids h s) (CrucPersistentState ids h s) + Simple Lens (CrucGenState arch ids s) (CrucPersistentState ids s) crucPStateLens = lens crucPState (\s v -> s { crucPState = v }) toBitsCacheLens :: - Simple Lens (CrucGenState arch ids h s) (MapF (PtrAtom s) (BVAtom s)) + Simple Lens (CrucGenState arch ids s) (MapF (PtrAtom s) (BVAtom s)) toBitsCacheLens = lens toBitsCache (\s v -> s { toBitsCache = v }) fromBitsCacheLens :: - Simple Lens (CrucGenState arch ids h s) (MapF (BVAtom s) (PtrAtom s)) + Simple Lens (CrucGenState arch ids s) (MapF (BVAtom s) (PtrAtom s)) fromBitsCacheLens = lens fromBitsCache (\s v -> s { fromBitsCache = v }) assignValueMapLens :: - Simple Lens (CrucPersistentState ids h s) + Simple Lens (CrucPersistentState ids s) (MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s))) assignValueMapLens = lens assignValueMap (\s v -> s { assignValueMap = v }) -type CrucGenRet arch ids h s = (CrucGenState arch ids h s, CR.TermStmt s (MacawFunctionResult arch)) +type CrucGenRet arch ids s = (CrucGenState arch ids s, CR.TermStmt s (MacawFunctionResult arch)) -- | The Crucible generator monad -- -- This monad provides an environment for constructing Crucible blocks from -- Macaw blocks, including the translation of values while preserving sharing -- and the construction of a control flow graph. -newtype CrucGen arch ids h s r +newtype CrucGen arch ids s r = CrucGen { unCrucGen - :: CrucGenState arch ids h s - -> (CrucGenState arch ids h s + :: CrucGenState arch ids s + -> (CrucGenState arch ids s -> r - -> ST h (CrucGenRet arch ids h s)) - -> ST h (CrucGenRet arch ids h s) + -> IO (CrucGenRet arch ids s)) + -> IO (CrucGenRet arch ids s) } -instance Functor (CrucGen arch ids h s) where +instance Functor (CrucGen arch ids s) where {-# INLINE fmap #-} fmap f m = CrucGen $ \s0 cont -> unCrucGen m s0 $ \s1 v -> cont s1 (f v) -instance Applicative (CrucGen arch ids h s) where +instance Applicative (CrucGen arch ids s) where {-# INLINE pure #-} pure !r = CrucGen $ \s cont -> cont s r {-# INLINE (<*>) #-} @@ -667,26 +666,26 @@ instance Applicative (CrucGen arch ids h s) where $ \s1 f -> unCrucGen ma s1 $ \s2 a -> cont s2 (f a) -instance Monad (CrucGen arch ids h s) where +instance Monad (CrucGen arch ids s) where {-# INLINE (>>=) #-} m >>= h = CrucGen $ \s0 cont -> unCrucGen m s0 $ \s1 r -> unCrucGen (h r) s1 cont -instance MonadState (CrucGenState arch ids h s) (CrucGen arch ids h s) where +instance MonadState (CrucGenState arch ids s) (CrucGen arch ids s) where get = CrucGen $ \s cont -> cont s s put s = CrucGen $ \_ cont -> cont s () -cgExecST :: ST h a -> CrucGen arch ids h s a +cgExecST :: IO a -> CrucGen arch ids s a cgExecST m = CrucGen $ \s cont -> m >>= cont s -- | A NatRepr corresponding to the architecture width. -archAddrWidth :: CrucGen arch ids h s (ArchAddrWidthRepr arch) +archAddrWidth :: CrucGen arch ids s (ArchAddrWidthRepr arch) archAddrWidth = crucGenAddrWidth . translateFns <$> get -- | Get current position -getPos :: CrucGen arch ids h s C.Position +getPos :: CrucGen arch ids s C.Position getPos = gets codePos -addStmt :: CR.Stmt (MacawExt arch) s -> CrucGen arch ids h s () +addStmt :: CR.Stmt (MacawExt arch) s -> CrucGen arch ids s () addStmt stmt = seq stmt $ do p <- getPos s <- get @@ -696,7 +695,7 @@ addStmt stmt = seq stmt $ do put $! s { prevStmts = pstmt : prev } addTermStmt :: CR.TermStmt s (MacawFunctionResult arch) - -> CrucGen arch ids h s a + -> CrucGen arch ids s a addTermStmt tstmt = do CrucGen $ \s _ -> pure (s, tstmt) {- @@ -714,27 +713,27 @@ addTermStmt tstmt = do -- Support a friendlier API such as that of Crucible's Generator -- monad.) addExtraBlock :: CR.Block (MacawExt arch) s (MacawFunctionResult arch) - -> CrucGen arch ids h s () + -> CrucGen arch ids s () addExtraBlock blk = modify' $ \s@(CrucGenState { extraBlocks = blks }) -> s { extraBlocks = blk : blks } -freshValueIndex :: CrucGen arch ids h s (Nonce s tp) +freshValueIndex :: CrucGen arch ids s (Nonce s tp) freshValueIndex = do s <- get let ps = crucPState s let ng = nonceGen ps cgExecST $ freshNonce ng -mmNonceGenerator :: MacawMonad arch ids h s (NonceGenerator (ST h) s) +mmNonceGenerator :: MacawMonad arch ids s (NonceGenerator IO s) mmNonceGenerator = gets nonceGen -mmFreshNonce :: MacawMonad arch ids h s (Nonce s tp) +mmFreshNonce :: MacawMonad arch ids s (Nonce s tp) mmFreshNonce = do ng <- gets nonceGen mmExecST $ freshNonce ng -mkAtom :: C.TypeRepr ctp -> CrucGen arch ids h s (CR.Atom s ctp) +mkAtom :: C.TypeRepr ctp -> CrucGen arch ids s (CR.Atom s ctp) mkAtom tp = do archFns <- gets translateFns crucGenArchConstraints archFns $ do @@ -749,7 +748,7 @@ mkAtom tp = do pure $! atom -- | Evaluate the crucible app and return a reference to the result. -evalAtom :: CR.AtomValue (MacawExt arch) s ctp -> CrucGen arch ids h s (CR.Atom s ctp) +evalAtom :: CR.AtomValue (MacawExt arch) s ctp -> CrucGen arch ids s (CR.Atom s ctp) evalAtom av = do archFns <- gets translateFns crucGenArchConstraints archFns $ do @@ -758,11 +757,11 @@ evalAtom av = do pure atom -- | Evaluate the crucible app and return a reference to the result. -crucibleValue :: C.App (MacawExt arch) (CR.Atom s) ctp -> CrucGen arch ids h s (CR.Atom s ctp) +crucibleValue :: C.App (MacawExt arch) (CR.Atom s) ctp -> CrucGen arch ids s (CR.Atom s ctp) crucibleValue = evalAtom . CR.EvalApp -- | Evaluate a Macaw expression extension -evalMacawExt :: MacawExprExtension arch (CR.Atom s) tp -> CrucGen arch ids h s (CR.Atom s tp) +evalMacawExt :: MacawExprExtension arch (CR.Atom s) tp -> CrucGen arch ids s (CR.Atom s tp) evalMacawExt = crucibleValue . C.ExtensionApp -- | Treat a register value as a bit-vector. @@ -770,7 +769,7 @@ toBits :: (1 <= w) => NatRepr w -> CR.Atom s (MM.LLVMPointerType w) -> - CrucGen arch ids h s (CR.Atom s (C.BVType w)) + CrucGen arch ids s (CR.Atom s (C.BVType w)) toBits w x = use (toBitsCacheLens . atF (PtrAtom x)) >>= \case Just (BVAtom x') -> @@ -786,7 +785,7 @@ fromBits :: (1 <= w) => NatRepr w -> CR.Atom s (C.BVType w) -> - CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w)) + CrucGen arch ids s (CR.Atom s (MM.LLVMPointerType w)) fromBits w x = use (fromBitsCacheLens . atF (BVAtom x)) >>= \case Just (PtrAtom x') -> @@ -797,12 +796,12 @@ fromBits w x = assign (toBitsCacheLens . atF (PtrAtom x')) (Just (BVAtom x)) return x' -getRegs :: CrucGen arch ids h s (CR.Atom s (ArchRegStruct arch)) +getRegs :: CrucGen arch ids s (CR.Atom s (ArchRegStruct arch)) getRegs = gets crucRegisterReg >>= evalAtom . CR.ReadReg -- | Return the value associated with the given register getRegValue :: M.ArchReg arch tp - -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp)) + -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp)) getRegValue r = do archFns <- gets translateFns idxMap <- gets crucRegIndexMap @@ -816,25 +815,25 @@ getRegValue r = do crucibleValue (C.GetStruct regStruct (crucibleIndex idx) tp) v2c :: M.Value arch ids tp - -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp)) + -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp)) v2c = valueToCrucible v2c' :: (1 <= w) => NatRepr w -> M.Value arch ids (M.BVType w) -> - CrucGen arch ids h s (CR.Atom s (C.BVType w)) + CrucGen arch ids s (CR.Atom s (C.BVType w)) v2c' w x = toBits w =<< valueToCrucible x -- | Evaluate the crucible app and return a reference to the result. appAtom :: C.App (MacawExt arch) (CR.Atom s) ctp -> - CrucGen arch ids h s (CR.Atom s ctp) + CrucGen arch ids s (CR.Atom s ctp) appAtom app = evalAtom (CR.EvalApp app) appBVAtom :: (1 <= w) => NatRepr w -> C.App (MacawExt arch) (CR.Atom s) (C.BVType w) -> - CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w)) + CrucGen arch ids s (CR.Atom s (MM.LLVMPointerType w)) appBVAtom w app = fromBits w =<< appAtom app addLemma :: (1 <= x, x + 1 <= y) => NatRepr x -> q y -> LeqProof 1 y @@ -848,7 +847,7 @@ addLemma x y = -- | Create a crucible value for a bitvector literal. -bvLit :: (1 <= w) => NatRepr w -> Integer -> CrucGen arch ids h s (CR.Atom s (C.BVType w)) +bvLit :: (1 <= w) => NatRepr w -> Integer -> CrucGen arch ids s (CR.Atom s (C.BVType w)) bvLit w i = crucibleValue (C.BVLit w (i .&. maxUnsigned w)) bitOp2 :: (1 <= w) @@ -858,14 +857,14 @@ bitOp2 :: (1 <= w) -> C.App (MacawExt arch) (CR.Atom s) (C.BVType w)) -> M.Value arch ids (M.BVType w) -> M.Value arch ids (M.BVType w) - -> CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w)) + -> CrucGen arch ids s (CR.Atom s (MM.LLVMPointerType w)) bitOp2 w f x y = fromBits w =<< appAtom =<< f <$> v2c' w x <*> v2c' w y appToCrucible - :: forall arch ids h s tp + :: forall arch ids s tp . M.App (M.Value arch ids) tp - -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp)) + -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp)) appToCrucible app = do archFns <- gets translateFns crucGenArchConstraints archFns $ do @@ -1050,7 +1049,7 @@ appToCrucible app = do let bvBit :: (1 <= i, i <= n) => NatRepr i - -> CrucGen arch ids h s (CR.Atom s (C.BVType n)) + -> CrucGen arch ids s (CR.Atom s (C.BVType n)) bvBit i | Refl <- minusPlusCancel i (knownNat @1) = do b <- appAtom $ C.BVSelect (subNat i (knownNat @1)) (knownNat @1) w x' @@ -1094,7 +1093,7 @@ countZeros :: (1 <= w) => NatRepr w -> (NatRepr w -> CR.Atom s (C.BVType w) -> CR.Atom s (C.BVType w) -> C.App (MacawExt arch) (CR.Atom s) (C.BVType w)) -> M.Value arch ids (M.BVType w) -> - CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w)) + CrucGen arch ids s (CR.Atom s (MM.LLVMPointerType w)) countZeros w f vx = do cx <- v2c vx >>= toBits w isZeros <- forM [0..intValue w-1] $ \i -> do @@ -1111,7 +1110,7 @@ countZeros w f vx = do -- -- This is in the 'CrucGen' monad so that it can preserve sharing in terms. valueToCrucible :: M.Value arch ids tp - -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp)) + -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp)) valueToCrucible v = do archFns <- gets translateFns crucGenArchConstraints archFns $ do @@ -1138,21 +1137,21 @@ valueToCrucible v = do -- | Create a fresh symbolic value of the given type. freshSymbolic :: M.TypeRepr tp - -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp)) + -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp)) freshSymbolic repr = evalMacawStmt (MacawFreshSymbolic repr) evalMacawStmt :: MacawStmtExtension arch (CR.Atom s) tp -> - CrucGen arch ids h s (CR.Atom s tp) + CrucGen arch ids s (CR.Atom s tp) evalMacawStmt = evalAtom . CR.EvalExt -- | Embed an architecture-specific Macaw statement into a Crucible program -- -- All architecture-specific statements return values (which can be unit). -evalArchStmt :: MacawArchStmtExtension arch (CR.Atom s) tp -> CrucGen arch ids h s (CR.Atom s tp) +evalArchStmt :: MacawArchStmtExtension arch (CR.Atom s) tp -> CrucGen arch ids s (CR.Atom s tp) evalArchStmt = evalMacawStmt . MacawArchStmtExtension assignRhsToCrucible :: M.AssignRhs arch (M.Value arch ids) tp - -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp)) + -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp)) assignRhsToCrucible rhs = gets translateFns >>= \archFns -> crucGenArchConstraints archFns $ @@ -1173,7 +1172,7 @@ assignRhsToCrucible rhs = fns <- translateFns <$> get crucGenArchFn fns f -addMacawStmt :: forall arch ids h s . M.ArchSegmentOff arch -> M.Stmt arch ids -> CrucGen arch ids h s () +addMacawStmt :: forall arch ids s . M.ArchSegmentOff arch -> M.Stmt arch ids -> CrucGen arch ids s () addMacawStmt baddr stmt = gets translateFns >>= \archFns -> crucGenArchConstraints archFns $ @@ -1213,9 +1212,9 @@ addMacawStmt baddr stmt = void $ evalMacawStmt crucStmt -- | Create a crucible struct for registers from a register state. -createRegStruct :: forall arch ids h s +createRegStruct :: forall arch ids s . M.RegState (M.ArchReg arch) (M.Value arch ids) - -> CrucGen arch ids h s (CR.Atom s (ArchRegStruct arch)) + -> CrucGen arch ids s (CR.Atom s (ArchRegStruct arch)) createRegStruct regs = do archFns <- gets translateFns @@ -1233,9 +1232,9 @@ createRegStruct regs = do updates <- createRegUpdates regs foldM addUpdate startingVals updates -createRegUpdates :: forall arch ids h s +createRegUpdates :: forall arch ids s . M.RegState (M.ArchReg arch) (M.Value arch ids) - -> CrucGen arch ids h s + -> CrucGen arch ids s [Pair (Ctx.Index (MacawCrucibleRegTypes arch)) (CR.Atom s)] createRegUpdates regs = do archFns <- gets translateFns @@ -1249,7 +1248,7 @@ createRegUpdates regs = do Just idx -> Just . Pair (crucibleIndex idx) <$> valueToCrucible val addMacawTermStmt :: M.TermStmt arch ids - -> CrucGen arch ids h s () + -> CrucGen arch ids s () addMacawTermStmt tstmt = case tstmt of M.FetchAndExecute regs -> do @@ -1265,24 +1264,24 @@ addMacawTermStmt tstmt = ----------------- -- | Monad for adding new blocks to a state. -newtype MacawMonad arch ids h s a - = MacawMonad ( ExceptT String (StateT (CrucPersistentState ids h s) (ST h)) a) +newtype MacawMonad arch ids s a + = MacawMonad ( ExceptT String (StateT (CrucPersistentState ids s) IO) a) deriving ( Functor , Applicative , Monad , MonadError String - , MonadState (CrucPersistentState ids h s) + , MonadState (CrucPersistentState ids s) ) -runMacawMonad :: CrucPersistentState ids h s - -> MacawMonad arch ids h s a - -> ST h (Either String a, CrucPersistentState ids h s) +runMacawMonad :: CrucPersistentState ids s + -> MacawMonad arch ids s a + -> IO (Either String a, CrucPersistentState ids s) runMacawMonad s (MacawMonad m) = runStateT (runExceptT m) s -mmExecST :: ST h a -> MacawMonad arch ids h s a +mmExecST :: IO a -> MacawMonad arch ids s a mmExecST = MacawMonad . lift . lift -runCrucGen :: forall arch ids h s +runCrucGen :: forall arch ids s . MacawSymbolicArchFunctions arch -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Base address map @@ -1292,8 +1291,8 @@ runCrucGen :: forall arch ids h s -- ^ Label for this block -> CR.Reg s (ArchRegStruct arch) -- ^ Crucible register for struct containing all Macaw registers. - -> CrucGen arch ids h s () - -> MacawMonad arch ids h s + -> CrucGen arch ids s () + -> MacawMonad arch ids s ( CR.Block (MacawExt arch ) s (MacawFunctionResult arch) -- Block created , [CR.Block (MacawExt arch) s (MacawFunctionResult arch)] @@ -1338,7 +1337,7 @@ addMacawBlock :: M.MemWidth (M.ArchAddrWidth arch) -> (M.ArchAddrWord arch -> C.Position) -- ^ Function for generating position from offset from start of this block. -> M.Block arch ids - -> MacawMonad arch ids h s + -> MacawMonad arch ids s ( CR.Block (MacawExt arch) s (MacawFunctionResult arch) , [CR.Block (MacawExt arch) s (MacawFunctionResult arch)] ) @@ -1372,7 +1371,7 @@ parsedBlockLabel blockLabelMap addr = -- | DO NOT CALL THIS FROM USER CODE. We count on the registers not -- changing until the end of the block. -setMachineRegs :: CR.Atom s (ArchRegStruct arch) -> CrucGen arch ids h s () +setMachineRegs :: CR.Atom s (ArchRegStruct arch) -> CrucGen arch ids s () setMachineRegs newRegs = do regReg <- gets crucRegisterReg addStmt $ CR.SetReg regReg newRegs @@ -1385,7 +1384,7 @@ addMacawParsedTermStmt :: BlockLabelMap arch s -> M.ArchSegmentOff arch -- ^ Address of this block -> M.ParsedTermStmt arch ids - -> CrucGen arch ids h s () + -> CrucGen arch ids s () addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do archFns <- translateFns <$> get crucGenArchConstraints archFns $ do @@ -1435,11 +1434,11 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do msgVal <- crucibleValue $ C.TextLit $ Text.pack $ "Could not identify block at " ++ show thisAddr addTermStmt $ CR.ErrorStmt msgVal -addSwitch :: forall arch s ids h +addSwitch :: forall arch s ids . BlockLabelMap arch s -> M.ArchAddrValue arch ids -> Vec.Vector (M.ArchSegmentOff arch) - -> CrucGen arch ids h s () + -> CrucGen arch ids s () addSwitch blockLabelMap idx possibleAddrs = do archFns <- translateFns <$> get crucGenArchConstraints archFns $ do @@ -1468,7 +1467,7 @@ addSwitch blockLabelMap idx possibleAddrs = do , CR.TermStmt s (MacawFunctionResult arch) ) -> ( Int , M.ArchSegmentOff arch ) - -> CrucGen arch ids h s + -> CrucGen arch ids s ( [CR.Stmt (MacawExt arch) s] , CR.TermStmt s (MacawFunctionResult arch) ) chain (elsStmts, elsTerm) (thnIdx, thnAddr) = do @@ -1524,7 +1523,7 @@ addSwitch blockLabelMap idx possibleAddrs = do mapM_ addStmt stmts addTermStmt termStmt -addParsedBlock :: forall arch ids h s +addParsedBlock :: forall arch ids s . MacawSymbolicArchFunctions arch -> MemSegmentMap (M.ArchAddrWidth arch) -- ^ Base address map @@ -1535,7 +1534,7 @@ addParsedBlock :: forall arch ids h s -> CR.Reg s (ArchRegStruct arch) -- ^ Register that stores Macaw registers -> M.ParsedBlock arch ids - -> MacawMonad arch ids h s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)] + -> MacawMonad arch ids s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)] addParsedBlock archFns memSegMap blockLabelMap posFn regReg macawBlock = do crucGenArchConstraints archFns $ do let base = M.pblockAddr macawBlock diff --git a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs index 5c422f58..3b81d10d 100644 --- a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs +++ b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs @@ -44,7 +44,6 @@ module Data.Macaw.Symbolic.PersistentState ) where -import Control.Monad.ST (ST) import qualified Data.Kind as K import qualified Data.Macaw.CFG as M import qualified Data.Macaw.Types as M @@ -227,9 +226,9 @@ instance TraversableFC MacawCrucibleValue where -- CrucPersistentState -- | State that needs to be persisted across block translations -data CrucPersistentState ids h s +data CrucPersistentState ids s = CrucPersistentState - { nonceGen :: NonceGenerator (ST h) s + { nonceGen :: NonceGenerator IO s -- ^ Generator used to get fresh ids for Crucible atoms. , assignValueMap :: !(MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s))) @@ -237,8 +236,8 @@ data CrucPersistentState ids h s } -- | Initial crucible persistent state -initCrucPersistentState :: NonceGenerator (ST h) s - -> CrucPersistentState ids h s +initCrucPersistentState :: NonceGenerator IO s + -> CrucPersistentState ids s initCrucPersistentState ng = CrucPersistentState { nonceGen = ng From 48c3ba1fed6c3b4acaa475ef7f863b3de55e68ee Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 19 Jul 2019 09:40:24 -0700 Subject: [PATCH 2/5] [symbolic] additional nonce-related adjustments from 'ST h' to 'IO'. --- symbolic/src/Data/Macaw/Symbolic.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs index 2285d1f4..eb75ae6a 100644 --- a/symbolic/src/Data/Macaw/Symbolic.hs +++ b/symbolic/src/Data/Macaw/Symbolic.hs @@ -222,22 +222,22 @@ type SymArchConstraints arch = -- Useful as an alternative to 'mkCrucCFG' if post-processing is -- desired (as this is easier to do with the registerized form); use -- 'toCoreCFG' to finish. -mkCrucRegCFG :: forall h arch ids +mkCrucRegCFG :: forall arch ids . MacawSymbolicArchFunctions arch -- ^ Crucible architecture-specific functions. - -> C.HandleAllocator h + -> C.HandleAllocator -- ^ Handle allocator to make function handles -> C.FunctionName -- ^ Name of function for pretty print purposes. - -> (forall s. MacawMonad arch ids h s (CR.Label s, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)])) + -> (forall s. MacawMonad arch ids s (CR.Label s, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)])) -- ^ Action to run - -> ST h (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) + -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)) mkCrucRegCFG archFns halloc nm action = do let crucRegTypes = crucArchRegTypes archFns let macawStructRepr = C.StructRepr crucRegTypes let argTypes = Empty :> macawStructRepr h <- C.mkHandle' halloc nm argTypes macawStructRepr - Some (ng :: NonceGenerator (ST h) s) <- newSTNonceGenerator + Some (ng :: NonceGenerator IO s) <- newIONonceGenerator let ps0 = initCrucPersistentState ng blockRes <- runMacawMonad ps0 action (entry, blks) <- From 1b4c11550fb356b1a88f34a8b6d019cc0ecd7fdb Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 19 Jul 2019 10:23:19 -0700 Subject: [PATCH 3/5] Update crucible dependency. --- deps/crucible | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/crucible b/deps/crucible index 0a7c3aff..847bd2d1 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 0a7c3afff84b3c34555c0812f15308bc5bf04c55 +Subproject commit 847bd2d1cd792f9dfa21a6fa58b7be50d7e46c19 From 40eff5802c32e52a5894515797b6f56160468ff8 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 19 Jul 2019 13:15:44 -0700 Subject: [PATCH 4/5] [x86_symbolic] updates for crucible nonce change from (ST h) to IO Changes for compatibility with Crucible pull request 285 (https://github.com/GaloisInc/crucible/pull/285) and the corresponding changes in macaw symbolic. --- x86_symbolic/src/Data/Macaw/X86/Symbolic.hs | 14 +++++++------- x86_symbolic/tests/Main.hs | 4 ++-- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs index 2d1747a5..a4fb8baf 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs @@ -276,27 +276,27 @@ instance TraversableFC X86StmtExtension where type instance MacawArchStmtExtension M.X86_64 = X86StmtExtension -crucGenX86Fn :: forall ids h s tp. M.X86PrimFn (M.Value M.X86_64 ids) tp - -> CrucGen M.X86_64 ids h s (C.Atom s (ToCrucibleType tp)) +crucGenX86Fn :: forall ids s tp. M.X86PrimFn (M.Value M.X86_64 ids) tp + -> CrucGen M.X86_64 ids s (C.Atom s (ToCrucibleType tp)) crucGenX86Fn fn = do - let f :: M.Value arch ids a -> CrucGen arch ids h s (AtomWrapper (C.Atom s) a) + let f :: M.Value arch ids a -> CrucGen arch ids s (AtomWrapper (C.Atom s) a) f x = AtomWrapper <$> valueToCrucible x r <- traverseFC f fn evalArchStmt (X86PrimFn r) -crucGenX86Stmt :: forall ids h s +crucGenX86Stmt :: forall ids s . M.X86Stmt (M.Value M.X86_64 ids) - -> CrucGen M.X86_64 ids h s () + -> CrucGen M.X86_64 ids s () crucGenX86Stmt stmt = do - let f :: M.Value M.X86_64 ids a -> CrucGen M.X86_64 ids h s (AtomWrapper (C.Atom s) a) + let f :: M.Value M.X86_64 ids a -> CrucGen M.X86_64 ids s (AtomWrapper (C.Atom s) a) f x = AtomWrapper <$> valueToCrucible x stmt' <- traverseF f stmt void (evalArchStmt (X86PrimStmt stmt')) crucGenX86TermStmt :: M.X86TermStmt ids -> M.RegState M.X86Reg (M.Value M.X86_64 ids) - -> CrucGen M.X86_64 ids h s () + -> CrucGen M.X86_64 ids s () crucGenX86TermStmt tstmt _regs = void (evalArchStmt (X86PrimTerm tstmt)) diff --git a/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs index 37ffce72..2bebf26b 100644 --- a/x86_symbolic/tests/Main.hs +++ b/x86_symbolic/tests/Main.hs @@ -95,7 +95,7 @@ main = do [] -> fail "Could not find add function" _ -> fail "Found multiple add functions" - memBaseVar <- stToIO $ C.freshGlobalVar halloc "add_mem_base" C.knownRepr + memBaseVar <- C.freshGlobalVar halloc "add_mem_base" C.knownRepr let memBaseVarMap :: MS.MemSegmentMap 64 memBaseVarMap = Map.singleton 1 memBaseVar @@ -113,7 +113,7 @@ main = do putStrLn $ "Analyzing " ++ show addr (_, Some funInfo) <- stToIO $ M.analyzeFunction logFn addAddr M.UserRequest ds0 - C.SomeCFG g <- stToIO $ MS.mkFunCFG x86ArchFns halloc memBaseVarMap "add" posFn funInfo + C.SomeCFG g <- MS.mkFunCFG x86ArchFns halloc memBaseVarMap "add" posFn funInfo regs <- MS.macawAssignToCrucM (mkReg x86ArchFns sym) (MS.crucGenRegAssignment x86ArchFns) From eb93bb4e3a9455c1ea766c21cafd30a496c4d970 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Fri, 19 Jul 2019 13:19:14 -0700 Subject: [PATCH 5/5] [ppc-symbolic] updates for crucible nonce change from (ST h) to IO Changes for compatibility with Crucible pull request 285 (https://github.com/GaloisInc/crucible/pull/285) and the corresponding changes in macaw symbolic. --- .../src/Data/Macaw/PPC/Symbolic.hs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs index 6df43d46..590602e7 100644 --- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs @@ -247,31 +247,31 @@ archUpdateReg regEntry reg val = Nothing -> error $ "unexpected register: " ++ show (MC.prettyF reg) -ppcGenFn :: forall ids h s tp v ppc +ppcGenFn :: forall ids s tp v ppc . ( ppc ~ MP.AnyPPC v ) => MP.PPCPrimFn ppc (MC.Value ppc ids) tp - -> MSB.CrucGen ppc ids h s (C.Atom s (MS.ToCrucibleType tp)) + -> MSB.CrucGen ppc ids s (C.Atom s (MS.ToCrucibleType tp)) ppcGenFn fn = do - let f :: MC.Value ppc ids a -> MSB.CrucGen ppc ids h s (A.AtomWrapper (C.Atom s) a) + let f :: MC.Value ppc ids a -> MSB.CrucGen ppc ids s (A.AtomWrapper (C.Atom s) a) f x = A.AtomWrapper <$> MSB.valueToCrucible x r <- FC.traverseFC f fn MSB.evalArchStmt (PPCPrimFn r) -ppcGenStmt :: forall v ids h s ppc +ppcGenStmt :: forall v ids s ppc . ( ppc ~ MP.AnyPPC v ) => MP.PPCStmt ppc (MC.Value ppc ids) - -> MSB.CrucGen ppc ids h s () + -> MSB.CrucGen ppc ids s () ppcGenStmt s = do - let f :: MC.Value ppc ids a -> MSB.CrucGen ppc ids h s (A.AtomWrapper (C.Atom s) a) + let f :: MC.Value ppc ids a -> MSB.CrucGen ppc ids s (A.AtomWrapper (C.Atom s) a) f x = A.AtomWrapper <$> MSB.valueToCrucible x s' <- TF.traverseF f s void (MSB.evalArchStmt (PPCPrimStmt s')) -ppcGenTermStmt :: forall v ids h s ppc +ppcGenTermStmt :: forall v ids s ppc . ( ppc ~ MP.AnyPPC v ) => MP.PPCTermStmt ids -> MC.RegState (MP.PPCReg ppc) (MC.Value ppc ids) - -> MSB.CrucGen ppc ids h s () + -> MSB.CrucGen ppc ids s () ppcGenTermStmt ts _rs = void (MSB.evalArchStmt (PPCPrimTerm ts))