mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-24 08:53:12 +03:00
Add blockAddr/symbolic updates.
This commit is contained in:
Joe Hendrix
parent
e71eff0a88
commit
b452cf51da
@ -1,5 +1,7 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
@ -8,11 +10,12 @@ module Data.Macaw.Symbolic
|
||||
) where
|
||||
|
||||
import Control.Monad.ST
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import qualified Data.Parameterized.Context as Ctx
|
||||
import qualified Data.Parameterized.Map as MapF
|
||||
import qualified Data.Set as Set
|
||||
import Data.Parameterized.TraversableFC
|
||||
import Data.String
|
||||
import Data.Word
|
||||
import qualified Lang.Crucible.CFG.Core as C
|
||||
@ -29,48 +32,103 @@ import Numeric (showHex)
|
||||
import System.IO (stdout)
|
||||
|
||||
import qualified Data.Macaw.CFG.Block as M
|
||||
import qualified Data.Macaw.CFG.Core as M
|
||||
import qualified Data.Macaw.Types as M
|
||||
|
||||
import Data.Macaw.Symbolic.App
|
||||
|
||||
data ReoptSimulatorState sym = ReoptSimulatorState
|
||||
|
||||
translateBlock :: Map Word64 (CR.Label s)
|
||||
-- ^ Map from block indices to the associated label.
|
||||
|
||||
|
||||
-- Return the types associated with a register assignment.
|
||||
regTypes :: Ctx.Assignment M.TypeRepr ctx
|
||||
-> Ctx.Assignment C.TypeRepr (CtxToCrucibleType ctx)
|
||||
regTypes a =
|
||||
case Ctx.view a of
|
||||
Ctx.AssignEmpty -> Ctx.empty
|
||||
Ctx.AssignExtend b tp -> regTypes b Ctx.%> typeToCrucible tp
|
||||
|
||||
-- | 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 =
|
||||
case Ctx.view a of
|
||||
Ctx.AssignEmpty -> pure Ctx.empty
|
||||
Ctx.AssignExtend b reg -> do
|
||||
varAssign <- regVars sym nameFn b
|
||||
c <- freshConstant sym (nameFn reg) (typeToCrucibleBase (M.typeRepr reg))
|
||||
pure (varAssign Ctx.%> C.RV c)
|
||||
|
||||
translateBlock :: CrucGenContext arch ids s
|
||||
-> M.Block arch ids
|
||||
-> Either String (CR.Block s (MacawFunctionResult arch))
|
||||
translateBlock idMap b = do
|
||||
let idx = M.blockLabel b
|
||||
lbl <-
|
||||
case Map.lookup idx idMap of
|
||||
Just lbl -> Right (CR.LabelID lbl)
|
||||
Nothing -> Left $ "Internal: Could not find block with index " ++ show idx
|
||||
let stmts = undefined
|
||||
term = undefined
|
||||
pure $ CR.mkBlock lbl Set.empty stmts term
|
||||
-> StateT (CrucPersistentState arch ids s) (ST s) ()
|
||||
translateBlock = undefined
|
||||
{-
|
||||
translateBlock ctx blockMap idx ip = do
|
||||
s <- get
|
||||
mr <- lift $ runExceptT (mkCrucibleBlock ctx undefined s b)
|
||||
case mr of
|
||||
Left err ->
|
||||
fail err
|
||||
Right r -> do
|
||||
undefined r
|
||||
-}
|
||||
|
||||
translateBlocks :: CrucGenContext arch ids s
|
||||
-> Map Word64 (M.Block arch ids)
|
||||
-> ST s (CrucGenHandles arch, [CR.Block s (MacawFunctionResult arch)])
|
||||
translateBlocks genCtx l = do
|
||||
let ps0 = CrucPersistentState
|
||||
{ handleMap = undefined
|
||||
, valueCount = 0
|
||||
, assignValueMap = MapF.empty
|
||||
, seenBlockMap = Map.empty
|
||||
}
|
||||
ps <- execStateT (mapM_ (translateBlock genCtx) (Map.elems l)) ps0
|
||||
pure (handleMap ps, Map.elems (seenBlockMap ps))
|
||||
|
||||
createHandleMap :: CrucGenHandles arch -> C.FunctionBindings ReoptSimulatorState sym
|
||||
createHandleMap = undefined
|
||||
|
||||
stepBlocks :: forall sym arch ids
|
||||
. IsSymInterface sym
|
||||
. (IsSymInterface sym, M.ArchConstraints arch)
|
||||
=> sym
|
||||
-> Ctx.Assignment C.TypeRepr (ArchRegContext arch)
|
||||
-> (forall tp . M.ArchReg arch tp -> SolverSymbol)
|
||||
-> Ctx.Assignment (M.ArchReg arch) (ArchRegContext arch)
|
||||
-> Word64
|
||||
-- ^ Starting IP for block
|
||||
-> Map Word64 (M.Block arch ids)
|
||||
-- ^ Map from block indices to block
|
||||
-> IO (C.ExecResult
|
||||
ReoptSimulatorState
|
||||
sym
|
||||
(C.RegEntry sym (C.StructType (ArchRegContext arch))))
|
||||
stepBlocks sym regTypes addr macawBlockMap = do
|
||||
let macawStructRepr = C.StructRepr regTypes
|
||||
(C.RegEntry sym (C.StructType (CtxToCrucibleType (ArchRegContext arch)))))
|
||||
stepBlocks sym nameFn regAssign addr macawBlockMap = do
|
||||
let macawStructRepr = C.StructRepr (regTypes (fmapFC M.typeRepr regAssign))
|
||||
halloc <- C.newHandleAllocator
|
||||
let argTypes = Ctx.empty Ctx.%> macawStructRepr
|
||||
let nm = fromString $ "macaw_0x" ++ showHex addr ""
|
||||
h <- stToIO $ C.mkHandle' halloc nm argTypes macawStructRepr
|
||||
-- Map block map to Crucible CFG
|
||||
let blockLabelMap :: Map Word64 (CR.Label ())
|
||||
let blockLabelMap :: Map Word64 (CR.Label RealWorld)
|
||||
blockLabelMap = Map.fromList [ (w, CR.Label (fromIntegral w)) | w <- Map.keys macawBlockMap ]
|
||||
let Right blks = traverse (translateBlock blockLabelMap) $ Map.elems macawBlockMap
|
||||
let genCtx = CrucGenContext { archConstraints = \x -> x
|
||||
, translateArchFn = undefined
|
||||
, translateArchStmt = undefined
|
||||
, handleAlloc = halloc
|
||||
, binaryPath = undefined
|
||||
, macawIndexToLabelMap = blockLabelMap
|
||||
, memSegmentMap = undefined
|
||||
, regValueMap = undefined
|
||||
, syscallHandle = undefined
|
||||
}
|
||||
(hndls, blks) <- stToIO $ translateBlocks genCtx macawBlockMap
|
||||
-- Create control flow graph
|
||||
let rg :: CR.CFG () (MacawFunctionArgs arch) (MacawFunctionResult arch)
|
||||
let rg :: CR.CFG RealWorld (MacawFunctionArgs arch) (MacawFunctionResult arch)
|
||||
rg = CR.CFG { CR.cfgHandle = h
|
||||
, CR.cfgBlocks = blks
|
||||
}
|
||||
@ -82,15 +140,16 @@ stepBlocks sym regTypes addr macawBlockMap = do
|
||||
, C.simConfig = cfg
|
||||
, C.simHandleAllocator = halloc
|
||||
, C.printHandle = stdout
|
||||
, C._functionBindings = C.emptyHandleMap
|
||||
, C._functionBindings = createHandleMap hndls
|
||||
, C._cruciblePersonality = ReoptSimulatorState
|
||||
}
|
||||
-- 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 nameFn regAssign
|
||||
let args :: C.RegMap sym (MacawFunctionArgs arch)
|
||||
args = undefined
|
||||
args = C.RegMap (Ctx.singleton (C.RegEntry macawStructRepr regStruct))
|
||||
-- Run the symbolic simulator.
|
||||
case C.toSSA rg of
|
||||
C.SomeCFG g ->
|
||||
|
||||
@ -6,15 +6,31 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# OPTIONS_GHC -Wwarn #-}
|
||||
module Data.Macaw.Symbolic.App where
|
||||
module Data.Macaw.Symbolic.App
|
||||
( CrucGenHandles(..)
|
||||
, emptyCrucGenHandles
|
||||
, CrucGenContext(..)
|
||||
, CrucPersistentState(..)
|
||||
, CrucSeenBlockMap
|
||||
, CtxToCrucibleType
|
||||
, ArchRegContext
|
||||
, MacawFunctionArgs
|
||||
, MacawFunctionResult
|
||||
, typeToCrucible
|
||||
, typeToCrucibleBase
|
||||
, addMacawBlock
|
||||
) where
|
||||
|
||||
import Control.Lens
|
||||
import Control.Monad.Except
|
||||
import Control.Monad.ST
|
||||
import Control.Monad.State.Strict
|
||||
import qualified Data.Macaw.CFG as M
|
||||
import qualified Data.Macaw.CFG.Block as M
|
||||
import qualified Data.Macaw.Memory as M
|
||||
import qualified Data.Macaw.Types as M
|
||||
import Data.Map.Strict (Map)
|
||||
@ -37,22 +53,33 @@ import qualified Lang.Crucible.FunctionHandle as C
|
||||
import Lang.Crucible.ProgramLoc as C
|
||||
import qualified Lang.Crucible.Types as C
|
||||
|
||||
type family ArchRegContext (arch :: *) :: Ctx C.CrucibleType
|
||||
type family ToCrucibleBaseType (mtp :: M.Type) :: C.BaseType where
|
||||
ToCrucibleBaseType (M.BVType w) = C.BaseBVType w
|
||||
ToCrucibleBaseType M.BoolType = C.BaseBoolType
|
||||
|
||||
type ArchRegStruct (arch :: *) = C.StructType (ArchRegContext arch)
|
||||
|
||||
type ToCrucibleType tp = C.BaseToType (ToCrucibleBaseType tp)
|
||||
|
||||
type family CtxToCrucibleType (mtp :: Ctx M.Type) :: Ctx C.CrucibleType where
|
||||
CtxToCrucibleType EmptyCtx = EmptyCtx
|
||||
CtxToCrucibleType (c ::> tp) = CtxToCrucibleType c ::> ToCrucibleType tp
|
||||
|
||||
-- | Type family for arm registe
|
||||
type family ArchRegContext (arch :: *) :: Ctx M.Type
|
||||
|
||||
type ArchRegStruct (arch :: *) = C.StructType (CtxToCrucibleType (ArchRegContext arch))
|
||||
|
||||
type MacawFunctionArgs arch = EmptyCtx ::> ArchRegStruct arch
|
||||
type MacawFunctionResult arch = ArchRegStruct arch
|
||||
|
||||
type family ToCrucibleType (mtp :: M.Type) :: C.CrucibleType where
|
||||
ToCrucibleType (M.BVType w) = C.BVType w
|
||||
ToCrucibleType M.BoolType = C.BoolType
|
||||
typeToCrucibleBase :: M.TypeRepr tp -> C.BaseTypeRepr (ToCrucibleBaseType tp)
|
||||
typeToCrucibleBase tp =
|
||||
case tp of
|
||||
M.BoolTypeRepr -> C.BaseBoolRepr
|
||||
M.BVTypeRepr w -> C.BaseBVRepr w
|
||||
|
||||
typeToCrucible :: M.TypeRepr tp -> C.TypeRepr (ToCrucibleType tp)
|
||||
typeToCrucible tp =
|
||||
case tp of
|
||||
M.BoolTypeRepr -> C.BoolRepr
|
||||
M.BVTypeRepr w -> C.BVRepr w
|
||||
typeToCrucible = C.baseToType . typeToCrucibleBase
|
||||
|
||||
memReprToCrucible :: M.MemRepr tp -> C.TypeRepr (ToCrucibleType tp)
|
||||
memReprToCrucible = typeToCrucible . M.typeRepr
|
||||
@ -69,7 +96,7 @@ newtype SymbolicHandle f tp = SymbolicHandle (f (ToCrucibleType tp))
|
||||
|
||||
type ArchAddrCrucibleType arch = C.BVType (M.ArchAddrWidth arch)
|
||||
|
||||
-- | Type
|
||||
-- | Type of a function that reads memory
|
||||
type ReadMemHandle arch = C.FnHandle (EmptyCtx ::> ArchAddrCrucibleType arch)
|
||||
|
||||
type WriteMemHandle arch tp
|
||||
@ -82,7 +109,7 @@ type FreshSymHandleMap = MapF M.TypeRepr (SymbolicHandle (C.FnHandle EmptyCtx))
|
||||
type ReadMemHandleMap arch = MapF M.MemRepr (SymbolicHandle (ReadMemHandle arch))
|
||||
type WriteMemHandleMap arch = MapF M.MemRepr (WriteMemWrapper arch)
|
||||
|
||||
-- | Structure for getitng information about what handles are used
|
||||
-- | Structure for getting information about what handles are used
|
||||
data CrucGenHandles arch
|
||||
= CrucGenHandles
|
||||
{ freshSymHandleMap :: !FreshSymHandleMap
|
||||
@ -102,55 +129,83 @@ readMemHandleMapLens = lens readMemHandleMap (\s v -> s { readMemHandleMap = v})
|
||||
writeMemHandleMapLens :: Simple Lens (CrucGenHandles arch) (WriteMemHandleMap arch)
|
||||
writeMemHandleMapLens = lens writeMemHandleMap (\s v -> s { writeMemHandleMap = v})
|
||||
|
||||
-- | State used for generating blocks
|
||||
data CrucGenState arch ids s
|
||||
= CrucGenState
|
||||
emptyCrucGenHandles :: CrucGenHandles arch
|
||||
emptyCrucGenHandles =
|
||||
CrucGenHandles { freshSymHandleMap = MapF.empty
|
||||
, readMemHandleMap = MapF.empty
|
||||
, writeMemHandleMap = MapF.empty
|
||||
}
|
||||
|
||||
data CrucGenContext arch ids s
|
||||
= CrucGenContext
|
||||
{ archConstraints :: !(forall a . (ArchConstraints arch => a) -> a)
|
||||
-- ^ Typeclass constraints for architecture
|
||||
, archWidthRepr :: !(NatRepr (M.ArchAddrWidth arch))
|
||||
-- ^ Width of the architecture
|
||||
, handleAlloc :: !(C.HandleAllocator s)
|
||||
-- ^ Handle allocator
|
||||
, binaryPath :: !Text
|
||||
-- ^ Name of binary these blocks come from.
|
||||
, codeAddr :: !Word64
|
||||
-- ^ Address of this code
|
||||
, translateArchFn :: !(forall tp
|
||||
. M.ArchFn arch ids tp
|
||||
-> CrucGen arch ids s (C.Atom s (ToCrucibleType tp)))
|
||||
-- ^ Function for translating an architecture specific function
|
||||
, translateArchStmt :: !(M.ArchStmt arch ids -> CrucGen arch ids s ())
|
||||
-- ^ Function for translating an architecture specific statement.
|
||||
, blockLabel :: (C.Label s)
|
||||
-- ^ Label for this block we are tranlating
|
||||
, handleMap :: !(CrucGenHandles arch)
|
||||
-- ^ Handles found so far
|
||||
, prevStmts :: ![C.Posd (C.Stmt s)]
|
||||
-- ^ List of states in reverse order
|
||||
, valueCount :: !Int
|
||||
-- ^ Counter used to get fresh indices for Crucible atoms.
|
||||
, handleAlloc :: !(C.HandleAllocator s)
|
||||
-- ^ Handle allocator
|
||||
, binaryPath :: !Text
|
||||
-- ^ Name of binary these blocks come from.
|
||||
, macawIndexToLabelMap :: !(Map Word64 (C.Label s))
|
||||
-- ^ Map from block indices to the associated label.
|
||||
, memSegmentMap :: !(Map M.SegmentIndex (C.Atom s (C.BVType (M.ArchAddrWidth arch))))
|
||||
-- ^ Map from segment indices to the Crucible value denoting the base.
|
||||
, regValueMap :: !(MapF (M.ArchReg arch) (WrappedAtom s))
|
||||
-- ^ Maps Macaw register initial values in block to associated Crucible value.
|
||||
, syscallHandle :: C.FnHandle (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
|
||||
-- ^ Function to call for system call
|
||||
}
|
||||
|
||||
type CrucSeenBlockMap s arch = Map Word64 (C.Block s (MacawFunctionResult arch))
|
||||
|
||||
-- | State that needs to be persisted across block translations
|
||||
data CrucPersistentState arch ids s
|
||||
= CrucPersistentState
|
||||
{ handleMap :: !(CrucGenHandles arch)
|
||||
-- ^ Handles found so far
|
||||
, valueCount :: !Int
|
||||
-- ^ Counter used to get fresh indices for Crucible atoms.
|
||||
, assignValueMap :: !(MapF (M.AssignId ids) (WrappedAtom s))
|
||||
-- ^ Map Macaw assign id to associated Crucible value.
|
||||
, seenBlockMap :: !(CrucSeenBlockMap s arch)
|
||||
-- ^ Map Macaw block indices to the associated crucible block
|
||||
}
|
||||
|
||||
handleMapLens :: Simple Lens (CrucGenState arch ids s) (CrucGenHandles arch)
|
||||
handleMapLens :: Simple Lens (CrucPersistentState arch ids s) (CrucGenHandles arch)
|
||||
handleMapLens = lens handleMap (\s v -> s { handleMap = v })
|
||||
|
||||
data CrucGenResult arch ids s
|
||||
= CrucGenResult
|
||||
{ resHandleMap :: !(CrucGenHandles arch)
|
||||
, resBlock :: !(C.Block s (MacawFunctionResult arch))
|
||||
seenBlockMapLens :: Simple Lens (CrucPersistentState arch ids s) (CrucSeenBlockMap s arch)
|
||||
seenBlockMapLens = lens seenBlockMap (\s v -> s { seenBlockMap = v })
|
||||
|
||||
-- | State used for generating blocks
|
||||
data CrucGenState arch ids s
|
||||
= CrucGenState
|
||||
{ crucCtx :: !(CrucGenContext arch ids s)
|
||||
, crucPState :: !(CrucPersistentState arch ids s)
|
||||
, blockLabel :: (C.Label s)
|
||||
-- ^ Label for this block we are translating
|
||||
, macawBlockIndex :: !Word64
|
||||
, codeAddr :: !Word64
|
||||
-- ^ Address of this code
|
||||
, prevStmts :: ![C.Posd (C.Stmt s)]
|
||||
-- ^ List of states in reverse order
|
||||
}
|
||||
|
||||
crucPStateLens :: Simple Lens (CrucGenState arch ids s) (CrucPersistentState arch ids s)
|
||||
crucPStateLens = lens crucPState (\s v -> s { crucPState = v })
|
||||
|
||||
assignValueMapLens :: Simple Lens (CrucGenState arch ids s) (MapF (M.AssignId ids) (WrappedAtom s))
|
||||
assignValueMapLens = crucPStateLens . lens assignValueMap (\s v -> s { assignValueMap = v })
|
||||
|
||||
newtype CrucGen arch ids s r
|
||||
= CrucGen { unContGen
|
||||
:: CrucGenState arch ids s
|
||||
-> (CrucGenState arch ids s -> r -> ST s (CrucGenResult arch ids s))
|
||||
-> ST s (CrucGenResult arch ids s)
|
||||
-> (CrucGenState arch ids s -> r -> ST s (CrucPersistentState arch ids s))
|
||||
-> ST s (CrucPersistentState arch ids s)
|
||||
}
|
||||
|
||||
instance Functor (CrucGen arch ids s) where
|
||||
@ -169,11 +224,14 @@ instance MonadState (CrucGenState arch ids s) (CrucGen arch ids s) where
|
||||
get = CrucGen $ \s cont -> cont s s
|
||||
put s = CrucGen $ \_ cont -> cont s ()
|
||||
|
||||
getCtx :: CrucGen arch ids s (CrucGenContext arch ids s)
|
||||
getCtx = gets crucCtx
|
||||
|
||||
liftST :: ST s r -> CrucGen arch ids s r
|
||||
liftST m = CrucGen $ \s cont -> m >>= cont s
|
||||
|
||||
getPos :: CrucGen arch ids s C.Position
|
||||
getPos = C.BinaryPos <$> gets binaryPath <*> gets codeAddr
|
||||
getPos = C.BinaryPos <$> (binaryPath <$> getCtx) <*> gets codeAddr
|
||||
|
||||
addStmt :: C.Stmt s -> CrucGen arch ids s ()
|
||||
addStmt stmt = seq stmt $ do
|
||||
@ -192,23 +250,20 @@ addTermStmt tstmt = do
|
||||
let stmts = Seq.fromList (reverse (prevStmts s))
|
||||
let term = C.Posd termPos tstmt
|
||||
let blk = C.mkBlock lbl Set.empty stmts term
|
||||
let res = CrucGenResult
|
||||
{ resHandleMap = handleMap s
|
||||
, resBlock = blk
|
||||
}
|
||||
pure $! res
|
||||
pure $! crucPState s & seenBlockMapLens %~ Map.insert (macawBlockIndex s) blk
|
||||
|
||||
freshValueIndex :: CrucGen arch ids s Int
|
||||
freshValueIndex = do
|
||||
s <- get
|
||||
let cnt = valueCount s
|
||||
put $! s { valueCount = cnt + 1 }
|
||||
let ps = crucPState s
|
||||
let cnt = valueCount ps
|
||||
put $! s { crucPState = ps { valueCount = cnt + 1 } }
|
||||
pure $! cnt
|
||||
|
||||
-- | Evaluate the crucible app and return a reference to the result.
|
||||
evalAtom :: C.AtomValue s ctp -> CrucGen arch ids s (C.Atom s ctp)
|
||||
evalAtom av = do
|
||||
fname <- gets binaryPath
|
||||
fname <- binaryPath <$> getCtx
|
||||
addr <- gets codeAddr
|
||||
let p = C.BinaryPos fname addr
|
||||
i <- freshValueIndex
|
||||
@ -240,7 +295,7 @@ appToCrucible app =
|
||||
valueToCrucible :: M.Value arch ids tp
|
||||
-> CrucGen arch ids s (C.Atom s (ToCrucibleType tp))
|
||||
valueToCrucible v = do
|
||||
cns <- gets archConstraints
|
||||
cns <- archConstraints <$> getCtx
|
||||
cns $ do
|
||||
case v of
|
||||
M.BVValue w c -> do
|
||||
@ -253,20 +308,20 @@ valueToCrucible v = do
|
||||
crucibleValue (C.BVLit w (toInteger base))
|
||||
Right (seg,off) -> do
|
||||
let idx = M.segmentIndex seg
|
||||
segMap <- gets memSegmentMap
|
||||
segMap <- memSegmentMap <$> getCtx
|
||||
case Map.lookup idx segMap of
|
||||
Just a -> do
|
||||
offset <- crucibleValue (C.BVLit w (toInteger off))
|
||||
crucibleValue (C.BVAdd w a offset)
|
||||
Nothing -> fail $ "internal: No Crucible address associated with segment."
|
||||
M.Initial r -> do
|
||||
regmap <- gets regValueMap
|
||||
regmap <- regValueMap <$> getCtx
|
||||
case MapF.lookup r regmap of
|
||||
Just (WrappedAtom a) -> pure a
|
||||
Nothing -> fail $ "internal: Register is not bound."
|
||||
M.AssignedValue asgn -> do
|
||||
let idx = M.assignId asgn
|
||||
amap <- gets assignValueMap
|
||||
amap <- use assignValueMapLens
|
||||
case MapF.lookup idx amap of
|
||||
Just (WrappedAtom r) -> pure r
|
||||
Nothing -> fail "internal: Assignment id is not bound."
|
||||
@ -274,75 +329,84 @@ valueToCrucible v = do
|
||||
freshSymbolicHandle :: M.TypeRepr tp
|
||||
-> CrucGen arch ids s (C.FnHandle EmptyCtx (ToCrucibleType tp))
|
||||
freshSymbolicHandle repr = do
|
||||
hmap <- use $ handleMapLens . freshSymHandleMapLens
|
||||
hmap <- use $ crucPStateLens . handleMapLens . freshSymHandleMapLens
|
||||
case MapF.lookup repr hmap of
|
||||
Just (SymbolicHandle h) -> pure h
|
||||
Nothing -> do
|
||||
let fnm = case repr of
|
||||
M.BoolTypeRepr -> "symbolicBool"
|
||||
M.BVTypeRepr w -> fromString $ "symbolicBV" ++ show w
|
||||
halloc <- gets handleAlloc
|
||||
halloc <- handleAlloc <$> getCtx
|
||||
hndl <- liftST $ C.mkHandle' halloc fnm Ctx.empty (typeToCrucible repr)
|
||||
handleMapLens . freshSymHandleMapLens %= MapF.insert repr (SymbolicHandle hndl)
|
||||
crucPStateLens . handleMapLens . freshSymHandleMapLens %= MapF.insert repr (SymbolicHandle hndl)
|
||||
pure $! hndl
|
||||
|
||||
archWidthRepr :: forall arch ids s . CrucGenContext arch ids s -> NatRepr (M.ArchAddrWidth arch)
|
||||
archWidthRepr ctx = archConstraints ctx $
|
||||
let arepr :: M.AddrWidthRepr (M.ArchAddrWidth arch)
|
||||
arepr = M.addrWidthRepr arepr
|
||||
in M.addrWidthNatRepr arepr
|
||||
|
||||
readMemHandle :: M.MemRepr tp
|
||||
-> CrucGen arch ids s (ReadMemHandle arch (ToCrucibleType tp))
|
||||
readMemHandle repr = do
|
||||
hmap <- use $ handleMapLens . readMemHandleMapLens
|
||||
hmap <- use $ crucPStateLens . handleMapLens . readMemHandleMapLens
|
||||
case MapF.lookup repr hmap of
|
||||
Just (SymbolicHandle r) -> pure r
|
||||
Nothing -> do
|
||||
cns <- gets archConstraints
|
||||
cns <- archConstraints <$> getCtx
|
||||
cns $ do
|
||||
halloc <- gets handleAlloc
|
||||
halloc <- handleAlloc <$> getCtx
|
||||
let fnm = case repr of
|
||||
M.BVMemRepr w _ -> fromString $ "readWord" ++ show (8 * natValue w)
|
||||
wrepr <- gets archWidthRepr
|
||||
wrepr <- archWidthRepr <$> getCtx
|
||||
let argTypes = Ctx.empty Ctx.%> C.BVRepr wrepr
|
||||
hndl <- liftST $ C.mkHandle' halloc fnm argTypes (memReprToCrucible repr)
|
||||
handleMapLens . readMemHandleMapLens %= MapF.insert repr (SymbolicHandle hndl)
|
||||
crucPStateLens . handleMapLens . readMemHandleMapLens %= MapF.insert repr (SymbolicHandle hndl)
|
||||
pure hndl
|
||||
|
||||
writeMemHandle :: M.MemRepr tp
|
||||
-> CrucGen arch ids s (WriteMemHandle arch (ToCrucibleType tp))
|
||||
writeMemHandle repr = do
|
||||
hmap <- use $ handleMapLens . writeMemHandleMapLens
|
||||
hmap <- use $ crucPStateLens . handleMapLens . writeMemHandleMapLens
|
||||
case MapF.lookup repr hmap of
|
||||
Just (WriteMemWrapper r) -> pure r
|
||||
Nothing -> do
|
||||
cns <- gets archConstraints
|
||||
cns <- archConstraints <$> getCtx
|
||||
cns $ do
|
||||
halloc <- gets handleAlloc
|
||||
halloc <- handleAlloc <$> getCtx
|
||||
let fnm = case repr of
|
||||
M.BVMemRepr w _ -> fromString $ "readWord" ++ show (8 * natValue w)
|
||||
wrepr <- gets archWidthRepr
|
||||
wrepr <- archWidthRepr <$> getCtx
|
||||
let argTypes = Ctx.empty Ctx.%> C.BVRepr wrepr Ctx.%> memReprToCrucible repr
|
||||
hndl <- liftST $ C.mkHandle' halloc fnm argTypes C.UnitRepr
|
||||
handleMapLens . writeMemHandleMapLens %= MapF.insert repr (WriteMemWrapper hndl)
|
||||
crucPStateLens . handleMapLens . writeMemHandleMapLens %= MapF.insert repr (WriteMemWrapper hndl)
|
||||
pure hndl
|
||||
|
||||
runCall :: C.FnHandle args ret
|
||||
-- | Call a function handle
|
||||
callFnHandle :: C.FnHandle args ret
|
||||
-- ^ Handle to call
|
||||
-> Ctx.Assignment (C.Atom s) args
|
||||
-> C.TypeRepr ret
|
||||
-- ^ Arguments to function
|
||||
-> CrucGen arch ids s (C.Atom s ret)
|
||||
runCall hndl args ret = do
|
||||
callFnHandle hndl args = do
|
||||
hatom <- crucibleValue (C.HandleLit hndl)
|
||||
evalAtom $ C.Call hatom args ret
|
||||
evalAtom $ C.Call hatom args (C.handleReturnType hndl)
|
||||
|
||||
-- | Create a fresh symbolic value of the given type.
|
||||
freshSymbolic :: M.TypeRepr tp -> CrucGen arch ids s (C.Atom s (ToCrucibleType tp))
|
||||
freshSymbolic repr = do
|
||||
hndl <- freshSymbolicHandle repr
|
||||
runCall hndl Ctx.empty (typeToCrucible repr)
|
||||
|
||||
callFnHandle hndl Ctx.empty
|
||||
|
||||
-- | Read the given memory address
|
||||
readMem :: M.ArchAddrValue arch ids
|
||||
-> M.MemRepr tp
|
||||
-> CrucGen arch ids s (C.Atom s (ToCrucibleType tp))
|
||||
readMem addr repr = do
|
||||
hndl <- readMemHandle repr
|
||||
caddr <- valueToCrucible addr
|
||||
runCall hndl (Ctx.empty Ctx.%> caddr) (memReprToCrucible repr)
|
||||
callFnHandle hndl (Ctx.empty Ctx.%> caddr)
|
||||
|
||||
writeMem :: M.ArchAddrValue arch ids
|
||||
-> M.MemRepr tp
|
||||
@ -353,7 +417,7 @@ writeMem addr repr val = do
|
||||
caddr <- valueToCrucible addr
|
||||
cval <- valueToCrucible val
|
||||
let args = Ctx.empty Ctx.%> caddr Ctx.%> cval
|
||||
void $ runCall hndl args C.UnitRepr
|
||||
void $ callFnHandle hndl args
|
||||
|
||||
assignRhsToCrucible :: M.AssignRhs arch ids tp
|
||||
-> CrucGen arch ids s (C.Atom s (ToCrucibleType tp))
|
||||
@ -363,25 +427,88 @@ assignRhsToCrucible rhs =
|
||||
M.SetUndefined mrepr -> freshSymbolic mrepr
|
||||
M.ReadMem addr repr -> readMem addr repr
|
||||
M.EvalArchFn f _ -> do
|
||||
fn <- gets translateArchFn
|
||||
fn <- translateArchFn <$> getCtx
|
||||
fn f
|
||||
|
||||
addMacawStmt :: M.Stmt arch ids -> CrucGen arch ids s ()
|
||||
addMacawStmt stmt = do
|
||||
addMacawStmt stmt =
|
||||
case stmt of
|
||||
M.AssignStmt asgn -> do
|
||||
let idx = M.assignId asgn
|
||||
a <- assignRhsToCrucible (M.assignRhs asgn)
|
||||
modify' $ \s -> s { assignValueMap = MapF.insert idx (WrappedAtom a) (assignValueMap s) }
|
||||
assignValueMapLens %= MapF.insert idx (WrappedAtom a)
|
||||
M.WriteMem addr repr val -> do
|
||||
writeMem addr repr val
|
||||
M.PlaceHolderStmt _vals msg -> do
|
||||
cmsg <- crucibleValue (C.TextLit (Text.pack msg))
|
||||
addTermStmt (C.ErrorStmt cmsg)
|
||||
M.InstructionStart _ _ ->
|
||||
pure ()
|
||||
M.InstructionStart addr _ -> do
|
||||
cns <- archConstraints <$> getCtx
|
||||
cns $ do
|
||||
modify $ \s -> s { codeAddr = fromIntegral addr }
|
||||
M.Comment _txt -> do
|
||||
pure ()
|
||||
M.ExecArchStmt astmt -> do
|
||||
f <- gets translateArchStmt
|
||||
f <- translateArchStmt <$> getCtx
|
||||
f astmt
|
||||
|
||||
lookupCrucibleLabel :: Word64 -> CrucGen arch ids s (C.Label s)
|
||||
lookupCrucibleLabel idx = do
|
||||
m <- macawIndexToLabelMap <$> getCtx
|
||||
case Map.lookup idx m of
|
||||
Nothing -> fail $ "Could not find label for block " ++ show idx
|
||||
Just l -> pure l
|
||||
|
||||
createRegStruct :: M.RegState (M.ArchReg arch) (M.Value arch ids)
|
||||
-> CrucGen arch ids s (C.Atom s (ArchRegStruct arch))
|
||||
createRegStruct _regs = do
|
||||
let ctx = undefined
|
||||
a = undefined
|
||||
crucibleValue (C.MkStruct ctx a)
|
||||
|
||||
addMacawTermStmt :: M.TermStmt arch ids -> CrucGen arch ids s ()
|
||||
addMacawTermStmt tstmt =
|
||||
case tstmt of
|
||||
M.FetchAndExecute regs -> do
|
||||
s <- createRegStruct regs
|
||||
addTermStmt (C.Return s)
|
||||
M.Branch macawPred macawTrueLbl macawFalseLbl -> do
|
||||
p <- valueToCrucible macawPred
|
||||
t <- lookupCrucibleLabel macawTrueLbl
|
||||
f <- lookupCrucibleLabel macawFalseLbl
|
||||
addTermStmt (C.Br p t f)
|
||||
M.Syscall regs -> do
|
||||
h <- syscallHandle <$> getCtx
|
||||
s <- createRegStruct regs
|
||||
s' <- callFnHandle h (Ctx.empty Ctx.%> s)
|
||||
addTermStmt (C.Return s')
|
||||
M.TranslateError _regs msg -> do
|
||||
cmsg <- crucibleValue (C.TextLit msg)
|
||||
addTermStmt (C.ErrorStmt cmsg)
|
||||
|
||||
addMacawBlock :: CrucGenContext arch ids s
|
||||
-> Word64 -- ^ Starting IP for block
|
||||
-> M.Block arch ids
|
||||
-> ExceptT String
|
||||
(StateT (CrucPersistentState arch ids s) (ST s))
|
||||
()
|
||||
addMacawBlock 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
|
||||
let s0 = CrucGenState { crucCtx = ctx
|
||||
, crucPState = pstate
|
||||
, blockLabel = lbl
|
||||
, macawBlockIndex = idx
|
||||
, codeAddr = addr
|
||||
, prevStmts = []
|
||||
}
|
||||
let cont _s () = fail "Unterminated crucible block"
|
||||
let action = do
|
||||
mapM_ addMacawStmt (M.blockStmts b)
|
||||
addMacawTermStmt (M.blockTerm b)
|
||||
r <- lift $ lift $ unContGen action s0 cont
|
||||
put $!r
|
||||
|
||||
@ -68,6 +68,8 @@ instance ( RegisterInfo(ArchReg arch)
|
||||
data Block arch ids
|
||||
= Block { blockLabel :: !Word64
|
||||
-- ^ Index of this block
|
||||
, blockAddr :: !(ArchSegmentOff arch)
|
||||
-- ^ Address at start of block
|
||||
, blockStmts :: !([Stmt arch ids])
|
||||
-- ^ List of statements in the block.
|
||||
, blockTerm :: !(TermStmt arch ids)
|
||||
|
||||
@ -483,7 +483,6 @@ class ( OrdF r
|
||||
-- | Registers used for passing system call arguments
|
||||
syscallArgumentRegs :: [r (BVType (RegAddrWidth r))]
|
||||
|
||||
|
||||
-- The value of the current instruction pointer.
|
||||
curIP :: RegisterInfo r
|
||||
=> Simple Lens (RegState r f) (f (BVType (RegAddrWidth r)))
|
||||
|
||||
@ -177,7 +177,8 @@ rewriteBlock b = do
|
||||
rewriteTermStmt (blockTerm b)
|
||||
-- Return new block
|
||||
pure $
|
||||
Block { blockLabel = blockLabel b
|
||||
Block { blockAddr = blockAddr b
|
||||
, blockLabel = blockLabel b
|
||||
, blockStmts = tgtStmts
|
||||
, blockTerm = tgtTermStmt
|
||||
}
|
||||
@ -208,9 +209,7 @@ addBlockDemands b = do
|
||||
-- | Return a block after filtering out statements not needed to compute it.
|
||||
elimDeadBlockStmts :: AssignIdSet ids -> Block arch ids -> Block arch ids
|
||||
elimDeadBlockStmts demandSet b =
|
||||
Block { blockLabel = blockLabel b
|
||||
, blockStmts = filter (stmtNeeded demandSet) (blockStmts b)
|
||||
, blockTerm = blockTerm b
|
||||
b { blockStmts = filter (stmtNeeded demandSet) (blockStmts b)
|
||||
}
|
||||
|
||||
------------------------------------------------------------------------
|
||||
@ -780,7 +779,7 @@ transferBlocks src finfo sz block_map =
|
||||
, _newFunctionAddrs = []
|
||||
}
|
||||
let (pblock, ps) = runState (parseBlock ctx b regs) ps0
|
||||
let pb = ParsedBlock { blockAddr = src
|
||||
let pb = ParsedBlock { pblockAddr = src
|
||||
, blockSize = sz
|
||||
, blockReason = foundReason finfo
|
||||
, blockAbstractState = foundAbstractState finfo
|
||||
@ -795,12 +794,13 @@ transferBlocks src finfo sz block_map =
|
||||
transfer :: ArchSegmentOff arch
|
||||
-> FunM arch ids ()
|
||||
transfer addr = do
|
||||
ainfo <- uses curFunCtx archInfo
|
||||
s <- use curFunCtx
|
||||
let ainfo = archInfo s
|
||||
withArchConstraints ainfo $ do
|
||||
mfinfo <- use $ foundAddrs . at addr
|
||||
let finfo = fromMaybe (error $ "transfer called on unfound address " ++ show addr ++ ".") $
|
||||
mfinfo
|
||||
mem <- uses curFunCtx memory
|
||||
let mem = memory s
|
||||
nonceGen <- gets funNonceGen
|
||||
prev_block_map <- use $ curFunBlocks
|
||||
-- Get maximum number of bytes to disassemble
|
||||
@ -813,33 +813,36 @@ transfer addr = do
|
||||
let ab = foundAbstractState finfo
|
||||
(bs0, sz, maybeError) <-
|
||||
liftST $ disassembleFn ainfo mem nonceGen addr max_size ab
|
||||
|
||||
-- If no blocks are returned, then we just add an empty parsed block.
|
||||
if null bs0 then do
|
||||
let errMsg = Text.pack $ fromMaybe "Unknown error" maybeError
|
||||
let stmts = StatementList
|
||||
{ stmtsIdent = 0
|
||||
, stmtsNonterm = []
|
||||
, stmtsTerm = ParsedTranslateError errMsg
|
||||
, stmtsAbsState = initAbsProcessorState mem (foundAbstractState finfo)
|
||||
}
|
||||
let pb = ParsedBlock { pblockAddr = addr
|
||||
, blockSize = sz
|
||||
, blockReason = foundReason finfo
|
||||
, blockAbstractState = foundAbstractState finfo
|
||||
, blockStatementList = stmts
|
||||
}
|
||||
curFunBlocks %= Map.insert addr pb
|
||||
else do
|
||||
-- Rewrite returned blocks to simplify expressions
|
||||
let ctx = RewriteContext { rwctxNonceGen = nonceGen
|
||||
, rwctxArchFn = rewriteArchFn ainfo
|
||||
, rwctxArchStmt = rewriteArchStmt ainfo
|
||||
, rwctxConstraints = \x -> x
|
||||
}
|
||||
bs1 <- liftST $ runRewriter ctx $ do
|
||||
traverse rewriteBlock bs0
|
||||
|
||||
bs1 <- liftST $ runRewriter ctx $ traverse rewriteBlock bs0
|
||||
-- Comute demand set
|
||||
let demandSet =
|
||||
runDemandComp (archDemandContext ainfo) $ do
|
||||
traverse_ addBlockDemands bs1
|
||||
let bs2 = elimDeadBlockStmts demandSet <$> bs1
|
||||
|
||||
-- Make sure at least one block is returned
|
||||
let bs | null bs2 =
|
||||
let -- TODO: Fix this to work with segmented memory
|
||||
w = addrWidthNatRepr (archAddrWidth ainfo)
|
||||
errState = mkRegState Initial
|
||||
& boundValue ip_reg .~ RelocatableValue w (relativeSegmentAddr addr)
|
||||
errMsg = Text.pack $ fromMaybe "Unknown error" maybeError
|
||||
errBlock = Block { blockLabel = 0
|
||||
, blockStmts = []
|
||||
, blockTerm = TranslateError errState errMsg
|
||||
}
|
||||
in [errBlock]
|
||||
| otherwise = bs2
|
||||
let bs = elimDeadBlockStmts demandSet <$> bs1
|
||||
-- Call transfer blocks to calculate parsedblocks
|
||||
let block_map = Map.fromList [ (blockLabel b, b) | b <- bs ]
|
||||
transferBlocks addr finfo sz block_map
|
||||
|
||||
|
||||
@ -295,7 +295,7 @@ rewriteStatementList b = do
|
||||
|
||||
-- | A contiguous region of instructions in memory.
|
||||
data ParsedBlock arch ids
|
||||
= ParsedBlock { blockAddr :: !(ArchSegmentOff arch)
|
||||
= ParsedBlock { pblockAddr :: !(ArchSegmentOff arch)
|
||||
-- ^ Address of region
|
||||
, blockSize :: !(ArchAddrWord arch)
|
||||
-- ^ The size of the region of memory covered by this.
|
||||
@ -316,8 +316,8 @@ instance ArchConstraints arch
|
||||
=> Pretty (ParsedBlock arch ids) where
|
||||
pretty b =
|
||||
let sl = blockStatementList b
|
||||
ppOff o = text (show (incAddr (toInteger o) (relativeSegmentAddr (blockAddr b))))
|
||||
in text (show (blockAddr b)) PP.<> text ":" <$$>
|
||||
ppOff o = text (show (incAddr (toInteger o) (relativeSegmentAddr (pblockAddr b))))
|
||||
in text (show (pblockAddr b)) PP.<> text ":" <$$>
|
||||
indent 2 (vcat (ppStmt ppOff <$> stmtsNonterm sl) <$$> ppTermStmt ppOff (stmtsTerm sl))
|
||||
|
||||
------------------------------------------------------------------------
|
||||
|
||||
@ -3,7 +3,7 @@ Copyright : (c) Galois Inc, 2015-2016
|
||||
Maintainer : jhendrix@galois.com
|
||||
|
||||
Declares 'Memory', a type for representing segmented memory with permissions.
|
||||
n-}
|
||||
-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
@ -206,6 +206,9 @@ instance Ord (MemWord w) where
|
||||
|
||||
-- | Typeclass for legal memory widths
|
||||
class (1 <= w) => MemWidth w where
|
||||
|
||||
addrWidthRepr :: p w -> AddrWidthRepr w
|
||||
|
||||
-- | @addrWidthMod w@ returns @2^(8 * addrSize w - 1)@.
|
||||
addrWidthMod :: p w -> Word64
|
||||
|
||||
@ -268,6 +271,7 @@ instance MemWidth w => Integral (MemWord w) where
|
||||
|
||||
|
||||
instance MemWidth 32 where
|
||||
addrWidthRepr _ = Addr32
|
||||
addrWidthMod _ = 0xffffffff
|
||||
addrRotate (MemWord w) i = MemWord (fromIntegral ((fromIntegral w :: Word32) `rotate` i))
|
||||
addrSize _ = 4
|
||||
@ -279,6 +283,7 @@ instance MemWidth 32 where
|
||||
LittleEndian -> Just $ MemWord $ fromIntegral $ bsWord32le s
|
||||
|
||||
instance MemWidth 64 where
|
||||
addrWidthRepr _ = Addr64
|
||||
addrWidthMod _ = 0xffffffffffffffff
|
||||
addrRotate (MemWord w) i = MemWord (w `rotate` i)
|
||||
addrSize _ = 8
|
||||
|
||||
Loading…
Reference in New Issue
Block a user