Module Search

This module includes the main search loop of the ccti.

Author: Jan Tikovsky

Version: December 2017

Summary of exported operations:

ppTestCase
                  ::  (AExpr TypeExpr,[AExpr TypeExpr]) -> Doc

Pretty printing of test cases

initCSState
                  ::  CCTOpts -> SMTInfo -> [Int] -> CSState

Initial state for the concolic search

execCSM
                  ::  CSM a -> CSState -> SMTSess CSState

gets
                  ::  (CSState -> a) -> CSM a

get
                  ::  CSM CSState

put
                  ::  CSState -> CSM ()

modify
                  ::  (CSState -> CSState) -> CSM ()

liftSMTSess
                  ::  SMTSess a -> CSM a

Lift SMT sessions to CSM

io
                  ::  IO a -> CSM a

Lift IO actions to CSM

getOpts
                  ::  CSM CCTOpts

Get concolic search options

getSymTree
                  ::  CSM (PQ Int SymNode)

Get current symbolic tree

setSymTree
                  ::  PQ Int SymNode -> CSM ()

getCoverMap
                  ::  CSM (ContextMap [Int] CoverInfo)

Get current map of unvisited branches

getSMTInfo
                  ::  CSM SMTInfo

Get SMTInfo object

getSymArgs
                  ::  CSM [Int]

Get symbolic arguments of expression to be tested

getTestCases
                  ::  CSM [(AExpr TypeExpr,[AExpr TypeExpr])]

Get current test suite

addTestCase
                  ::  (AExpr TypeExpr,[AExpr TypeExpr]) -> CSM Bool

Add a test case to the current test suite Return True if its a new test case and False otherwise

addSMTFail
                  ::  [SMTError] -> [Int] -> [Command] -> CSM ()

Add information on SMT solver failure

getCovered
                  ::  [Int] -> CSM CoveredCs

Get the constructors / constraints already covered for a given context

updSymInfo
                  ::  [Decision] -> CSM ()

processTrace
                  ::  CCTOpts -> [Decision] -> PQ Int SymNode -> ContextMap [Int] CoverInfo -> SMTInfo -> (PQ Int SymNode,ContextMap [Int] CoverInfo,SMTInfo)

csearch
                  ::  CCTOpts -> [AFuncDecl (TypeExpr,Maybe Int,Bool)] -> Int -> SMTInfo -> AExpr (TypeExpr,Maybe Int,Bool) -> IO [(AExpr TypeExpr,[AExpr TypeExpr])]

Generate constraint information Generate a path constraint

searchLoop
                  ::  FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> CEState -> AExpr (TypeExpr,Maybe Int,Bool) -> CSM ()

searchLoopN
                  ::  Int -> CSM () -> FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> CEState -> AExpr (TypeExpr,Maybe Int,Bool) -> CSM ()

main loop of concolic search

renameTraces
                  ::  ([AExpr (TypeExpr,Maybe Int,Bool)],[[Decision]],Int) -> CSM ([AExpr (TypeExpr,Maybe Int,Bool)],[[Decision]],Int)

Renaming of trace variables

nextSymNode
                  ::  CSM (Maybe SymNode)

Get next symbolic node from search tree if there is still one left abort criterion

rmvSymNode
                  ::  CSM ()

Remove next node from symbolic tree

genSMTCmds
                  ::  Int -> SymNode -> CSM [Command]

Generate SMT-LIB commands for the variable declarations and the assertion of path constraints for the given symbolic node

getSMTArgs
                  ::  SymNode -> FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> [Int]

Get variable indices for arguments of concolically tested expression

genSMTFail
                  ::  SMTFail -> [Command] -> [Command]

Generate SMT commands from SMTFails

skipSymNode
                  ::  SymNode -> CSM ()

Skip a node in the symbolic execution tree by marking all its branches as covered

Exported datatypes:

CoverMap

Map of unvisited symbolic nodes, i.e. case branches

Type synonym: CoverMap = ContextMap Context CoverInfo

SymTree

Represent symbolic execution tree by priority queue

Type synonym: SymTree = PQ Depth SymNode

TestCase

Test case data: function call with arguments and corresponding non-deterministic results

Type synonym: TestCase = (AExpr TypeExpr,[AExpr TypeExpr])

SMTFail

Information on SMT solver failures

Constructors:

SMTFail :: [SMTError] -> [VarIndex] -> [Command] -> SMTFail

CSState

Constructors:

CSState :: CCTOpts -> SMTInfo -> SymTree -> CoverMap -> [TestCase] -> [VarIndex] -> [SMTFail] -> CSState
Fields:
- cssCCTOpts :: CCTOpts
- cssSMTInfo :: SMTInfo
- cssTree :: SymTree
- cssCoverMap :: CoverMap
- cssTests :: [TestCase]
- cssSymArgs :: [VarIndex]
- cssSMTFails :: [SMTFail]

CSM

Concolic search monad

Constructors:

CS :: (CSState -> SMTSess (a,CSState)) -> CSM a
Fields:
- runCSM :: (CSState -> SMTSess (a,CSState))

UpdSymInfo

Type synonym: UpdSymInfo = SymTree -> CoverMap -> SMTInfo -> (SymTree,CoverMap,SMTInfo)

Exported operations:

ppTestCase :: (AExpr TypeExpr,[AExpr TypeExpr]) -> Doc

Pretty printing of test cases

initCSState :: CCTOpts -> SMTInfo -> [Int] -> CSState

Initial state for the concolic search

execCSM :: CSM a -> CSState -> SMTSess CSState

gets :: (CSState -> a) -> CSM a

get :: CSM CSState

put :: CSState -> CSM ()

modify :: (CSState -> CSState) -> CSM ()

liftSMTSess :: SMTSess a -> CSM a

Lift SMT sessions to CSM

io :: IO a -> CSM a

Lift IO actions to CSM

getOpts :: CSM CCTOpts

Get concolic search options

getSymTree :: CSM (PQ Int SymNode)

Get current symbolic tree

setSymTree :: PQ Int SymNode -> CSM ()

getCoverMap :: CSM (ContextMap [Int] CoverInfo)

Get current map of unvisited branches

getSMTInfo :: CSM SMTInfo

Get SMTInfo object

getSymArgs :: CSM [Int]

Get symbolic arguments of expression to be tested

getTestCases :: CSM [(AExpr TypeExpr,[AExpr TypeExpr])]

Get current test suite

addTestCase :: (AExpr TypeExpr,[AExpr TypeExpr]) -> CSM Bool

Add a test case to the current test suite Return True if its a new test case and False otherwise

addSMTFail :: [SMTError] -> [Int] -> [Command] -> CSM ()

Add information on SMT solver failure

getCovered :: [Int] -> CSM CoveredCs

Get the constructors / constraints already covered for a given context

updSymInfo :: [Decision] -> CSM ()

processTrace :: CCTOpts -> [Decision] -> PQ Int SymNode -> ContextMap [Int] CoverInfo -> SMTInfo -> (PQ Int SymNode,ContextMap [Int] CoverInfo,SMTInfo)

csearch :: CCTOpts -> [AFuncDecl (TypeExpr,Maybe Int,Bool)] -> Int -> SMTInfo -> AExpr (TypeExpr,Maybe Int,Bool) -> IO [(AExpr TypeExpr,[AExpr TypeExpr])]

Generate constraint information Generate a path constraint

searchLoop :: FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> CEState -> AExpr (TypeExpr,Maybe Int,Bool) -> CSM ()

searchLoopN :: Int -> CSM () -> FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> CEState -> AExpr (TypeExpr,Maybe Int,Bool) -> CSM ()

main loop of concolic search

renameTraces :: ([AExpr (TypeExpr,Maybe Int,Bool)],[[Decision]],Int) -> CSM ([AExpr (TypeExpr,Maybe Int,Bool)],[[Decision]],Int)

Renaming of trace variables

nextSymNode :: CSM (Maybe SymNode)

Get next symbolic node from search tree if there is still one left abort criterion

rmvSymNode :: CSM ()

Remove next node from symbolic tree

genSMTCmds :: Int -> SymNode -> CSM [Command]

Generate SMT-LIB commands for the variable declarations and the assertion of path constraints for the given symbolic node

getSMTArgs :: SymNode -> FM Int (AExpr (TypeExpr,Maybe Int,Bool)) -> [Int]

Get variable indices for arguments of concolically tested expression

genSMTFail :: SMTFail -> [Command] -> [Command]

Generate SMT commands from SMTFails

skipSymNode :: SymNode -> CSM ()

Skip a node in the symbolic execution tree by marking all its branches as covered