GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-28 08:34:23 +03:00
Code Issues Projects Releases Wiki Activity

Start support for ParsedBlock.

Browse Source
This commit is contained in:
Joe Hendrix 2018-01-05 11:02:11 -08:00
parent 250c41d40b
commit 7ee4f6ef28
No known key found for this signature in database
GPG Key ID: 8DFA5FF784098C4F
5 changed files with 371 additions and 153 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
base/src/Data/Macaw/Discovery/State.hs
View File

@ -1,5 +1,5 @@
{-|
Copyright : (c) Galois, Inc 2016-2017
Copyright : (c) Galois, Inc 2016-2018
Maintainer : jhendrix@galois.com
This defines the main data structure for storing information learned from code

4
base/src/Data/Macaw/Memory.hs
View File

@ -659,8 +659,8 @@ memAsAddrPairs mem end = addrWidthClass (memAddrWidth mem) $ do
------------------------------------------------------------------------
-- MemAddr
-- | A memory address is either an absolute value in memory or an offset of segment that
-- could be relocated.
-- | A memory address is either an absolute value in memory or an
-- offset of segment that could be relocated.
--
-- This representation does not require that the address is mapped to
-- actual memory (see `MemSegmentOff` for an address representation

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

@ -11,29 +11,36 @@ module Data.Macaw.Symbolic
( Data.Macaw.Symbolic.CrucGen.CrucGenArchFunctions(..)
, Data.Macaw.Symbolic.CrucGen.CrucGen
, MacawSimulatorState
, stepBlocks
, freshVarsForRegs
, runCodeBlock
, runBlocks
, mkBlocksCFG
, mkFunCFG
, Data.Macaw.Symbolic.PersistentState.ArchRegContext
, Data.Macaw.Symbolic.PersistentState.ToCrucibleType
, Data.Macaw.Symbolic.PersistentState.UsedHandleSet
) where
import Control.Monad.Except
import Control.Monad.ST
import Control.Monad.State.Strict
import Control.Lens ((^.))
import Control.Monad (forM)
import Control.Monad.ST (ST, RealWorld, stToIO)
import Data.Foldable
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.TraversableFC
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Word
import qualified Lang.Crucible.Analysis.Postdom as C
import qualified Lang.Crucible.CFG.Core as C
import qualified Lang.Crucible.CFG.Reg as CR
import qualified Lang.Crucible.CFG.SSAConversion as C
import qualified Lang.Crucible.Config as C
import qualified Lang.Crucible.FunctionHandle as C
import qualified Lang.Crucible.FunctionName as C
import qualified Lang.Crucible.ProgramLoc as C
import qualified Lang.Crucible.Simulator.ExecutionTree as C
import qualified Lang.Crucible.Simulator.GlobalState as C
import qualified Lang.Crucible.Simulator.OverrideSim as C
@ -43,6 +50,7 @@ import System.IO (stdout)
import qualified Data.Macaw.CFG.Block as M
import qualified Data.Macaw.CFG.Core as M
import qualified Data.Macaw.Discovery.State as M
import qualified Data.Macaw.Memory as M
import qualified Data.Macaw.Types as M
@ -52,20 +60,20 @@ import Data.Macaw.Symbolic.PersistentState
data MacawSimulatorState sym = MacawSimulatorState
-- | Create the variables from a collection of registers.
regVars :: (IsSymInterface sym, M.HasRepr reg M.TypeRepr)
=> sym
-> (forall tp . reg tp -> SolverSymbol)
-> Ctx.Assignment reg ctx
-> IO (Ctx.Assignment (C.RegValue' sym) (CtxToCrucibleType ctx))
regVars sym nameFn a =
freshVarsForRegs :: (IsSymInterface sym, M.HasRepr reg M.TypeRepr)
=> sym
-> (forall tp . reg tp -> SolverSymbol)
-> Ctx.Assignment reg ctx
-> IO (Ctx.Assignment (C.RegValue' sym) (CtxToCrucibleType ctx))
freshVarsForRegs sym nameFn a =
case a of
Empty -> pure Ctx.empty
b :> reg -> do
varAssign <- regVars sym nameFn b
varAssign <- freshVarsForRegs sym nameFn b
c <- freshConstant sym (nameFn reg) (typeToCrucibleBase (M.typeRepr reg))
pure (varAssign :> C.RV c)
#if !MIN_VERSION_base(4,10,0)
_ -> error "internal: regVars encountered case non-exhaustive pattern"
_ -> error "internal: freshVarsForRegs encountered case non-exhaustive pattern"
#endif
-- | An override that creates a fresh value with the given type.
@ -95,28 +103,28 @@ runWriteMemOverride :: M.AddrWidthRepr w -- ^ Width of a pointer
(C.RegValue sym C.UnitType)
runWriteMemOverride = undefined
createHandleBinding :: CrucGenContext arch s
createHandleBinding :: M.AddrWidthRepr (M.ArchAddrWidth arch)
-> HandleId arch '(args, rtp)
-> C.OverrideSim MacawSimulatorState sym ret args rtp (C.RegValue sym rtp)
createHandleBinding ctx hid =
createHandleBinding w hid =
case hid of
MkFreshSymId repr -> runFreshSymOverride repr
ReadMemId repr -> runReadMemOverride (archWidthRepr ctx) repr
WriteMemId repr -> runWriteMemOverride (archWidthRepr ctx) repr
ReadMemId repr -> runReadMemOverride w repr
WriteMemId repr -> runWriteMemOverride w repr
-- | This function identifies all the handles needed, and returns
-- function bindings for each one.
createHandleMap :: forall arch s sym
. CrucGenContext arch s
createHandleMap :: forall arch sym
. M.AddrWidthRepr (M.ArchAddrWidth arch)
-> UsedHandleSet arch
-> C.FunctionBindings MacawSimulatorState sym
createHandleMap ctx = MapF.foldrWithKey go C.emptyHandleMap
createHandleMap w = MapF.foldrWithKey go C.emptyHandleMap
where go :: HandleId arch pair
-> HandleVal pair
-> C.FunctionBindings MacawSimulatorState sym
-> C.FunctionBindings MacawSimulatorState sym
go hid (HandleVal h) b =
let o = C.mkOverride' (handleIdName hid) (handleIdRetType hid) (createHandleBinding ctx hid)
let o = C.mkOverride' (handleIdName hid) (handleIdRetType hid) (createHandleBinding w hid)
in C.insertHandleMap h (C.UseOverride o) b
mkMemSegmentBinding :: (1 <= w)
@ -141,57 +149,144 @@ mkMemBaseVarMap halloc mem = do
]
Map.fromList <$> traverse (mkMemSegmentBinding halloc (M.memWidth mem)) (Set.toList baseIndices)
stepBlocks :: forall sym arch ids
. (IsSymInterface sym, M.ArchConstraints arch)
=> sym
-> CrucGenArchFunctions arch
-> M.Memory (M.ArchAddrWidth arch)
-- ^ Memory image for executable
-> Text
-- ^ Name of executable
-> C.FunctionName
-- ^ Name of function for pretty print purposes.
-> Word64
-- ^ Code address
-> [M.Block arch ids]
-- ^ List of blocks
-> IO (C.ExecResult
MacawSimulatorState
sym
(C.RegEntry sym (C.StructType (CtxToCrucibleType (ArchRegContext arch)))))
stepBlocks sym sinfo mem binPath nm addr macawBlocks = do
let regAssign = crucGenRegAssignment sinfo
-- | Create a Crucible CFG from a list of blocks
mkCrucCFG :: forall s arch ids
. M.ArchConstraints arch
=> C.HandleAllocator s
-- ^ Handle allocator to make function handles
-> CrucGenArchFunctions arch
-- ^ Crucible architecture-specific functions.
-> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address
-> C.FunctionName
-- ^ Name of function for pretty print purposes.
-> (CrucGenContext arch s
-> MacawMonad arch ids s [CR.Block s (MacawFunctionResult arch)])
-- ^ Action to run
-> ST s (UsedHandleSet arch, C.SomeCFG (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkCrucCFG halloc archFns memBaseVarMap nm action = do
let regAssign = crucGenRegAssignment archFns
let crucRegTypes = typeCtxToCrucible (fmapFC M.typeRepr regAssign)
let macawStructRepr = C.StructRepr crucRegTypes
halloc <- C.newHandleAllocator
let argTypes = Empty :> macawStructRepr
h <- stToIO $ C.mkHandle' halloc nm argTypes macawStructRepr
-- Map block map to Crucible CFG
let blockLabelMap :: Map Word64 (CR.Label RealWorld)
blockLabelMap = Map.fromList [ (w, CR.Label (fromIntegral w))
| w <- M.blockLabel <$> macawBlocks ]
memBaseVarMap <- stToIO $ mkMemBaseVarMap halloc mem
h <- C.mkHandle' halloc nm argTypes macawStructRepr
let genCtx = CrucGenContext { archConstraints = \x -> x
, macawRegAssign = regAssign
, regIndexMap = mkRegIndexMap regAssign (Ctx.size crucRegTypes)
, handleAlloc = halloc
, binaryPath = binPath
, macawIndexToLabelMap = blockLabelMap
, memBaseAddrMap = memBaseVarMap
}
let ps0 = initCrucPersistentState
blockRes <- stToIO $ runStateT (runExceptT (mapM_ (addMacawBlock sinfo genCtx addr) macawBlocks)) ps0
ps <-
blockRes <- runMacawMonad ps0 (action genCtx)
(blks, ps) <-
case blockRes of
(Left err, _) -> fail err
(Right _, s) -> pure s
(Right blks, s) -> pure (blks, s)
-- Create control flow graph
let rg :: CR.CFG RealWorld (MacawFunctionArgs arch) (MacawFunctionResult arch)
let rg :: CR.CFG s (MacawFunctionArgs arch) (MacawFunctionResult arch)
rg = CR.CFG { CR.cfgHandle = h
, CR.cfgBlocks = Map.elems (seenBlockMap ps)
, CR.cfgBlocks = blks
}
pure $ (handleMap ps, C.toSSA rg)
-- | Create a Crucible CFG from a list of blocks
addBlocksCFG :: forall s arch ids
. M.ArchConstraints arch
=> CrucGenArchFunctions arch
-- ^ Crucible specific functions.
-> CrucGenContext arch s
-> (M.ArchAddrWord arch -> C.Position)
-- ^ Function that maps offsets from start of block to Crucible position.
-> [M.Block arch ids]
-- ^ List of blocks for this region.
-> MacawMonad arch ids s [CR.Block s (MacawFunctionResult arch)]
addBlocksCFG archFns ctx posFn macawBlocks = do
-- Map block map to Crucible CFG
let blockLabelMap :: Map Word64 (CR.Label s)
blockLabelMap = Map.fromList [ (w, CR.Label (fromIntegral w))
| w <- M.blockLabel <$> macawBlocks ]
forM macawBlocks $ \b -> do
addMacawBlock archFns ctx blockLabelMap posFn b
-- | Create a Crucible CFG from a list of blocks
mkBlocksCFG :: forall s arch ids
. M.ArchConstraints arch
=> C.HandleAllocator s
-- ^ Handle allocator to make the blocks
-> CrucGenArchFunctions arch
-- ^ Crucible specific functions.
-> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address
-> C.FunctionName
-- ^ Name of function for pretty print purposes.
-> (M.ArchAddrWord arch -> C.Position)
-- ^ Function that maps offsets from start of block to Crucible position.
-> [M.Block arch ids]
-- ^ List of blocks for this region.
-> ST s (UsedHandleSet arch, C.SomeCFG (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkBlocksCFG halloc archFns memBaseVarMap nm posFn macawBlocks = do
mkCrucCFG halloc archFns memBaseVarMap nm $ \ctx -> do
addBlocksCFG archFns ctx posFn macawBlocks
type FunBlockMap arch s = Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
mkFunCFG :: forall s arch ids
. M.ArchConstraints arch
=> C.HandleAllocator s
-- ^ Handle allocator to make the blocks
-> CrucGenArchFunctions arch
-- ^ Crucible specific functions.
-> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address
-> C.FunctionName
-- ^ Name of function for pretty print purposes.
-> (M.ArchSegmentOff arch -> C.Position)
-- ^ Function that maps function address to Crucible position
-> M.DiscoveryFunInfo arch ids
-- ^ List of blocks for this region.
-> ST s (UsedHandleSet arch, C.SomeCFG (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkFunCFG halloc archFns memBaseVarMap nm posFn fn = do
mkCrucCFG halloc archFns memBaseVarMap nm $ \ctx -> do
let insSentences :: M.ArchSegmentOff arch
-> (FunBlockMap arch s,Int)
-> [M.StatementList arch ids]
-> (FunBlockMap arch s,Int)
insSentences _ m [] = m
insSentences base (m,c) (s:r) =
insSentences base
(Map.insert (base,M.stmtsIdent s) (CR.Label c) m,c+1)
(nextStatements (M.stmtsTerm s) ++ r)
let insBlock :: (FunBlockMap arch s,Int) -> M.ParsedBlock arch ids -> (FunBlockMap arch s,Int)
insBlock m b = insSentences (M.pblockAddr b) m [M.blockStatementList b]
let blockLabelMap :: FunBlockMap arch s
blockLabelMap = fst $ foldl' insBlock (Map.empty,0) (Map.elems (fn^.M.parsedBlocks))
fmap concat $
forM (Map.elems (fn^.M.parsedBlocks)) $ \b -> do
addParsedBlock archFns ctx blockLabelMap posFn b
-- | Run the simulator over a contiguous set of code.
runCodeBlock :: forall sym arch blocks
. (IsSymInterface sym, M.ArchConstraints arch)
=> sym
-> CrucGenArchFunctions arch
-> C.HandleAllocator RealWorld
-> UsedHandleSet arch
-- ^ Handle map
-> C.CFG blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
-> Ctx.Assignment (C.RegValue' sym) (ArchCrucibleRegTypes arch)
-- ^ Register assignment
-> IO (C.ExecResult
MacawSimulatorState
sym
(C.RegEntry sym (ArchRegStruct arch)))
runCodeBlock sym archFns halloc hmap g regStruct = do
let regAssign = crucGenRegAssignment archFns
let crucRegTypes = typeCtxToCrucible (fmapFC M.typeRepr regAssign)
let macawStructRepr = C.StructRepr crucRegTypes
-- Run the symbolic simulator.
cfg <- C.initialConfig 0 []
let ptrWidth :: M.AddrWidthRepr (M.ArchAddrWidth arch)
ptrWidth = M.addrWidthRepr ptrWidth
let ctx :: C.SimContext MacawSimulatorState sym
ctx = C.SimContext { C._ctxSymInterface = sym
, C.ctxSolverProof = \a -> a
@ -199,18 +294,41 @@ stepBlocks sym sinfo mem binPath nm addr macawBlocks = do
, C.simConfig = cfg
, C.simHandleAllocator = halloc
, C.printHandle = stdout
, C._functionBindings = createHandleMap genCtx (handleMap ps)
, C._functionBindings =
C.insertHandleMap (C.cfgHandle g) (C.UseCFG g (C.postdomInfo g)) $
createHandleMap ptrWidth hmap
, C._cruciblePersonality = MacawSimulatorState
}
-- Create the symbolic simulator state
let s = C.initSimState ctx C.emptyGlobals C.defaultErrorHandler
-- Define the arguments to call the Reopt CFG with.
-- This should be a symbolic variable for each register in the architecture.
regStruct <- regVars sym (crucGenArchRegName sinfo) regAssign
let args :: C.RegMap sym (MacawFunctionArgs arch)
args = C.RegMap (Ctx.singleton (C.RegEntry macawStructRepr regStruct))
C.runOverrideSim s macawStructRepr $ do
let args :: C.RegMap sym (MacawFunctionArgs arch)
args = C.RegMap (Ctx.singleton (C.RegEntry macawStructRepr regStruct))
C.regValue <$> C.callCFG g args
-- | Run the simulator over a contiguous set of code.
runBlocks :: forall sym arch ids
. (IsSymInterface sym, M.ArchConstraints arch)
=> sym
-> CrucGenArchFunctions arch
-- ^ Crucible specific functions.
-> M.Memory (M.ArchAddrWidth arch)
-- ^ Memory image for executable
-> C.FunctionName
-- ^ Name of function for pretty print purposes.
-> (M.ArchAddrWord arch -> C.Position)
-- ^ Function that maps offsets from start of block to Crucible position.
-> [M.Block arch ids]
-- ^ List of blocks for this region.
-> Ctx.Assignment (C.RegValue' sym) (CtxToCrucibleType (ArchRegContext arch))
-- ^ Register assignment
-> IO (C.ExecResult
MacawSimulatorState
sym
(C.RegEntry sym (C.StructType (CtxToCrucibleType (ArchRegContext arch)))))
runBlocks sym archFns mem nm posFn macawBlocks regStruct = do
halloc <- C.newHandleAllocator
memBaseVarMap <- stToIO $ mkMemBaseVarMap halloc mem
(hmap, C.SomeCFG g) <- stToIO $ mkBlocksCFG halloc archFns memBaseVarMap nm posFn macawBlocks
-- Run the symbolic simulator.
case C.toSSA rg of
C.SomeCFG g ->
C.runOverrideSim s macawStructRepr $ do
C.regValue <$> C.callCFG g args
runCodeBlock sym archFns halloc hmap g regStruct

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

@ -8,19 +8,24 @@ This defines the core operations for mapping from Reopt to Crucible.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wwarn #-}
module Data.Macaw.Symbolic.CrucGen
( CrucGenArchFunctions(..)
-- ** Operations for implementing new backends.
, CrucGen
, MacawMonad
, runMacawMonad
, addMacawBlock
, addParsedBlock
, nextStatements
) where
import Control.Lens hiding (Empty, (:>))
@ -30,8 +35,10 @@ import Control.Monad.State.Strict
import Data.Bits
import qualified Data.Macaw.CFG as M
import qualified Data.Macaw.CFG.Block as M
import qualified Data.Macaw.Discovery.State as M
import qualified Data.Macaw.Memory as M
import qualified Data.Macaw.Types as M
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Parameterized.Context as Ctx
import Data.Parameterized.Map (MapF)
@ -83,10 +90,12 @@ data CrucGenState arch ids s
, crucCtx :: !(CrucGenContext arch s)
, crucPState :: !(CrucPersistentState arch ids s)
-- ^ State that persists across blocks.
, macawPositionFn :: !(M.ArchAddrWord arch -> C.Position)
-- ^ Map from offset to Crucible position.
, blockLabel :: (CR.Label s)
-- ^ Label for this block we are translating
, crucPos :: !C.Position
-- ^ Position in the crucible file.
, codeOff :: !(M.ArchAddrWord arch)
-- ^ Offset
, prevStmts :: ![C.Posd (CR.Stmt s)]
-- ^ List of states in reverse order
}
@ -98,13 +107,15 @@ assignValueMapLens :: Simple Lens (CrucPersistentState arch ids s)
(MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s)))
assignValueMapLens = lens assignValueMap (\s v -> s { assignValueMap = v })
type CrucGenRet arch ids s = (CrucGenState arch ids s, CR.TermStmt s (MacawFunctionResult arch))
newtype CrucGen arch ids s r
= CrucGen { unCrucGen
:: CrucGenState arch ids s
-> (CrucGenState arch ids s
-> r
-> ST s (CrucPersistentState arch ids s, CR.Block s (MacawFunctionResult arch)))
-> ST s (CrucPersistentState arch ids s, CR.Block s (MacawFunctionResult arch))
-> ST s (CrucGenRet arch ids s))
-> ST s (CrucGenRet arch ids s)
}
instance Functor (CrucGen arch ids s) where
@ -131,7 +142,7 @@ liftST m = CrucGen $ \s cont -> m >>= cont s
-- | Get current position
getPos :: CrucGen arch ids s C.Position
getPos = gets crucPos
getPos = gets $ \s -> macawPositionFn s (codeOff s)
addStmt :: CR.Stmt s -> CrucGen arch ids s ()
addStmt stmt = seq stmt $ do
@ -144,13 +155,15 @@ addStmt stmt = seq stmt $ do
addTermStmt :: CR.TermStmt s (MacawFunctionResult arch)
-> CrucGen arch ids s a
addTermStmt tstmt = do
termPos <- getPos
CrucGen $ \s _ -> do
CrucGen $ \s _ -> pure (s, tstmt)
{-
let termPos = macawPositionFn s (codeOff s)
let lbl = blockLabel s
let stmts = Seq.fromList (reverse (prevStmts s))
let term = C.Posd termPos tstmt
let blk = CR.mkBlock (CR.LabelID lbl) Set.empty stmts term
pure $ (crucPState s, blk)
-}
freshValueIndex :: CrucGen arch ids s Int
freshValueIndex = do
@ -235,28 +248,18 @@ bvAdc w x y c = do
cbv <- appAtom =<< C.BVIte c w <$> bvLit w 1 <*> bvLit w 0
appAtom $ C.BVAdd w s cbv
appToCrucible :: M.App (M.Value arch ids) tp
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
appToCrucible app = do
ctx <- getCtx
archConstraints ctx $ do
case app of
M.Eq x y ->
case M.typeRepr x of
M.BoolTypeRepr -> do
eq <- appAtom =<< C.BoolXor <$> v2c x <*> v2c y
appAtom (C.Not eq)
M.BVTypeRepr w -> do
appAtom =<< C.BVEq w <$> v2c x <*> v2c y
M.TupleTypeRepr _ -> undefined -- TODO: Fix this
M.Mux tp c t f ->
case tp of
M.BoolTypeRepr ->
appAtom =<< C.BoolIte <$> v2c c <*> v2c t <*> v2c f
M.BVTypeRepr w ->
appAtom =<< C.BVIte <$> v2c c <*> pure w <*> v2c t <*> v2c f
M.TupleTypeRepr _ -> undefined -- TODO: Fix this
M.Eq x y -> do
let btp = typeToCrucibleBase (M.typeRepr x)
appAtom =<< C.BaseIsEq btp <$> v2c x <*> v2c y
M.Mux tp c t f -> do
let btp = typeToCrucibleBase tp
appAtom =<< C.BaseIte btp <$> v2c c <*> v2c t <*> v2c f
M.TupleField tps x i ->
undefined tps x i -- TODO: Fix this
@ -367,7 +370,7 @@ mkHandleVal hid = do
Just (HandleVal h) -> pure h
Nothing -> do
ctx <- getCtx
let argTypes = handleIdArgTypes ctx hid
let argTypes = handleIdArgTypes (archWidthRepr ctx) hid
let retType = handleIdRetType hid
hndl <- liftST $ C.mkHandle' (handleAlloc ctx) (handleIdName hid) argTypes retType
crucPStateLens . handleMapLens %= MapF.insert hid (HandleVal hndl)
@ -421,7 +424,8 @@ assignRhsToCrucible rhs =
fns <- translateFns <$> get
crucGenArchFn fns f
addMacawStmt :: M.Stmt arch ids -> CrucGen arch ids s ()
addMacawStmt :: M.Stmt arch ids
-> CrucGen arch ids s ()
addMacawStmt stmt =
case stmt of
M.AssignStmt asgn -> do
@ -433,20 +437,21 @@ addMacawStmt stmt =
M.PlaceHolderStmt _vals msg -> do
cmsg <- crucibleValue (C.TextLit (Text.pack msg))
addTermStmt (CR.ErrorStmt cmsg)
M.InstructionStart addr _ -> do
M.InstructionStart off _ -> do
-- Update the position
modify $ \s ->
crucGenArchConstraints (translateFns s) $
s { crucPos = C.BinaryPos (binaryPath (crucCtx s)) (fromIntegral addr) }
modify $ \s -> s { codeOff = off }
M.Comment _txt -> do
pure ()
M.ExecArchStmt astmt -> do
fns <- translateFns <$> get
crucGenArchStmt fns astmt
lookupCrucibleLabel :: Word64 -> CrucGen arch ids s (CR.Label s)
lookupCrucibleLabel idx = do
m <- macawIndexToLabelMap <$> getCtx
lookupCrucibleLabel :: Map Word64 (CR.Label s)
-- ^ Map from block index to Crucible label
-> Word64
-- ^ Index of crucible block
-> CrucGen arch ids s (CR.Label s)
lookupCrucibleLabel m idx = do
case Map.lookup idx m of
Nothing -> fail $ "Could not find label for block " ++ show idx
Just l -> pure l
@ -464,16 +469,19 @@ createRegStruct regs = do
fields <- macawAssignToCrucM valueToCrucible a
crucibleValue $ C.MkStruct (typeCtxToCrucible tps) fields
addMacawTermStmt :: M.TermStmt arch ids -> CrucGen arch ids s ()
addMacawTermStmt tstmt =
addMacawTermStmt :: Map Word64 (CR.Label s)
-- ^ Map from block index to Crucible label
-> M.TermStmt arch ids
-> CrucGen arch ids s ()
addMacawTermStmt blockLabelMap tstmt =
case tstmt of
M.FetchAndExecute regs -> do
s <- createRegStruct regs
addTermStmt (CR.Return s)
M.Branch macawPred macawTrueLbl macawFalseLbl -> do
p <- valueToCrucible macawPred
t <- lookupCrucibleLabel macawTrueLbl
f <- lookupCrucibleLabel macawFalseLbl
t <- lookupCrucibleLabel blockLabelMap macawTrueLbl
f <- lookupCrucibleLabel blockLabelMap macawFalseLbl
addTermStmt (CR.Br p t f)
M.ArchTermStmt ts regs -> do
fns <- translateFns <$> get
@ -485,32 +493,133 @@ addMacawTermStmt tstmt =
-----------------
-- | Monad for adding new blocks to a state.
type MacawMonad arch ids s = ExceptT String (StateT (CrucPersistentState arch ids s) (ST s))
newtype MacawMonad arch ids s a
= MacawMonad ( ExceptT String (StateT (CrucPersistentState arch ids s) (ST s)) a)
deriving ( Functor
, Applicative
, Monad
, MonadError String
, MonadState (CrucPersistentState arch ids s)
)
addMacawBlock :: CrucGenArchFunctions arch
-> CrucGenContext arch s
-> Word64
-- ^ Code address
-> M.Block arch ids
-> MacawMonad arch ids s ()
addMacawBlock tfns ctx addr b = do
pstate <- get
let idx = M.blockLabel b
lbl <-
case Map.lookup idx (macawIndexToLabelMap ctx) of
Just lbl -> pure lbl
Nothing -> throwError $ "Internal: Could not find block with index " ++ show idx
runMacawMonad :: CrucPersistentState arch ids s
-> MacawMonad arch ids s a
-> ST s (Either String a, CrucPersistentState arch ids s)
runMacawMonad s (MacawMonad m) = runStateT (runExceptT m) s
mmExecST :: ST s a -> MacawMonad arch ids s a
mmExecST = MacawMonad . lift . lift
runCrucGen :: CrucGenArchFunctions arch
-> CrucGenContext arch s
-> (M.ArchAddrWord arch -> C.Position)
-- ^ Function for generating position from offset from start of this block.
-> M.ArchAddrWord arch
-- ^ Offset
-> CR.Label s
-> CrucGen arch ids s ()
-> MacawMonad arch ids s (CR.Block s (MacawFunctionResult arch), M.ArchAddrWord arch)
runCrucGen tfns ctx posFn off lbl action = do
ps <- get
let s0 = CrucGenState { translateFns = tfns
, crucCtx = ctx
, crucPState = pstate
, crucPState = ps
, macawPositionFn = posFn
, blockLabel = lbl
, crucPos = C.BinaryPos (binaryPath ctx) addr
, codeOff = off
, prevStmts = []
}
let cont _s () = fail "Unterminated crucible block"
let action = do
mapM_ addMacawStmt (M.blockStmts b)
addMacawTermStmt (M.blockTerm b)
(ps, blk) <- lift $ lift $ unCrucGen action s0 cont
put $ ps & seenBlockMapLens %~ Map.insert idx blk
(s, tstmt) <- mmExecST $ unCrucGen action s0 cont
put (crucPState s)
let termPos = macawPositionFn s (codeOff s)
let stmts = Seq.fromList (reverse (prevStmts s))
let term = C.Posd termPos tstmt
let blk = CR.mkBlock (CR.LabelID lbl) Set.empty stmts term
pure (blk, codeOff s)
addMacawBlock :: M.MemWidth (M.ArchAddrWidth arch)
=> CrucGenArchFunctions arch
-> CrucGenContext arch s
-> Map Word64 (CR.Label s)
-- ^ Map from block index to Crucible label
-> (M.ArchAddrWord arch -> C.Position)
-- ^ Function for generating position from offset from start of this block.
-> M.Block arch ids
-> MacawMonad arch ids s (CR.Block s (MacawFunctionResult arch))
addMacawBlock tfns ctx blockLabelMap posFn b = do
let idx = M.blockLabel b
lbl <-
case Map.lookup idx blockLabelMap of
Just lbl ->
pure lbl
Nothing ->
throwError $ "Internal: Could not find block with index " ++ show idx
fmap fst $ runCrucGen tfns ctx posFn 0 lbl $ do
mapM_ addMacawStmt (M.blockStmts b)
addMacawTermStmt blockLabelMap (M.blockTerm b)
addMacawParsedTermStmt :: M.ParsedTermStmt arch ids
-> CrucGen arch ids s ()
addMacawParsedTermStmt tstmt =
case tstmt of
M.ParsedCall{} -> undefined
M.ParsedJump{} -> undefined
M.ParsedLookupTable{} -> undefined
M.ParsedReturn{} -> undefined
M.ParsedIte{} -> undefined
M.ParsedArchTermStmt{} -> undefined
M.ParsedTranslateError{} -> undefined
M.ClassifyFailure{} -> undefined
nextStatements :: M.ParsedTermStmt arch ids -> [M.StatementList arch ids]
nextStatements tstmt =
case tstmt of
M.ParsedIte _ x y -> [x, y]
_ -> []
addStatementList :: M.MemWidth (M.ArchAddrWidth arch)
=> CrucGenArchFunctions arch
-> CrucGenContext arch s
-> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
-- ^ Map from block index to Crucible label
-> M.ArchSegmentOff arch
-- ^ Address of statements
-> (M.ArchAddrWord arch -> C.Position)
-- ^ Function for generating position from offset from start of this block.
-> [(M.ArchAddrWord arch, M.StatementList arch ids)]
-> [CR.Block s (MacawFunctionResult arch)]
-> MacawMonad arch ids s [CR.Block s (MacawFunctionResult arch)]
addStatementList _ _ _ _ _ [] rlist =
pure (reverse rlist)
addStatementList tfns ctx blockLabelMap addr posFn ((off,stmts):rest) r = do
let idx = M.stmtsIdent stmts
lbl <-
case Map.lookup (addr, idx) blockLabelMap of
Just lbl ->
pure lbl
Nothing ->
throwError $ "Internal: Could not find block with address " ++ show addr ++ " index " ++ show idx
(b,off') <-
runCrucGen tfns ctx posFn off lbl $ do
mapM_ addMacawStmt (M.stmtsNonterm stmts)
addMacawParsedTermStmt (M.stmtsTerm stmts)
let new = (off',) <$> nextStatements (M.stmtsTerm stmts)
addStatementList tfns ctx blockLabelMap addr posFn (new ++ rest) (b:r)
addParsedBlock :: forall arch ids s
. M.MemWidth (M.ArchAddrWidth arch)
=> CrucGenArchFunctions arch
-> CrucGenContext arch s
-> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
-- ^ Map from block index to Crucible label
-> (M.ArchSegmentOff arch -> C.Position)
-- ^ Function for generating position from offset from start of this block.
-> M.ParsedBlock arch ids
-> MacawMonad arch ids s [CR.Block s (MacawFunctionResult arch)]
addParsedBlock tfns ctx blockLabelMap posFn b = do
let base = M.pblockAddr b
let thisPosFn :: M.ArchAddrWord arch -> C.Position
thisPosFn off = posFn r
where Just r = M.incSegmentOff base (toInteger off)
addStatementList tfns ctx blockLabelMap (M.pblockAddr b) thisPosFn [(0, M.blockStatementList b)] []

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

@ -21,7 +21,6 @@ module Data.Macaw.Symbolic.PersistentState
CrucPersistentState(..)
, initCrucPersistentState
, handleMapLens
, seenBlockMapLens
-- * Types
, ToCrucibleBaseType
, ToCrucibleType
@ -54,8 +53,6 @@ module Data.Macaw.Symbolic.PersistentState
, IndexPair(..)
-- * Values
, MacawCrucibleValue(..)
-- * Blocks
, CrucSeenBlockMap
) where
import Control.Lens hiding (Index, (:>), Empty)
@ -64,7 +61,6 @@ import qualified Data.Macaw.CFG as M
import qualified Data.Macaw.Memory as M
import qualified Data.Macaw.Types as M
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Parameterized.Classes
import Data.Parameterized.Context
import qualified Data.Parameterized.List as P
@ -74,8 +70,6 @@ import Data.Parameterized.NatRepr
import Data.Parameterized.TraversableF
import Data.Parameterized.TraversableFC
import Data.String
import Data.Text (Text)
import Data.Word
import qualified Lang.Crucible.CFG.Common as C
import qualified Lang.Crucible.CFG.Reg as CR
import qualified Lang.Crucible.FunctionHandle as C
@ -195,6 +189,10 @@ type ArchConstraints arch
-- | Map from indices of segments without a fixed base address to a
-- global variable storing the base address.
--
-- This uses a global variable so that we can do the translation, and then
-- decide where to locate it without requiring us to also pass the values
-- around arguments.
type MemSegmentMap w = Map M.RegionIndex (C.GlobalVar (C.BVType w))
--- | Information that does not change during generating Crucible from MAcaw
@ -203,14 +201,11 @@ data CrucGenContext arch s
{ archConstraints :: !(forall a . (ArchConstraints arch => a) -> a)
-- ^ Typeclass constraints for architecture
, macawRegAssign :: !(Assignment (M.ArchReg arch) (ArchRegContext arch))
-- ^ Assignment from register to the context
-- ^ Assignment from register index to the register identifier.
, regIndexMap :: !(RegIndexMap arch)
-- ^ Map from register identifier to the index in Macaw/Crucible.
, handleAlloc :: !(C.HandleAllocator s)
-- ^ Handle allocator
, binaryPath :: !Text
-- ^ Name of binary these blocks come from.
, macawIndexToLabelMap :: !(Map Word64 (CR.Label s))
-- ^ Map from block indices to the associated label.
, memBaseAddrMap :: !(MemSegmentMap (M.ArchAddrWidth arch))
-- ^ Map from indices of segments without a fixed base address to a global
-- variable storing the base address.
@ -276,16 +271,21 @@ handleIdName h =
WriteMemId (M.BVMemRepr w end) ->
fromString $ "writeMem_" ++ show (8 * natValue w) ++ "_" ++ endName end
handleIdArgTypes :: CrucGenContext arch s
widthTypeRepr :: M.AddrWidthRepr w -> C.TypeRepr (C.BVType w)
widthTypeRepr M.Addr32 = C.knownRepr
widthTypeRepr M.Addr64 = C.knownRepr
handleIdArgTypes :: M.AddrWidthRepr (M.ArchAddrWidth arch)
-> HandleId arch '(args, ret)
-> Assignment C.TypeRepr args
handleIdArgTypes ctx h =
handleIdArgTypes ptrRepr h =
case h of
MkFreshSymId _repr -> empty
ReadMemId _repr -> archConstraints ctx $
empty :> C.BVRepr (M.addrWidthNatRepr (archWidthRepr ctx))
WriteMemId repr -> archConstraints ctx $
empty :> C.BVRepr (M.addrWidthNatRepr (archWidthRepr ctx))
ReadMemId _repr ->
empty :> widthTypeRepr ptrRepr
WriteMemId repr ->
empty :> widthTypeRepr ptrRepr
:> memReprToCrucible repr
handleIdRetType :: HandleId arch '(args, ret)
@ -310,9 +310,6 @@ type UsedHandleSet arch = MapF (HandleId arch) HandleVal
-- | A Crucible value with a Macaw type.
data MacawCrucibleValue f tp = MacawCrucibleValue (f (ToCrucibleType tp))
-- | Map from block indices to the associated crucible block.
type CrucSeenBlockMap s arch = Map Word64 (CR.Block s (MacawFunctionResult arch))
------------------------------------------------------------------------
-- CrucPersistentState
@ -325,8 +322,6 @@ data CrucPersistentState arch ids s
-- ^ Counter used to get fresh indices for Crucible atoms.
, assignValueMap :: !(MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s)))
-- ^ Map Macaw assign id to associated Crucible value.
, seenBlockMap :: !(CrucSeenBlockMap s arch)
-- ^ Map Macaw block indices to the associated crucible block
}
-- | Initial crucible persistent state
@ -339,11 +334,7 @@ initCrucPersistentState =
{ handleMap = MapF.empty
, valueCount = sizeInt argCount
, assignValueMap = MapF.empty
, seenBlockMap = Map.empty
}
handleMapLens :: Simple Lens (CrucPersistentState arch ids s) (UsedHandleSet arch)
handleMapLens = lens handleMap (\s v -> s { handleMap = v })
seenBlockMapLens :: Simple Lens (CrucPersistentState arch ids s) (CrucSeenBlockMap s arch)
seenBlockMapLens = lens seenBlockMap (\s v -> s { seenBlockMap = v })