{-# LANGUAGE DeriveDataTypeable #-}
module Main where
import Language.Boogie.AST
import Language.Boogie.Util
import Language.Boogie.Position
import qualified Language.Boogie.Parser as Parser (program)
import Language.Boogie.TypeChecker
import Language.Boogie.PrettyPrinter
import Language.Boogie.Heap
import Language.Boogie.Environment
import Language.Boogie.Interpreter
import Language.Boogie.Generator
import System.Environment
import System.Console.CmdArgs
import System.Console.ANSI
import System.Random
import Data.Time.Calendar
import Data.List
import Data.Map (Map, (!))
import qualified Data.Map as M
import Control.Monad.State
import Control.Monad.Stream
import Control.Applicative
import Control.Lens hiding (Context, at)
import Text.PrettyPrint hiding (mode)
import Text.ParserCombinators.Parsec (parse, parseFromFile)
programName = "boogaloo"
versionName = "0.2"
releaseDate = fromGregorian 2013 2 5
-- | Execute or test a Boogie program, according to command-line arguments
main = do
res <- cmdArgsRun $ mode
case res of
Exec file proc_ bound random seed btmax invalid nexec pass fail outMax sum debug ->
executeFromFile file proc_ (natToMaybe bound) random seed btmax invalid nexec pass fail (natToMaybe outMax) sum debug
Test file proc_ bound outMax debug ->
executeFromFile file proc_ (natToMaybe bound) False Nothing Nothing True True True True (natToMaybe outMax) True debug
RTest file proc_ bound seed outMax debug ->
executeFromFile file proc_ (natToMaybe bound) True seed Nothing True True True True (natToMaybe outMax) True debug
where
natToMaybe n
| n >= 0 = Just n
| otherwise = Nothing
{- Command line arguments -}
data CommandLineArgs
= Exec {
file :: String,
proc_ :: String,
branch_max :: Integer,
random_ :: Bool,
seed :: Maybe Int,
exec_max :: Maybe Int,
invalid :: Bool,
nexec :: Bool,
pass :: Bool,
fail_ :: Bool,
out_max :: Int,
summary_ :: Bool,
debug :: Bool
}
| Test {
file :: String,
proc_ :: String,
branch_max :: Integer,
out_max :: Int,
debug :: Bool
}
| RTest {
file :: String,
proc_ :: String,
branch_max :: Integer,
seed :: Maybe Int,
out_max :: Int,
debug :: Bool
}
deriving (Data, Typeable, Show, Eq)
-- | Default branching
defaultBranch = 128
-- | Default branching in exhaustive testing
defaultExBranch = 8
-- | Default number of test cases in random testing
defaultRTC = 100
execute = Exec {
proc_ = "Main" &= help "Program entry point (default: Main)" &= typ "PROCEDURE",
file = "" &= typFile &= argPos 0,
branch_max = defaultBranch &= help ("Maximum number of possibilities for each non-deterministic choice; " ++
"unbounded if negative (default: " ++ show defaultBranch ++ ")"),
random_ = False &= help "Make non-deterministic choices randomly (default: false)",
seed = Nothing &= help "Seed for the random number generator" &= typ "NUM",
exec_max = Nothing &= help "Maximum number of executions to try (default: unlimited)",
invalid = False &= help "Display invalid executions (default: false)" &= name "I",
nexec = True &= help "Display executions that cannot be carried out completely (default: true)" &= name "N",
pass = True &= help "Display passing executions (default: true)" &= name "P",
fail_ = True &= help "Display failing executions (default: true)" &= name "F",
out_max = 1 &= help "Maximum number of executions to display; unbounded if negative (default: 1)",
summary_ = False &= help "Only print a summary of all executions and a list of unique failures (default: false)" &= name "S",
debug = False &= help "Debug output (default: false)"
} &= auto &= help "Execute program"
test = Test {
proc_ = "Main" &= help "Program entry point (default: Main)" &= typ "PROCEDURE",
file = "" &= typFile &= argPos 0,
branch_max = defaultExBranch &= help ("Maximum number of possibilities for each non-deterministic choice; " ++
"unbounded if negative (default: " ++ show defaultExBranch ++ ")"),
out_max = -1 &= help "Maximum number of test cases; unbounded if negative (default: -1)",
debug = False &= help "Debug output (default: false)"
} &= help "Test program exhaustively"
rtest = RTest {
proc_ = "Main" &= help "Program entry point (default: Main)" &= typ "PROCEDURE",
file = "" &= typFile &= argPos 0,
branch_max = defaultBranch &= help ("Maximum number of possibilities for each non-deterministic choice; " ++
"unbounded if negative (default: " ++ show defaultBranch ++ ")"),
seed = Nothing &= help "Seed for the random number generator" &= typ "NUM",
out_max = defaultRTC &= help ("Number of test cases; unbounded if negative (default: " ++ show defaultRTC ++")"),
debug = False &= help "Debug output (default: false)"
} &= help "Test program on random inputs"
mode = cmdArgsMode $ modes [execute, test, rtest] &=
help "Boogie interpreter" &=
program programName &=
summary (programName ++ " v" ++ versionName ++ ", " ++ showGregorian releaseDate)
{- Interfacing internal modules -}
-- | Execute procedure proc_ from file
-- | and output either errors or the final values of global variables
executeFromFile :: String -> String -> Maybe Integer -> Bool -> Maybe Int -> Maybe Int -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Bool -> Bool -> IO ()
executeFromFile file proc_ branch_max random seed exec_max invalid nexec pass fail out_max summary debug = runOnFile printFinalState file
where
printFinalState p context = case M.lookup proc_ (ctxProcedures context) of
Nothing -> printError (text "Cannot find procedure" <+> text proc_)
Just _ -> do
rGen <- case seed of
Nothing -> getStdGen
Just s -> return $ mkStdGen s
let generator = if random then randomGenerator rGen branch_max else exhaustiveGenerator branch_max
let outs = (maybeTake out_max . filter keep . maybeTake exec_max) (outcomes p context generator)
if summary
then do
let sum = testSessionSummary outs
print $ summaryDoc sum
zipWithM_ (printOne "Failure") [0..] (sUniqueFailures sum)
else if null outs
then printAux $ text "No executions to display"
else zipWithM_ (printOne "Execution") [0..] outs
outcomes p context generator = if exec_max == Just 1 || (keepAll && out_max == Just 1)
then [executeProgramDet p context branch_max proc_]
else executeProgram p context generator branch_max proc_
keepAll = invalid && nexec && pass && fail
maybeTake mLimit = case mLimit of
Nothing -> id
Just n -> take n
keep tc =
(if invalid then True else (not . isInvalid) tc) &&
(if nexec then True else (not . isNonexecutable) tc) &&
(if pass then True else (not . isPass) tc) &&
(if fail then True else (not . isFail) tc)
printTestCase tc = do
print $ testCaseSummary debug tc
case tcFailure tc of
Just err -> do
printNewline
printError $ runtimeFailureDoc debug err
when debug (printSeparate $ finalStateDoc True tc)
Nothing -> printSeparate $ finalStateDoc debug tc
printOne title n tc = do
when (n > 0) $ do printNewline; printNewline
printAux $ text title <+> integer n
printTestCase tc
-- | Parse file, type-check the resulting program, then execute command on the resulting program and type context
runOnFile :: (Program -> Context -> IO ()) -> String -> IO ()
runOnFile command file = do
parseResult <- parseFromFile Parser.program file
case parseResult of
Left parseErr -> printError parseErr
Right p -> case typeCheckProgram p of
Left typeErrs -> printError (typeErrorsDoc typeErrs)
Right context -> command p context
{- Output -}
-- | Output errors in red
printError e = do
setSGR [SetColor Foreground Vivid Red]
print e
setSGR [Reset]
-- | Output auxiliary messages in khaki
printAux msg = do
setSGR [SetColor Foreground Dull Yellow]
print msg
setSGR [Reset]
printNewline = putStr "\n"
printSeparate doc = when (not (isEmpty doc)) (do printNewline; print doc)
{- Helpers for testing internal functions -}
-- | Harness for testing various internal functions
harness file = runOnFile printOutcome file
where
printOutcome p context = do
let env = head (toList (execStateT (preprocess p) (initEnv context (exhaustiveGenerator (Just defaultBranch)) (Just defaultBranch))))
-- print $ memoryDoc True (env^.envMemory)
print $ abstractStoreDoc (env ^. envConstraints . amGlobals)