module ContractProver ( addPreConditions, verifyPostConditions, verifyPreConditions ) where import Control.Monad ( unless ) import Contract.Names import Control.Monad.IO.Class ( liftIO ) import Control.Monad.Trans.Class ( lift ) import Control.Monad.Trans.State ( evalStateT, gets, put ) import Data.List ( elemIndex, find, init, intercalate , maximum, minimum ) import Data.Maybe ( isJust ) import FlatCurry.Annotated.Goodies import FlatCurry.Annotated.Types import FlatCurry.Show ( showCurryType ) import FlatCurry.Types ( showQName ) import Language.SMTLIB.Goodies import qualified Language.SMTLIB.Types as SMT import CheckSMT import Common import Curry2SMT import FlatCurry.Typed.Build import FlatCurry.Typed.Read import FlatCurry.Typed.Simplify import FlatCurry.Typed.Types import ToolOptions import TransState import VerifierState ------------------------------------------------------------------------ -- Try to verify postconditions: If an operation `f` has a postcondition, -- a proof for the validity of the postcondition is extracted. -- If the proof is not successful, a postcondition check is added to `f`. verifyPostConditions :: TAProg -> VStateM TAProg verifyPostConditions prog = do postconds <- gets $ postConds . trInfo -- Operations with postcondition checks: let fdecls = progFuncs prog newfuns <- provePostConds postconds fdecls return $ updProgFuncs (const newfuns) prog where provePostConds [] fdecls = return fdecls provePostConds (pof : pofs) fdecls = provePostCondition pof fdecls >>= provePostConds pofs provePostCondition :: TAFuncDecl -> [TAFuncDecl] -> VStateM [TAFuncDecl] provePostCondition postfun allfuns = do maybe (do liftIO $ putStrLn $ "Postcondition: " ++ pcname ++ "\n" ++ "Operation of this postcondition not found!" return allfuns) (\checkfun -> evalStateT (provePC (simpFuncDecl checkfun)) emptyTransState) (find (\fd -> toPostCondName (snd (funcName fd)) == decodeContractName pcname) allfuns) where pcname = snd (funcName postfun) provePC :: TAFuncDecl -> TransStateM [TAFuncDecl] provePC checkfun = do let (postmn,postfn) = funcName postfun mainfunc = snd (funcName checkfun) orgqn = (postmn, reverse (drop 5 (reverse postfn))) farity = funcArity checkfun ftype = funcType checkfun targsr = zip [1..] (argTypes ftype ++ [resultType ftype]) bodyformula <- extractPostConditionProofObligation [1 .. farity] (farity+1) (funcName checkfun) (funcRule checkfun) precondformula <- preCondExpOf orgqn (init targsr) postcondformula <- applyFunc postfun targsr >>= pred2SMT let title = "verify postcondition of '" ++ mainfunc ++ "'..." lift $ printWhenIntermediate $ "Trying to " ++ title mbsmt <- checkPostCon ("SMT script to " ++ title) (tand [precondformula, bodyformula]) true postcondformula maybe (lift $ do printWhenStatus $ mainfunc ++ ": POSTCOND CHECK ADDED" addPostCondToStats mainfunc False return $ map (addPostConditionTo (funcName postfun)) allfuns) (\proof -> lift $ do printWhenStatus $ mainfunc ++ ": POSTCONDITION VERIFIED" whenOption optStoreProof $ liftIO $ writeFile ("PROOF_" ++ showQNameNoDots orgqn ++ "_" ++ "SatisfiesPostCondition.smt") proof addPostCondToStats mainfunc True return allfuns) mbsmt -- If the function declaration is the declaration of the given function name, -- decorate it with a postcondition check. addPostConditionTo :: QName -> TAFuncDecl -> TAFuncDecl addPostConditionTo pfname fdecl = let fn = funcName fdecl in if toPostCondQName fn == pfname then updFuncBody (const (addPostConditionCheck fn (funcRule fdecl))) fdecl else fdecl -- Adds a postcondition check to a program rule of a given operation. addPostConditionCheck :: QName -> TARule -> TAExpr addPostConditionCheck _ (AExternal _ _) = error $ "Trying to add postcondition to external function!" addPostConditionCheck qf@(mn,fn) (ARule ty lhs rhs) = --ALit boolType (Intc 42) AComb ty FuncCall ((mn, "checkPostCond_" ++ type2ID tt ++ "_" ++ type2ID (annExpr rhs)), FuncType ty (FuncType (FuncType ty boolType) (FuncType stringType (FuncType tt ty)))) [ rhs , AComb boolType (FuncPartCall 1) (toPostCondQName qf, ty) args , string2TAFCY fn , tupleExpr args ] where args = map (\ (i,t) -> AVar t i) lhs tt = tupleType (map annExpr args) extractPostConditionProofObligation :: [Int] -> Int -> QName -> TARule -> TransStateM SMT.Term extractPostConditionProofObligation _ _ _ (AExternal _ s) = return $ tcomb ("External: " ++ s) [] extractPostConditionProofObligation args resvar fname (ARule ty orgargs orgexp) = do let exp = rnmAllVars renameRuleVar orgexp rtype = resType (length orgargs) (stripForall ty) put $ makeTransState (maximum (resvar : allVars exp) + 1) ((resvar, rtype, Just (fname, 0, 1)) : map (\(i,x,y) -> (x, y, Just (fname, i, 1))) (zip3 [1..] args $ map snd orgargs)) binding2SMT True (resvar,exp) where maxArgResult = maximum (resvar : args) renameRuleVar r = maybe (r + maxArgResult + 1) (args!!) (elemIndex r (map fst orgargs)) resType n te = if n==0 then te else case te of FuncType _ rt -> resType (n-1) rt _ -> error $ "Internal errror: resType: " ++ show te --------------------------------------------------------------------------- -- Try to verify preconditions: If an operation `f` occurring in some -- right-hand side has a precondition, a proof for the validity of -- this precondition is extracted. -- If the proof is not successful, a precondition check is added to this call. verifyPreConditions :: TAProg -> VStateM TAProg verifyPreConditions prog = do newfuns <- mapM provePreCondition $ progFuncs prog return (updProgFuncs (const newfuns) prog) provePreCondition :: TAFuncDecl -> VStateM TAFuncDecl provePreCondition fdecl = do printWhenIntermediate $ "Operation to be checked: " ++ snd (funcName fdecl) newrule <- optPreConditionInRule (funcName fdecl) (funcRule fdecl) return (updFuncRule (const newrule) fdecl) optPreConditionInRule :: QName -> TARule -> VStateM TARule optPreConditionInRule _ rl@(AExternal _ _) = return rl optPreConditionInRule qn@(_,fn) (ARule rty rargs rhs) = do let targs = zip [1..] (map snd rargs) st = makeTransState (maximum (0 : map fst rargs ++ allVars rhs) + 1) (map (\(i,(x,y)) -> (x, y, Just (qn, i, 0))) (zip [1..] rargs)) (flip evalStateT) st $ do -- compute precondition of operation: precondformula <- preCondExpOf qn targs setAssertion precondformula newrhs <- optPreCondInExp rhs return $ ARule rty rargs newrhs where optPreCondInExp exp = case exp of AComb ty ct (qf,tys) args -> do precond <- getAssertion nargs <- mapM optPreCondInExp args preconds <- lift $ gets $ preConds . trInfo if toPreCondQName qf `elem` map funcName preconds then do lift $ printWhenIntermediate $ "Checking call to " ++ snd qf (bs,_) <- normalizeArgs nargs setNameOfVars qf $ map fst bs bindexps <- mapM (binding2SMT True) bs precondcall <- preCondExpOf qf (zip (map fst bs) (map annExpr args)) -- TODO: select from 'bindexps' only demanded argument positions let title = "SMT script to verify precondition of '" ++ snd qf ++ "' in function '" ++ fn ++ "'" valid <- checkPreCon title precond (tand bindexps) precondcall fn (map fst rargs) if valid == Just True then lift $ do printWhenStatus $ fn ++ ": PRECONDITION OF '" ++ snd qf ++ "': VERIFIED" addPreCondToStats (snd qf ++ "(" ++ fn ++ ")") True return $ AComb ty ct (toNoCheckQName qf, tys) nargs else lift $ do printWhenStatus $ fn ++ ": PRECOND CHECK ADDED TO '" ++ snd qf ++ "'" addPreCondToStats (snd qf ++ "("++ fn ++ ")") False return $ AComb ty ct (qf,tys) nargs else return $ AComb ty ct (qf,tys) nargs ACase ty ct e brs -> do ne <- optPreCondInExp e freshvar <- getFreshVar be <- binding2SMT True (freshvar,ne) addToAssertion be addVarTypes [ (freshvar, annExpr ne) ] nbrs <- mapM (optPreCondInBranch freshvar) brs return $ ACase ty ct ne nbrs AOr ty e1 e2 -> do ne1 <- optPreCondInExp e1 ne2 <- optPreCondInExp e2 return $ AOr ty ne1 ne2 ALet ty bs e -> do nes <- mapM optPreCondInExp (map snd bs) ne <- optPreCondInExp e return $ ALet ty (zip (map fst bs) nes) ne AFree ty fvs e -> do ne <- optPreCondInExp e return $ AFree ty fvs ne ATyped ty e et -> do ne <- optPreCondInExp e return $ ATyped ty ne et _ -> return exp optPreCondInBranch dvar branch = do ABranch p e <- renamePatternVars branch addToAssertion (tvar dvar =% pat2SMT p) ne <- optPreCondInExp e return (ABranch p ne) -- Rename argument variables of constructor pattern renamePatternVars :: TABranchExpr -> TransStateM TABranchExpr renamePatternVars (ABranch p e) = 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 --------------------------------------------------------------------------- -- Add (non-trivial) preconditions: -- If an operation `f` has some precondition `f'pre`, -- replace the rule `f xs = rhs` by the following rules: -- -- f xs = checkPreCond (f'NOCHECK xs) (f'pre xs) "f" xs -- f'NOCHECK xs = rhs addPreConditions :: TAProg -> VStateM TAProg addPreConditions prog = do newfuns <- mapM addPreCondition (progFuncs prog) return $ updProgFuncs (const (concat newfuns)) prog where addPreCondition fdecl@(AFunc qf ar vis fty rule) = do preconds <- gets $ preConds . trInfo return $ if toPreCondQName qf `elem` map funcName preconds then let newrule = checkPreCondRule qf rule in [updFuncRule (const newrule) fdecl, AFunc (toNoCheckQName qf) ar vis fty rule] else [fdecl] checkPreCondRule :: QName -> TARule -> TARule checkPreCondRule qn (ARule rty rargs _) = ARule rty rargs (addPreConditionCheck rty FuncCall qn rty (map (\ (v,t) -> AVar t v) rargs)) checkPreCondRule qn (AExternal _ _) = error $ "addPreConditions: cannot add precondition to external operation '" ++ snd qn ++ "'!" -- Adds a precondition check to a original call of the form -- `AComb ty ct (qf,tys) args`. addPreConditionCheck :: TypeExpr -> CombType -> QName -> TypeExpr -> [TAExpr] -> TAExpr addPreConditionCheck ty ct qf@(mn,fn) tys args = AComb ty FuncCall ((mn, "checkPreCond_" ++ type2ID tt), FuncType ty (FuncType boolType (FuncType stringType (FuncType tt ty)))) [ AComb ty ct (toNoCheckQName qf,tys) args , AComb boolType ct (toPreCondQName qf, pctype) args , string2TAFCY fn , tupleExpr args ] where argtypes = map annExpr args tt = tupleType argtypes pctype = foldr FuncType boolType argtypes -- Translate a type expression into an identifier which is the suffix -- of `checkPreCond` which is a type-specialized instance. type2ID :: TypeExpr -> String type2ID te = case te of TCons (mn,tc) tes | mn == "Prelude" && null tes -> intercalate "_" (tc2ID tc : map type2ID tes) _ -> "Any" where tc2ID tc | tc == "[]" = "List" | tc == "()" = "Unit" | otherwise = tc --------------------------------------------------------------------------- -- Auxiliaries: --- Transform a qualified name into a name of the corresponding function --- without precondition checking by adding the suffix "'NOCHECK". toNoCheckQName :: (String,String) -> (String,String) toNoCheckQName (mn,fn) = (mn, fn ++ "'NOCHECK") -- Shows a qualified name by replacing all dots by underscores. showQNameNoDots :: QName -> String showQNameNoDots = map (\c -> if c=='.' then '_' else c) . showQName ---------------------------------------------------------------------------