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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
module VerifierState where
import IOExts
import List ( find, isSuffixOf )
import Contract.Names ( isNonFailName, isPreCondName, isPostCondName )
import FlatCurry.Typed.Types
import FlatCurry.Annotated.Goodies
import ToolOptions
data VerifyInfo = VerifyInfo
{ toolOpts :: Options
, allFuncs :: [TAFuncDecl]
, preConds :: [TAFuncDecl]
, postConds :: [TAFuncDecl]
, nfConds :: [TAFuncDecl]
}
initVerifyInfo :: Options -> VerifyInfo
initVerifyInfo opts = VerifyInfo opts [] [] [] []
addFunsToVerifyInfo :: [TAFuncDecl] -> VerifyInfo -> VerifyInfo
addFunsToVerifyInfo fdecls ti =
ti { allFuncs = fdecls ++ allFuncs ti
, preConds = preconds ++ preConds ti
, postConds = postconds ++ postConds ti
, nfConds = nfconds ++ nfConds ti
}
where
preconds = filter (isPreCondName . snd . funcName) fdecls
postconds = filter (isPostCondName . snd . funcName) fdecls
nfconds = filter (isNonFailName . snd . funcName) fdecls
isContractOp :: QName -> Bool
isContractOp (_,fn) = isNonFailName fn || isPreCondName fn || isPostCondName fn
isProperty :: TAFuncDecl -> Bool
isProperty fdecl =
resultType (funcType fdecl)
`elem` map (\tc -> TCons tc [])
[("Test.Prop","Prop"),("Test.EasyCheck","Prop")]
data VState = VState
{ trInfo :: VerifyInfo
, failedFuncs :: [(String,String)]
, numAllFuncs :: Int
, numNFCFuncs :: Int
, numPatTests :: Int
, numFailTests :: Int
, currTAProgs :: [TAProg]
}
initVState :: VerifyInfo -> VState
initVState info = VState info [] 0 0 0 0 []
readVerifyInfoRef :: IORef VState -> IO VerifyInfo
readVerifyInfoRef vstref = readIORef vstref >>= return . trInfo
showStats :: VState -> String
showStats vstate = unlines $
[ "TESTED OPERATIONS : " ++ show (numAllFuncs vstate)
, "NONFAIL CONDITIONS : " ++ show (numNFCFuncs vstate)
, "TESTS OF MISSING PATTERNS: " ++ show (numPatTests vstate)
, "TESTS OF NON-FAIL CALLS : " ++ show (numFailTests vstate) ] ++
showStat "POSSIBLY FAILING OPERATIONS" (failedFuncs vstate) ++
if isVerified vstate then ["NON-FAILURE VERIFICATION SUCCESSFUL!"] else []
where
showStat t fs =
if null fs
then []
else (t ++ ":") :
map (\ (fn,reason) -> fn ++ " (" ++ reason ++ ")")
(reverse fs)
isVerified :: VState -> Bool
isVerified vstate = null (failedFuncs vstate)
addFailedFuncToStats :: String -> String -> VState -> VState
addFailedFuncToStats fn qfun vstate =
vstate { failedFuncs = (fn,qfun) : failedFuncs vstate }
incNumAllInStats :: VState -> VState
incNumAllInStats vstate = vstate { numAllFuncs = numAllFuncs vstate + 1 }
incNumNFCInStats :: VState -> VState
incNumNFCInStats vstate = vstate { numNFCFuncs = numNFCFuncs vstate + 1 }
incPatTestInStats :: VState -> VState
incPatTestInStats vstate = vstate { numPatTests = numPatTests vstate + 1 }
incFailTestInStats :: VState -> VState
incFailTestInStats vstate = vstate { numFailTests = numFailTests vstate + 1 }
addProgToState :: AProg TypeExpr -> VState -> VState
addProgToState prog vstate = vstate { currTAProgs = prog : currTAProgs vstate }
tdeclOf :: VState -> QName -> Maybe TypeDecl
tdeclOf vst tcons@(mn,_) =
maybe Nothing
(\p -> find (\td -> typeName td == tcons) (progTypes p))
(find (\p -> progName p == mn) (currTAProgs vst))
|