mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-29 17:17:05 +03:00
Migrate Syscall to Architecture-specific statement.
This commit is contained in:
parent
00a087b294
commit
2c229bcaac
@ -32,11 +32,6 @@ data TermStmt arch ids
|
|||||||
= FetchAndExecute !(RegState (ArchReg arch) (Value arch ids))
|
= FetchAndExecute !(RegState (ArchReg arch) (Value arch ids))
|
||||||
-- | Branch and execute one block or another.
|
-- | Branch and execute one block or another.
|
||||||
| Branch !(Value arch ids BoolType) !Word64 !Word64
|
| Branch !(Value arch ids BoolType) !Word64 !Word64
|
||||||
-- | The syscall instruction.
|
|
||||||
-- We model system calls as terminal instructions because from the
|
|
||||||
-- application perspective, the semantics will depend on the operating
|
|
||||||
-- system.
|
|
||||||
| Syscall !(RegState (ArchReg arch) (Value arch ids))
|
|
||||||
-- | The block ended prematurely due to an error in instruction
|
-- | The block ended prematurely due to an error in instruction
|
||||||
-- decoding or translation.
|
-- decoding or translation.
|
||||||
--
|
--
|
||||||
@ -58,9 +53,6 @@ instance ArchConstraints arch
|
|||||||
indent 2 (pretty s)
|
indent 2 (pretty s)
|
||||||
pretty (Branch c x y) =
|
pretty (Branch c x y) =
|
||||||
text "branch" <+> ppValue 0 c <+> text (show x) <+> text (show y)
|
text "branch" <+> ppValue 0 c <+> text (show x) <+> text (show y)
|
||||||
pretty (Syscall s) =
|
|
||||||
text "syscall" <$$>
|
|
||||||
indent 2 (pretty s)
|
|
||||||
pretty (TranslateError s msg) =
|
pretty (TranslateError s msg) =
|
||||||
text "ERROR: " <+> text (Text.unpack msg) <$$>
|
text "ERROR: " <+> text (Text.unpack msg) <$$>
|
||||||
indent 2 (pretty s)
|
indent 2 (pretty s)
|
||||||
|
@ -194,8 +194,6 @@ rewriteTermStmt info tstmt = do
|
|||||||
pure $ Branch cn f t
|
pure $ Branch cn f t
|
||||||
| otherwise ->
|
| otherwise ->
|
||||||
pure $ Branch tgtCond t f
|
pure $ Branch tgtCond t f
|
||||||
Syscall regs ->
|
|
||||||
Syscall <$> traverseF rewriteValue regs
|
|
||||||
TranslateError regs msg ->
|
TranslateError regs msg ->
|
||||||
TranslateError <$> traverseF rewriteValue regs
|
TranslateError <$> traverseF rewriteValue regs
|
||||||
<*> pure msg
|
<*> pure msg
|
||||||
@ -229,8 +227,6 @@ addTermDemands t = do
|
|||||||
traverseF_ addValueDemands regs
|
traverseF_ addValueDemands regs
|
||||||
Branch v _ _ -> do
|
Branch v _ _ -> do
|
||||||
addValueDemands v
|
addValueDemands v
|
||||||
Syscall regs -> do
|
|
||||||
traverseF_ addValueDemands regs
|
|
||||||
TranslateError regs _ -> do
|
TranslateError regs _ -> do
|
||||||
traverseF_ addValueDemands regs
|
traverseF_ addValueDemands regs
|
||||||
ArchTermStmt _ regs -> do
|
ArchTermStmt _ regs -> do
|
||||||
@ -768,23 +764,6 @@ parseBlock ctx b regs = do
|
|||||||
, stmtsAbsState = absProcState'
|
, stmtsAbsState = absProcState'
|
||||||
}
|
}
|
||||||
|
|
||||||
Syscall s' -> do
|
|
||||||
mapM_ (recordWriteStmt arch_info mem absProcState') (blockStmts b)
|
|
||||||
let abst = finalAbsBlockState absProcState' s'
|
|
||||||
case concretizeAbsCodePointers mem (abst^.absRegState^.curIP) of
|
|
||||||
[] -> error "Could not identify concrete system call address"
|
|
||||||
[addr] -> do
|
|
||||||
-- Merge system call result with possible next IPs.
|
|
||||||
let post = archPostSyscallAbsState arch_info abst addr
|
|
||||||
|
|
||||||
intraJumpTargets %= ((addr, post):)
|
|
||||||
pure $! StatementList { stmtsIdent = idx
|
|
||||||
, stmtsNonterm = blockStmts b
|
|
||||||
, stmtsTerm = ParsedSyscall s' addr
|
|
||||||
, stmtsAbsState = absProcState'
|
|
||||||
}
|
|
||||||
_ -> error "Multiple system call addresses."
|
|
||||||
|
|
||||||
FetchAndExecute s' -> do
|
FetchAndExecute s' -> do
|
||||||
parseFetchAndExecute ctx idx (blockStmts b) regs s'
|
parseFetchAndExecute ctx idx (blockStmts b) regs s'
|
||||||
|
|
||||||
|
@ -168,9 +168,6 @@ data ParsedTermStmt arch ids
|
|||||||
-- ^ A return with the given registers.
|
-- ^ A return with the given registers.
|
||||||
| ParsedIte !(Value arch ids BoolType) !(StatementList arch ids) !(StatementList arch ids)
|
| ParsedIte !(Value arch ids BoolType) !(StatementList arch ids) !(StatementList arch ids)
|
||||||
-- ^ An if-then-else
|
-- ^ An if-then-else
|
||||||
| ParsedSyscall !(RegState (ArchReg arch) (Value arch ids))
|
|
||||||
!(ArchSegmentOff arch)
|
|
||||||
-- ^ A system call with the registers prior to call and given return address.
|
|
||||||
| ParsedArchTermStmt !(ArchTermStmt arch ids)
|
| ParsedArchTermStmt !(ArchTermStmt arch ids)
|
||||||
!(RegState (ArchReg arch) (Value arch ids))
|
!(RegState (ArchReg arch) (Value arch ids))
|
||||||
!(ArchSegmentOff arch)
|
!(ArchSegmentOff arch)
|
||||||
@ -217,9 +214,6 @@ ppTermStmt ppOff tstmt =
|
|||||||
text "ite" <+> pretty c <$$>
|
text "ite" <+> pretty c <$$>
|
||||||
ppStatementList ppOff t <$$>
|
ppStatementList ppOff t <$$>
|
||||||
ppStatementList ppOff f
|
ppStatementList ppOff f
|
||||||
ParsedSyscall s addr ->
|
|
||||||
text "syscall, return to" <+> text (show addr) <$$>
|
|
||||||
indent 2 (pretty s)
|
|
||||||
ParsedArchTermStmt ts s addr ->
|
ParsedArchTermStmt ts s addr ->
|
||||||
prettyF ts <> text ", return to" <+> text (show addr) <$$>
|
prettyF ts <> text ", return to" <+> text (show addr) <$$>
|
||||||
indent 2 (pretty s)
|
indent 2 (pretty s)
|
||||||
@ -254,51 +248,6 @@ data StatementList arch ids
|
|||||||
deriving instance ArchConstraints arch
|
deriving instance ArchConstraints arch
|
||||||
=> Show (StatementList arch ids)
|
=> Show (StatementList arch ids)
|
||||||
|
|
||||||
------------------------------------------------------------------------
|
|
||||||
-- Rewriting parsed blocks
|
|
||||||
|
|
||||||
{-
|
|
||||||
-- | Apply optimizations to a parsed terminal statement.
|
|
||||||
rewriteParsedTermStmt :: ParsedTermStmt arch src -> Rewriter arch src tgt (ParsedTermStmt arch tgt)
|
|
||||||
rewriteParsedTermStmt tstmt =
|
|
||||||
case tstmt of
|
|
||||||
ParsedCall regs mr -> do
|
|
||||||
ParsedCall <$> traverseF rewriteValue regs
|
|
||||||
<*> pure mr
|
|
||||||
ParsedJump regs a -> do
|
|
||||||
ParsedJump <$> traverseF rewriteValue regs
|
|
||||||
<*> pure a
|
|
||||||
ParsedLookupTable regs idx tbl -> do
|
|
||||||
ParsedLookupTable <$> traverseF rewriteValue regs
|
|
||||||
<*> rewriteValue idx
|
|
||||||
<*> pure tbl
|
|
||||||
ParsedReturn regs -> do
|
|
||||||
ParsedReturn <$> traverseF rewriteValue regs
|
|
||||||
ParsedIte c t f ->
|
|
||||||
ParsedIte <$> rewriteValue c
|
|
||||||
<*> rewriteStatementList t
|
|
||||||
<*> rewriteStatementList f
|
|
||||||
ParsedSyscall regs next ->
|
|
||||||
ParsedSyscall <$> traverseF rewriteValue regs
|
|
||||||
<*> pure next
|
|
||||||
ParsedTranslateError txt -> pure (ParsedTranslateError txt)
|
|
||||||
ClassifyFailure regs -> ClassifyFailure <$> traverseF rewriteValue regs
|
|
||||||
|
|
||||||
-- | Apply optimizations to code in the block
|
|
||||||
rewriteStatementList :: StatementList arch src -> Rewriter arch src tgt (StatementList arch tgt)
|
|
||||||
rewriteStatementList b = do
|
|
||||||
(tgtStmts, tgtTermStmt) <- collectRewrittenStmts $ do
|
|
||||||
mapM_ rewriteStmt (stmtsNonterm b)
|
|
||||||
rewriteParsedTermStmt (stmtsTerm b)
|
|
||||||
-- Return new block
|
|
||||||
pure $
|
|
||||||
StatementList { stmtsIdent = stmtsIdent b
|
|
||||||
, stmtsNonterm = tgtStmts
|
|
||||||
, stmtsTerm = tgtTermStmt
|
|
||||||
,
|
|
||||||
}
|
|
||||||
-}
|
|
||||||
|
|
||||||
------------------------------------------------------------------------
|
------------------------------------------------------------------------
|
||||||
-- ParsedBlock
|
-- ParsedBlock
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user