------------------------------------------------------------------------ --- A transformation from a Curry program with pre/postconditions --- into a Curry program where these conditions are integrated --- into the code ------------------------------------------------------------------------ import AbstractCurry.Types import AbstractCurry.Files import AbstractCurryComments import AbstractCurry.Pretty import AbstractCurry.Build import AbstractCurry.Select import AbstractCurry.Transform import Directory import Distribution import FilePath ( () ) import List import Maybe ( fromJust ) import System import Time import Unsafe import DSDCurryPackageConfig(packagePath) dsdSourceDir :: String dsdSourceDir = packagePath "src" banner :: String banner = unlines [bannerLine,bannerText,bannerLine] where bannerText = "DSDCurry Transformation Tool (Version of 02/05/16)" bannerLine = take (length bannerText) (repeat '=') ------------------------------------------------------------------------ -- Data type for transformation parameters data TParam = TParam Bool -- generate code for lazy assertions? Bool -- use enforcable lazy assertions? Bool -- encapsulate assertion checking by set functions? Bool -- use single results of postconds as implement.s? Bool -- load and execute transformed program? Bool -- debug assertions during execution? defaultTParam = TParam False False False False False False setStrictAssert (TParam _ _ sf pcs ep db) = TParam False False sf pcs ep db setLazyAssert (TParam _ _ sf pcs ep db) = TParam True False sf pcs ep db setEnforceAssert (TParam _ _ sf pcs ep db) = TParam True True sf pcs ep db setEncapsulate (TParam la fa _ pcs ep db) = TParam la fa True pcs ep db withEncapsulate (TParam _ _ sf _ _ _) = sf setSinglePostSpecs (TParam la fa sf _ ep db) = TParam la fa sf True ep db withSinglePostSpecs (TParam _ _ _ pcs _ _) = pcs executeProg (TParam _ _ _ _ execprog _) = execprog setExecuteProg (TParam la fa sf pcs _ db) = TParam la fa sf pcs True db withDebugging (TParam _ _ _ _ _ db) = db setDebugging (TParam la fa sf pcs ep _) = TParam la fa sf pcs ep True -- get kind of assertion checking from parameters: checkKind :: TParam -> CExpr checkKind (TParam la fa _ _ _ _) = constF (aMod $ if la && fa then "Enforceable" else if la then "Lazy" else "Strict") ------------------------------------------------------------------------ main :: IO () main = do putStrLn banner args <- getArgs processArgs defaultTParam args where processArgs tparam args = case args of ("-s":moreargs) -> processArgs (setStrictAssert tparam) moreargs ("-l":moreargs) -> processArgs (setLazyAssert tparam) moreargs ("-f":moreargs) -> processArgs (setEnforceAssert tparam) moreargs ("-e":moreargs) -> processArgs (setEncapsulate tparam) moreargs ("-pcs":moreargs) -> processArgs (setSinglePostSpecs tparam) moreargs ("-r":moreargs) -> processArgs (setExecuteProg tparam) moreargs ("-d":moreargs) -> processArgs (setDebugging tparam) moreargs [mname] -> transform tparam (stripCurrySuffix mname) _ -> putStrLn $ "ERROR: Illegal arguments for transformation: " ++ unwords args ++ "\n" ++ "Usage: dsdcurry [-s|-f|-l|-e|-pcs|-r|-d] \n"++ "-s : generate strict assertions (default)\n"++ "-l : generate lazy assertions\n"++ "-f : generate lazy enforceable assertions\n"++ "-e : encapsulate nondeterminism of assertions\n"++ "-pcs : take single result of functions generated from postconditions\n"++ "-r : load the transformed program into PAKCS\n"++ "-d : show assertion results during execution (with -r)\n" -- Specifies how the name of the transformed module is built from the -- name of the original module. transformedModName :: String -> String transformedModName m = m++"C" -- start PAKCS and load a module: loadPAKCS :: TParam -> String -> IO () loadPAKCS tparam m = do putStrLn $ "\nStarting PAKCS and loading module '"++m++"'..." if withDebugging tparam then setEnviron "ASSERTDEBUG" "yes" else done system $ installDir "bin" "pakcs :l " ++ m done -- The main transformation function. transform :: TParam -> String -> IO () transform tparam modname = do let acyfile = abstractCurryFileName modname doesFileExist acyfile >>= \b -> if b then removeFile acyfile else done prog <- readCurryWithComments modname >>= return . addCmtFuncInProg doesFileExist acyfile >>= \b -> if b then done else error "Source program incorrect" let realfdecls = filter isRealFuncDecl (functions prog) funspecs = getFunSpecifications prog specnames = map (dropSpecName . snd . funcName) funspecs preconds = getPreConditions prog prenames = map (dropPreCondName . snd . funcName) preconds postconds = getPostConditions prog postnames = map (dropPostCondName . snd . funcName) postconds newfuns = union specnames postnames \\ (map (snd . funcName) realfdecls) checkfuns = union specnames (union prenames postnames) onlyprecond = prenames \\ (specnames ++ postnames ++ map (snd . funcName) realfdecls) saveprog = transformProgram tparam realfdecls funspecs preconds postconds prog savefile = transformedModName modname ++ ".curry" if null onlyprecond then done else error ("Operations with precondition but without implemenation/specification: " ++ unwords onlyprecond) if null newfuns then done else putStrLn $ "Generating new definitions for operations: " ++ unwords newfuns if null checkfuns then done else putStrLn $ "Adding pre/postcondition checking to: " ++ unwords checkfuns if null (funspecs++preconds++postconds) then putStrLn "No specifcations or pre/postconditions found, no transformation required!" else do putStrLn $ "Writing transformed module to '" ++ savefile ++ "'..." writeFile savefile (showCProg saveprog) copyImportModules tparam if executeProg tparam then loadPAKCS tparam (transformedModName modname) else done -- Is a function declaration a real implementation, i.e., -- is the body different from "unknown"? isRealFuncDecl :: CFuncDecl -> Bool isRealFuncDecl (CFunc _ _ _ _ rs) = not (isUnknown rs) isRealFuncDecl (CmtFunc _ _ _ _ _ rs) = not (isUnknown rs) isUnknown :: [CRule] -> Bool isUnknown rules = case rules of [CRule _ (CSimpleRhs e [])] -> e == CSymbol ("Prelude","unknown") _ -> False -- copy imported modules if necessary: copyImportModules tparam = do cdir <- getCurrentDirectory if cdir==dsdSourceDir then done else mapIO_ (\m -> copyFileOnDemand (dsdSourceDir m++".curry") (cdir m++".curry")) ["Assert"] let paramMod = if withEncapsulate tparam then "AssertParamEncapsulate" else "AssertParamNonEncapsulate" copyFileOnDemand (dsdSourceDir paramMod++".curry") (cdir "AssertParam.curry") -- get the specifcation functions from a Curry module getFunSpecifications :: CurryProg -> [CFuncDecl] getFunSpecifications prog = filter (isSpecName . snd . funcName) (functions prog) -- get the preconditions from a Curry module getPreConditions :: CurryProg -> [CFuncDecl] getPreConditions prog = filter (isPreCondName . snd . funcName) (functions prog) -- get the postconditions from a Curry module getPostConditions :: CurryProg -> [CFuncDecl] getPostConditions prog = filter (isPostCondName . snd . funcName) (functions prog) -- Transform a given program w.r.t. given specifications and pre/postconditions transformProgram :: TParam -> [CFuncDecl] -> [CFuncDecl] -> [CFuncDecl] -> [CFuncDecl] -> CurryProg -> CurryProg transformProgram tparam allfdecls specdecls predecls postdecls (CurryProg mname imps tdecls fdecls opdecls) = let newspecfuns = concatMap (genFunction4Spec tparam fdecls) specdecls newpostspecs = concatMap (genFunction4PostCond tparam fdecls) postdecls newpostspecnames = map (snd . funcName) newpostspecs newpostconds = concatMap (genPostCond4Spec tparam allfdecls postdecls) specdecls newfunnames = map (snd . funcName) (newpostconds ++ newspecfuns ++ newpostspecs) wonewfuns = filter (\fd -> snd (funcName fd) `notElem` newfunnames) fdecls -- remove functions having new gen. defs. -- compute postconditions actually used for contract checking: contractpcs = filter (\fd -> dropPostCondName (snd (funcName fd)) `notElem` newpostspecnames) (postdecls++newpostconds) rename (mn,fn) = (if mn==mname then transformedModName mname else mn, fn) in renameCurryModule (transformedModName mname) $ CurryProg mname (nub ("Assert":"SetFunctions":imps)) tdecls (map deleteCmtIfEmpty (map (addContract tparam predecls contractpcs) (newspecfuns++newpostspecs++wonewfuns) ++ newpostconds ++ map genAssertInstance tdecls)) opdecls -- Add an empty comment to each function which has no comment addCmtFuncInProg :: CurryProg -> CurryProg addCmtFuncInProg (CurryProg mname imps tdecls fdecls opdecls) = CurryProg mname imps tdecls (map addCmtFunc fdecls) opdecls where addCmtFunc (CFunc qn ar vis texp rs) = CmtFunc "" qn ar vis texp rs addCmtFunc (CmtFunc cmt qn ar vis texp rs) = CmtFunc cmt qn ar vis texp rs -- Generate a function definition from a specification if there is no function -- for this specification present: genFunction4Spec :: TParam -> [CFuncDecl] -> CFuncDecl -> [CFuncDecl] genFunction4Spec _ allfuncs (CmtFunc cmt (m,f) ar vis texp _) = let fname = dropSpecName f deffuncs = filter (\fd -> isRealFuncDecl fd && snd (funcName fd) == fname) allfuncs argvars = map (\i -> (i,"y"++show i)) [1..ar] in if null deffuncs then [cmtfunc cmt (m,fname) ar vis texp [simpleRule (map CPVar argvars) (applyF (m,f) (map CVar argvars))]] else [] -- Generate a postcondition from a specification that is parameterized -- by an "observation function". -- If the specification is deterministic, generate an equality check, -- otherwise generate a set containment check. genPostCond4Spec :: TParam -> [CFuncDecl] -> [CFuncDecl] -> CFuncDecl -> [CFuncDecl] genPostCond4Spec _ allfdecls postdecls (CmtFunc _ (m,f) ar vis texp _) = let fname = dropSpecName f detspec = isDetSpecName f -- determ. spec? (later: use prog.ana.) fpostname = fname++"'post" fpgenname = fpostname++"'generic" oldfpostc = filter (\fd -> snd (funcName fd) == fpostname) postdecls oldcmt = if null oldfpostc then "" else '\n' : funcComment (head oldfpostc) varg = (0,"g") argvars = map (\i -> (i,"x"++show i)) [1..(ar+1)] spargvars = take ar argvars resultvar = last argvars gtype = CTVar (0,"grt") -- result type of observation function varz = (ar+2,"z") obsfun = maybe (pre "id") funcName (find (\fd -> snd (funcName fd) == fpostname++"'observe") allfdecls) postcheck = CLetDecl [CLocalPat (CPVar varz) (CSimpleRhs (CApply (CVar varg) (CVar resultvar)) []), CLocalFunc (cfunc (m,"gspec") ar Private (replaceResultType texp gtype) [let gsargvars = map (\i -> (i,"y"++show i)) [1..ar] in simpleRule (map CPVar gsargvars) (CApply (CVar varg) (applyF (m,f) (map CVar gsargvars)))])] (if detspec then applyF (pre "==") [CVar varz, applyF (m,"gspec") (map CVar spargvars)] else applyF (pre "&&") [applyF (pre "==") [CVar varz, CVar varz], applyF (sfMod "valueOf") [CVar varz, applyF (sfMod $ "set"++show ar) (constF (m,"gspec") : map CVar spargvars)]]) rename qf = if qf==(m,fpostname) then (m,fpostname++"'org") else qf in [cmtfunc ("Parametric postcondition for '"++fname++ "' (generated from specification). "++oldcmt) (m,fpgenname) (ar+2) vis ((resultType texp ~> gtype) ~> extendFuncType texp boolType) [if null oldfpostc then simpleRule (map CPVar (varg:argvars)) postcheck else simpleRuleWithLocals (map CPVar (varg:argvars)) (applyF (pre "&&") [applyF (rename (funcName (head oldfpostc))) (map CVar argvars), postcheck]) [updQNamesInCLocalDecl rename (CLocalFunc (deleteCmt (head oldfpostc)))]] ,cmtfunc ("Postcondition for '"++fname++"' (generated from specification). "++ oldcmt) (m,fpostname) (ar+1) vis (extendFuncType texp boolType) [simpleRule (map CPVar argvars) (applyF (m,fpgenname) (constF obsfun : map CVar argvars))] ] -- Generate a function definition from a postcondition if there is -- neither a specification nor an implementation for this function, -- i.e., consider this postcondition as a specification for an implementation: genFunction4PostCond :: TParam -> [CFuncDecl] -> CFuncDecl -> [CFuncDecl] genFunction4PostCond tparam allfuncs (CmtFunc cmt (m,f) _ vis texp _) = let fname = dropPostCondName f flname = if withSinglePostSpecs tparam then fname++"''" else fname ar = arityOfType texp - 1 ftype = transPCType f texp deffuncs = filter (\fd -> isRealFuncDecl fd && (snd (funcName fd) == fname || dropSpecName (snd (funcName fd)) == fname)) allfuncs argvars = map (\i -> (i,"y"++show i)) [1..ar] resultvar = (ar+1,"y0") postcall = applyF (m,f) (map CVar (argvars++[resultvar])) in if null deffuncs then let postfun = cmtfunc cmt (m,flname) ar vis ftype [guardedRule (map CPVar argvars) [(postcall, CVar resultvar)] [CLocalVars [resultvar]]] in [if withSinglePostSpecs tparam then cmtfunc "" (m,fname) ar vis ftype [simpleRuleWithLocals [] (applyF (aMod $ "someValueOf"++show ar) [setFun ar (m,flname) []]) [CLocalFunc postfun]] else postfun] else [] -- adds contract checking to a function if it has a pre- or postcondition addContract :: TParam -> [CFuncDecl] -> [CFuncDecl] -> CFuncDecl -> CFuncDecl addContract tparam predecls postdecls fdecl@(CmtFunc cmt (m,f) ar vis texp _) = let asrttypes = map toPolymorphicAssertTypes (getArgResultTypes texp) argvars = map (\i -> (i,"x"++show i)) [1..ar] predecl = find (\fd -> dropPreCondName(snd(funcName fd)) == f) predecls prename = funcName (fromJust predecl) postdecl = find (\fd-> dropPostCondName(snd(funcName fd)) == f) postdecls postname = funcName (fromJust postdecl) encaps fn n = if withEncapsulate tparam then setFun n fn [] else constF fn asrtCall = if predecl==Nothing then applyF (aMod $ "withPostContract" ++ show ar) (checkKind tparam : asrttypes ++ [string2ac f, encaps postname (ar+1), constF (m,f++"'")] ++ map CVar argvars) else if postdecl==Nothing then applyF (aMod $ "withPreContract" ++ show ar) (checkKind tparam : asrttypes ++ [string2ac f, encaps prename ar, constF (m,f++"'")] ++ map CVar argvars) else applyF (aMod $ "withContract" ++ show ar) (checkKind tparam : asrttypes ++ [string2ac f, encaps prename ar, encaps postname (ar+1), constF (m,f++"'")] ++ map CVar argvars) rename qf = if qf==(m,f) then (m,f++"'") else qf in if predecl==Nothing && postdecl==Nothing then fdecl else cmtfunc cmt (transformedModName m,f) ar vis texp [simpleRuleWithLocals (map CPVar argvars) asrtCall [updQNamesInCLocalDecl rename (CLocalFunc (deleteCmt fdecl))]] -- Get types of arguments and result getArgResultTypes t = case t of CFuncType t1 t2 -> t1 : getArgResultTypes t2 _ -> [t] -- Transforms a monomorphic type expression into an assertion instance -- expression of this type. toPolymorphicAssertTypes :: CTypeExpr -> CExpr toPolymorphicAssertTypes = toAssertTypes (\_ -> constF (aMod "aPolyType")) -- Transforms a type expression into an assertion instance expression -- of this type. The first argument specifies the mapping for -- type variables. toAssertTypes :: ((Int,String) -> CExpr) -> CTypeExpr -> CExpr toAssertTypes mapvar (CTVar tv) = mapvar tv toAssertTypes mapvar (CFuncType t1 t2) = applyF (aMod "aFun") (map (toAssertTypes mapvar) [t1,t2]) toAssertTypes mapvar (CTCons (tm,tc) targs) = applyF (if tm=="Prelude" then aMod (preludeTCons2Assert tc) else (tm,'a':tc)) (map (toAssertTypes mapvar) targs) where preludeTCons2Assert c = case c of "Int" -> "aInt" "Float" -> "aFloat" "Char" -> "aChar" "Bool" -> "aBool" "Success" -> "aSuccess" "Ordering" -> "aOrdering" "[]" -> "aList" "String" -> "aString" "Maybe" -> "aMaybe" "Either" -> "aEither" "()" -> "aUnit" "(,)" -> "aPair" "(,,)" -> "aTriple" "(,,,)" -> "aTuple4" _ -> error ("Lazy assertion of type '"++c++"' not yet supported!") -- Transforms the type of a postcondition into a type for the -- corresponding function. transPCType f t = case t of CFuncType t1 (CTCons _ _) -> t1 CFuncType t1 t2 -> CFuncType t1 (transPCType f t2) _ -> error ("Illegal type of postcondition \""++f++"\"!") -- Computes the (first-order) arity of a type. arityOfType t = case t of CFuncType _ t' -> 1 + arityOfType t' _ -> 0 -- Is this the name of a specification? isSpecName f = let rf = reverse f in take 5 rf == "ceps'" || take 6 rf == "dceps'" -- Is this the name of a deterministic specification? isDetSpecName f = take 6 (reverse f) == "dceps'" -- Drop the specification suffix from the name: dropSpecName f = let rf = reverse f in reverse (drop (if take 5 rf == "ceps'" then 5 else if take 6 rf == "dceps'" then 6 else 0) rf) -- Is this the name of a precondition? isPreCondName f = take 4 (reverse f) == "erp'" -- Drop the precondition suffix from the name: dropPreCondName f = let rf = reverse f in reverse (drop (if take 4 rf == "erp'" then 4 else 0) rf) -- Is this the name of a precondition? isPostCondName f = take 5 (reverse f) == "tsop'" -- Drop the postcondition suffix from the name: dropPostCondName f = let rf = reverse f in reverse (drop (if take 5 rf == "tsop'" then 5 else 0) rf) -- An operation of the module Assert: aMod f = ("Assert",f) -- An operation of the module SetFunctions: sfMod f = ("SetFunctions",f) -- Set function for a function name with given arity and arguments: setFun :: Int -> QName -> [CExpr] -> CExpr setFun n qn args = applyF (sfMod $ "set"++show n) (constF qn : args) ------------------------------------------------------------------------ -- Generate code for Assert instances on user-defined types. genAssertInstance :: CTypeDecl -> CFuncDecl genAssertInstance (CTypeSyn (mn,tc) _ targs texp) = cfunc (mn,'a':tc) 1 Public (foldr (\tv t -> CTCons (aMod "Assert") [CTVar tv] ~> t) (CTCons (aMod "Assert") [CTCons (mn,tc) (map CTVar targs)]) targs) [simpleRule (map (\ (i,s) -> CPVar (i,"assert_"++s)) targs) (toLocalAssertType texp)] genAssertInstance (CType (mn,tc) _ targs tcs) = cfunc (mn,'a':tc) 1 Public (foldr (\tv t -> CTCons (aMod "Assert") [CTVar tv] ~> t) (CTCons (aMod "Assert") [mtype]) targs) [simpleRuleWithLocals (map (\ (i,s) -> CPVar (i,"assert_"++s)) targs) (applyF (aMod "makeAssert") [CSymbol (mn,"wait"++tc), CSymbol (mn,"ddunif"++tc)]) [CLocalFunc $ cfunc (mn,"wait"++tc) 1 Private (mtype ~> mtype) [simpleRule [CPVar wvar] (CCase CRigid (CVar wvar) (map tc2waitbranch tcs))], CLocalFunc $ cfunc (mn,"ddunif"++tc) 1 Private (mtype ~> mtype ~> mtype) [simpleRule [CPVar uvar1, CPVar uvar2] (CCase CRigid (CVar uvar2) (map tc2unifbranch tcs))] ]] where mtype = CTCons (mn,tc) (map CTVar targs) wvar = (1,"wv") uvar1 = (1,"x") uvar2 = (2,"exp") tc2waitbranch (CCons (_,cons) _ texps) = let n = length texps in (CPComb (mn,cons) (map (\i -> CPVar (i,'x':show i)) [1..n]), CSimpleRhs (applyF (mn,cons) (map (\ (i,texp) -> texp2wait texp [CVar (i,'x':show i)]) (zip [1..n] texps))) []) tc2unifbranch (CCons (_,cons) _ texps) = let n = length texps in (CPComb (mn,cons) (map (\i -> CPVar (i,'x':show i)) [1..n]), CSimpleRhs (letExpr (map (\i -> CLocalVars [(i+100,'y':show i)]) [1..n]) (applyF (pre "&>") [applyF (pre "=:=") [CVar uvar1, applyF (mn,cons) (map (\i -> CVar (i+100,'y':show i)) [1..n])], applyF (mn,cons) (map (\ (i,texp) -> texp2unif texp [CVar (i+100,'y':show i), CVar (i,'x':show i)]) (zip [1..n] texps))])) []) texp2wait (CTVar (i,tv)) args = applyF (aMod "waitOf") (CVar (i,"assert_"++tv) : args) texp2wait texp@(CFuncType _ _) args = applyF (aMod "waitOf") (toLocalAssertType texp : args) texp2wait texp@(CTCons (tm,tcons) _) args = if texp==mtype -- recursive type? then applyF (tm,"wait"++tcons) args else applyF (aMod "waitOf") (toLocalAssertType texp : args) texp2unif (CTVar (i,tv)) args = applyF (aMod "ddunifOf") (CVar (i,"assert_"++tv) : args) texp2unif texp@(CFuncType _ _) args = applyF (aMod "ddunifOf") (toLocalAssertType texp : args) texp2unif texp@(CTCons (tm,tcons) _) args = if texp==mtype -- recursive type? then applyF (tm,"ddunif"++tcons) args else applyF (aMod "ddunifOf") (toLocalAssertType texp : args) -- Transforms a type expression into an assertion instance expression -- of this type. toLocalAssertType = toAssertTypes (\ (i,tv) -> CVar (i,"assert_"++tv)) -- Computes result type of a function type resultType :: CTypeExpr -> CTypeExpr resultType texp = case texp of CFuncType _ t -> resultType t _ -> texp -- Replaces a result type of a function type by a new type replaceResultType :: CTypeExpr -> CTypeExpr -> CTypeExpr replaceResultType texp ntype = case texp of CFuncType t1 t2 -> CFuncType t1 (replaceResultType t2 ntype) _ -> ntype -- Transform a n-ary function type into a (n+1)-ary function type with -- a given new result type extendFuncType :: CTypeExpr -> CTypeExpr -> CTypeExpr extendFuncType t@(CTVar _) texp = t ~> texp extendFuncType t@(CTCons _ _) texp = t ~> texp extendFuncType (CFuncType t1 t2) texp = t1 ~> (extendFuncType t2 texp) ------------------------------------------------------------------------ -- Auxiliary operations: --- Copy a file on demand, i.e., do not copy it if the target file --- exists with the same time stamp and size. copyFileOnDemand :: String -> String -> IO () copyFileOnDemand source target = do let copycmd = do putStrLn "Copying auxiliary module:" putStrLn (source++" -> "++target) copyFile source target exfile <- doesFileExist target if exfile then do odate <- getModificationTime source ndate <- getModificationTime target osize <- fileSize source nsize <- fileSize target if compareClockTime ndate odate /= LT && osize == nsize then done else copycmd else copycmd ------------------------------------------------------------------------ --- Deletes the comment in a function declaration. deleteCmt (CFunc qn ar vis texp rules) = CFunc qn ar vis texp rules deleteCmt (CmtFunc _ qn ar vis texp rules) = CFunc qn ar vis texp rules --- Deletes the comment in a function declaration if it is the empty string. deleteCmtIfEmpty (CFunc qn ar vis texp rules) = CFunc qn ar vis texp rules deleteCmtIfEmpty (CmtFunc cmt qn ar vis texp rules) = if null cmt then CFunc qn ar vis texp rules else CmtFunc cmt qn ar vis texp rules ------------------------------------------------------------------------