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

Analysis.Propagation

Description

We assume a class where we can do predicate transformation through function tau, and we can merge two predicates through function join. Moreover, we assume an implementation of a function implies that implements symbolic implication. Given these functions, we provide a generic abstract interpretation algorithm.

Synopsis

Documentation

class Show pred => Propagator ctxt pred where Source #

A class that allows propagation of predicates over a CFG.

Methods

tau :: ctxt -> [Instruction] -> Maybe [Instruction] -> pred -> (pred, Set VerificationCondition) Source #

Predicate transformation for an edge in in a CFG, over a basic blocks.

join :: ctxt -> pred -> pred -> pred Source #

A lattice-join

implies :: ctxt -> pred -> pred -> Bool Source #

Symbolic implication

Instances

Instances details
Propagator FContext Pred Source # 
Instance details

Defined in Analysis.SymbolicExecution

do_prop Source #

Arguments

:: Propagator ctxt pred 
=> ctxt

The context

-> CFG

The CFG

-> Int

The entry address

-> pred

The initial predicate

-> (IntMap pred, Set VerificationCondition) 

Start propagation at the given entry address with the given initial predicate. Returns a set of invariants, i.e., a mapping of instruction addresses to predicates.

supremum :: Propagator ctxt pred => ctxt -> [pred] -> pred Source #

The supremum of a list of predicates