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

---------------------------------------------------------------------------
-- Some global information used by the verification process:
data VerifyInfo = VerifyInfo
  { toolOpts      :: Options      -- options passed to the tool
  , allFuncs      :: [TAFuncDecl] -- all defined operations
  , preConds      :: [TAFuncDecl] -- all precondition operations
  , postConds     :: [TAFuncDecl] -- all postcondition operations
  , nfConds       :: [TAFuncDecl] -- all non-failure condition operations
  }

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
  -- Precondition operations:
  preconds  = filter (isPreCondName  . snd . funcName) fdecls
  -- Postcondition operations:
  postconds = filter (isPostCondName . snd . funcName) fdecls
  -- Non-failure condition operations:
  nfconds   = filter (isNonFailName  . snd . funcName) fdecls

--- Is an operation name the name of a contract or similar?
isContractOp :: QName -> Bool
isContractOp (_,fn) = isNonFailName fn || isPreCondName fn || isPostCondName fn

--- Is a function declaration a property?
isProperty :: TAFuncDecl -> Bool
isProperty fdecl =
  resultType (funcType fdecl)
    `elem` map (\tc -> TCons tc [])
               [("Test.Prop","Prop"),("Test.EasyCheck","Prop")]

---------------------------------------------------------------------------
-- The global state of the verification process keeps some
-- statistical information and the programs that are already read (to
-- avoid multiple readings).
data VState = VState
  { trInfo       :: VerifyInfo        -- information used by the verifier
  , failedFuncs  :: [(String,String)] -- partially defined operations
                                      -- and their failing reason
  , numAllFuncs  :: Int               -- number of analyzed operations
  , numNFCFuncs  :: Int               -- number of operations with non-trivial
                                      -- non-failing conditions
  , numPatTests  :: Int               -- number of missing pattern tests
  , numFailTests :: Int               -- number of tests of failure calls
  , currTAProgs  :: [TAProg]          -- already read typed FlatCurry programs
  }

initVState :: VerifyInfo -> VState
initVState info = VState info [] 0 0 0 0 []

--- Reads VerifyInfo from VState IORef.
readVerifyInfoRef :: IORef VState -> IO VerifyInfo
readVerifyInfoRef vstref = readIORef vstref >>= return . trInfo

--- Shows the statistics in human-readable format.
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)

--- Are all non-failing properties verified?
isVerified :: VState -> Bool
isVerified vstate = null (failedFuncs vstate)

--- Adds a possibly failing call in a functions and the called function.
addFailedFuncToStats :: String -> String -> VState -> VState
addFailedFuncToStats fn qfun vstate =
  vstate { failedFuncs = (fn,qfun) : failedFuncs vstate }

--- Increments the number of all tested functions.
incNumAllInStats :: VState -> VState
incNumAllInStats vstate = vstate { numAllFuncs = numAllFuncs vstate + 1 }

--- Increments the number of operations with nonfail conditions.
incNumNFCInStats :: VState -> VState
incNumNFCInStats vstate = vstate { numNFCFuncs = numNFCFuncs vstate + 1 }

--- Increments the number of missing pattern tests.
incPatTestInStats :: VState -> VState
incPatTestInStats vstate = vstate { numPatTests = numPatTests vstate + 1 }

--- Increments the number of test of posibble failure calls.
incFailTestInStats :: VState -> VState
incFailTestInStats vstate = vstate { numFailTests = numFailTests vstate + 1 }

--- Adds a new typed FlatCurry program to the state.
addProgToState :: AProg TypeExpr -> VState -> VState
addProgToState prog vstate = vstate { currTAProgs = prog : currTAProgs vstate }

---------------------------------------------------------------------------
--- Selects the type declaration of a type constructor from the state.
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))

---------------------------------------------------------------------------