foxdec-0.1.0.0: Formally Verified x86-64 Decompilation

VerificationReportInterface

Description

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.

Synopsis

# Documentation

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.

Function Entries are simply integers

Arguments

 :: 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 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.

Retrieve all function entries.

Returns a set of funtion entries.

Returns a set of instruction addresses.

Retrieve all indirections

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

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

Retrieve invariant for a given function entry and instruction address

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

Retrieve all internal function calls for a given function entry

Returns a set of function entries.

Retrieve a CFG for a given function entry

Retrieve a function initialization for a given function entry

Retrieve a function initialization for a given function entry