mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-29 00:59:09 +03:00
Update for crucible syntax-extensions.
This commit is contained in:
Joe Hendrix
parent
b89f60bf2b
commit
9530bf97bb
@ -78,7 +78,7 @@ freshVarsForRegs sym nameFn a =
|
||||
|
||||
-- | An override that creates a fresh value with the given type.
|
||||
runFreshSymOverride :: M.TypeRepr tp
|
||||
-> C.OverrideSim MacawSimulatorState sym ret
|
||||
-> C.OverrideSim MacawSimulatorState sym MacawExt ret
|
||||
EmptyCtx
|
||||
(ToCrucibleType tp)
|
||||
(C.RegValue sym (ToCrucibleType tp))
|
||||
@ -88,7 +88,7 @@ runFreshSymOverride tp = do
|
||||
-- | Run override that reads a value from memory.
|
||||
runReadMemOverride :: M.AddrWidthRepr w -- ^ Width of the address.
|
||||
-> M.MemRepr tp -- ^ Type of value to read.
|
||||
-> C.OverrideSim MacawSimulatorState sym ret
|
||||
-> C.OverrideSim MacawSimulatorState sym MacawExt ret
|
||||
(EmptyCtx ::> C.BVType w)
|
||||
(ToCrucibleType tp)
|
||||
(C.RegValue sym (ToCrucibleType tp))
|
||||
@ -97,7 +97,7 @@ runReadMemOverride = undefined
|
||||
-- | Run override that writes a value to memory.
|
||||
runWriteMemOverride :: M.AddrWidthRepr w -- ^ Width of a pointer
|
||||
-> M.MemRepr tp -- ^ Type of value to write to memory.
|
||||
-> C.OverrideSim MacawSimulatorState sym ret
|
||||
-> C.OverrideSim MacawSimulatorState sym MacawExt ret
|
||||
(EmptyCtx ::> C.BVType w ::> ToCrucibleType tp)
|
||||
C.UnitType
|
||||
(C.RegValue sym C.UnitType)
|
||||
@ -105,7 +105,7 @@ runWriteMemOverride = undefined
|
||||
|
||||
createHandleBinding :: M.AddrWidthRepr (M.ArchAddrWidth arch)
|
||||
-> HandleId arch '(args, rtp)
|
||||
-> C.OverrideSim MacawSimulatorState sym ret args rtp (C.RegValue sym rtp)
|
||||
-> C.OverrideSim MacawSimulatorState sym MacawExt ret args rtp (C.RegValue sym rtp)
|
||||
createHandleBinding w hid =
|
||||
case hid of
|
||||
MkFreshSymId repr -> runFreshSymOverride repr
|
||||
@ -117,12 +117,12 @@ createHandleBinding w hid =
|
||||
createHandleMap :: forall arch sym
|
||||
. M.AddrWidthRepr (M.ArchAddrWidth arch)
|
||||
-> UsedHandleSet arch
|
||||
-> C.FunctionBindings MacawSimulatorState sym
|
||||
-> C.FunctionBindings MacawSimulatorState sym MacawExt
|
||||
createHandleMap w = MapF.foldrWithKey go C.emptyHandleMap
|
||||
where go :: HandleId arch pair
|
||||
-> HandleVal pair
|
||||
-> C.FunctionBindings MacawSimulatorState sym
|
||||
-> C.FunctionBindings MacawSimulatorState sym
|
||||
-> C.FunctionBindings MacawSimulatorState sym MacawExt
|
||||
-> C.FunctionBindings MacawSimulatorState sym MacawExt
|
||||
go hid (HandleVal h) b =
|
||||
let o = C.mkOverride' (handleIdName hid) (handleIdRetType hid) (createHandleBinding w hid)
|
||||
in C.insertHandleMap h (C.UseOverride o) b
|
||||
@ -161,9 +161,11 @@ mkCrucCFG :: forall s arch ids
|
||||
-> C.FunctionName
|
||||
-- ^ Name of function for pretty print purposes.
|
||||
-> (CrucGenContext arch s
|
||||
-> MacawMonad arch ids s [CR.Block s (MacawFunctionResult arch)])
|
||||
-> MacawMonad arch ids s [CR.Block MacawExt s (MacawFunctionResult arch)])
|
||||
-- ^ Action to run
|
||||
-> ST s (UsedHandleSet arch, C.SomeCFG (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
|
||||
-> ST s ( UsedHandleSet arch
|
||||
, C.SomeCFG MacawExt (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
|
||||
)
|
||||
mkCrucCFG halloc archFns memBaseVarMap nm action = do
|
||||
let regAssign = crucGenRegAssignment archFns
|
||||
let crucRegTypes = typeCtxToCrucible (fmapFC M.typeRepr regAssign)
|
||||
@ -183,7 +185,7 @@ mkCrucCFG halloc archFns memBaseVarMap nm action = do
|
||||
(Left err, _) -> fail err
|
||||
(Right blks, s) -> pure (blks, s)
|
||||
-- Create control flow graph
|
||||
let rg :: CR.CFG s (MacawFunctionArgs arch) (MacawFunctionResult arch)
|
||||
let rg :: CR.CFG MacawExt s (MacawFunctionArgs arch) (MacawFunctionResult arch)
|
||||
rg = CR.CFG { CR.cfgHandle = h
|
||||
, CR.cfgBlocks = blks
|
||||
}
|
||||
@ -199,7 +201,7 @@ addBlocksCFG :: forall s arch ids
|
||||
-- ^ Function that maps offsets from start of block to Crucible position.
|
||||
-> [M.Block arch ids]
|
||||
-- ^ List of blocks for this region.
|
||||
-> MacawMonad arch ids s [CR.Block s (MacawFunctionResult arch)]
|
||||
-> MacawMonad arch ids s [CR.Block MacawExt s (MacawFunctionResult arch)]
|
||||
addBlocksCFG archFns ctx posFn macawBlocks = do
|
||||
-- Map block map to Crucible CFG
|
||||
let blockLabelMap :: Map Word64 (CR.Label s)
|
||||
@ -223,7 +225,9 @@ mkBlocksCFG :: forall s arch ids
|
||||
-- ^ Function that maps offsets from start of block to Crucible position.
|
||||
-> [M.Block arch ids]
|
||||
-- ^ List of blocks for this region.
|
||||
-> ST s (UsedHandleSet arch, C.SomeCFG (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
|
||||
-> ST s ( UsedHandleSet arch
|
||||
, C.SomeCFG MacawExt (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
|
||||
@ -244,7 +248,9 @@ mkFunCFG :: forall s arch ids
|
||||
-- ^ Function that maps function address to Crucible position
|
||||
-> M.DiscoveryFunInfo arch ids
|
||||
-- ^ List of blocks for this region.
|
||||
-> ST s (UsedHandleSet arch, C.SomeCFG (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
|
||||
-> ST s ( UsedHandleSet arch
|
||||
, C.SomeCFG MacawExt (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
|
||||
@ -272,12 +278,13 @@ runCodeBlock :: forall sym arch blocks
|
||||
-> C.HandleAllocator RealWorld
|
||||
-> UsedHandleSet arch
|
||||
-- ^ Handle map
|
||||
-> C.CFG blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
|
||||
-> C.CFG MacawExt blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
|
||||
-> Ctx.Assignment (C.RegValue' sym) (ArchCrucibleRegTypes arch)
|
||||
-- ^ Register assignment
|
||||
-> IO (C.ExecResult
|
||||
MacawSimulatorState
|
||||
sym
|
||||
MacawExt
|
||||
(C.RegEntry sym (ArchRegStruct arch)))
|
||||
runCodeBlock sym archFns halloc hmap g regStruct = do
|
||||
let regAssign = crucGenRegAssignment archFns
|
||||
@ -287,13 +294,14 @@ runCodeBlock sym archFns halloc hmap g regStruct = do
|
||||
cfg <- C.initialConfig 0 []
|
||||
let ptrWidth :: M.AddrWidthRepr (M.ArchAddrWidth arch)
|
||||
ptrWidth = M.addrWidthRepr ptrWidth
|
||||
let ctx :: C.SimContext MacawSimulatorState sym
|
||||
let ctx :: C.SimContext MacawSimulatorState sym MacawExt
|
||||
ctx = C.SimContext { C._ctxSymInterface = sym
|
||||
, C.ctxSolverProof = \a -> a
|
||||
, C.ctxIntrinsicTypes = MapF.empty
|
||||
, C.simConfig = cfg
|
||||
, C.simHandleAllocator = halloc
|
||||
, C.printHandle = stdout
|
||||
, C.extensionImpl = undefined
|
||||
, C._functionBindings =
|
||||
C.insertHandleMap (C.cfgHandle g) (C.UseCFG g (C.postdomInfo g)) $
|
||||
createHandleMap ptrWidth hmap
|
||||
@ -325,6 +333,7 @@ runBlocks :: forall sym arch ids
|
||||
-> IO (C.ExecResult
|
||||
MacawSimulatorState
|
||||
sym
|
||||
MacawExt
|
||||
(C.RegEntry sym (C.StructType (CtxToCrucibleType (ArchRegContext arch)))))
|
||||
runBlocks sym archFns mem nm posFn macawBlocks regStruct = do
|
||||
halloc <- C.newHandleAllocator
|
||||
|
||||
@ -19,6 +19,7 @@ This defines the core operations for mapping from Reopt to Crucible.
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.Symbolic.CrucGen
|
||||
( CrucGenArchFunctions(..)
|
||||
, MacawExt
|
||||
-- ** Operations for implementing new backends.
|
||||
, CrucGen
|
||||
, MacawMonad
|
||||
@ -83,6 +84,8 @@ data CrucGenArchFunctions arch
|
||||
-- ^ Generate crucible for architecture-specific terminal statement.
|
||||
}
|
||||
|
||||
type MacawExt = ()
|
||||
|
||||
-- | State used for generating blocks
|
||||
data CrucGenState arch ids s
|
||||
= CrucGenState
|
||||
@ -96,7 +99,7 @@ data CrucGenState arch ids s
|
||||
-- ^ Label for this block we are translating
|
||||
, codeOff :: !(M.ArchAddrWord arch)
|
||||
-- ^ Offset
|
||||
, prevStmts :: ![C.Posd (CR.Stmt s)]
|
||||
, prevStmts :: ![C.Posd (CR.Stmt MacawExt s)]
|
||||
-- ^ List of states in reverse order
|
||||
}
|
||||
|
||||
@ -144,7 +147,7 @@ liftST m = CrucGen $ \s cont -> m >>= cont s
|
||||
getPos :: CrucGen arch ids s C.Position
|
||||
getPos = gets $ \s -> macawPositionFn s (codeOff s)
|
||||
|
||||
addStmt :: CR.Stmt s -> CrucGen arch ids s ()
|
||||
addStmt :: CR.Stmt MacawExt s -> CrucGen arch ids s ()
|
||||
addStmt stmt = seq stmt $ do
|
||||
p <- getPos
|
||||
s <- get
|
||||
@ -174,7 +177,7 @@ freshValueIndex = do
|
||||
pure $! cnt
|
||||
|
||||
-- | Evaluate the crucible app and return a reference to the result.
|
||||
evalAtom :: CR.AtomValue s ctp -> CrucGen arch ids s (CR.Atom s ctp)
|
||||
evalAtom :: CR.AtomValue MacawExt s ctp -> CrucGen arch ids s (CR.Atom s ctp)
|
||||
evalAtom av = do
|
||||
p <- getPos
|
||||
i <- freshValueIndex
|
||||
@ -188,7 +191,7 @@ evalAtom av = do
|
||||
pure $! atom
|
||||
|
||||
-- | Evaluate the crucible app and return a reference to the result.
|
||||
crucibleValue :: C.App (CR.Atom s) ctp -> CrucGen arch ids s (CR.Atom s ctp)
|
||||
crucibleValue :: C.App MacawExt (CR.Atom s) ctp -> CrucGen arch ids s (CR.Atom s ctp)
|
||||
crucibleValue app = evalAtom (CR.EvalApp app)
|
||||
|
||||
-- | Evaluate the crucible app and return a reference to the result.
|
||||
@ -212,7 +215,7 @@ v2c :: M.Value arch ids tp
|
||||
v2c = valueToCrucible
|
||||
|
||||
-- | Evaluate the crucible app and return a reference to the result.
|
||||
appAtom :: C.App (CR.Atom s) ctp -> CrucGen arch ids s (CR.Atom s ctp)
|
||||
appAtom :: C.App MacawExt (CR.Atom s) ctp -> CrucGen arch ids s (CR.Atom s ctp)
|
||||
appAtom app = evalAtom (CR.EvalApp app)
|
||||
|
||||
-- | Create a crucible value for a bitvector literal.
|
||||
@ -394,19 +397,19 @@ freshSymbolic repr = do
|
||||
callFnHandle hndl Ctx.empty
|
||||
|
||||
-- | Read the given memory address
|
||||
readMem :: M.ArchAddrValue arch ids
|
||||
-> M.MemRepr tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
|
||||
readMem addr repr = do
|
||||
callReadMem :: M.ArchAddrValue arch ids
|
||||
-> M.MemRepr tp
|
||||
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
|
||||
callReadMem addr repr = do
|
||||
hndl <- mkHandleVal (ReadMemId repr)
|
||||
caddr <- valueToCrucible addr
|
||||
callFnHandle hndl (Empty :> caddr)
|
||||
|
||||
writeMem :: M.ArchAddrValue arch ids
|
||||
-> M.MemRepr tp
|
||||
-> M.Value arch ids tp
|
||||
-> CrucGen arch ids s ()
|
||||
writeMem addr repr val = do
|
||||
callWriteMem :: M.ArchAddrValue arch ids
|
||||
-> M.MemRepr tp
|
||||
-> M.Value arch ids tp
|
||||
-> CrucGen arch ids s ()
|
||||
callWriteMem addr repr val = do
|
||||
hndl <- mkHandleVal (WriteMemId repr)
|
||||
caddr <- valueToCrucible addr
|
||||
cval <- valueToCrucible val
|
||||
@ -418,8 +421,9 @@ assignRhsToCrucible rhs =
|
||||
case rhs of
|
||||
M.EvalApp app -> appToCrucible app
|
||||
M.SetUndefined mrepr -> freshSymbolic mrepr
|
||||
M.ReadMem addr repr -> readMem addr repr
|
||||
M.CondReadMem repr c addr def -> undefined repr c addr def
|
||||
M.ReadMem addr repr -> callReadMem addr repr
|
||||
M.CondReadMem repr c addr def -> do
|
||||
undefined repr c addr def
|
||||
M.EvalArchFn f _ -> do
|
||||
fns <- translateFns <$> get
|
||||
crucGenArchFn fns f
|
||||
@ -433,7 +437,7 @@ addMacawStmt stmt =
|
||||
a <- assignRhsToCrucible (M.assignRhs asgn)
|
||||
crucPStateLens . assignValueMapLens %= MapF.insert idx (MacawCrucibleValue a)
|
||||
M.WriteMem addr repr val -> do
|
||||
writeMem addr repr val
|
||||
callWriteMem addr repr val
|
||||
M.PlaceHolderStmt _vals msg -> do
|
||||
cmsg <- crucibleValue (C.TextLit (Text.pack msg))
|
||||
addTermStmt (CR.ErrorStmt cmsg)
|
||||
@ -518,7 +522,7 @@ runCrucGen :: CrucGenArchFunctions arch
|
||||
-- ^ Offset
|
||||
-> CR.Label s
|
||||
-> CrucGen arch ids s ()
|
||||
-> MacawMonad arch ids s (CR.Block s (MacawFunctionResult arch), M.ArchAddrWord arch)
|
||||
-> MacawMonad arch ids s (CR.Block MacawExt s (MacawFunctionResult arch), M.ArchAddrWord arch)
|
||||
runCrucGen tfns ctx posFn off lbl action = do
|
||||
ps <- get
|
||||
let s0 = CrucGenState { translateFns = tfns
|
||||
@ -546,7 +550,7 @@ addMacawBlock :: M.MemWidth (M.ArchAddrWidth arch)
|
||||
-> (M.ArchAddrWord arch -> C.Position)
|
||||
-- ^ Function for generating position from offset from start of this block.
|
||||
-> M.Block arch ids
|
||||
-> MacawMonad arch ids s (CR.Block s (MacawFunctionResult arch))
|
||||
-> MacawMonad arch ids s (CR.Block MacawExt s (MacawFunctionResult arch))
|
||||
addMacawBlock tfns ctx blockLabelMap posFn b = do
|
||||
let idx = M.blockLabel b
|
||||
lbl <-
|
||||
@ -588,8 +592,8 @@ addStatementList :: M.MemWidth (M.ArchAddrWidth arch)
|
||||
-> (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)]
|
||||
-> [CR.Block MacawExt s (MacawFunctionResult arch)]
|
||||
-> MacawMonad arch ids s [CR.Block MacawExt s (MacawFunctionResult arch)]
|
||||
addStatementList _ _ _ _ _ [] rlist =
|
||||
pure (reverse rlist)
|
||||
addStatementList tfns ctx blockLabelMap addr posFn ((off,stmts):rest) r = do
|
||||
@ -616,7 +620,7 @@ addParsedBlock :: forall arch ids s
|
||||
-> (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)]
|
||||
-> MacawMonad arch ids s [CR.Block MacawExt s (MacawFunctionResult arch)]
|
||||
addParsedBlock tfns ctx blockLabelMap posFn b = do
|
||||
let base = M.pblockAddr b
|
||||
let thisPosFn :: M.ArchAddrWord arch -> C.Position
|
||||
|
||||
Loading…
Reference in New Issue
Block a user