GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-18 11:31:35 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #60 from GaloisInc/nonce_handle_deparameterize

Browse Source 
Nonce handle deparameterize
This commit is contained in:
Kevin Quick 2019-07-21 22:53:58 -07:00 committed by GitHub
commit 1c25aa59b6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 135 additions and 138 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
deps/crucible vendored

@ -1 +1 @@
Subproject commit 0a7c3afff84b3c34555c0812f15308bc5bf04c55 Subproject commit 847bd2d1cd792f9dfa21a6fa58b7be50d7e46c19

16
macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
View File

@ -247,31 +247,31 @@ archUpdateReg regEntry reg val =
Nothing -> error $ "unexpected register: " ++ show (MC.prettyF reg) 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 ) . ( ppc ~ MP.AnyPPC v )
=> MP.PPCPrimFn ppc (MC.Value ppc ids) tp => 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 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 f x = A.AtomWrapper <$> MSB.valueToCrucible x
r <- FC.traverseFC f fn r <- FC.traverseFC f fn
MSB.evalArchStmt (PPCPrimFn r) MSB.evalArchStmt (PPCPrimFn r)
ppcGenStmt :: forall v ids h s ppc ppcGenStmt :: forall v ids s ppc
. ( ppc ~ MP.AnyPPC v ) . ( ppc ~ MP.AnyPPC v )
=> MP.PPCStmt ppc (MC.Value ppc ids) => MP.PPCStmt ppc (MC.Value ppc ids)
-> MSB.CrucGen ppc ids h s () -> MSB.CrucGen ppc ids s ()
ppcGenStmt s = do 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 f x = A.AtomWrapper <$> MSB.valueToCrucible x
s' <- TF.traverseF f s s' <- TF.traverseF f s
void (MSB.evalArchStmt (PPCPrimStmt s')) void (MSB.evalArchStmt (PPCPrimStmt s'))
ppcGenTermStmt :: forall v ids h s ppc ppcGenTermStmt :: forall v ids s ppc
. ( ppc ~ MP.AnyPPC v ) . ( ppc ~ MP.AnyPPC v )
=> MP.PPCTermStmt ids => MP.PPCTermStmt ids
-> MC.RegState (MP.PPCReg ppc) (MC.Value ppc ids) -> MC.RegState (MP.PPCReg ppc) (MC.Value ppc ids)
-> MSB.CrucGen ppc ids h s () -> MSB.CrucGen ppc ids s ()
ppcGenTermStmt ts _rs = ppcGenTermStmt ts _rs =
void (MSB.evalArchStmt (PPCPrimTerm ts)) void (MSB.evalArchStmt (PPCPrimTerm ts))

73
symbolic/src/Data/Macaw/Symbolic.hs
View File

@ -111,13 +111,12 @@ import GHC.TypeLits
import Control.Lens ((^.)) import Control.Lens ((^.))
import Control.Monad import Control.Monad
import Control.Monad.IO.Class import Control.Monad.IO.Class
import Control.Monad.ST (ST, RealWorld, stToIO)
import Data.Foldable import Data.Foldable
import qualified Data.Map.Strict as Map import qualified Data.Map.Strict as Map
import Data.Maybe import Data.Maybe
import Data.Parameterized.Context (EmptyCtx, (::>), pattern Empty, pattern (:>)) import Data.Parameterized.Context (EmptyCtx, (::>), pattern Empty, pattern (:>))
import qualified Data.Parameterized.Context as Ctx 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 Data.Parameterized.Some ( Some(Some) )
import qualified Data.Parameterized.TraversableFC as FC import qualified Data.Parameterized.TraversableFC as FC
import qualified Data.Vector as V import qualified Data.Vector as V
@ -225,22 +224,22 @@ type SymArchConstraints arch =
-- Useful as an alternative to 'mkCrucCFG' if post-processing is -- Useful as an alternative to 'mkCrucCFG' if post-processing is
-- desired (as this is easier to do with the registerized form); use -- desired (as this is easier to do with the registerized form); use
-- 'toCoreCFG' to finish. -- 'toCoreCFG' to finish.
mkCrucRegCFG :: forall h arch ids mkCrucRegCFG :: forall arch ids
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-- ^ Crucible architecture-specific functions. -- ^ Crucible architecture-specific functions.
-> C.HandleAllocator h -> C.HandleAllocator
-- ^ Handle allocator to make function handles -- ^ Handle allocator to make function handles
-> C.FunctionName -> C.FunctionName
-- ^ Name of function for pretty print purposes. -- ^ 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 -- ^ 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 mkCrucRegCFG archFns halloc nm action = do
let crucRegTypes = crucArchRegTypes archFns let crucRegTypes = crucArchRegTypes archFns
let macawStructRepr = C.StructRepr crucRegTypes let macawStructRepr = C.StructRepr crucRegTypes
let argTypes = Empty :> macawStructRepr let argTypes = Empty :> macawStructRepr
h <- C.mkHandle' halloc nm argTypes 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 let ps0 = initCrucPersistentState ng
blockRes <- runMacawMonad ps0 action blockRes <- runMacawMonad ps0 action
(entry, blks) <- (entry, blks) <-
@ -257,7 +256,7 @@ mkCrucRegCFG archFns halloc nm action = do
pure $ CR.SomeCFG rg pure $ CR.SomeCFG rg
-- | Create a Crucible CFG from a list of blocks -- | Create a Crucible CFG from a list of blocks
addBlocksCFG :: forall h s arch ids addBlocksCFG :: forall s arch ids
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-- ^ Crucible specific functions. -- ^ Crucible specific functions.
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
@ -268,7 +267,7 @@ addBlocksCFG :: forall h s arch ids
-- ^ Function that maps offsets from start of block to Crucible position. -- ^ Function that maps offsets from start of block to Crucible position.
-> M.Block arch ids -> M.Block arch ids
-- ^ Macaw block for this region. -- ^ 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 addBlocksCFG archFns baseAddrMap addr posFn macawBlock = do
crucGenArchConstraints archFns $ do crucGenArchConstraints archFns $ do
-- Map block map to Crucible CFG -- Map block map to Crucible CFG
@ -285,10 +284,10 @@ addBlocksCFG archFns baseAddrMap addr posFn macawBlock = do
-- --
-- Also note that any 'M.FetchAndExecute' terminators are turned into Crucible -- Also note that any 'M.FetchAndExecute' terminators are turned into Crucible
-- return statements. -- return statements.
mkBlocksRegCFG :: forall s arch ids mkBlocksRegCFG :: forall arch ids
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-- ^ Crucible specific functions. -- ^ Crucible specific functions.
-> C.HandleAllocator s -> C.HandleAllocator
-- ^ Handle allocator to make the blocks -- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address -- ^ Map from region indices to their address
@ -300,7 +299,7 @@ mkBlocksRegCFG :: forall s arch ids
-- ^ Function that maps offsets from start of block to Crucible position. -- ^ Function that maps offsets from start of block to Crucible position.
-> M.Block arch ids -> M.Block arch ids
-- ^ List of blocks for this region. -- ^ 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 mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock = do
mkCrucRegCFG archFns halloc nm $ do mkCrucRegCFG archFns halloc nm $ do
addBlocksCFG archFns memBaseVarMap addr posFn macawBlock addBlocksCFG archFns memBaseVarMap addr posFn macawBlock
@ -314,10 +313,10 @@ mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock = do
-- --
-- Also note that any 'M.FetchAndExecute' terminators are turned into Crucible -- Also note that any 'M.FetchAndExecute' terminators are turned into Crucible
-- return statements. -- return statements.
mkBlocksCFG :: forall s arch ids mkBlocksCFG :: forall arch ids
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-- ^ Crucible specific functions. -- ^ Crucible specific functions.
-> C.HandleAllocator s -> C.HandleAllocator
-- ^ Handle allocator to make the blocks -- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address -- ^ Map from region indices to their address
@ -329,15 +328,15 @@ mkBlocksCFG :: forall s arch ids
-- ^ Function that maps offsets from start of block to Crucible position. -- ^ Function that maps offsets from start of block to Crucible position.
-> M.Block arch ids -> M.Block arch ids
-- ^ List of blocks for this region. -- ^ 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 = mkBlocksCFG archFns halloc memBaseVarMap nm addr posFn macawBlock =
toCoreCFG archFns <$> toCoreCFG archFns <$>
mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock
-- | Create a map from Macaw @(address, index)@ pairs to Crucible labels -- | 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 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 insBlock m b = do
let base = M.pblockAddr b let base = M.pblockAddr b
n <- mmFreshNonce n <- mmFreshNonce
@ -388,10 +387,10 @@ termStmtToJump tm0 addr =
-- This is useful as an alternative to 'mkParsedBlockCFG' if post-processing is -- This is useful as an alternative to 'mkParsedBlockCFG' if post-processing is
-- desired (as this is easier on the registerized form). Use 'toCoreCFG' to -- desired (as this is easier on the registerized form). Use 'toCoreCFG' to
-- finish by translating the registerized CFG to SSA. -- finish by translating the registerized CFG to SSA.
mkParsedBlockRegCFG :: forall h arch ids mkParsedBlockRegCFG :: forall arch ids
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions. -- ^ Architecture specific functions.
-> C.HandleAllocator h -> C.HandleAllocator
-- ^ Handle allocator to make the blocks -- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address -- ^ Map from region indices to their address
@ -399,7 +398,7 @@ mkParsedBlockRegCFG :: forall h arch ids
-- ^ Function that maps function address to Crucible position -- ^ Function that maps function address to Crucible position
-> M.ParsedBlock arch ids -> M.ParsedBlock arch ids
-- ^ Block to translate -- ^ 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 mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraints archFns $ do
mkCrucRegCFG archFns halloc "" $ do mkCrucRegCFG archFns halloc "" $ do
let strippedBlock = b { M.pblockTermStmt = termStmtToReturn (M.pblockTermStmt b) } let strippedBlock = b { M.pblockTermStmt = termStmtToReturn (M.pblockTermStmt b) }
@ -454,10 +453,10 @@ mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraint
-- --
-- Note that this function takes 'M.ParsedBlock's, which are the blocks -- Note that this function takes 'M.ParsedBlock's, which are the blocks
-- available in the 'M.DiscoveryFunInfo'. -- available in the 'M.DiscoveryFunInfo'.
mkParsedBlockCFG :: forall s arch ids mkParsedBlockCFG :: forall arch ids
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions. -- ^ Architecture specific functions.
-> C.HandleAllocator s -> C.HandleAllocator
-- ^ Handle allocator to make the blocks -- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address -- ^ Map from region indices to their address
@ -465,15 +464,15 @@ mkParsedBlockCFG :: forall s arch ids
-- ^ Function that maps function address to Crucible position -- ^ Function that maps function address to Crucible position
-> M.ParsedBlock arch ids -> M.ParsedBlock arch ids
-- ^ Block to translate -- ^ 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 = mkParsedBlockCFG archFns halloc memBaseVarMap posFn b =
toCoreCFG archFns <$> mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b toCoreCFG archFns <$> mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b
mkBlockPathRegCFG mkBlockPathRegCFG
:: forall h arch ids :: forall arch ids
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions. -- ^ Architecture specific functions.
-> C.HandleAllocator h -> C.HandleAllocator
-- ^ Handle allocator to make the blocks -- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address -- ^ Map from region indices to their address
@ -481,7 +480,7 @@ mkBlockPathRegCFG
-- ^ Function that maps function address to Crucible position -- ^ Function that maps function address to Crucible position
-> [M.ParsedBlock arch ids] -> [M.ParsedBlock arch ids]
-- ^ Bloc path to translate -- ^ 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 = mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks =
crucGenArchConstraints arch_fns $ mkCrucRegCFG arch_fns halloc "" $ do crucGenArchConstraints arch_fns $ mkCrucRegCFG arch_fns halloc "" $ do
let entry_addr = M.pblockAddr $ head blocks let entry_addr = M.pblockAddr $ head blocks
@ -555,10 +554,10 @@ mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks =
init_extra_crucible_blocks ++ concat crucible_blocks) init_extra_crucible_blocks ++ concat crucible_blocks)
mkBlockPathCFG mkBlockPathCFG
:: forall s arch ids :: forall arch ids
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions. -- ^ Architecture specific functions.
-> C.HandleAllocator s -> C.HandleAllocator
-- ^ Handle allocator to make the blocks -- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address -- ^ Map from region indices to their address
@ -566,7 +565,7 @@ mkBlockPathCFG
-- ^ Function that maps function address to Crucible position -- ^ Function that maps function address to Crucible position
-> [M.ParsedBlock arch ids] -> [M.ParsedBlock arch ids]
-- ^ Block to translate -- ^ 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 = mkBlockPathCFG arch_fns halloc mem_base_var_map pos_fn blocks =
toCoreCFG arch_fns <$> toCoreCFG arch_fns <$>
mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks
@ -577,10 +576,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 -- 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 -- of the CFG (e.g., instrumentation) prior to the SSA conversion (which can be
-- done using 'toCoreCFG'). -- done using 'toCoreCFG').
mkFunRegCFG :: forall h arch ids mkFunRegCFG :: forall arch ids
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions. -- ^ Architecture specific functions.
-> C.HandleAllocator h -> C.HandleAllocator
-- ^ Handle allocator to make the blocks -- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address -- ^ Map from region indices to their address
@ -590,7 +589,7 @@ mkFunRegCFG :: forall h arch ids
-- ^ Function that maps function address to Crucible position -- ^ Function that maps function address to Crucible position
-> M.DiscoveryFunInfo arch ids -> M.DiscoveryFunInfo arch ids
-- ^ List of blocks for this region. -- ^ 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 mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn = crucGenArchConstraints archFns $ do
mkCrucRegCFG archFns halloc nm $ do mkCrucRegCFG archFns halloc nm $ do
-- Get entry point address for function -- Get entry point address for function
@ -636,10 +635,10 @@ mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn = crucGenArchConstraints ar
initExtraCrucibleBlocks ++ concat restCrucibleBlocks) initExtraCrucibleBlocks ++ concat restCrucibleBlocks)
-- | Translate a macaw function (passed as a 'M.DiscoveryFunInfo') into a Crucible 'C.CFG' (in SSA form) -- | 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 . MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions. -- ^ Architecture specific functions.
-> C.HandleAllocator s -> C.HandleAllocator
-- ^ Handle allocator to make the blocks -- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address -- ^ Map from region indices to their address
@ -649,7 +648,7 @@ mkFunCFG :: forall s arch ids
-- ^ Function that maps function address to Crucible position -- ^ Function that maps function address to Crucible position
-> M.DiscoveryFunInfo arch ids -> M.DiscoveryFunInfo arch ids
-- ^ List of blocks for this region. -- ^ 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 = mkFunCFG archFns halloc memBaseVarMap nm posFn fn =
toCoreCFG archFns <$> mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn toCoreCFG archFns <$> mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn
@ -879,7 +878,7 @@ runCodeBlock
-> MacawSymbolicArchFunctions arch -> MacawSymbolicArchFunctions arch
-- ^ Translation functions -- ^ Translation functions
-> SB.MacawArchEvalFn sym arch -> SB.MacawArchEvalFn sym arch
-> C.HandleAllocator RealWorld -> C.HandleAllocator
-> (MM.MemImpl sym, GlobalMap sym (M.ArchAddrWidth arch)) -> (MM.MemImpl sym, GlobalMap sym (M.ArchAddrWidth arch))
-> LookupFunctionHandle sym arch -> LookupFunctionHandle sym arch
-> C.CFG (MacawExt arch) blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch) -> C.CFG (MacawExt arch) blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
@ -892,7 +891,7 @@ runCodeBlock
(MacawExt arch) (MacawExt arch)
(C.RegEntry sym (ArchRegStruct arch))) (C.RegEntry sym (ArchRegStruct arch)))
runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH g regStruct = do 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 crucRegTypes = crucArchRegTypes archFns
let macawStructRepr = C.StructRepr crucRegTypes let macawStructRepr = C.StructRepr crucRegTypes

155
symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
View File

@ -80,7 +80,6 @@ module Data.Macaw.Symbolic.CrucGen
import Control.Lens hiding (Empty, (:>)) import Control.Lens hiding (Empty, (:>))
import Control.Monad ( foldM ) import Control.Monad ( foldM )
import Control.Monad.Except import Control.Monad.Except
import Control.Monad.ST
import Control.Monad.State.Strict import Control.Monad.State.Strict
import Data.Bits import Data.Bits
import qualified Data.Kind as K import qualified Data.Kind as K
@ -194,17 +193,17 @@ data MacawSymbolicArchFunctions arch
-- LOT of memory---TypeReprs were dominating the heap). -- LOT of memory---TypeReprs were dominating the heap).
, crucGenArchRegName :: !(forall tp . M.ArchReg arch tp -> C.SolverSymbol) , crucGenArchRegName :: !(forall tp . M.ArchReg arch tp -> C.SolverSymbol)
-- ^ Provides a solver name to use for referring to register. -- ^ 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 . 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. -- ^ Generate crucible for architecture-specific function.
, crucGenArchStmt , 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. -- ^ Generate crucible for architecture-specific statement.
, crucGenArchTermStmt :: !(forall ids h s , crucGenArchTermStmt :: !(forall ids s
. M.ArchTermStmt arch ids . M.ArchTermStmt arch ids
-> M.RegState (M.ArchReg arch) (M.Value 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. -- ^ 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)) type MemSegmentMap w = Map M.RegionIndex (CR.GlobalVar (C.BVType w))
-- | State used for generating blocks -- | State used for generating blocks
data CrucGenState arch ids h s data CrucGenState arch ids s
= CrucGenState = CrucGenState
{ translateFns :: !(MacawSymbolicArchFunctions arch) { translateFns :: !(MacawSymbolicArchFunctions arch)
, crucMemBaseAddrMap :: !(MemSegmentMap (M.ArchAddrWidth arch)) , crucMemBaseAddrMap :: !(MemSegmentMap (M.ArchAddrWidth arch))
-- ^ Map from memory region to base address -- ^ Map from memory region to base address
, crucRegIndexMap :: !(RegIndexMap arch) , crucRegIndexMap :: !(RegIndexMap arch)
-- ^ Map from architecture register to Crucible/Macaw index pair. -- ^ Map from architecture register to Crucible/Macaw index pair.
, crucPState :: !(CrucPersistentState ids h s) , crucPState :: !(CrucPersistentState ids s)
-- ^ State that persists across blocks. -- ^ State that persists across blocks.
, crucRegisterReg :: !(CR.Reg s (ArchRegStruct arch)) , crucRegisterReg :: !(CR.Reg s (ArchRegStruct arch))
, macawPositionFn :: !(M.ArchAddrWord arch -> C.Position) , macawPositionFn :: !(M.ArchAddrWord arch -> C.Position)
@ -623,43 +622,43 @@ instance OrdF (BVAtom s) where
GTF -> GTF GTF -> GTF
crucPStateLens :: 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 }) crucPStateLens = lens crucPState (\s v -> s { crucPState = v })
toBitsCacheLens :: 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 }) toBitsCacheLens = lens toBitsCache (\s v -> s { toBitsCache = v })
fromBitsCacheLens :: 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 }) fromBitsCacheLens = lens fromBitsCache (\s v -> s { fromBitsCache = v })
assignValueMapLens :: assignValueMapLens ::
Simple Lens (CrucPersistentState ids h s) Simple Lens (CrucPersistentState ids s)
(MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s))) (MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s)))
assignValueMapLens = lens assignValueMap (\s v -> s { assignValueMap = v }) 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 -- | The Crucible generator monad
-- --
-- This monad provides an environment for constructing Crucible blocks from -- This monad provides an environment for constructing Crucible blocks from
-- Macaw blocks, including the translation of values while preserving sharing -- Macaw blocks, including the translation of values while preserving sharing
-- and the construction of a control flow graph. -- and the construction of a control flow graph.
newtype CrucGen arch ids h s r newtype CrucGen arch ids s r
= CrucGen { unCrucGen = CrucGen { unCrucGen
:: CrucGenState arch ids h s :: CrucGenState arch ids s
-> (CrucGenState arch ids h s -> (CrucGenState arch ids s
-> r -> r
-> ST h (CrucGenRet arch ids h s)) -> IO (CrucGenRet arch ids s))
-> ST h (CrucGenRet arch ids h s) -> IO (CrucGenRet arch ids s)
} }
instance Functor (CrucGen arch ids h s) where instance Functor (CrucGen arch ids s) where
{-# INLINE fmap #-} {-# INLINE fmap #-}
fmap f m = CrucGen $ \s0 cont -> unCrucGen m s0 $ \s1 v -> cont s1 (f v) 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 #-} {-# INLINE pure #-}
pure !r = CrucGen $ \s cont -> cont s r pure !r = CrucGen $ \s cont -> cont s r
{-# INLINE (<*>) #-} {-# INLINE (<*>) #-}
@ -667,26 +666,26 @@ instance Applicative (CrucGen arch ids h s) where
$ \s1 f -> unCrucGen ma s1 $ \s1 f -> unCrucGen ma s1
$ \s2 a -> cont s2 (f a) $ \s2 a -> cont s2 (f a)
instance Monad (CrucGen arch ids h s) where instance Monad (CrucGen arch ids s) where
{-# INLINE (>>=) #-} {-# INLINE (>>=) #-}
m >>= h = CrucGen $ \s0 cont -> unCrucGen m s0 $ \s1 r -> unCrucGen (h r) s1 cont 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 get = CrucGen $ \s cont -> cont s s
put s = CrucGen $ \_ cont -> cont 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 cgExecST m = CrucGen $ \s cont -> m >>= cont s
-- | A NatRepr corresponding to the architecture width. -- | 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 archAddrWidth = crucGenAddrWidth . translateFns <$> get
-- | Get current position -- | Get current position
getPos :: CrucGen arch ids h s C.Position getPos :: CrucGen arch ids s C.Position
getPos = gets codePos 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 addStmt stmt = seq stmt $ do
p <- getPos p <- getPos
s <- get s <- get
@ -696,7 +695,7 @@ addStmt stmt = seq stmt $ do
put $! s { prevStmts = pstmt : prev } put $! s { prevStmts = pstmt : prev }
addTermStmt :: CR.TermStmt s (MacawFunctionResult arch) addTermStmt :: CR.TermStmt s (MacawFunctionResult arch)
-> CrucGen arch ids h s a -> CrucGen arch ids s a
addTermStmt tstmt = do addTermStmt tstmt = do
CrucGen $ \s _ -> pure (s, tstmt) CrucGen $ \s _ -> pure (s, tstmt)
{- {-
@ -714,27 +713,27 @@ addTermStmt tstmt = do
-- Support a friendlier API such as that of Crucible's Generator -- Support a friendlier API such as that of Crucible's Generator
-- monad.) -- monad.)
addExtraBlock :: CR.Block (MacawExt arch) s (MacawFunctionResult arch) addExtraBlock :: CR.Block (MacawExt arch) s (MacawFunctionResult arch)
-> CrucGen arch ids h s () -> CrucGen arch ids s ()
addExtraBlock blk = addExtraBlock blk =
modify' $ \s@(CrucGenState { extraBlocks = blks }) -> modify' $ \s@(CrucGenState { extraBlocks = blks }) ->
s { extraBlocks = blk : blks } s { extraBlocks = blk : blks }
freshValueIndex :: CrucGen arch ids h s (Nonce s tp) freshValueIndex :: CrucGen arch ids s (Nonce s tp)
freshValueIndex = do freshValueIndex = do
s <- get s <- get
let ps = crucPState s let ps = crucPState s
let ng = nonceGen ps let ng = nonceGen ps
cgExecST $ freshNonce ng cgExecST $ freshNonce ng
mmNonceGenerator :: MacawMonad arch ids h s (NonceGenerator (ST h) s) mmNonceGenerator :: MacawMonad arch ids s (NonceGenerator IO s)
mmNonceGenerator = gets nonceGen mmNonceGenerator = gets nonceGen
mmFreshNonce :: MacawMonad arch ids h s (Nonce s tp) mmFreshNonce :: MacawMonad arch ids s (Nonce s tp)
mmFreshNonce = do mmFreshNonce = do
ng <- gets nonceGen ng <- gets nonceGen
mmExecST $ freshNonce ng 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 mkAtom tp = do
archFns <- gets translateFns archFns <- gets translateFns
crucGenArchConstraints archFns $ do crucGenArchConstraints archFns $ do
@ -749,7 +748,7 @@ mkAtom tp = do
pure $! atom pure $! atom
-- | Evaluate the crucible app and return a reference to the result. -- | 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 evalAtom av = do
archFns <- gets translateFns archFns <- gets translateFns
crucGenArchConstraints archFns $ do crucGenArchConstraints archFns $ do
@ -758,11 +757,11 @@ evalAtom av = do
pure atom pure atom
-- | Evaluate the crucible app and return a reference to the result. -- | 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 crucibleValue = evalAtom . CR.EvalApp
-- | Evaluate a Macaw expression extension -- | 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 evalMacawExt = crucibleValue . C.ExtensionApp
-- | Treat a register value as a bit-vector. -- | Treat a register value as a bit-vector.
@ -770,7 +769,7 @@ toBits ::
(1 <= w) => (1 <= w) =>
NatRepr w -> NatRepr w ->
CR.Atom s (MM.LLVMPointerType 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 = toBits w x =
use (toBitsCacheLens . atF (PtrAtom x)) >>= \case use (toBitsCacheLens . atF (PtrAtom x)) >>= \case
Just (BVAtom x') -> Just (BVAtom x') ->
@ -786,7 +785,7 @@ fromBits ::
(1 <= w) => (1 <= w) =>
NatRepr w -> NatRepr w ->
CR.Atom s (C.BVType 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 = fromBits w x =
use (fromBitsCacheLens . atF (BVAtom x)) >>= \case use (fromBitsCacheLens . atF (BVAtom x)) >>= \case
Just (PtrAtom x') -> Just (PtrAtom x') ->
@ -797,12 +796,12 @@ fromBits w x =
assign (toBitsCacheLens . atF (PtrAtom x')) (Just (BVAtom x)) assign (toBitsCacheLens . atF (PtrAtom x')) (Just (BVAtom x))
return 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 getRegs = gets crucRegisterReg >>= evalAtom . CR.ReadReg
-- | Return the value associated with the given register -- | Return the value associated with the given register
getRegValue :: M.ArchReg arch tp 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 getRegValue r = do
archFns <- gets translateFns archFns <- gets translateFns
idxMap <- gets crucRegIndexMap idxMap <- gets crucRegIndexMap
@ -816,25 +815,25 @@ getRegValue r = do
crucibleValue (C.GetStruct regStruct (crucibleIndex idx) tp) crucibleValue (C.GetStruct regStruct (crucibleIndex idx) tp)
v2c :: M.Value arch ids 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 = valueToCrucible
v2c' :: (1 <= w) => v2c' :: (1 <= w) =>
NatRepr w -> NatRepr w ->
M.Value arch ids (M.BVType 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 v2c' w x = toBits w =<< valueToCrucible x
-- | Evaluate the crucible app and return a reference to the result. -- | Evaluate the crucible app and return a reference to the result.
appAtom :: C.App (MacawExt arch) (CR.Atom s) ctp -> 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) appAtom app = evalAtom (CR.EvalApp app)
appBVAtom :: appBVAtom ::
(1 <= w) => (1 <= w) =>
NatRepr w -> NatRepr w ->
C.App (MacawExt arch) (CR.Atom s) (C.BVType 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 appBVAtom w app = fromBits w =<< appAtom app
addLemma :: (1 <= x, x + 1 <= y) => NatRepr x -> q y -> LeqProof 1 y 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. -- | 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)) bvLit w i = crucibleValue (C.BVLit w (i .&. maxUnsigned w))
bitOp2 :: (1 <= w) bitOp2 :: (1 <= w)
@ -858,14 +857,14 @@ bitOp2 :: (1 <= w)
-> C.App (MacawExt arch) (CR.Atom s) (C.BVType 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)
-> 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 bitOp2 w f x y = fromBits w =<< appAtom =<< f <$> v2c' w x <*> v2c' w y
appToCrucible appToCrucible
:: forall arch ids h s tp :: forall arch ids s tp
. M.App (M.Value arch ids) 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 appToCrucible app = do
archFns <- gets translateFns archFns <- gets translateFns
crucGenArchConstraints archFns $ do crucGenArchConstraints archFns $ do
@ -1050,7 +1049,7 @@ appToCrucible app = do
let bvBit let bvBit
:: (1 <= i, i <= n) :: (1 <= i, i <= n)
=> NatRepr i => 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 bvBit i | Refl <- minusPlusCancel i (knownNat @1) = do
b <- appAtom $ b <- appAtom $
C.BVSelect (subNat i (knownNat @1)) (knownNat @1) w x' C.BVSelect (subNat i (knownNat @1)) (knownNat @1) w x'
@ -1094,7 +1093,7 @@ countZeros :: (1 <= w) =>
NatRepr 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)) -> (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) -> 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 countZeros w f vx = do
cx <- v2c vx >>= toBits w cx <- v2c vx >>= toBits w
isZeros <- forM [0..intValue w-1] $ \i -> do 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. -- This is in the 'CrucGen' monad so that it can preserve sharing in terms.
valueToCrucible :: M.Value arch ids tp 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 valueToCrucible v = do
archFns <- gets translateFns archFns <- gets translateFns
crucGenArchConstraints archFns $ do crucGenArchConstraints archFns $ do
@ -1138,21 +1137,21 @@ valueToCrucible v = do
-- | Create a fresh symbolic value of the given type. -- | Create a fresh symbolic value of the given type.
freshSymbolic :: M.TypeRepr tp 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) freshSymbolic repr = evalMacawStmt (MacawFreshSymbolic repr)
evalMacawStmt :: MacawStmtExtension arch (CR.Atom s) tp -> 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 evalMacawStmt = evalAtom . CR.EvalExt
-- | Embed an architecture-specific Macaw statement into a Crucible program -- | Embed an architecture-specific Macaw statement into a Crucible program
-- --
-- All architecture-specific statements return values (which can be unit). -- 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 evalArchStmt = evalMacawStmt . MacawArchStmtExtension
assignRhsToCrucible :: M.AssignRhs arch (M.Value arch ids) tp 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 = assignRhsToCrucible rhs =
gets translateFns >>= \archFns -> gets translateFns >>= \archFns ->
crucGenArchConstraints archFns $ crucGenArchConstraints archFns $
@ -1173,7 +1172,7 @@ assignRhsToCrucible rhs =
fns <- translateFns <$> get fns <- translateFns <$> get
crucGenArchFn fns f 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 = addMacawStmt baddr stmt =
gets translateFns >>= \archFns -> gets translateFns >>= \archFns ->
crucGenArchConstraints archFns $ crucGenArchConstraints archFns $
@ -1213,9 +1212,9 @@ addMacawStmt baddr stmt =
void $ evalMacawStmt crucStmt void $ evalMacawStmt crucStmt
-- | Create a crucible struct for registers from a register state. -- | 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) . 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 createRegStruct regs = do
archFns <- gets translateFns archFns <- gets translateFns
@ -1233,9 +1232,9 @@ createRegStruct regs = do
updates <- createRegUpdates regs updates <- createRegUpdates regs
foldM addUpdate startingVals updates foldM addUpdate startingVals updates
createRegUpdates :: forall arch ids h s createRegUpdates :: forall arch ids s
. M.RegState (M.ArchReg arch) (M.Value arch ids) . 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)] [Pair (Ctx.Index (MacawCrucibleRegTypes arch)) (CR.Atom s)]
createRegUpdates regs = do createRegUpdates regs = do
archFns <- gets translateFns archFns <- gets translateFns
@ -1249,7 +1248,7 @@ createRegUpdates regs = do
Just idx -> Just . Pair (crucibleIndex idx) <$> valueToCrucible val Just idx -> Just . Pair (crucibleIndex idx) <$> valueToCrucible val
addMacawTermStmt :: M.TermStmt arch ids addMacawTermStmt :: M.TermStmt arch ids
-> CrucGen arch ids h s () -> CrucGen arch ids s ()
addMacawTermStmt tstmt = addMacawTermStmt tstmt =
case tstmt of case tstmt of
M.FetchAndExecute regs -> do M.FetchAndExecute regs -> do
@ -1265,24 +1264,24 @@ addMacawTermStmt tstmt =
----------------- -----------------
-- | Monad for adding new blocks to a state. -- | Monad for adding new blocks to a state.
newtype MacawMonad arch ids h s a newtype MacawMonad arch ids s a
= MacawMonad ( ExceptT String (StateT (CrucPersistentState ids h s) (ST h)) a) = MacawMonad ( ExceptT String (StateT (CrucPersistentState ids s) IO) a)
deriving ( Functor deriving ( Functor
, Applicative , Applicative
, Monad , Monad
, MonadError String , MonadError String
, MonadState (CrucPersistentState ids h s) , MonadState (CrucPersistentState ids s)
) )
runMacawMonad :: CrucPersistentState ids h s runMacawMonad :: CrucPersistentState ids s
-> MacawMonad arch ids h s a -> MacawMonad arch ids s a
-> ST h (Either String a, CrucPersistentState ids h s) -> IO (Either String a, CrucPersistentState ids s)
runMacawMonad s (MacawMonad m) = runStateT (runExceptT m) 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 mmExecST = MacawMonad . lift . lift
runCrucGen :: forall arch ids h s runCrucGen :: forall arch ids s
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Base address map -- ^ Base address map
@ -1292,8 +1291,8 @@ runCrucGen :: forall arch ids h s
-- ^ Label for this block -- ^ Label for this block
-> CR.Reg s (ArchRegStruct arch) -> CR.Reg s (ArchRegStruct arch)
-- ^ Crucible register for struct containing all Macaw registers. -- ^ Crucible register for struct containing all Macaw registers.
-> CrucGen arch ids h s () -> CrucGen arch ids s ()
-> MacawMonad arch ids h s -> MacawMonad arch ids s
( CR.Block (MacawExt arch ) s (MacawFunctionResult arch) ( CR.Block (MacawExt arch ) s (MacawFunctionResult arch)
-- Block created -- Block created
, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)] , [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
@ -1338,7 +1337,7 @@ addMacawBlock :: M.MemWidth (M.ArchAddrWidth arch)
-> (M.ArchAddrWord arch -> C.Position) -> (M.ArchAddrWord arch -> C.Position)
-- ^ Function for generating position from offset from start of this block. -- ^ Function for generating position from offset from start of this block.
-> M.Block arch ids -> 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)
, [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 -- | DO NOT CALL THIS FROM USER CODE. We count on the registers not
-- changing until the end of the block. -- 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 setMachineRegs newRegs = do
regReg <- gets crucRegisterReg regReg <- gets crucRegisterReg
addStmt $ CR.SetReg regReg newRegs addStmt $ CR.SetReg regReg newRegs
@ -1385,7 +1384,7 @@ addMacawParsedTermStmt :: BlockLabelMap arch s
-> M.ArchSegmentOff arch -> M.ArchSegmentOff arch
-- ^ Address of this block -- ^ Address of this block
-> M.ParsedTermStmt arch ids -> M.ParsedTermStmt arch ids
-> CrucGen arch ids h s () -> CrucGen arch ids s ()
addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
archFns <- translateFns <$> get archFns <- translateFns <$> get
crucGenArchConstraints archFns $ do 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 msgVal <- crucibleValue $ C.TextLit $ Text.pack $ "Could not identify block at " ++ show thisAddr
addTermStmt $ CR.ErrorStmt msgVal addTermStmt $ CR.ErrorStmt msgVal
addSwitch :: forall arch s ids h addSwitch :: forall arch s ids
. BlockLabelMap arch s . BlockLabelMap arch s
-> M.ArchAddrValue arch ids -> M.ArchAddrValue arch ids
-> Vec.Vector (M.ArchSegmentOff arch) -> Vec.Vector (M.ArchSegmentOff arch)
-> CrucGen arch ids h s () -> CrucGen arch ids s ()
addSwitch blockLabelMap idx possibleAddrs = do addSwitch blockLabelMap idx possibleAddrs = do
archFns <- translateFns <$> get archFns <- translateFns <$> get
crucGenArchConstraints archFns $ do crucGenArchConstraints archFns $ do
@ -1468,7 +1467,7 @@ addSwitch blockLabelMap idx possibleAddrs = do
, CR.TermStmt s (MacawFunctionResult arch) ) , CR.TermStmt s (MacawFunctionResult arch) )
-> ( Int -> ( Int
, M.ArchSegmentOff arch ) , M.ArchSegmentOff arch )
-> CrucGen arch ids h s -> CrucGen arch ids s
( [CR.Stmt (MacawExt arch) s] ( [CR.Stmt (MacawExt arch) s]
, CR.TermStmt s (MacawFunctionResult arch) ) , CR.TermStmt s (MacawFunctionResult arch) )
chain (elsStmts, elsTerm) (thnIdx, thnAddr) = do chain (elsStmts, elsTerm) (thnIdx, thnAddr) = do
@ -1524,7 +1523,7 @@ addSwitch blockLabelMap idx possibleAddrs = do
mapM_ addStmt stmts mapM_ addStmt stmts
addTermStmt termStmt addTermStmt termStmt
addParsedBlock :: forall arch ids h s addParsedBlock :: forall arch ids s
. MacawSymbolicArchFunctions arch . MacawSymbolicArchFunctions arch
-> MemSegmentMap (M.ArchAddrWidth arch) -> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Base address map -- ^ Base address map
@ -1535,7 +1534,7 @@ addParsedBlock :: forall arch ids h s
-> CR.Reg s (ArchRegStruct arch) -> CR.Reg s (ArchRegStruct arch)
-- ^ Register that stores Macaw registers -- ^ Register that stores Macaw registers
-> M.ParsedBlock arch ids -> 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 addParsedBlock archFns memSegMap blockLabelMap posFn regReg macawBlock = do
crucGenArchConstraints archFns $ do crucGenArchConstraints archFns $ do
let base = M.pblockAddr macawBlock let base = M.pblockAddr macawBlock

9
symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
View File

@ -44,7 +44,6 @@ module Data.Macaw.Symbolic.PersistentState
) where ) where
import Control.Monad.ST (ST)
import qualified Data.Kind as K import qualified Data.Kind as K
import qualified Data.Macaw.CFG as M import qualified Data.Macaw.CFG as M
import qualified Data.Macaw.Types as M import qualified Data.Macaw.Types as M
@ -227,9 +226,9 @@ instance TraversableFC MacawCrucibleValue where
-- CrucPersistentState -- CrucPersistentState
-- | State that needs to be persisted across block translations -- | State that needs to be persisted across block translations
data CrucPersistentState ids h s data CrucPersistentState ids s
= CrucPersistentState = CrucPersistentState
{ nonceGen :: NonceGenerator (ST h) s { nonceGen :: NonceGenerator IO s
-- ^ Generator used to get fresh ids for Crucible atoms. -- ^ Generator used to get fresh ids for Crucible atoms.
, assignValueMap :: , assignValueMap ::
!(MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s))) !(MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s)))
@ -237,8 +236,8 @@ data CrucPersistentState ids h s
} }
-- | Initial crucible persistent state -- | Initial crucible persistent state
initCrucPersistentState :: NonceGenerator (ST h) s initCrucPersistentState :: NonceGenerator IO s
-> CrucPersistentState ids h s -> CrucPersistentState ids s
initCrucPersistentState ng = initCrucPersistentState ng =
CrucPersistentState CrucPersistentState
{ nonceGen = ng { nonceGen = ng

14
x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
View File

@ -276,27 +276,27 @@ instance TraversableFC X86StmtExtension where
type instance MacawArchStmtExtension M.X86_64 = X86StmtExtension type instance MacawArchStmtExtension M.X86_64 = X86StmtExtension
crucGenX86Fn :: forall ids h s tp. M.X86PrimFn (M.Value M.X86_64 ids) tp crucGenX86Fn :: forall ids s tp. M.X86PrimFn (M.Value M.X86_64 ids) tp
-> CrucGen M.X86_64 ids h s (C.Atom s (ToCrucibleType tp)) -> CrucGen M.X86_64 ids s (C.Atom s (ToCrucibleType tp))
crucGenX86Fn fn = do 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 f x = AtomWrapper <$> valueToCrucible x
r <- traverseFC f fn r <- traverseFC f fn
evalArchStmt (X86PrimFn r) evalArchStmt (X86PrimFn r)
crucGenX86Stmt :: forall ids h s crucGenX86Stmt :: forall ids s
. M.X86Stmt (M.Value M.X86_64 ids) . M.X86Stmt (M.Value M.X86_64 ids)
-> CrucGen M.X86_64 ids h s () -> CrucGen M.X86_64 ids s ()
crucGenX86Stmt stmt = do 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 f x = AtomWrapper <$> valueToCrucible x
stmt' <- traverseF f stmt stmt' <- traverseF f stmt
void (evalArchStmt (X86PrimStmt stmt')) void (evalArchStmt (X86PrimStmt stmt'))
crucGenX86TermStmt :: M.X86TermStmt ids crucGenX86TermStmt :: M.X86TermStmt ids
-> M.RegState M.X86Reg (M.Value M.X86_64 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 = crucGenX86TermStmt tstmt _regs =
void (evalArchStmt (X86PrimTerm tstmt)) void (evalArchStmt (X86PrimTerm tstmt))

4
x86_symbolic/tests/Main.hs
View File

@ -95,7 +95,7 @@ main = do
[] -> fail "Could not find add function" [] -> fail "Could not find add function"
_ -> fail "Found multiple add functions" _ -> 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 let memBaseVarMap :: MS.MemSegmentMap 64
memBaseVarMap = Map.singleton 1 memBaseVar memBaseVarMap = Map.singleton 1 memBaseVar
@ -113,7 +113,7 @@ main = do
putStrLn $ "Analyzing " ++ show addr putStrLn $ "Analyzing " ++ show addr
(_, Some funInfo) <- stToIO $ M.analyzeFunction logFn addAddr M.UserRequest ds0 (_, 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) regs <- MS.macawAssignToCrucM (mkReg x86ArchFns sym) (MS.crucGenRegAssignment x86ArchFns)