foxdec-0.1.0.0: Formaly Verified x86-64 Decompilation
Safe HaskellNone
LanguageHaskell2010

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.

type FunctionEntry = Int Source #

Function Entries are simply integers

type InstructionAddress = Int Source #

Instruction Addresses are simply integers

ctxt_read_report Source #

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.

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 (Instr, 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