Safe Haskell	None
Language	Haskell2010

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

class Show pred => Propagator ctxt pred where
- tau :: ctxt -> [Instruction] -> Maybe [Instruction] -> pred -> (pred, Set VerificationCondition)
- join :: ctxt -> pred -> pred -> pred
- implies :: ctxt -> pred -> pred -> Bool
do_prop :: Propagator ctxt pred => ctxt -> CFG -> Int -> pred -> (IntMap pred, Set VerificationCondition)
supremum :: Propagator ctxt pred => ctxt -> [pred] -> pred

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 Methods tau :: FContext -> [Instruction] -> Maybe [Instruction] -> Pred -> (Pred, Set VerificationCondition) Source # join :: FContext -> Pred -> Pred -> Pred Source # implies :: FContext -> Pred -> Pred -> Bool Source #

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