GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-26 09:22:20 +03:00
Code Issues Projects Releases Wiki Activity

Minor cleanups.

Browse Source
This commit is contained in:
Joe Hendrix 2018-01-24 10:49:12 -08:00
parent c1d82cdfc4
commit cfeabfde05
No known key found for this signature in database
GPG Key ID: 8DFA5FF784098C4F
2 changed files with 21 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -178,8 +178,6 @@ mkBlocksCFG archFns halloc memBaseVarMap nm posFn macawBlocks = do
mkCrucCFG archFns halloc nm $ do
addBlocksCFG archFns memBaseVarMap posFn macawBlocks
type FunBlockMap arch s = Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
mkFunCFG :: forall s arch ids
. MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions.
@ -197,17 +195,17 @@ mkFunCFG :: forall s arch ids
mkFunCFG archFns halloc memBaseVarMap nm posFn fn = do
mkCrucCFG archFns halloc nm $ do
let insSentences :: M.ArchSegmentOff arch
-> (FunBlockMap arch s,Int)
-> (BlockLabelMap arch s,Int)
-> [M.StatementList arch ids]
-> (FunBlockMap arch s,Int)
-> (BlockLabelMap 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)
let insBlock :: (BlockLabelMap arch s,Int) -> M.ParsedBlock arch ids -> (BlockLabelMap arch s,Int)
insBlock m b = insSentences (M.pblockAddr b) m [M.blockStatementList b]
let blockLabelMap :: FunBlockMap arch s
let blockLabelMap :: BlockLabelMap arch s
blockLabelMap = fst $ foldl' insBlock (Map.empty,0) (Map.elems (fn^.M.parsedBlocks))
let regReg = CR.Reg { CR.regPosition = posFn (M.discoveredFunAddr fn)
, CR.regId = 0

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

@ -38,6 +38,7 @@ module Data.Macaw.Symbolic.CrucGen
, MacawMonad
, runMacawMonad
, addMacawBlock
, BlockLabelMap
, addParsedBlock
, nextStatements
, valueToCrucible
@ -738,8 +739,11 @@ setMachineRegs newRegs = do
regReg <- gets crucRegisterReg
addStmt $ CR.SetReg regReg newRegs
addMacawParsedTermStmt :: Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
-- ^ Map from block addresses to starting label
-- | Map from block information to Crucible label (used to generate term statements)
type BlockLabelMap arch s = Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
addMacawParsedTermStmt :: BlockLabelMap arch s
-- ^ Block label map for this function
-> M.ArchSegmentOff arch
-- ^ Address of this block
-> M.ParsedTermStmt arch ids
@ -760,8 +764,13 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
M.ParsedJump regs nextAddr -> do
setMachineRegs =<< createRegStruct regs
addTermStmt $ CR.Jump (parsedBlockLabel blockLabelMap nextAddr 0)
M.ParsedLookupTable _regs _idx _possibleAddrs -> do
error "Crucible symbolic generator does not yet support lookup tables."
M.ParsedLookupTable regs _idx _possibleAddrs -> do
setMachineRegs =<< createRegStruct regs
let cond = undefined
-- TODO: Add ability in CrucGen to generate new labels and add new blocks.
let tlbl = undefined
let flbl = undefined
addTermStmt $! CR.Br cond tlbl flbl
M.ParsedReturn regs -> do
regValues <- createRegStruct regs
addTermStmt $ CR.Return regValues
@ -771,7 +780,6 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
let flbl = parsedBlockLabel blockLabelMap thisAddr (M.stmtsIdent f)
addTermStmt $! CR.Br crucCond tlbl flbl
M.ParsedArchTermStmt aterm regs _mret -> do
archFns <- gets translateFns
crucGenArchTermStmt archFns aterm regs
M.ParsedTranslateError msg -> do
msgVal <- crucibleValue (C.TextLit msg)
@ -789,7 +797,7 @@ nextStatements tstmt =
addStatementList :: MacawSymbolicArchFunctions arch
-> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Base address map
-> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
-> BlockLabelMap arch s
-- ^ Map from block index to Crucible label
-> M.ArchSegmentOff arch
-- ^ Address of block that starts statements
@ -822,7 +830,7 @@ addParsedBlock :: forall arch ids s
. MacawSymbolicArchFunctions arch
-> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Base address map
-> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
-> BlockLabelMap arch s
-- ^ Map from block index to Crucible label
-> (M.ArchSegmentOff arch -> C.Position)
-- ^ Function for generating position from offset from start of this block.
@ -836,4 +844,5 @@ addParsedBlock tfns baseAddrMap blockLabelMap posFn regReg b = do
let thisPosFn :: M.ArchAddrWord arch -> C.Position
thisPosFn off = posFn r
where Just r = M.incSegmentOff base (toInteger off)
addStatementList tfns baseAddrMap blockLabelMap (M.pblockAddr b) thisPosFn regReg [(0, M.blockStatementList b)] []
addStatementList tfns baseAddrMap blockLabelMap
(M.pblockAddr b) thisPosFn regReg [(0, M.blockStatementList b)] []