module Language.Boogie.Tester (
testProgram,
testSessionSummary,
TestSettings (..),
defaultGenericTypeRange,
defaultMapTypeRange,
ExhaustiveSettings (..),
RandomSettings (..),
Outcome (..),
outcomeDoc,
TestCase (..),
testCaseDoc,
Summary (..),
summaryDoc
) where
import Language.Boogie.AST
import Language.Boogie.Util
import Language.Boogie.Position
import Language.Boogie.TypeChecker
import Language.Boogie.Tokens
import Language.Boogie.PrettyPrinter
import Language.Boogie.Interpreter
import Language.Boogie.DataFlow
import System.Random
import Data.Maybe
import Data.List
import Data.Map (Map, (!))
import qualified Data.Map as M
import Control.Monad.Error
import Control.Applicative
import Control.Monad.State
import Text.PrettyPrint
testProgram :: TestSettings s => s -> Program -> Context -> [Id] -> [TestCase]
testProgram settings p tc procNames = evalState testExecution (settings, initEnvironment)
where
initEnvironment = emptyEnv { envTypeContext = tc }
testExecution = do
changeState snd (mapSnd . const) $ collectDefinitions p
concat <$> forM procNames testProcedure
testProcedure name = do
sig <- gets (procSig name . envTypeContext . snd)
defs <- gets (lookupProcedure name . snd)
concat <$> forM defs (testImplementation sig)
testSessionSummary :: [TestCase] -> Summary
testSessionSummary tcs = let
passing = [ x | x@(TestCase _ _ _ _ Pass) <- tcs ]
failing = [ x | x@(TestCase _ _ _ _ (Fail _)) <- tcs ]
invalid = [ x | x@(TestCase _ _ _ _ (Invalid _)) <- tcs ]
in Summary {
sPassCount = length passing,
sFailCount = length failing,
sInvalidCount = length invalid,
sUniqueFailures = nubBy equivalent failing
}
class TestSettings s where
generateIntInput :: State s [Integer]
generateBoolInput :: State s [Bool]
combineInputs :: (a -> State s [b]) -> [a] -> State s [[b]]
mapDomainSettings :: s -> ExhaustiveSettings
genericTypeRange :: s -> [Type]
mapTypeRange :: s -> [Type]
defaultGenericTypeRange _ = [BoolType]
defaultMapTypeRange context = [BoolType, IntType] ++ [Instance name [] | name <- M.keys (M.filter (== 0) (ctxTypeConstructors context))]
data ExhaustiveSettings = ExhaustiveSettings {
esIntRange :: [Integer],
esIntMapDomainRange :: [Integer],
esGenericTypeRange :: [Type],
esMapTypeRange :: [Type]
}
instance TestSettings ExhaustiveSettings where
generateIntInput = gets esIntRange
generateBoolInput = return [False, True]
combineInputs genOne args = sequence <$> mapM genOne args
mapDomainSettings s = s { esIntRange = esIntMapDomainRange s }
genericTypeRange = esGenericTypeRange
mapTypeRange = esMapTypeRange
data RandomSettings = RandomSettings {
rsRandomGen :: StdGen,
rsCount :: Int,
rsIntLimits :: (Integer, Integer),
rsIntMapDomainRange :: [Integer],
rsGenericTypeRange :: [Type],
rsMapTypeRange :: [Type]
}
setRandomGen gen rs = rs { rsRandomGen = gen }
instance TestSettings RandomSettings where
generateIntInput = do
randomGen <- gets rsRandomGen
limits <- gets rsIntLimits
n <- gets rsCount
changeState rsRandomGen setRandomGen $ replicateM n (state (randomR limits))
generateBoolInput = do
randomGen <- gets rsRandomGen
n <- gets rsCount
changeState rsRandomGen setRandomGen $ replicateM n (state random)
combineInputs genOne args = transpose <$> mapM genOne args
mapDomainSettings s = ExhaustiveSettings {
esIntRange = rsIntMapDomainRange s,
esIntMapDomainRange = rsIntMapDomainRange s,
esGenericTypeRange = rsGenericTypeRange s,
esMapTypeRange = rsMapTypeRange s
}
genericTypeRange = rsGenericTypeRange
mapTypeRange = rsMapTypeRange
type TestSession s a = State (s, Environment) a
instance Eq RuntimeFailure where
f == f' = rtfSource f == rtfSource f' && rtfPos f == rtfPos f'
data Outcome = Pass | Fail RuntimeFailure | Invalid RuntimeFailure
deriving Eq
outcomeDoc :: Outcome -> Doc
outcomeDoc Pass = text "passed"
outcomeDoc (Fail err) = text "failed: " <+> runtimeFailureDoc err
outcomeDoc (Invalid err) = text "invalid: " <+> runtimeFailureDoc err
instance Show Outcome where show o = show (outcomeDoc o)
data TestCase = TestCase {
tcProcedure :: Id,
tcLiveIns :: [Id],
tcLiveGlobals :: [Id],
tcInput :: [Value],
tcOutcome :: Outcome
} deriving Eq
testCaseDoc :: TestCase -> Doc
testCaseDoc (TestCase procName liveIns liveGlobals input outcome) = text procName <>
parens (commaSep (zipWith argDoc (liveIns ++ (map ("var " ++) liveGlobals)) input)) <+>
outcomeDoc outcome
where
argDoc name val = text name <+> text "=" <+> valueDoc val
instance Show TestCase where show tc = show (testCaseDoc tc)
equivalent tc1 tc2 = tcProcedure tc1 == tcProcedure tc2 && tcOutcome tc1 == tcOutcome tc2
data Summary = Summary {
sPassCount :: Int,
sFailCount :: Int,
sInvalidCount :: Int,
sUniqueFailures :: [TestCase]
}
totalCount s = sPassCount s + sFailCount s + sInvalidCount s
summaryDoc :: Summary -> Doc
summaryDoc summary =
text "Test cases:" <+> int (totalCount summary) $+$
text "Passed:" <+> int (sPassCount summary) $+$
text "Invalid:" <+> int (sInvalidCount summary) $+$
text "Failed:" <+> int (sFailCount summary) <+> parens (int (length (sUniqueFailures summary)) <+> text "unique") $+$
vsep (map testCaseDoc (sUniqueFailures summary))
instance Show Summary where show s = show (summaryDoc s)
testImplementation :: TestSettings s => PSig -> PDef -> TestSession s [TestCase]
testImplementation sig def = do
let paramTypes = map itwType (psigParams sig)
tc <- gets (envTypeContext . snd)
typeRange <- gets (genericTypeRange . fst)
let typeInputs = generateInputTypes typeRange tc { ctxTypeVars = psigTypeVars sig } paramTypes
concat <$> mapM typeTestCase typeInputs
where
typeTestCase :: TestSettings s => [Type] -> TestSession s [TestCase]
typeTestCase typeInputs = do
let localName index = [nonIdChar] ++ show index
let localNames = map localName [0..length (psigParams sig) 1]
modify $ mapSnd (modifyTypeContext (`setLocals` (M.fromList $ zip localNames typeInputs)))
tc <- gets (envTypeContext . snd)
let (inParams, outParams) = splitAt (length (psigArgs sig)) localNames
let (liveIns, liveGlobals) = liveInputVariables sig def
let livePositions = map (fromJust . (`elemIndex` pdefIns def)) liveIns
let liveActualIns = map localName livePositions
let liveGlobalVars = filter (`M.member` ctxGlobals tc) liveGlobals
let inputVars = liveActualIns ++ liveGlobalVars
let inTypes = map (typeInputs !!) livePositions ++ map (ctxGlobals tc !) liveGlobalVars
let execTestCase input = changeState snd (mapSnd . const) $ testCase inParams outParams inputVars input
let reportTestCase input = TestCase (psigName sig) liveIns liveGlobalVars input <$> execTestCase input
let genInputs = combineInputs (generateInputValue tc) inTypes
inputs <- changeState fst (mapFst . const) genInputs
mapM reportTestCase inputs
testCase :: [Id] -> [Id] -> [Id] -> [Value] -> SafeExecution Outcome
testCase inParams outParams inputVars inputVals = do
setAll inputVars inputVals
let inExpr = map (gen . Var) inParams
let outExpr = map (gen . Var) outParams
execSafely (execProcedure (assumePreconditions sig) def inExpr outExpr >> return Pass) failureReport
failureReport err = if failureKind err == Unreachable || failureKind err == Nonexecutable
then return $ Invalid err
else return $ Fail err
generateInputValue :: TestSettings s => Context -> Type -> State s [Value]
generateInputValue _ BoolType = map BoolValue <$> generateBoolInput
generateInputValue _ IntType = map IntValue <$> generateIntInput
generateInputValue c (MapType tv domains range) = do
typeRange <- gets mapTypeRange
let polyTypes = generateInputTypes typeRange c { ctxTypeVars = tv } (range : domains)
maps <- combineInputs monomorphicMap polyTypes
return $ map (MapValue . M.unions) maps
where
monomorphicMap (range : domains) = do
args <- withLocalState mapDomainSettings (combineInputs (generateInputValue c) domains)
rets <- combineInputs (generateInputValue c) (replicate (length args) range)
return $ map (\r -> M.fromList (zip args r)) rets
generateInputValue _ (Instance _ _) = map CustomValue <$> generateIntInput
generateInputTypes :: [Type] -> Context -> [Type] -> [[Type]]
generateInputTypes range c ts = do
let freeVars = filter (\x -> any (x `isFreeIn`) ts) (ctxTypeVars c)
actuals <- replicateM (length freeVars) range
let binding = M.fromList (zip freeVars actuals)
return $ map (typeSubst binding) ts