| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
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
- type Retrieve a = Context -> Either String a
- type FunctionEntry = Int
- type InstructionAddress = Int
- ctxt_read_report :: String -> String -> IO Context
- retrieve_io :: Either String a -> IO a
- ctxt_get_function_entries :: Retrieve (Set FunctionEntry)
- ctxt_get_instruction_addresses :: Retrieve (Set InstructionAddress)
- ctxt_get_indirections :: Retrieve Indirections
- ctxt_get_instruction :: InstructionAddress -> Retrieve (Instruction, String)
- ctxt_get_invariant :: FunctionEntry -> InstructionAddress -> Retrieve Pred
- ctxt_get_internal_function_calls :: FunctionEntry -> Retrieve (Set FunctionEntry)
- ctxt_get_cfg :: FunctionEntry -> Retrieve CFG
- ctxt_get_function_init :: FunctionEntry -> Retrieve FInit
- ctxt_get_postcondition :: FunctionEntry -> Retrieve FReturnBehavior
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
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