----------------------------------------------------------------------------- --- A tool to verify non-failure properties of Curry operations. --- --- @author Michael Hanus --- @version May 2021 --------------------------------------------------------------------------- module Main where import Control.Monad ( unless, when ) import Data.IORef import Data.List ( (\\), elemIndex, find, maximum, minimum , partition, union ) import Data.Maybe ( catMaybes ) import System.Environment ( getArgs ) -- Imports from dependencies: import Analysis.ProgInfo import Analysis.TotallyDefined ( siblingCons ) import Analysis.Types import CASS.Server ( analyzeGeneric, analyzePublic ) import Contract.Names import Contract.Usage ( checkContractUsage ) import Control.Monad.Trans.Class ( lift ) import Control.Monad.Trans.State ( StateT, get, put, evalStateT ) import Debug.Profile import FlatCurry.TypeAnnotated.TypeSubst ( substRule ) import FlatCurry.Files ( readFlatCurryInt ) import FlatCurry.Types import FlatCurry.Annotated.Goodies import FlatCurry.ShowIntMod ( showCurryModule ) import System.FilePath ( () ) import System.IOExts ( evalCmd ) import System.Path ( fileInPath ) import System.Process ( exitWith ) -- Imports from package modules: import ESMT import Curry2SMT import FlatCurry.Typed.Read import FlatCurry.Typed.Goodies import FlatCurry.Typed.Names import FlatCurry.Typed.Types import PackageConfig ( packagePath ) import ToolOptions import VerifierState ------------------------------------------------------------------------ -- To support testing: test :: Int -> String -> IO () test v = verifyNonFailingMod defaultOptions { optVerb = v } testv :: String -> IO () testv = test 3 testcv :: String -> IO () testcv = verifyNonFailingMod defaultOptions { optVerb = 3, optContract = True } ------------------------------------------------------------------------ banner :: String banner = unlines [bannerLine,bannerText,bannerLine] where bannerText = "Fail-Free Verification Tool for Curry (Version of 27/05/21)" 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 $ "Non-failure condition for '" ++ optname ++ "':\n" ++ encodeContractName (optname ++ "'nonfail") else do 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 verifier to work" putStrLn "but the program 'z3' is not found on the PATH!" exitWith 1 verifyNonFailingModules :: Options -> [String] -> [String] -> IO () verifyNonFailingModules _ _ [] = return () 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 <- readSimpTypedFlatCurryWithSpec opts modname let errs = checkContractUsage (progName prog) (map (\fd -> (snd (funcName fd), funcType fd)) (progFuncs prog)) unless (null errs) $ do putStr $ unlines (map showOpError errs) exitWith 1 impprogs <- mapM (readSimpTypedFlatCurryWithSpec opts) (progImports prog) let allprogs = prog : impprogs vinfo = foldr addFunsToVerifyInfo (initVerifyInfo opts) (map progFuncs allprogs) vstate = foldr addProgToState (initVState vinfo) allprogs siblingconsinfo <- loadAnalysisWithImports siblingCons prog pi1 <- getProcessInfos printWhenAll opts $ unlines $ ["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg prog), line] vstref <- newIORef vstate proveNonFailingFuncs opts siblingconsinfo vstref (progFuncs prog) stats <- readIORef vstref 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 '-') showOpError (qf,err) = snd qf ++ " (module " ++ fst qf ++ "): " ++ err -- Loads CASS analysis results for a module and its imported entities. loadAnalysisWithImports :: (Read a, Show a) => Analysis a -> TAProg -> IO (ProgInfo a) loadAnalysisWithImports analysis prog = do maininfo <- analyzeGeneric analysis (progName prog) >>= return . either id error impinfos <- mapM (\m -> analyzePublic analysis m >>= return . either id error) (progImports prog) return $ foldr combineProgInfo maininfo impinfos --------------------------------------------------------------------------- -- 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 { cAssertion :: Term , freshVar :: Int , varTypes :: [(Int,TypeExpr)] } makeTransState :: Int -> [(Int,TypeExpr)] -> TransState makeTransState = TransState tTrue emptyTransState :: TransState emptyTransState = makeTransState 0 [] -- The type of the state monad contains the transformation state. --type TransStateM a = State TransState a type TransStateM a = StateT TransState IO a -- Gets the current fresh variable index of the state. getFreshVarIndex :: TransStateM Int getFreshVarIndex = get >>= return . freshVar -- Sets the fresh variable index in the state. setFreshVarIndex :: Int -> TransStateM () setFreshVarIndex fvi = do st <- get put $ st { freshVar = fvi } -- Gets a fresh variable index and increment the index in the state. getFreshVar :: TransStateM Int getFreshVar = do st <- get put $ st { freshVar = freshVar st + 1 } return $ freshVar st -- Increments fresh variable index. incFreshVarIndex :: TransState -> TransState incFreshVarIndex st = st { freshVar = freshVar st + 1 } -- Gets the variables and their types stored in the state. getVarTypes :: TransStateM [(Int,TypeExpr)] getVarTypes = get >>= return . varTypes -- Adds variables and their types to the state. addVarTypes :: [(Int,TypeExpr)] -> TransStateM () addVarTypes vts = do st <- get put $ st { varTypes = vts ++ varTypes st } -- Gets the current assertion stored in the state. getAssertion :: TransStateM Term getAssertion = get >>= return . cAssertion -- Sets the current assertion in the state. setAssertion :: Term -> TransStateM () setAssertion formula = do st <- get put $ st { cAssertion = formula } -- Add a formula to the current assertion in the state by conjunction. addToAssertion :: Term -> TransStateM () addToAssertion formula = do st <- get put $ st { cAssertion = tConj [cAssertion st, formula] } --------------------------------------------------------------------------- -- Prove that a list of defined functions is fail free (w.r.t. their -- non-fail conditions). proveNonFailingFuncs :: Options -> ProgInfo [(QName,Int)] -> IORef VState -> [TAFuncDecl] -> IO () proveNonFailingFuncs opts siblingconsinfo vstref = mapM_ (proveNonFailingFunc opts siblingconsinfo vstref) -- Prove that a function is fail free (w.r.t. their non-fail condition). proveNonFailingFunc :: Options -> ProgInfo [(QName,Int)] -> IORef VState -> TAFuncDecl -> IO () proveNonFailingFunc opts siblingconsinfo 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 vstref (funcName efdecl) (funcType efdecl) (funcRule efdecl) -- Prove that a function rule is fail free (w.r.t. their non-fail condition). -- The rule is in eta-expanded form. proveNonFailingRule :: Options -> ProgInfo [(QName,Int)] -> IORef VState -> QName -> TypeExpr -> TARule -> IO () proveNonFailingRule _ _ vstref qn ftype (AExternal _ _) = do ti <- readVerifyInfoRef vstref let atypes = argTypes ftype args = zip [1 .. length atypes] atypes nfcond <- evalStateT (nonfailPreCondExpOf ti qn ftype args) emptyTransState unless (nfcond == tTrue) $ modifyIORef vstref incNumNFCInStats proveNonFailingRule opts siblingconsinfo vstref qn@(_,fn) ftype (ARule _ rargs rhs) = do ti <- readVerifyInfoRef vstref let st = makeTransState (maximum (0 : map fst rargs ++ allVars rhs) + 1) rargs (flip evalStateT) st $ do -- compute non-fail precondition of operation: precondformula <- nonfailPreCondExpOf ti qn ftype rargs setAssertion precondformula unless (precondformula == tTrue) $ lift $ modifyIORef vstref incNumNFCInStats -- verify only if the precondition is different from always failing: unless (precondformula == tFalse) $ proveNonFailExp ti rhs where proveNonFailExp ti exp = case simpExpr exp of AComb _ ct (qf,qfty) args -> do mapM_ (proveNonFailExp ti) args when (isCombTypeFuncPartCall ct) $ let qnnonfail = toNonFailQName qf in maybe (return ()) -- h.o. call nonfailing if op. has no non-fail cond. (\_ -> lift $ 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 == qnnonfail) (nfConds ti)) when (ct==FuncCall) $ do lift $ printWhenIntermediate opts $ "Analyzing call to " ++ snd qf precond <- getAssertion (bs,_) <- normalizeArgs args bindexps <- mapM (binding2SMT True ti) bs let callargs = zip (map fst bs) (map annExpr args) nfcondcall <- nonfailPreCondExpOf ti qf qfty callargs -- TODO: select from 'bindexps' only demanded argument positions vartypes <- getVarTypes valid <- if nfcondcall == tTrue then return (Just True) -- true non-fail cond. is valid else lift $ do modifyIORef vstref incFailTestInStats let title = "SMT script to verify non-failing call of '" ++ snd qf ++ "' in function '" ++ fn ++ "'" checkImplicationWithSMT opts vstref title vartypes precond (tConj bindexps) nfcondcall if valid == Just True then lift $ printWhenIntermediate opts $ fn ++ ": NON-FAILING CALL OF '" ++ snd qf ++ "'" else lift $ 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 ti e maybe (do -- check a case expression for missing constructors: freshvar <- getFreshVar let freshtypedvar = (freshvar, annExpr e) be <- binding2SMT True ti (freshvar,e) addToAssertion be addVarTypes [freshtypedvar] let misscons = missingConsInBranch siblingconsinfo brs st <- get -- use same state to prove missing and non-fail branches mapM_ (verifyMissingCons freshtypedvar exp) misscons put st mapM_ (proveNonFailBranch ti freshtypedvar) brs ) (\ (fe,te) -> do -- check a Boolean case with True/False branch: be <- pred2SMT e st <- get addToAssertion (tNot be) proveNonFailExp ti fe put st addToAssertion be proveNonFailExp ti te ) (testBoolCase brs) AOr _ e1 e2 -> do st <- get -- use same state for both branches proveNonFailExp ti e1 put st proveNonFailExp ti e2 ALet _ bs e -> do (rbs,re) <- renameLetVars bs e mapM_ (proveNonFailExp ti) (map snd rbs) proveNonFailExp ti re AFree _ fvs e -> do (_,re) <- renameFreeVars fvs e proveNonFailExp ti re ATyped _ e _ -> proveNonFailExp ti e AVar _ _ -> return () ALit _ _ -> return () -- verify whether a variable (2. argument) can have the constructor (3. arg.) -- as a value w.r.t. the collected assertions verifyMissingCons (var,vartype) exp (cons,_) = do let title = "check missing constructor case '" ++ snd cons ++ "' in function '" ++ fn ++ "'" lift $ printWhenIntermediate opts $ title ++ "\nVAR: " ++ show (var,vartype) ++ "\nCASE:: " ++ show (unAnnExpr (simpExpr exp)) lift $ modifyIORef vstref incPatTestInStats vartypes <- getVarTypes precond <- getAssertion valid <- lift $ checkImplicationWithSMT opts vstref ("SMT script to " ++ title) vartypes precond tTrue (tNot (constructorTest False cons (TSVar var) vartype)) unless (valid == Just True) $ lift $ 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 ti (var,vartype) branch = do ABranch p e <- renamePatternVars branch -- set pattern type correctly (important for [] pattern) let bpat = pat2SMT (setAnnPattern vartype p) addToAssertion (tEquVar var bpat) proveNonFailExp ti 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 binding of a variable (represented by its index in the first -- component) to 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. binding2SMT :: Bool -> VerifyInfo -> (Int,TAExpr) -> TransStateM Term binding2SMT demanded ti (resvar,exp) = case simpExpr exp of AVar _ i -> return $ if resvar==i then tTrue else tEquVar resvar (TSVar i) ALit _ l -> return (tEquVar resvar (lit2SMT l)) AComb rtype ct (qf,_) args -> do (bs,nargs) <- normalizeArgs args -- TODO: select from 'bindexps' only demanded argument positions bindexps <- mapM (binding2SMT (isPrimOp qf || optStrict (toolOpts ti)) ti) bs comb2bool qf rtype ct nargs bs bindexps ALet _ bs e -> do bindexps <- mapM (binding2SMT False ti) (map (\ ((i,_),ae) -> (i,ae)) bs) bexp <- binding2SMT demanded ti (resvar,e) return (tConj (bindexps ++ [bexp])) AOr _ e1 e2 -> do bexp1 <- binding2SMT demanded ti (resvar,e1) bexp2 <- binding2SMT demanded ti (resvar,e2) return (tDisj [bexp1, bexp2]) ACase _ _ e brs -> do freshvar <- getFreshVar addVarTypes [(freshvar, annExpr e)] argbexp <- binding2SMT demanded ti (freshvar,e) bbrs <- mapM branch2bool (map (\b->(freshvar,b)) brs) return (tConj [argbexp, tDisj bbrs]) ATyped _ e _ -> binding2SMT demanded ti (resvar,e) AFree _ _ _ -> error "Free variables not yet supported!" where comb2bool qf rtype 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... = return (tEquVar resvar tTrue) | ct == ConsCall = return (tConj (bindexps ++ [tEquVar resvar (TComb (cons2SMT (null nargs) False qf rtype) (map arg2bool nargs))])) | qf == pre "apply" = -- cannot translate h.o. apply: ignore it return tTrue | isPrimOp qf = return (tConj (bindexps ++ [tEquVar resvar (TComb (cons2SMT True False qf rtype) (map arg2bool nargs))])) | otherwise -- non-primitive operation: add contract only if demanded = do let targs = zip (map fst bs) (map annExpr nargs) precond <- preCondExpOf ti qf targs postcond <- postCondExpOf ti qf (targs ++ [(resvar,rtype)]) return (tConj (bindexps ++ if demanded && optContract (toolOpts ti) then [precond,postcond] else [])) branch2bool (cvar, ABranch p e) = do branchbexp <- binding2SMT demanded ti (resvar,e) addVarTypes patvars return (tConj [ tEquVar cvar (pat2SMT p), branchbexp]) where patvars = if isConsPattern p then patArgs p else [] arg2bool e = case e of AVar _ i -> TSVar i ALit _ l -> lit2SMT l _ -> error $ "Not normalized: " ++ show e -- 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 :: VerifyInfo -> QName -> TypeExpr -> [(Int,TypeExpr)] -> TransStateM Term nonfailPreCondExpOf ti qf ftype args = if optContract (toolOpts ti) then do (fvars,nfcond) <- nonfailCondExpOf ti qf ftype args precond <- preCondExpOf ti qf (args ++ fvars) -- simplify term in order to check later for trivial precondition return (simpTerm (tConj [nfcond,precond])) else do (_,rt) <- nonfailCondExpOf ti qf ftype args return rt -- Returns the non-failure condition expression for a given operation -- and its arguments (which are assumed to be variable indices). -- All local variables are renamed by adding the `freshvar` index to them. -- If the non-failure condition requires more arguments (due to a -- higher-order call), fresh arguments are added which are also returned. nonfailCondExpOf :: VerifyInfo -> QName -> TypeExpr -> [(Int,TypeExpr)] -> TransStateM ([(Int,TypeExpr)], Term) nonfailCondExpOf ti qf ftype args = maybe (predefs qf) (\fd -> let moreargs = funcArity fd - length args in if moreargs > 0 then do -- eta-expand function call with fresh variables so that one -- can check non-fail conditions with a greater arity: let etatypes = argTypes (dropArgTypes (length args) ftype) fvars <- getFreshVarsForTypes (take moreargs etatypes) rt <- applyFunc fd (args ++ fvars) >>= pred2SMT return (fvars,rt) else if moreargs < 0 then error $ "Operation '" ++ snd qf ++ "': nonfail condition has too few arguments!" else do rt <- applyFunc fd args >>= pred2SMT return ([],rt) ) (find (\fd -> decodeContractQName (funcName fd) == toNonFailQName qf) (nfConds ti)) where predefs qn | qn `elem` [pre "failed", pre "=:="] || (qn == pre "error" && optError (toolOpts ti)) = return ([], tFalse) | otherwise = return ([], tTrue) -- 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 :: VerifyInfo -> QName -> [(Int,TypeExpr)] -> TransStateM Term preCondExpOf ti qf args = maybe (return tTrue) (\fd -> applyFunc fd args >>= pred2SMT) (find (\fd -> funcName fd == toPreCondQName qf) (preConds ti)) -- 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 :: VerifyInfo -> QName -> [(Int,TypeExpr)] -> TransStateM Term postCondExpOf ti qf args = maybe (return tTrue) (\fd -> applyFunc fd args >>= pred2SMT) (find (\fd -> funcName fd == toPostCondQName qf) (postConds ti)) -- 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,TypeExpr)] -> TransStateM TAExpr applyFunc fdecl targs = do fv <- getFreshVarIndex let tsub = maybe (error $ "applyFunc: types\n" ++ show (argTypes (funcType fdecl)) ++ "\n" ++ show (map snd targs) ++ "\ndo not match!") id (matchTypes (argTypes (funcType fdecl)) (map snd targs)) (ARule _ orgargs orgexp) = substRule tsub (funcRule fdecl) exp = rnmAllVars (renameRuleVar fv orgargs) orgexp setFreshVarIndex (max fv (maximum (0 : args ++ allVars exp) + 1)) return $ simpExpr $ applyArgs exp (drop (length orgargs) args) where args = map fst targs -- renaming function for variables in original rule: renameRuleVar fv orgargs r = maybe (r + fv) (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 (pre "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). pred2SMT :: TAExpr -> TransStateM Term pred2SMT exp = case simpExpr exp of AVar _ i -> return (TSVar i) ALit _ l -> return (lit2SMT l) AComb _ ct (qf,ftype) args -> comb2bool qf ftype ct (length args) args _ -> return (tComb (show exp) []) -- TODO! where comb2bool qf ftype ct ar args | qf == pre "[]" && ar == 0 = return (sortedConst "nil" (polytype2sort (annExpr exp))) | qf == pre "not" && ar == 1 = do barg <- pred2SMT (head args) return (tNot barg) | qf == pre "null" && ar == 1 = do let arg = head args barg <- pred2SMT arg vartype <- typeOfVar arg return (tEqu barg (sortedConst "nil" (polytype2sort vartype))) | qf == pre "apply" = do -- cannot translate h.o. apply: replace it by new variable fvar <- getFreshVar addVarTypes [(fvar,annExpr exp)] return (TSVar fvar) | qf == pre "/=" = do be <- comb2bool (pre "==") ftype ct ar args return (tNot be) | otherwise = do bargs <- mapM pred2SMT args return (TComb (cons2SMT (ct /= ConsCall || not (null bargs)) False qf ftype) bargs) typeOfVar e = do vartypes <- getVarTypes case e of AVar _ i -> maybe (error $ "pred2SMT: variable " ++ show i ++ " not found") return (lookup i vartypes) _ -> return $ annExpr e -- might not be correct due to applyFunc! normalizeArgs :: [TAExpr] -> TransStateM ([(Int,TAExpr)],[TAExpr]) normalizeArgs [] = return ([],[]) normalizeArgs (e:es) = case e of AVar _ i -> do (bs,nes) <- normalizeArgs es return ((i,e):bs, e:nes) _ -> do fvar <- getFreshVar addVarTypes [(fvar,annExpr e)] (bs,nes) <- normalizeArgs es return ((fvar,e):bs, AVar (annExpr e) fvar : nes) -- Get for the types (given in the first argument) fresh typed variables. getFreshVarsForTypes :: [TypeExpr] -> TransStateM [(VarIndex, TypeExpr)] getFreshVarsForTypes types = do fv <- getFreshVarIndex let n = length types vars = take n [fv ..] tvars = zip vars types setFreshVarIndex (fv + n) addVarTypes tvars return tvars -- Rename let-bound variables in a let expression. renameLetVars :: [((VarIndex, TypeExpr), TAExpr)] -> TAExpr -> TransStateM ([((VarIndex, TypeExpr), TAExpr)], TAExpr) renameLetVars bindings exp = do fv <- getFreshVarIndex let args = map (fst . fst) bindings minarg = minimum (0 : args) maxarg = maximum (0 : args) rnm i = if i `elem` args then i - minarg + fv else i nargs = map (\ ((v,t),_) -> (rnm v,t)) bindings setFreshVarIndex (fv + maxarg - minarg + 1) addVarTypes nargs return (map (\ ((v,t),be) -> ((rnm v,t), rnmAllVars rnm be)) bindings, rnmAllVars rnm exp) -- Rename free variables introduced in an expression. renameFreeVars :: [(VarIndex, TypeExpr)] -> TAExpr -> TransStateM ([(VarIndex, TypeExpr)], TAExpr) renameFreeVars freevars exp = do fv <- getFreshVarIndex let args = map fst freevars minarg = minimum (0 : args) maxarg = maximum (0 : args) rnm i = if i `elem` args then i - minarg + fv else i nargs = map (\ (v,t) -> (rnm v,t)) freevars setFreshVarIndex (fv + maxarg - minarg + 1) addVarTypes nargs return (map (\ (v,t) -> (rnm v,t)) freevars, rnmAllVars rnm exp) -- Rename argument variables of constructor pattern renamePatternVars :: TABranchExpr -> TransStateM TABranchExpr renamePatternVars (ABranch p e) = do if isConsPattern p then do fv <- getFreshVarIndex let args = map fst (patArgs p) minarg = minimum (0 : args) maxarg = maximum (0 : args) rnm i = if i `elem` args then i - minarg + fv else i nargs = map (\ (v,t) -> (rnm v,t)) (patArgs p) setFreshVarIndex (fv + maxarg - minarg + 1) addVarTypes nargs return $ ABranch (updPatArgs (map (\ (v,t) -> (rnm v,t))) p) (rnmAllVars rnm e) else return $ ABranch p e --------------------------------------------------------------------------- -- Calls the SMT solver to check whether an assertion implies some -- property. checkImplicationWithSMT :: Options -> IORef VState -> String -> [(Int,TypeExpr)] -> Term -> Term -> Term -> IO (Maybe Bool) checkImplicationWithSMT opts vstref scripttitle vartypes assertion impbindings imp = do let (pretypes,usertypes) = partition ((== "Prelude") . fst) (foldr union [] (map (tconsOfTypeExpr . snd) vartypes)) vst <- readIORef vstref let allsyms = catMaybes (map (\n -> maybe Nothing Just (untransOpName n)) (map qidName (allQIdsOfTerm (tConj [assertion, impbindings, imp])))) unless (null allsyms) $ printWhenIntermediate opts $ "Translating operations into SMT: " ++ unwords (map showQName allsyms) smtfuncs <- funcs2SMT vstref allsyms let decls = map (maybe (error "Internal error: some datatype not found!") id) (map (tdeclOf vst) usertypes) smt = concatMap preludeType2SMT (map snd pretypes) ++ [ EmptyLine ] ++ (if null decls then [] else [ Comment "User-defined datatypes:" ] ++ map tdecl2SMT decls) ++ [ EmptyLine, smtfuncs, EmptyLine , Comment "Free variables:" ] ++ map typedVar2SMT vartypes ++ [ EmptyLine , Comment "Boolean formula of assertion (known properties):" , sAssert assertion, EmptyLine , Comment "Bindings of implication:" , sAssert impbindings, EmptyLine , Comment "Assert negated implication:" , sAssert (tNot imp), EmptyLine , Comment "check satisfiability:" , CheckSat , Comment "if unsat, the implication is valid" ] --putStrLn $ "SMT commands as Curry term:\n" ++ show smt smtprelude <- readFile (packagePath "include" "Prelude.smt") let smtinput = "; " ++ scripttitle ++ "\n\n" ++ smtprelude ++ showSMT smt printWhenAll opts $ "SMT SCRIPT:\n" ++ showWithLineNums smtinput printWhenAll opts $ "CALLING Z3 (with options: -smt2 -T:5)..." (ecode,out,err) <- evalCmd "z3" ["-smt2", "-in", "-T:5"] smtinput when (ecode>0) $ do printWhenAll opts $ "EXIT CODE: " ++ show ecode writeFile "error.smt" smtinput 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) -- 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"] --------------------------------------------------------------------------- -- Translate a typed variables to an SMT declaration: typedVar2SMT :: (Int,TypeExpr) -> Command typedVar2SMT (i,te) = DeclareVar (SV i (polytype2sort 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) tconsOfTypeExpr (ForallType _ te) = tconsOfTypeExpr te --------------------------------------------------------------------------- -- Auxiliaries: --- 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 --- Shows a text with line numbers prefixed: showWithLineNums :: String -> String showWithLineNums txt = let txtlines = lines txt maxlog = ilog (length txtlines + 1) showNum n = (take (maxlog - ilog n) (repeat ' ')) ++ show n ++ ": " in unlines . map (uncurry (++)) . zip (map showNum [1..]) $ txtlines --- The value of `ilog n` is the floor of the logarithm --- in the base 10 of `n`. --- Fails if `n <= 0`. --- For positive integers, the returned value is --- 1 less the number of digits in the decimal representation of `n`. --- --- @param n - The argument. --- @return the floor of the logarithm in the base 10 of `n`. ilog :: Int -> Int ilog n | n>0 = if n<10 then 0 else 1 + ilog (n `div` 10) --------------------------------------------------------------------------- {- Still to be done: - consider encapsulated search Verified system libraries: - Prelude - Char - Either - ErrorState - Integer - Maybe - State - ShowS Prelude Char Either ErrorState Integer Maybe State ShowS -}