----------------------------------------------------------------------------- --- A tool to verify non-failure properties of Curry operations. --- --- @author Michael Hanus --- @version August 2018 --------------------------------------------------------------------------- module Main where import Directory ( doesFileExist ) import FilePath ( () ) import IOExts import List ( (\\), elemIndex, find, isPrefixOf, isSuffixOf , maximum, minimum, splitOn, union ) import Maybe ( catMaybes ) import Profile import ReadNumeric ( readHex ) import State import System -- Imports from dependencies: import Analysis.ProgInfo import Analysis.TotallyDefined ( siblingCons ) import Analysis.Types import CASS.Server ( analyzeGeneric, analyzePublic ) import FlatCurry.Annotated.Types import FlatCurry.Files import FlatCurry.Types import qualified FlatCurry.Goodies as FCG import FlatCurry.Annotated.Goodies import ShowFlatCurry ( showCurryModule ) -- Imports from package modules: import BoolExp import Curry2SMT import PackageConfig ( packagePath ) import PatternAnalysis import ToolOptions import TypedFlatCurryGoodies import VerifierState ------------------------------------------------------------------------ -- To support testing: test :: Int -> String -> IO () test v = verifyNonFailingMod defaultOptions { optVerb = v } testv :: String -> IO () testv = test 3 ------------------------------------------------------------------------ banner :: String banner = unlines [bannerLine,bannerText,bannerLine] where bannerText = "Fail-Free Verification Tool for Curry (Version of 30/08/18)" bannerLine = take (length bannerText) (repeat '=') --------------------------------------------------------------------------- main :: IO () main = do args <- getArgs (opts,progs) <- processOptions banner args z3exists <- fileInPath "z3" if z3exists then do when (optVerb opts > 0) $ putStrLn banner verifyNonFailingModules opts [] progs else do putStrLn "NON-FAILING ANALYSIS SKIPPED:" putStrLn "The SMT solver Z3 is required for the analyzer to work" putStrLn "but the program 'z3' is not found on the PATH!" exitWith 1 verifyNonFailingModules :: Options -> [String] -> [String] -> IO () verifyNonFailingModules _ _ [] = done verifyNonFailingModules opts verifiedmods (mod:mods) | mod `elem` verifiedmods = verifyNonFailingModules opts verifiedmods mods | optRec opts = do (Prog _ imps _ _ _) <- readFlatCurryInt mod let newimps = filter (`notElem` verifiedmods) imps if null newimps then do printWhenStatus opts "" verifyNonFailingMod opts mod verifyNonFailingModules opts (mod:verifiedmods) mods else verifyNonFailingModules opts verifiedmods (newimps ++ mod : (mods \\ newimps)) | otherwise -- non-recursive = do verifyNonFailingMod opts mod verifyNonFailingModules opts (mod:verifiedmods) mods verifyNonFailingMod :: Options -> String -> IO () verifyNonFailingMod opts modname = do printWhenStatus opts $ "Analyzing module '" ++ modname ++ "':" prog <- readTypedFlatCurryWithSpec opts modname impprogs <- mapIO (readTypedFlatCurryWithSpec opts) (progImports prog) let vstate = foldr addProgToState initVState (prog:impprogs) tinfo = foldr addFunsToTransInfo (initTransInfo opts) (map progFuncs (prog:impprogs)) siblingconsinfo <- loadAnalysisWithImports siblingCons prog pi1 <- getProcessInfos printWhenAll opts $ unlines $ ["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg prog), line] stats <- proveNonFailingFuncs opts siblingconsinfo tinfo (progFuncs prog) vstate pi2 <- getProcessInfos let tdiff = maybe 0 id (lookup ElapsedTime pi2) - maybe 0 id (lookup ElapsedTime pi1) when (optTime opts) $ putStrLn $ "TOTAL VERIFICATION TIME : " ++ show tdiff ++ " msec" when (optVerb opts > 0 || not (isVerified stats)) $ putStr (showStats stats) where line = take 78 (repeat '-') -- Loads CASS analysis results for a module and its imported entities. loadAnalysisWithImports :: Analysis a -> TAProg -> IO (ProgInfo a) loadAnalysisWithImports analysis prog = do maininfo <- analyzeGeneric analysis (progName prog) >>= return . either id error impinfos <- mapIO (\m -> analyzePublic analysis m >>= return . either id error) (progImports prog) return $ foldr combineProgInfo maininfo impinfos --------------------------------------------------------------------------- -- Some global information used by the transformation process: data TransInfo = TransInfo { toolOpts :: Options -- options passed to all defined operations , allFuncs :: [TAFuncDecl] -- all defined operations , preConds :: [TAFuncDecl] -- all precondition operations , postConds :: [TAFuncDecl] -- all postcondition operations , nfConds :: [TAFuncDecl] -- all non-failure condition operations } initTransInfo :: Options -> TransInfo initTransInfo opts = TransInfo opts [] [] [] [] addFunsToTransInfo :: [TAFuncDecl] -> TransInfo -> TransInfo addFunsToTransInfo fdecls ti = ti { allFuncs = fdecls ++ allFuncs ti , preConds = preconds ++ preConds ti , postConds = postconds ++ postConds ti , nfConds = nfconds ++ nfConds ti } where -- Precondition operations: preconds = filter (\fd -> "'pre" `isSuffixOf` snd (funcName fd)) fdecls -- Postcondition operations: postconds = filter (\fd -> "'post" `isSuffixOf` snd (funcName fd)) fdecls -- Non-failure condition operations: nfconds = filter (\fd -> "'nonfail" `isSuffixOf` snd (funcName fd)) fdecls --- Is an operation name the name of a contract or similar? isContractOp :: QName -> Bool isContractOp (_,fn) = "'nonfail" `isSuffixOf` fn || "'pre" `isSuffixOf` fn || "'post" `isSuffixOf` 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 state of the transformation process contains -- * the current assertion -- * a fresh variable index -- * a list of all introduced variables and their types: data TransState = TransState { preCond :: BoolExp , freshVar :: Int , varTypes :: [(Int,TypeExpr)] } makeTransState :: Int -> [(Int,TypeExpr)] -> TransState makeTransState = TransState bTrue -- Increments fresh variable index. incFreshVarIndex :: TransState -> TransState incFreshVarIndex st = st { freshVar = freshVar st + 1 } -- Adds variables to the state. addVarTypes :: [(Int,TypeExpr)] -> TransState -> TransState addVarTypes vts st = st { varTypes = vts ++ varTypes st } --------------------------------------------------------------------------- -- Eliminate possible preconditions checks: -- If an operation `f` occurring in a right-hand side has -- a precondition check, a proof for the validity of the precondition -- is extracted and, if the proof is successful, the operation without -- the precondtion check `f'WithoutPreCondCheck` is called instead. proveNonFailingFuncs :: Options -> ProgInfo [(QName,Int)] -> TransInfo -> [TAFuncDecl] -> VState -> IO VState proveNonFailingFuncs opts siblingconsinfo ti fdecls stats = do vstref <- newIORef stats mapIO_ (proveNonFailingFunc opts siblingconsinfo ti vstref) fdecls readIORef vstref proveNonFailingFunc :: Options -> ProgInfo [(QName,Int)] -> TransInfo -> IORef VState -> TAFuncDecl -> IO () proveNonFailingFunc opts siblingconsinfo ti vstref fdecl = unless (isContractOp (funcName fdecl) || isProperty fdecl) $ do printWhenIntermediate opts $ "Operation to be analyzed: " ++ snd (funcName fdecl) modifyIORef vstref incNumAllInStats let efdecl = etaExpandFuncDecl fdecl proveNonFailingRule opts siblingconsinfo ti (funcName efdecl) (funcArity efdecl) (funcRule efdecl) vstref proveNonFailingRule :: Options -> ProgInfo [(QName,Int)] -> TransInfo -> QName -> Int -> TARule -> IORef VState -> IO () proveNonFailingRule _ _ ti qn farity (AExternal _ _) vstref = do let (nfcond,_) = nonfailPreCondExpOf ti qn [1..farity] (makeTransState 0 []) unless (nfcond == bTrue) $ modifyIORef vstref incNumNFCInStats proveNonFailingRule opts siblingconsinfo ti qn@(_,fn) _ (ARule _ rargs rhs) vstref = do let farity = length rargs -- compute non-fail precondition of operation: s0 = makeTransState (maximum (0 : map fst rargs ++ allVars rhs) + 1) rargs (precondformula,s1) = nonfailPreCondExpOf ti qn [1..farity] s0 s2 = s1 { preCond = precondformula } unless (precondformula == bTrue) $ modifyIORef vstref incNumNFCInStats -- verify only if the precondition is different from always failing: unless (precondformula == bFalse) $ proveNonFailExp s2 rhs where proveNonFailExp pts exp = case simpExpr exp of AComb ty ct (qf,_) args -> do mapIO_ (proveNonFailExp pts) args when (isCombTypeFuncPartCall ct) $ let qnpre = addSuffix qf "'nonfail" in maybe done -- h.o. call nonfailing if op. has no non-fail cond. (\_ -> do let reason = "due to call '" ++ ppTAExpr exp ++ "'" modifyIORef vstref (addFailedFuncToStats fn reason) printWhenIntermediate opts $ fn ++ ": POSSIBLY FAILING CALL OF '" ++ snd qf ++ "'") (find (\fd -> funcName fd == qnpre) (nfConds ti)) when (ct==FuncCall) $ do printWhenIntermediate opts $ "Analyzing call to " ++ snd qf let ((bs,_) ,pts1) = normalizeArgs args pts (bindexps ,pts2) = mapS (exp2bool True ti) bs pts1 (nfcondcall,pts3) = nonfailPreCondExpOf ti qf (map fst bs) pts2 -- TODO: select from 'bindexps' only demanded argument positions valid <- if nfcondcall == bTrue then return (Just True) -- true non-fail cond. is valid else do modifyIORef vstref incFailTestInStats checkImplicationWithSMT opts vstref (varTypes pts3) (preCond pts) (Conj bindexps) nfcondcall if valid == Just True then do printWhenIntermediate opts $ fn ++ ": NON-FAILING CALL OF '" ++ snd qf ++ "'" else do let reason = if valid == Nothing then "due to SMT error" else "due to call '" ++ ppTAExpr exp ++ "'" modifyIORef vstref (addFailedFuncToStats fn reason) printWhenIntermediate opts $ fn ++ ": POSSIBLY FAILING CALL OF '" ++ snd qf ++ "'" ACase _ _ e brs -> do proveNonFailExp pts e maybe (-- check a case expression for missing constructors: let freshvar = freshVar pts freshtypedvar = (freshvar, annExpr e) (be,pts1) = exp2bool True ti (freshvar,e) (incFreshVarIndex pts) pts2 = pts1 { preCond = Conj [preCond pts, be] , varTypes = freshtypedvar : varTypes pts1 } misscons = missingConsInBranch siblingconsinfo brs in do mapIO_ (verifyMissingCons pts2 freshtypedvar) misscons mapIO_ (proveNonFailBranch pts2 freshtypedvar) brs ) (\ (fe,te) -> -- check a Boolean case with True/False branch: let (be,pts1) = pred2bool e pts ptsf = pts1 { preCond = Conj [preCond pts, bNot be] } ptst = pts1 { preCond = Conj [preCond pts, be] } in do proveNonFailExp ptsf fe proveNonFailExp ptst te ) (testBoolCase brs) AOr _ e1 e2 -> do proveNonFailExp pts e1 proveNonFailExp pts e2 ALet _ bs e -> do let ((rbs,re), pts1) = renameLetVars pts bs e mapIO_ (proveNonFailExp pts1) (map snd rbs) proveNonFailExp pts1 re AFree _ fvs e -> do let ((_,re), pts1) = renameFreeVars pts fvs e proveNonFailExp pts1 re ATyped _ e _ -> proveNonFailExp pts e AVar _ _ -> done ALit _ _ -> done -- verify whether a variable (2. argument) can have the constructor (3. arg.) -- as a value w.r.t. the collected assertions verifyMissingCons pts (var,vartype) (cons,_) = do printWhenIntermediate opts $ fn ++ ": checking missing constructor case '" ++ snd cons ++ "'" modifyIORef vstref incPatTestInStats valid <- checkImplicationWithSMT opts vstref (varTypes pts) (preCond pts) bTrue (bNot (constructorTest cons (BVar var) vartype)) unless (valid == Just True) $ do let reason = if valid == Nothing then "due to SMT error" else "maybe not defined on constructor '" ++ showQName cons ++ "'" modifyIORef vstref (addFailedFuncToStats fn reason) printWhenIntermediate opts $ "POSSIBLY FAILING BRANCH in function '" ++ fn ++ "' with constructor " ++ snd cons proveNonFailBranch pts (var,vartype) branch = do let (ABranch p e, pts1) = renamePatternVars pts branch -- set pattern type correctly (important for [] pattern) bpat = pat2bool (setAnnPattern vartype p) npts = pts1 { preCond = Conj [preCond pts1, bEquVar var bpat] } proveNonFailExp npts e -- Returns the constructors (name/arity) which are missing in the given -- branches of a case construct. missingConsInBranch :: ProgInfo [(QName,Int)] -> [TABranchExpr] -> [(QName,Int)] missingConsInBranch _ [] = error "missingConsInBranch: case with empty branches!" missingConsInBranch _ (ABranch (ALPattern _ _) _ : _) = error "TODO: case with literal pattern" missingConsInBranch siblingconsinfo (ABranch (APattern _ (cons,_) _) _ : brs) = let othercons = maybe (error $ "Sibling constructors of " ++ showQName cons ++ " not found!") id (lookupProgInfo cons siblingconsinfo) branchcons = map (patCons . branchPattern) brs in filter ((`notElem` branchcons) . fst) othercons -- Simplifies a FlatCurry expression (only at the top-level!) -- by considering the semantics of some predefined operations. simpExpr :: TAExpr -> TAExpr simpExpr exp = case exp of AComb ty FuncCall (qf,_) args -> if qf == pre "?" then AOr ty (args!!0) (args!!1) else if qf == pre "ord" || qf == pre "id" -- ops without preconditions then head args -- note: Char is implemented as Int in SMT else exp _ -> exp -- Translates a FlatCurry expression to a Boolean formula representing -- the between a variable (represented by its index in the first -- component) and the translated expression (second component). -- The translated expression is normalized when necessary. -- For this purpose, a "fresh variable index" is passed as a state. -- Moreover, the returned state contains also the types of all fresh variables. -- If the first argument is `False`, the expression is not strictly demanded, -- i.e., possible contracts of it (if it is a function call) are ignored. exp2bool :: Bool -> TransInfo -> (Int,TAExpr) -> State TransState BoolExp exp2bool demanded ti (resvar,exp) = case simpExpr exp of AVar _ i -> returnS $ if resvar==i then bTrue else bEquVar resvar (BVar i) ALit _ l -> returnS (bEquVar resvar (lit2bool l)) AComb ty ct (qf,_) args -> normalizeArgs args `bindS` \ (bs,nargs) -> -- TODO: select from 'bindexps' only demanded argument positions mapS (exp2bool (isPrimOp qf || optStrict (toolOpts ti)) ti) bs `bindS` \bindexps -> comb2bool qf ct nargs bs bindexps ALet _ bs e -> mapS (exp2bool False ti) (map (\ ((i,_),ae) -> (i,ae)) bs) `bindS` \bindexps -> exp2bool demanded ti (resvar,e) `bindS` \bexp -> returnS (Conj (bindexps ++ [bexp])) AOr _ e1 e2 -> exp2bool demanded ti (resvar,e1) `bindS` \bexp1 -> exp2bool demanded ti (resvar,e2) `bindS` \bexp2 -> returnS (Disj [bexp1, bexp2]) ACase _ _ e brs -> getS `bindS` \ts -> let freshvar = freshVar ts in putS (addVarTypes [(freshvar, annExpr e)] (incFreshVarIndex ts)) `bindS_` exp2bool demanded ti (freshvar,e) `bindS` \argbexp -> mapS branch2bool (map (\b->(freshvar,b)) brs) `bindS` \bbrs -> returnS (Conj [argbexp, Disj bbrs]) ATyped _ e _ -> exp2bool demanded ti (resvar,e) AFree _ _ _ -> error "Free variables not yet supported!" where comb2bool qf ct nargs bs bindexps | qf == pre "otherwise" -- specific handling for the moment since the front end inserts it -- as the last alternative of guarded rules... = returnS (bEquVar resvar bTrue) | qf == pre "[]" = returnS (bEquVar resvar (BTerm "nil" [])) | ct == ConsCall = returnS (Conj (bindexps ++ [bEquVar resvar (BTerm (transOpName qf) (map arg2bool nargs))])) | qf == pre "apply" = -- cannot translate h.o. apply: ignore it returnS bTrue | isPrimOp qf = returnS (Conj (bindexps ++ [bEquVar resvar (BTerm (transOpName qf) (map arg2bool nargs))])) | otherwise -- non-primitive operation: add contract only if demanded = preCondExpOf ti qf (map fst bs) `bindS` \precond -> postCondExpOf ti qf (map fst bs ++ [resvar]) `bindS` \postcond -> returnS (Conj (bindexps ++ if demanded && optContract (toolOpts ti) then [precond,postcond] else [])) branch2bool (cvar, (ABranch p e)) = exp2bool demanded ti (resvar,e) `bindS` \branchbexp -> getS `bindS` \ts -> putS ts { varTypes = patvars ++ varTypes ts} `bindS_` returnS (Conj [ bEquVar cvar (pat2bool p), branchbexp]) where patvars = if isConsPattern p then patArgs p else [] arg2bool e = case e of AVar _ i -> BVar i ALit _ l -> lit2bool l _ -> error $ "Not normalized: " ++ show e -- Transforms an operation name starting with `op_xh1...hn'`, where -- each `hi` is a two digit hexadecimal number, into the name -- of corresponding to the ord values of `h1...hn`. -- For instance, `op_x263E'nonfail` is transformed into `&>'nonfail`. transSpecialName :: QName -> QName transSpecialName qn@(mn,fn) | "op_x" `isPrefixOf` fn && not (null fntail) = fromHex [] (drop 4 fnop) | otherwise = qn where (fnop,fntail) = break (==''') fn fromHex s "" = (mn, reverse s ++ fntail) fromHex _ [_] = qn fromHex s (c1:c2:cs) = maybe qn (\ (i,r) -> if null r then fromHex (chr i : s) cs else qn) (readHex [c1,c2]) -- Returns the conjunction of the non-failure condition and precondition -- (if the tool option `contract` is set) expression for a given operation -- and its arguments (which are assumed to be variable indices). -- Rename all local variables by adding the `freshvar` index to them. nonfailPreCondExpOf :: TransInfo -> QName -> [Int] -> State TransState BoolExp nonfailPreCondExpOf ti qf args = if optContract (toolOpts ti) then nonfailCondExpOf ti qf args `bindS` \nfcond -> preCondExpOf ti qf args `bindS` \precond -> returnS (simpBE (Conj [nfcond,precond])) else nonfailCondExpOf ti qf args -- Returns the non-failure condition expression for a given operation -- and its arguments (which are assumed to be variable indices). -- Rename all local variables by adding the `freshvar` index to them. nonfailCondExpOf :: TransInfo -> QName -> [Int] -> State TransState BoolExp nonfailCondExpOf ti qf args = maybe (predefs qf) (\fd -> if funcArity fd /= length args then error $ "Operation '" ++ snd qf ++ "': nonfail condition has incorrect arity!" else applyFunc fd args `bindS` pred2bool) (find (\fd -> transSpecialName (funcName fd) == qnpre) (nfConds ti)) where qnpre = addSuffix qf "'nonfail" predefs qn | qn `elem` [pre "failed", pre "=:="] || (qn == pre "error" && optError (toolOpts ti)) = returnS bFalse | otherwise = returnS bTrue -- Returns the precondition expression for a given operation -- and its arguments (which are assumed to be variable indices). -- Rename all local variables by adding the `freshvar` index to them. preCondExpOf :: TransInfo -> QName -> [Int] -> State TransState BoolExp preCondExpOf ti qf args = maybe (returnS bTrue) (\fd -> applyFunc fd args `bindS` pred2bool) (find (\fd -> funcName fd == qnpre) (preConds ti)) where qnpre = addSuffix qf "'pre" -- Returns the postcondition expression for a given operation -- and its arguments (which are assumed to be variable indices). -- Rename all local variables by adding `freshvar` to them and -- return the new freshvar value. postCondExpOf :: TransInfo -> QName -> [Int] -> State TransState BoolExp postCondExpOf ti qf args = maybe (returnS bTrue) (\fd -> applyFunc fd args `bindS` pred2bool) (find (\fd -> funcName fd == qnpost) (postConds ti)) where qnpost = addSuffix qf "'post" -- Applies a function declaration on a list of arguments, -- which are assumed to be variable indices, and returns -- the renamed body of the function declaration. -- All local variables are renamed by adding `freshvar` to them. -- Also the new fresh variable index is returned. applyFunc :: TAFuncDecl -> [Int] -> State TransState TAExpr applyFunc fdecl args s0 = let (ARule _ orgargs orgexp) = funcRule fdecl exp = rnmAllVars (renameRuleVar orgargs) orgexp s1 = s0 { freshVar = max (freshVar s0) (maximum (0 : args ++ allVars exp) + 1) } in (applyArgs exp (drop (length orgargs) args), s1) where -- renaming function for variables in original rule: renameRuleVar orgargs r = maybe (r + freshVar s0) (args!!) (elemIndex r (map fst orgargs)) applyArgs e [] = e applyArgs e (v:vs) = -- simple hack for eta-expansion since the type annotations are not used: -- TODO: compute correct type annotations!!! (required for overloaded nils) let e_v = AComb failed FuncCall (("Prelude","apply"),failed) [e, AVar failed v] in applyArgs e_v vs -- Translates a Boolean FlatCurry expression into a Boolean formula. -- Calls to user-defined functions are replaced by the first argument -- (which might be true or false). pred2bool :: TAExpr -> State TransState BoolExp pred2bool exp = case simpExpr exp of AVar _ i -> returnS (BVar i) ALit _ l -> returnS (lit2bool l) AComb _ _ (qf,_) args -> comb2bool qf (length args) args _ -> returnS (BTerm (show exp) []) where comb2bool qf ar args | qf == pre "[]" && ar == 0 = returnS (BTerm "as" [BTerm "nil" [], polytype2SMTExp (annExpr exp)]) | qf == pre "not" && ar == 1 = pred2bool (head args) `bindS` \barg -> returnS (Not barg) | qf == pre "null" && ar == 1 = let arg = head args in pred2bool arg `bindS` \barg -> getS `bindS` \tstate -> returnS (bEqu barg (BTerm "as" [BTerm "nil" [], polytype2SMTExp (typeOfVar tstate arg)])) | qf == pre "apply" && ar == 2 && isComb (head args) = -- "defunctionalization": if the first argument is a -- combination, append the second argument to its arguments mapS pred2bool args `bindS` \bargs -> case bargs of [BTerm bn bas, barg2] -> returnS (BTerm bn (bas++[barg2])) _ -> returnS (BTerm (show exp) []) -- no translation possible | qf == pre "apply" = -- cannot translate h.o. apply: replace it by new variable getS `bindS` \ts -> let fvar = freshVar ts nts = addVarTypes [(fvar,annExpr exp)] (incFreshVarIndex ts) in putS nts `bindS_` returnS (BVar fvar) | qf == pre "/=" = comb2bool (pre "==") ar args `bindS` \be -> returnS (bNot be) | otherwise = mapS pred2bool args `bindS` \bargs -> returnS (BTerm (transOpName qf) bargs) typeOfVar tstate e = case e of AVar _ i -> maybe (error $ "pred2bool: variable " ++ show i ++ " not found") id (lookup i (varTypes tstate)) _ -> annExpr e -- might not be correct due to applyFunc! normalizeArgs :: [TAExpr] -> State TransState ([(Int,TAExpr)],[TAExpr]) normalizeArgs [] = returnS ([],[]) normalizeArgs (e:es) = case e of AVar _ i -> normalizeArgs es `bindS` \ (bs,nes) -> returnS ((i,e):bs, e:nes) _ -> getS `bindS` \ts -> let fvar = freshVar ts nts = addVarTypes [(fvar,annExpr e)] (incFreshVarIndex ts) in putS nts `bindS_` normalizeArgs es `bindS` \ (bs,nes) -> returnS ((fvar,e):bs, AVar (annExpr e) fvar : nes) -- Rename let-bound variables in a let expression. renameLetVars :: TransState -> [((VarIndex, TypeExpr), TAExpr)] -> TAExpr -> (([((VarIndex, TypeExpr), TAExpr)], TAExpr),TransState) renameLetVars pts bindings exp = let args = map (fst . fst) bindings minarg = minimum (0 : args) maxarg = maximum (0 : args) fv = freshVar pts rnm i = if i `elem` args then i - minarg + fv else i nargs = map (\ ((v,t),_) -> (rnm v,t)) bindings in ((map (\ ((v,t),be) -> ((rnm v,t), rnmAllVars rnm be)) bindings, rnmAllVars rnm exp), pts { freshVar = fv + maxarg - minarg + 1 , varTypes = nargs ++ varTypes pts }) -- Rename free variables introduced in an expression. renameFreeVars :: TransState -> [(VarIndex, TypeExpr)] -> TAExpr -> (([(VarIndex, TypeExpr)], TAExpr),TransState) renameFreeVars pts freevars exp = let args = map fst freevars minarg = minimum (0 : args) maxarg = maximum (0 : args) fv = freshVar pts rnm i = if i `elem` args then i - minarg + fv else i nargs = map (\ (v,t) -> (rnm v,t)) freevars in ((map (\ (v,t) -> (rnm v,t)) freevars, rnmAllVars rnm exp), pts { freshVar = fv + maxarg - minarg + 1 , varTypes = nargs ++ varTypes pts }) -- Rename argument variables of constructor pattern renamePatternVars :: TransState -> TABranchExpr -> (TABranchExpr,TransState) renamePatternVars pts (ABranch p e) = if isConsPattern p then let args = map fst (patArgs p) minarg = minimum (0 : args) maxarg = maximum (0 : args) fv = freshVar pts rnm i = if i `elem` args then i - minarg + fv else i nargs = map (\ (v,t) -> (rnm v,t)) (patArgs p) in (ABranch (updPatArgs (map (\ (v,t) -> (rnm v,t))) p) (rnmAllVars rnm e), pts { freshVar = fv + maxarg - minarg + 1 , varTypes = nargs ++ varTypes pts }) else (ABranch p e, pts) -- Adds a suffix to some qualified name: addSuffix :: QName -> String -> QName addSuffix (mn,fn) s = (mn, fn ++ s) --------------------------------------------------------------------------- -- Calls the SMT solver to check whether an assertion implies some -- (pre/post) condition. checkImplicationWithSMT :: Options -> IORef VState -> [(Int,TypeExpr)] -> BoolExp -> BoolExp -> BoolExp -> IO (Maybe Bool) checkImplicationWithSMT opts vstref vartypes assertion impbindings imp = do let usertypes = filter (\ (mn,_) -> mn /= "Prelude") (foldr union [] (map (tconsOfTypeExpr . snd) vartypes)) vst <- readIORef vstref let decls = map (maybe (error "Internal error: some datatype not found!") id) (map (tdeclOf vst) usertypes) smtdatatypes = unlines [ "; User-defined datatypes:" , unlines (map tdecl2SMT decls) ] smt = unlines [ "; Free variables:" , typedVars2SMT vartypes , "; Boolean formula of assertion (known properties):" , showBoolExp (assertSMT assertion) , "" , "; Bindings of implication:" , showBoolExp (assertSMT impbindings) , "" , "; Assert negated implication:" , showBoolExp (assertSMT (Not imp)) , "" , "; check satisfiability:" , "(check-sat)" , "; if unsat, the implication is valid" ] let allsymbols = allSymbolsOfBE (Conj [assertion, impbindings, imp]) allqsymbols = catMaybes (map untransOpName allsymbols) unless (null allqsymbols) $ printWhenIntermediate opts $ "Translating operations into SMT: " ++ unwords (map showQName allqsymbols) smtfuncs <- funcs2SMT vstref allqsymbols smtprelude <- readFile (packagePath "include" "Prelude.smt") let smtinput = smtprelude ++ smtdatatypes ++ smtfuncs ++ smt printWhenAll opts $ unlines ["SMT SCRIPT:", line, smtinput, line] printWhenAll opts $ "CALLING Z3 (with options: -smt2 -T:5)..." (ecode,out,err) <- evalCmd "z3" ["-smt2", "-in", "-T:5"] smtinput when (ecode>0) $ printWhenAll opts $ "EXIT CODE: " ++ show ecode printWhenAll opts $ "RESULT:\n" ++ out unless (null err) $ printWhenAll opts $ "ERROR:\n" ++ err let pcvalid = let ls = lines out in not (null ls) && head ls == "unsat" return (if ecode>0 then Nothing else Just pcvalid) where line = take 78 (repeat '-') -- Operations axiomatized by specific smt scripts (no longer necessary -- since these scripts are now automatically generated by Curry2SMT.funcs2SMT). -- However, for future work, it might be reasonable to cache these scripts -- for faster contract checking. axiomatizedOps :: [String] axiomatizedOps = ["Prelude_null","Prelude_take","Prelude_length"] --------------------------------------------------------------------------- -- Translates a list of type variables to SMT declarations: typedVars2SMT :: [(Int,TypeExpr)] -> String typedVars2SMT tvars = unlines (map tvar2SMT tvars) where tvar2SMT (i,te) = withBracket $ unwords ["declare-const", smtBE (BVar i), smtBE (polytype2SMTExp te)] -- Gets all type constructors of a type expression. tconsOfTypeExpr :: TypeExpr -> [QName] tconsOfTypeExpr (TVar _) = [] tconsOfTypeExpr (FuncType a b) = union (tconsOfTypeExpr a) (tconsOfTypeExpr b) tconsOfTypeExpr (TCons qName texps) = foldr union [qName] (map tconsOfTypeExpr texps) --------------------------------------------------------------------------- -- Auxiliaries: --- Checks whether a file exists in one of the directories on the PATH. fileInPath :: String -> IO Bool fileInPath file = do path <- getEnviron "PATH" dirs <- return $ splitOn ":" path (liftIO (any id)) $ mapIO (doesFileExist . ( file)) dirs --- Tests whether the given branches of a case expressions --- are a Boolean case distinction. --- If yes, the expressions of the `False` and `True` branch --- are returned. testBoolCase :: [TABranchExpr] -> Maybe (TAExpr,TAExpr) testBoolCase brs = if length brs /= 2 then Nothing else case (brs!!0, brs!!1) of (ABranch (APattern _ (c1,_) _) e1, ABranch (APattern _ (c2,_) _) e2) -> if c1 == pre "False" && c2 == pre "True" then Just (e1,e2) else if c1 == pre "True" && c2 == pre "False" then Just (e2,e1) else Nothing _ -> Nothing --------------------------------------------------------------------------- {- Still to be done: - consider encapsulated search - type-specialize polymorphic operations when axiomatizing them in SMT Verified system libraries: - Prelude - AnsiCodes - Either - ErrorState - Integer - Maybe - State - Nat - ShowS - Socket - Array - Char -}