Module Symbolic

This module provides data structures for tracing symbolic information.

Author: Jan Tikovsky

Version: December 2017

Summary of exported operations:

prelSymCons
                  ::  String -> TypeExpr -> SymObj

Create a symbolic constructor for a typed FlatCurry Prelude constructor

soType
                  ::  SymObj -> TypeExpr

Get the type of a symbolic object

lcNeg
                  ::  LConstr -> LConstr

Negate a literal constraint

lcMirror
                  ::  LConstr -> LConstr

Mirror literal constraint due to swapping of argument order

getLConstr
                  ::  (String,String) -> AExpr TypeExpr -> Maybe (Int,SymObj)

Generate a literal constraint from the given FlatCurry expression, if possible

rmvApplies
                  ::  AExpr TypeExpr -> AExpr TypeExpr

isApplyCall
                  ::  AExpr a -> Bool

litConstrs
                  ::  [((String,String),LConstr)]

List of supported literal constraints

ppTrace
                  ::  [Decision] -> Doc

Pretty printing of a symbolic trace

getSVars
                  ::  Decision -> [Int]

Get all symbolic variables of a decision

rnmTrace
                  ::  [Int] -> [Decision] -> ([[Decision]],Int) -> ([[Decision]],Int)

Rename all variables occuring in a symbolic trace

mkCoveredCs
                  ::  SymObj -> [Int] -> CoveredCs

Create information on covered constructors / constraint

Exported datatypes:

SymObj

Symbolic objects Symbolic object

symbolic FlatCurry constructor
constraint on symbolic literal

Constructors:

SymCons :: QName -> TypeExpr -> SymObj
SymLit :: LConstr -> Literal -> SymObj

LConstr

Literal constraint

Constructors:

E :: LConstr
NE :: LConstr
L :: LConstr
LE :: LConstr
G :: LConstr
GE :: LConstr

Trace

Symbolic tracing of case branches Symbolic trace

Type synonym: Trace = [Decision]

Decision

Symbolic information for branch decisions

identifier of case expression
number of selected branch
associated symbolic variable
symbolic object (i.e. chosen constructor or literal constraint)
possible symbolic variables for arguments

Constructors:

Decision :: CaseID -> BranchNr -> VarIndex -> SymObj -> [VarIndex] -> Decision

CaseID

Case identifier

Type synonym: CaseID = VarIndex

BranchNr

Branch number, i.e. branch m of n branches

Constructors:

BNr :: Int -> Int -> BranchNr

PathConstr

Nodes of symbolic execution tree Representation of path constraints, i.e.

decision variable
symbolic object
argument variables

Type synonym: PathConstr = (VarIndex,SymObj,[VarIndex])

SymNode

A symbolic node includes the following information:

the depth of the node in the execution tree,
the context of the node, i.e. its case id and preceeding case ids,
indices of SMT-LIB constants which are required for the SMT-LIB model
possible path constraints and
the decision variables introduced up to this node
the decision variable of this node

Constructors:

SymNode :: Depth -> Context -> [VarIndex] -> [PathConstr] -> [VarIndex] -> VarIndex -> SymNode
Fields:
- depth :: Depth
- context :: Context
- constants :: [VarIndex]
- pcs :: [PathConstr]
- dvars :: [VarIndex]
- dvar :: VarIndex

Depth

Node depth in a symbolic execution tree

Type synonym: Depth = Int

Context

A context is a case identifier followed by a sequence of preceeding case identifiers

Type synonym: Context = [VarIndex]

CoverInfo

Coverage information Coverage information for case expressions

ids of uncovered branches
information on already covered constructors / literal constraints

Constructors:

CoverInfo :: [Int] -> CoveredCs -> CoverInfo
Fields:
- uncovered :: [Int]
- coveredCs :: CoveredCs

CoveredCs

Covered constructors / literal constraints

Constructors:

CCons :: [(SymObj,[VarIndex])] -> CoveredCs
CConstr :: LConstr -> Literal -> CoveredCs

Exported operations:

prelSymCons :: String -> TypeExpr -> SymObj

Create a symbolic constructor for a typed FlatCurry Prelude constructor

Further infos:

solution complete, i.e., able to compute all solutions

soType :: SymObj -> TypeExpr

Get the type of a symbolic object

lcNeg :: LConstr -> LConstr

Negate a literal constraint

Further infos:

solution complete, i.e., able to compute all solutions

lcMirror :: LConstr -> LConstr

Mirror literal constraint due to swapping of argument order

getLConstr :: (String,String) -> AExpr TypeExpr -> Maybe (Int,SymObj)

Generate a literal constraint from the given FlatCurry expression, if possible

rmvApplies :: AExpr TypeExpr -> AExpr TypeExpr

isApplyCall :: AExpr a -> Bool

litConstrs :: [((String,String),LConstr)]

List of supported literal constraints

ppTrace :: [Decision] -> Doc

Pretty printing of a symbolic trace

getSVars :: Decision -> [Int]

Get all symbolic variables of a decision

Further infos:

solution complete, i.e., able to compute all solutions

rnmTrace :: [Int] -> [Decision] -> ([[Decision]],Int) -> ([[Decision]],Int)

Rename all variables occuring in a symbolic trace

mkCoveredCs :: SymObj -> [Int] -> CoveredCs

Create information on covered constructors / constraint

Further infos:

solution complete, i.e., able to compute all solutions