Skip to content

x86: Small change to use a total helper function from Macaw #2672

Description

@langston-barrett

This function has a case marked Bug?:

callHandler :: Overrides -> CallHandler
callHandler callMap sym = Macaw.LookupFunctionHandle $ \st mem regs -> do
case lookupX86Reg X86_IP regs of
Just (RV ptr) | LLVMPointer base off <- ptr ->
case (asNat base, BV.asUnsigned <$> asBV off) of
(Just b, Just o) ->
case Map.lookup (b,o) callMap of
Just h -> case h sym of
Macaw.LookupFunctionHandle f -> f st mem regs
Nothing ->
fail ("No over-ride for function: " ++ show (ppPtr ptr))
_ -> fail ("Non-static call: " ++ show (ppPtr ptr))
_ -> fail "[Bug?] Failed to obtain the value of the IP register."

Indeed, it is actually an infeasible case. This could be made more obvious by indexing into the register struct with rip from macaw-symbolic. For an example of how this is done, see this GREASE commit.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

subprojectIssues involving one of the various subprojects SAW depends onsubsystem: x86Issues related to verifying x86 binaries via Macawtech debtIssues that document or involve technical debttopics: error-handlingIssues involving the way SAW responds to an error conditiontype: bugIssues reporting bugs or unexpected/unwanted behavior

Type

No type

Projects

No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions