summaryrefslogtreecommitdiff
path: root/Tests.hs
blob: 9848ea19485e6d99649044ca37ec5ac17ab79475 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
module Main where

import Language.Boogie.Parser
import Language.Boogie.PrettyPrinter
import Language.Boogie.TypeChecker
import Language.Boogie.Interpreter hiding (TestCase)
import qualified Language.Boogie.Interpreter as I
import Language.Boogie.Generator
import Data.Map (Map, (!))
import qualified Data.Map as M
import System.FilePath
import Text.ParserCombinators.Parsec (parse, parseFromFile)
import Test.HUnit

main = runTestTT allTests

allTests = TestList [parserTests, typeCheckerTests, interpreterTests]

parserTests = TestLabel "Parser" $ TestList [
  testCase parserSuccess "AttributeParsing"
  ]

typeCheckerTests = TestLabel "TypeChecker" $ TestList [
  testCase (typeCheckerFailure 8)   "BadLabels",
  testCase (typeCheckerFailure 4)   "Orderings",
  testCase (typeCheckerFailure 4)   "WhereResolution",
  testCase (typeCheckerFailure 35)  "Arrays",
  testCase (typeCheckerFailure 15)  "Frame",
  testCase (typeCheckerFailure 3)   "FunBody",
  testCase (typeCheckerFailure 3)   "IfThenElse",
  testCase (typeCheckerFailure 4)   "Lambda",
  testCase (typeCheckerFailure 12)  "UpdateExprTyping",
  testCase (typeCheckerFailure 1)   "TypeVarClash",
  testCase (typeCheckerFailure 8)   "GenericReturn",
  testCase (typeCheckerFailure 3)   "MissingTV",
  testCase typeCheckerSuccess       "DafnyPrelude",
  testCase typeCheckerSuccess       "VccPrelude"
  ]

interpreterTests = TestLabel "Interpreter" $ TestList [
  testCase interpreterSuccess "NoGuards",
  testCase interpreterSuccess "EmptyDomains",
  testCase interpreterSuccess "MapInit",
  testCase interpreterSuccess "MapLocals",
  testCase interpreterSuccess "OldND",
  testCase interpreterSuccess "OldMaps",
  testCase interpreterSuccess "MapEquality",
  testCase interpreterSuccess "Constraints"
  ]
  
-- | Directory with test programs  
testDir = "tests"  
-- | Entry point for test programs      
entryPoint = "Test"        
  
testCase kind name = TestLabel name (TestCase $ kind (testDir </> name <.> "bpl")) 
  
-- | Test that parser fails on file  
parserFailure file = do 
  parseResult <- parseFromFile program file
  case parseResult of
    Left parseErr -> return ()
    Right p -> assertFailure ("Undetected syntax error")  
  
-- | Test that parser succeeds on file, and re-parsing pretty printer code produces the same AST
parserSuccess file = do 
  parseResult <- parseFromFile program file
  case parseResult of
    Left parseErr -> assertFailure (show parseErr)
    Right p -> case parse program ('*' : file) (show p) of
      Left parseErr' -> assertFailure (show parseErr')
      Right p' -> if p == p'
        then return ()
        else assertFailure "Re-parsing resulted in a different AST"
  
-- | Test that type checker reports n errors on file  
typeCheckerFailure n file = do 
  parseResult <- parseFromFile program file
  case parseResult of
    Left parseErr -> assertFailure (show parseErr)
    Right p -> case typeCheckProgram p of
      Left typeErrs -> let m = length typeErrs in assertBool ("Expected " ++ show n ++ " type errors and got " ++ show m) (m == n)
      Right context -> assertFailure ("Expected " ++ show n ++ " type errors and got 0")
      
-- | Test that type checker succeeds on file
typeCheckerSuccess file = do 
  parseResult <- parseFromFile program file
  case parseResult of
    Left parseErr -> assertFailure (show parseErr)
    Right p -> case typeCheckProgram p of
      Left typeErrs -> assertFailure (show (typeErrorsDoc typeErrs))
      Right context -> return ()
      
-- | Test that interpreter succeeds (no run-time failures or crashes) on procedure entryPoint in file      
interpreterSuccess file = do 
  parseResult <- parseFromFile program file
  case parseResult of
    Left parseErr -> assertFailure (show parseErr)
    Right p -> case typeCheckProgram p of
      Left typeErrs -> assertFailure (show (typeErrorsDoc typeErrs))
      Right context -> case (head . filter (not . isInvalid)) (executeProgram p context (exhaustiveGenerator Nothing) Nothing entryPoint) of
        I.TestCase _ _ (Just err) -> assertFailure (show err)
        otherwise -> return ()