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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
|
module Main where
import Control.Monad ( unless, when )
import Control.Monad.Trans.Class ( lift )
import Control.Monad.Trans.State ( evalStateT, get, gets )
import Data.List ( (\\) )
import Data.Maybe ( fromJust )
import System.Environment ( getArgs )
import System.FilePath ( (</>) )
import System.Path ( fileInPath )
import System.Process ( exitWith )
import Contract.Names ( encodeContractName )
import Contract.Usage ( checkContractUsage )
import Debug.Profile ( ProcessInfo(ElapsedTime), getProcessInfos )
import FlatCurry.Annotated.Goodies
import FlatCurry.Files ( readFlatCurryInt, writeFlatCurry )
import FlatCurry.ShowIntMod ( showCurryModule )
import FlatCurry.TypeAnnotated.Files ( readTypeAnnotatedFlatCurry
, writeTypeAnnotatedFlatCurry )
import FlatCurry.Types ( Prog(Prog) )
import FlatCurry.Typed.Simplify ( simpProg )
import ContractProver
import Failfree
import FlatCurry.Typed.Read
import PackageConfig ( packagePath )
import ToolOptions
import VerifierState
test :: Int -> String -> IO ()
test v s = evalStateT (verifyMod s) $
initVState $ defaultOptions { optVerb = v }
testv :: String -> IO ()
testv = test 3
testcv :: String -> IO ()
testcv s = evalStateT (verifyMod s) $
initVState $ defaultOptions { optVerb = 3, optConFail = True }
banner :: String
banner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText = "Property Verification Tool for Curry (Version of 11/02/22)"
bannerLine = take (length bannerText) (repeat '=')
main :: IO ()
main = do
args <- getArgs
(opts,progs) <- processOptions banner args
let optname = optName opts
if not (null optname)
then putStrLn $ showEncodedNames optname
else do
z3exists <- fileInPath "z3"
if z3exists
then do
when (optVerb opts > 0) $ putStrLn banner
evalStateT (verifyModules [] progs) (initVState opts)
else do
putStrLn "PROPERTY VERIFICATION SKIPPED:"
putStrLn "The SMT solver Z3 is required for the verifier to work"
putStrLn "but the program 'z3' is not found on the PATH!"
exitWith 1
showEncodedNames :: String -> String
showEncodedNames cid = unlines
[ "Names to specify properties of operation '" ++ cid ++ "':"
, "Non-fail condition: " ++ encodeContractName (cid ++ "'nonfail")
, "Precondition: " ++ encodeContractName (cid ++ "'pre")
, "Postcondition: " ++ encodeContractName (cid ++ "'post")
]
verifyModules :: [String] -> [String] -> VStateM ()
verifyModules _ [] = return ()
verifyModules verifiedmods (mod : mods)
| mod `elem` verifiedmods = verifyModules verifiedmods mods
| otherwise = do
isRec <- getOption optRec
if isRec
then do
(Prog _ imps _ _ _) <- lift $ readFlatCurryInt mod
let newimps = filter (`notElem` verifiedmods) imps
if null newimps
then do
printWhenStatus ""
verifyMod mod
verifyModules (mod : verifiedmods) mods
else
verifyModules verifiedmods $ newimps ++ mod : (mods \\ newimps)
else do
verifyMod mod
verifyModules (mod : verifiedmods) mods
verifyMod :: String -> VStateM ()
verifyMod modname = do
printWhenStatus $ "Analyzing module '" ++ modname ++ "':"
oprog <- readTypedFlatCurryWithSpec modname
let errs = checkContractUsage (progName oprog)
(map (\fd -> (snd (funcName fd), funcType fd)) (progFuncs oprog))
unless (null errs) $ lift $ do
putStr $ unlines (map showOpError errs)
exitWith 1
let prog = simpProg oprog
failfree <- getOption optFailfree
impprogs <- if failfree
then mapM readSimpTypedFlatCurryWithSpec $ progImports prog
else return []
let allprogs = prog : impprogs
addProgsToState allprogs
addFunsToVerifyInfo $ concatMap progFuncs allprogs
pi1 <- lift getProcessInfos
printWhenAll $ unlines $
["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg oprog), line,
"SIMPLIFIED PROGRAM:", line, showCurryModule (unAnnProg prog), line]
whenOption optFailfree $ proveNonFailingFuncs prog
evalOption optContract (> 0) $ do
modifyOptions (\opts -> opts { optConFail = True })
prog1 <- verifyPostConditions oprog >>= verifyPreConditions
whenOption (\o -> optFCY o || optAFCY o) $ do
prog2 <- addPreConditions prog1
tprog <- lift $ do
ccprog <- fromJust <$>
readTypedFlatCurryFromPath "include" "ContractChecks"
let ccfuncs = progFuncs (rnmProg modname ccprog)
return $ updProgFuncs (++ ccfuncs) prog2
printWhenAll $ unlines $
["TRANSFORMED PROGRAM WITH CONTRACT CHECKING:", line,
showCurryModule (unAnnProg tprog), line]
whenOption optFCY $ lift $ writeFlatCurry $ unAnnProg tprog
whenOption optAFCY $ lift $ writeTypeAnnotatedFlatCurry tprog
pi2 <- lift $ getProcessInfos
let tdiff = maybe 0 id (lookup ElapsedTime pi2) -
maybe 0 id (lookup ElapsedTime pi1)
whenOption optTime $ lift $ putStrLn $
"TOTAL VERIFICATION TIME : " ++ show tdiff ++ " msec"
showStats
where
line = take 78 (repeat '-')
showOpError (qf,err) =
snd qf ++ " (module " ++ fst qf ++ "): " ++ err
axiomatizedOps :: [String]
axiomatizedOps = ["Prelude_null","Prelude_take","Prelude_length"]
|