foxdec- Formally Verified x86-64 Decompilation
Safe HaskellNone



The interface to the .report generated after running FoxDec. After running FoxDec, a "verification report" (an object of type Context) can be retrieved from the generated .report file (see function ctxt_read_report). Essentially, this module provides hooks into some of the information retrieved and derived from the binary, including instructions, invariants, function entry points, etc.

A verification report is represented by the type Context, as internally it is just the context passed around and maintained during verification.

The main flow is to read the .report file and use these functions to retrieve information. The following example reads in a .report file provided as first command-line parameter and outputs the function entries:

 main = do
   args <- getArgs
   ctxt <- ctxt_read_report (args !! 0) (args !! 1)
   putStrLn $ show $ ctxt_get_function_entries ctxt

Some of the information is automatically also exported in plain-text format, for easy access.



type Retrieve a = Context -> Either String a Source #

The return type when retrieving information from a verification report: either an error message or a result.

type FunctionEntry = Int Source #

Function Entries are simply integers

type InstructionAddress = Int Source #

Instruction Addresses are simply integers

ctxt_read_report Source #


:: String

The filename of the .report file

-> String

The file name of the binary

-> IO Context 

Read in the .report file from a file with the given file name. May produce an error if no report can be read from the file. Returns the verification report stored in the .report file.

retrieve_io :: Either String a -> IO a Source #

Retrieve information from a Context read from a .report file, or die with an error message. For example:

  retrieve_io $ ctxt_get_instruction a ctxt

This code reads in a .report file with the given filename, and reads the instruction at address a if any.

ctxt_get_function_entries :: Retrieve (Set FunctionEntry) Source #

Retrieve all function entries.

Returns a set of funtion entries.

ctxt_get_instruction_addresses :: Retrieve (Set InstructionAddress) Source #

Retrieve all instruction addresses.

Returns a set of instruction addresses.

ctxt_get_indirections :: Retrieve Indirections Source #

Retrieve all indirections

Returns a mapping that provides for some instruction addresses a set of jump targets.

ctxt_get_instruction :: InstructionAddress -> Retrieve (Instruction, String) Source #

Retrieve instruction for a given instruction address, both as datastructure and pretty-printed

ctxt_get_invariant :: FunctionEntry -> InstructionAddress -> Retrieve Pred Source #

Retrieve invariant for a given function entry and instruction address

An invariant is a predicate provding information over registers, memory, flags, and verification conditions.

ctxt_get_internal_function_calls :: FunctionEntry -> Retrieve (Set FunctionEntry) Source #

Retrieve all internal function calls for a given function entry

Returns a set of function entries.

ctxt_get_cfg :: FunctionEntry -> Retrieve CFG Source #

Retrieve a CFG for a given function entry

ctxt_get_function_init :: FunctionEntry -> Retrieve FInit Source #

Retrieve a function initialization for a given function entry

ctxt_get_postcondition :: FunctionEntry -> Retrieve FReturnBehavior Source #

Retrieve a function initialization for a given function entry