mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-28 08:34:23 +03:00
Cache TypeRepr
and Position
values
Generating the type of the register structure on demand was causing `TypeRepr` to be the biggest chunk of the heap. Similarly, we only need to create a new `Position` when we change the offset.
This commit is contained in:
parent
bc5442a223
commit
5a8fba6d08
@ -172,6 +172,10 @@ data MacawSymbolicArchFunctions arch
|
|||||||
:: !(forall a . ((M.RegisterInfo (M.ArchReg arch), MacawArchConstraints arch) => a) -> a)
|
:: !(forall a . ((M.RegisterInfo (M.ArchReg arch), MacawArchConstraints arch) => a) -> a)
|
||||||
, crucGenRegAssignment :: !(Ctx.Assignment (M.ArchReg arch) (ArchRegContext arch))
|
, crucGenRegAssignment :: !(Ctx.Assignment (M.ArchReg arch) (ArchRegContext arch))
|
||||||
-- ^ Map from indices in the ArchRegContext to the associated register.
|
-- ^ Map from indices in the ArchRegContext to the associated register.
|
||||||
|
, crucGenRegStructType :: !(C.TypeRepr (ArchRegStruct arch))
|
||||||
|
-- ^ Type of structure with arch regs. This can be computed from
|
||||||
|
-- @crucGenRegAssignment@, but is cached here to save memory (A
|
||||||
|
-- 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 h s tp
|
||||||
@ -196,9 +200,8 @@ crucGenAddrWidth fns =
|
|||||||
crucArchRegTypes ::
|
crucArchRegTypes ::
|
||||||
MacawSymbolicArchFunctions arch ->
|
MacawSymbolicArchFunctions arch ->
|
||||||
Assignment C.TypeRepr (CtxToCrucibleType (ArchRegContext arch))
|
Assignment C.TypeRepr (CtxToCrucibleType (ArchRegContext arch))
|
||||||
crucArchRegTypes archFns = crucGenArchConstraints archFns $
|
crucArchRegTypes archFns = case crucGenRegStructType archFns of
|
||||||
typeCtxToCrucible (fmapFC M.typeRepr regAssign)
|
C.StructRepr tps -> tps
|
||||||
where regAssign = crucGenRegAssignment archFns
|
|
||||||
|
|
||||||
------------------------------------------------------------------------
|
------------------------------------------------------------------------
|
||||||
-- MacawExprExtension
|
-- MacawExprExtension
|
||||||
@ -543,6 +546,8 @@ data CrucGenState arch ids h s
|
|||||||
-- ^ Label for this block we are translating
|
-- ^ Label for this block we are translating
|
||||||
, codeOff :: !(M.ArchAddrWord arch)
|
, codeOff :: !(M.ArchAddrWord arch)
|
||||||
-- ^ Offset
|
-- ^ Offset
|
||||||
|
, codePos :: !C.Position
|
||||||
|
-- ^ Position (cached from 'codeOff')
|
||||||
, prevStmts :: ![C.Posd (CR.Stmt (MacawExt arch) s)]
|
, prevStmts :: ![C.Posd (CR.Stmt (MacawExt arch) s)]
|
||||||
-- ^ List of states in reverse order
|
-- ^ List of states in reverse order
|
||||||
}
|
}
|
||||||
@ -601,7 +606,7 @@ archAddrWidth = crucGenAddrWidth . translateFns <$> get
|
|||||||
|
|
||||||
-- | Get current position
|
-- | Get current position
|
||||||
getPos :: CrucGen arch ids h s C.Position
|
getPos :: CrucGen arch ids h s C.Position
|
||||||
getPos = gets $ \s -> macawPositionFn s (codeOff s)
|
getPos = gets codePos
|
||||||
|
|
||||||
addStmt :: CR.Stmt (MacawExt arch) s -> CrucGen arch ids h s ()
|
addStmt :: CR.Stmt (MacawExt arch) s -> CrucGen arch ids h s ()
|
||||||
addStmt stmt = seq stmt $ do
|
addStmt stmt = seq stmt $ do
|
||||||
@ -696,9 +701,8 @@ getRegValue r = do
|
|||||||
Just idx -> do
|
Just idx -> do
|
||||||
reg <- gets crucRegisterReg
|
reg <- gets crucRegisterReg
|
||||||
regStruct <- evalAtom (CR.ReadReg reg)
|
regStruct <- evalAtom (CR.ReadReg reg)
|
||||||
let tp = M.typeRepr (crucGenRegAssignment archFns Ctx.! macawIndex idx)
|
let tp = crucArchRegTypes archFns Ctx.! crucibleIndex idx
|
||||||
crucibleValue (C.GetStruct regStruct (crucibleIndex idx)
|
crucibleValue (C.GetStruct regStruct (crucibleIndex idx) tp)
|
||||||
(typeToCrucible 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 h s (CR.Atom s (ToCrucibleType tp))
|
||||||
@ -1115,10 +1119,9 @@ createRegStructAssignment regs = do
|
|||||||
archFns <- gets translateFns
|
archFns <- gets translateFns
|
||||||
crucGenArchConstraints archFns $ do
|
crucGenArchConstraints archFns $ do
|
||||||
let regAssign = crucGenRegAssignment archFns
|
let regAssign = crucGenRegAssignment archFns
|
||||||
let tps = fmapFC M.typeRepr regAssign
|
|
||||||
let a = fmapFC (\r -> regs ^. M.boundValue r) regAssign
|
let a = fmapFC (\r -> regs ^. M.boundValue r) regAssign
|
||||||
fields <- macawAssignToCrucM valueToCrucible a
|
fields <- macawAssignToCrucM valueToCrucible a
|
||||||
return (typeCtxToCrucible tps, fields)
|
return (crucArchRegTypes archFns, fields)
|
||||||
|
|
||||||
addMacawTermStmt :: Map Word64 (CR.Label s)
|
addMacawTermStmt :: Map Word64 (CR.Label s)
|
||||||
-- ^ Map from block index to Crucible label
|
-- ^ Map from block index to Crucible label
|
||||||
@ -1187,6 +1190,7 @@ runCrucGen archFns baseAddrMap posFn off lbl regReg action = crucGenArchConstrai
|
|||||||
, macawPositionFn = posFn
|
, macawPositionFn = posFn
|
||||||
, blockLabel = lbl
|
, blockLabel = lbl
|
||||||
, codeOff = off
|
, codeOff = off
|
||||||
|
, codePos = posFn off
|
||||||
, prevStmts = []
|
, prevStmts = []
|
||||||
}
|
}
|
||||||
let cont _s () = fail "Unterminated crucible block"
|
let cont _s () = fail "Unterminated crucible block"
|
||||||
|
@ -145,6 +145,10 @@ x86RegAssignment =
|
|||||||
<++> (repeatAssign (M.X86_YMMReg . F.ymmReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 16 (M.BVType 256)))
|
<++> (repeatAssign (M.X86_YMMReg . F.ymmReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 16 (M.BVType 256)))
|
||||||
|
|
||||||
|
|
||||||
|
x86RegStructType :: C.TypeRepr (ArchRegStruct M.X86_64)
|
||||||
|
x86RegStructType =
|
||||||
|
C.StructRepr (typeCtxToCrucible $ fmapFC M.typeRepr x86RegAssignment)
|
||||||
|
|
||||||
regIndexMap :: RegIndexMap M.X86_64
|
regIndexMap :: RegIndexMap M.X86_64
|
||||||
regIndexMap = mkRegIndexMap x86RegAssignment
|
regIndexMap = mkRegIndexMap x86RegAssignment
|
||||||
$ Ctx.size $ crucArchRegTypes x86_64MacawSymbolicFns
|
$ Ctx.size $ crucArchRegTypes x86_64MacawSymbolicFns
|
||||||
@ -306,6 +310,7 @@ x86_64MacawSymbolicFns =
|
|||||||
MacawSymbolicArchFunctions
|
MacawSymbolicArchFunctions
|
||||||
{ crucGenArchConstraints = \x -> x
|
{ crucGenArchConstraints = \x -> x
|
||||||
, crucGenRegAssignment = x86RegAssignment
|
, crucGenRegAssignment = x86RegAssignment
|
||||||
|
, crucGenRegStructType = x86RegStructType
|
||||||
, crucGenArchRegName = x86RegName
|
, crucGenArchRegName = x86RegName
|
||||||
, crucGenArchFn = crucGenX86Fn
|
, crucGenArchFn = crucGenX86Fn
|
||||||
, crucGenArchStmt = crucGenX86Stmt
|
, crucGenArchStmt = crucGenX86Stmt
|
||||||
|
Loading…
Reference in New Issue
Block a user