foxdec-0.1.0.0: Formaly Verified x86-64 Decompilation

VerificationReportInterface

Description

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 $head args 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 -> 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 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