foxdec-0.1.0.0: Formally Verified x86-64 Decompilation
This package contains tools for decompilation based on formal methods.
Modules
foxdec-0.1.0.0
- Algorithm
- Algorithm.Dominance Dominance
- Algorithm.SCC Strongly Connectd Components
- Base Some base functions, imported by almost all other modules.
- Binary
- Binary.Elf
- Binary.FunctionNames Provides functions to
- Binary.Generic
- Binary.Macho
- Binary.Read
- Config Some customizable constants.
- Conventions In this file, we eumerate assumptions made on calling conventions and over external functions.
- Data
- Data.CFG
- Data.Indirection
- Data.JumpTarget A datatype for resolving the operand of a jump/call
- Data.L0
- Data.SPointer
- Data.SValue
- Data.Size
- Data.Symbol
- Data.SymbolicExpression A datatype for symbolic expressions and symbolic predicates.
- Data.VerificationCondition
- X86
- Disassembler
- OutputGeneration
- OutputGeneration.Metrics
- NASM
- OutputGeneration.NASM.L0ToNASM Lift the L0 representation of the binary to symbolized and recompilable NASM.
- OutputGeneration.NASM.NASM A datastructure for storing NASM code.
- OutputGeneration.NASM.NASMToC Lift the L0 representation of the binary to symbolized and recompilable NASM.
- OutputGeneration.Reconstruction Reconstruct source-level constructs from the binary
- WithAbstractPredicates
- WithAbstractPredicates.Class
- WithAbstractPredicates.ContextSensitiveAnalysis
- WithAbstractPredicates.ControlFlow Contains functions pertaining to control flow graph generation.
- WithAbstractPredicates.GenerateCFG
- WithAbstractPredicates.GenerateInvariants
- WithAbstractSymbolicValues
- WithNoAbstraction
- WithNoAbstraction.Pointers Functions for dealing with symbolic pointers and abstraction.
- WithNoAbstraction.SymbolicExecution Provides an instantiation of all functions necessary to do symbolic propagation