Commit 2e3a1f8f authored by Michael Hanus's avatar Michael Hanus
Browse files

Code refactoring, simplification of postconditions added to currycheck

parent bb371ce1
......@@ -7,14 +7,14 @@
--- * All EasyCheck tests are extracted and checked
--- * For all functions declared as deterministic,
--- determinism properties are generated and checked.
--- * For functions with post-conditions (f'post), checks for post-conditions
--- are generated (together with possible pre-conditions)
--- * For functions with postconditions (f'post), checks for postconditions
--- are generated (together with possible preconditions)
--- * For functions with specification (f'spec), checks for satisfaction
--- of these specifications are generated
--- (together with possible pre-conditions).
--- (together with possible preconditions).
---
--- @author Michael Hanus, Jan-Patrick Baye
--- @version June 2016
--- @version August 2016
-------------------------------------------------------------------------
import AbstractCurry.Types
......@@ -24,9 +24,6 @@ import AbstractCurry.Build
import AbstractCurry.Pretty (showCProg)
import AbstractCurry.Transform (renameCurryModule,updCProg,updQNamesInCProg)
import AnsiCodes
import CheckDetUsage (checkDetUse, containsDetOperations)
import ContractUsage
import DefaultRuleUsage (checkDefaultRules, containsDefaultRules)
import Distribution
import FilePath ((</>), takeDirectory)
import qualified FlatCurry.Types as FC
......@@ -38,7 +35,12 @@ import List
import Maybe (fromJust, isJust)
import ReadNumeric (readNat)
import System (system, exitWith, getArgs, getPID)
import CheckDetUsage (checkDetUse, containsDetOperations)
import ContractUsage
import DefaultRuleUsage (checkDefaultRules, containsDefaultRules)
import TheoremUsage
import SimplifyPostConds (simplifyPostConditionsWithTheorems)
import UsageCheck (checkBlacklistUse, checkSetUse)
--- Maximal arity of check functions and tuples currently supported:
......@@ -50,7 +52,7 @@ ccBanner :: String
ccBanner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText =
"CurryCheck: a tool for testing Curry programs (version of 22/06/2016)"
"CurryCheck: a tool for testing Curry programs (version of 12/08/2016)"
bannerLine = take (length bannerText) (repeat '-')
-- Help text
......@@ -95,8 +97,8 @@ options =
, Option "q" ["quiet"] (NoArg (\opts -> opts { optVerb = 0 }))
"run quietly (no output, only exit code)"
, Option "v" ["verbosity"]
(OptArg (maybe (checkVerb 2) (safeReadNat checkVerb)) "<n>")
"verbosity level:\n0: quiet (same as `-q')\n1: show test names (default)\n2: show test data (same as `-v')\n3: keep intermediate program files"
(OptArg (maybe (checkVerb 3) (safeReadNat checkVerb)) "<n>")
"verbosity level:\n0: quiet (same as `-q')\n1: show test names (default)\n2: show more information about test generation\n3: show test data (same as `-v')\n4: keep intermediate program files"
, Option "m" ["maxtests"]
(ReqArg (safeReadNat (\n opts -> opts { optMaxTest = n })) "<n>")
"maximal number of tests (default: 100)"
......@@ -129,7 +131,7 @@ options =
(\ (n,rs) -> if null rs then opttrans n opts else numError)
(readNat s)
checkVerb n opts = if n>=0 && n<4
checkVerb n opts = if n>=0 && n<5
then opts { optVerb = n }
else error "Illegal verbosity level (try `-h' for help)"
......@@ -320,7 +322,7 @@ easyCheckConfig :: Options -> QName
easyCheckConfig opts =
(easyCheckExecModule,
if isQuiet opts then "quietConfig" else
if optVerb opts > 1 then "verboseConfig"
if optVerb opts > 2 then "verboseConfig"
else "easyConfig")
-- Translates a type expression into calls to generator operations.
......@@ -404,48 +406,47 @@ classifyTests = map makeProperty
then IOTest (funcName test) 0
else PropTest (funcName test) (funcType test) 0
-- Extracts all tests and transforms all polymorphic tests into tests on a
-- base type.
-- The result contains a pair consisting of all actual tests and all
-- ignored tests.
transformTests :: Options -> CurryProg -> ([CFuncDecl],[CFuncDecl],CurryProg)
transformTests opts (CurryProg mname imports typeDecls functions opDecls) =
(map snd realtests, map snd ignoredtests,
CurryProg mname
(nub (easyCheckModule:imports))
typeDecls
(funcs ++ map snd (realtests ++ ignoredtests))
opDecls)
-- Extracts all tests from a given Curry module and transforms
-- all polymorphic tests into tests on a base type.
-- The result contains a triple consisting of all actual tests,
-- all ignored tests, and the public version of the original module.
transformTests :: Options -> CurryProg -> IO ([CFuncDecl],[CFuncDecl],CurryProg)
transformTests opts prog@(CurryProg mname imps typeDecls functions opDecls) = do
theofuncs <- getTheoremFunctions prog
simpfuncs <- simplifyPostConditionsWithTheorems (optVerb opts) theofuncs funcs
let preCondOps = preCondOperations simpfuncs
postCondOps = map ((\ (mn,fn) -> (mn, fromPostCondName fn)) . funcName)
(funDeclsWith isPostCondName simpfuncs)
specOps = map ((\ (mn,fn) -> (mn, fromSpecName fn)) . funcName)
(funDeclsWith isSpecName simpfuncs)
-- generate post condition tests:
postCondTests = concatMap (genPostCondTest preCondOps postCondOps) funcs
-- generate specification tests:
specOpTests = concatMap (genSpecTest preCondOps specOps) funcs
(realtests,ignoredtests) = partition fst $
if not (optProp opts)
then []
else concatMap (poly2default (optDefType opts)) $
filter (\fd -> funcName fd `notElem` map funcName theofuncs) usertests ++
(if optSpec opts then postCondTests ++ specOpTests else [])
return (map snd realtests,
map snd ignoredtests,
CurryProg mname
(nub (easyCheckModule:imps))
typeDecls
(simpfuncs ++ map snd (realtests ++ ignoredtests))
opDecls)
where
(usertests, funcs) = partition isTest functions
preCondOps = preCondOperations functions
postCondOps = map ((\ (mn,fn) -> (mn, fromPostCondName fn)) . funcName)
(filter (\fd -> isPostCondName (snd (funcName fd)))
functions)
specOps = map ((\ (mn,fn) -> (mn, fromSpecName fn)) . funcName)
(filter (\fd -> isSpecName (snd (funcName fd)))
functions)
-- generate post condition tests:
postCondTests = concatMap (genPostCondTest preCondOps postCondOps) functions
-- generate specification tests:
specOpTests = concatMap (genSpecTest preCondOps specOps) functions
(realtests,ignoredtests) = partition fst $
if not (optProp opts)
then []
else concatMap (poly2default (optDefType opts)) $
usertests ++
(if optSpec opts then postCondTests ++ specOpTests else [])
-- Extracts all determinism tests and transforms deterministic operations
-- back into non-deterministic operations.
-- The result contains a pair consisting of all actual determinism tests
-- and all ignored tests (since they are polymorphic).
-- Extracts all determinism tests from a given Curry module and
-- transforms deterministic operations back into non-deterministic operations
-- in order to test their determinism property.
-- The result contains a triple consisting of all actual determinism tests,
-- all ignored tests (since they are polymorphic), and the public version
-- of the transformed original module.
transformDetTests :: Options -> [String] -> CurryProg
-> ([CFuncDecl],[CFuncDecl],CurryProg)
transformDetTests opts prooffiles
......@@ -478,8 +479,11 @@ transformDetTests opts prooffiles
preCondOperations :: [CFuncDecl] -> [QName]
preCondOperations fdecls =
map ((\ (mn,fn) -> (mn,fromPreCondName fn)) . funcName)
(filter (\fd -> isPreCondName (snd (funcName fd)))
fdecls)
(funDeclsWith isPreCondName fdecls)
-- Filter functions having a name satisfying a given predicate.
funDeclsWith :: (String -> Bool) -> [CFuncDecl] -> [CFuncDecl]
funDeclsWith pred = filter (pred . snd . funcName)
-- Transforms a function type into a property type, i.e.,
-- t1 -> ... -> tn -> t is transformed into t1 -> ... -> tn -> Prop
......@@ -582,7 +586,7 @@ genDetProp prefuns (CFunc (mn,fn) ar _ texp _) =
forgcall = applyF (mn,forg) (map CVar cvars)
rnumcall = applyF (easyCheckModule,"#<") [forgcall, cInt 2]
-- Generates auxiliary (Boolean-instantiated) test functions for
-- Generates auxiliary (base-type instantiated) test functions for
-- polymorphically typed test function.
-- The flag indicates whether the test function should be actually passed
-- to the test tool.
......@@ -669,10 +673,10 @@ analyseCurryProg opts modname orgprog = do
let words = map firstWord (lines progtxt)
staticerrs = missingCPP ++ map (showOpError words) staticoperrs
putStrIfVerbose opts "Generating property tests...\n"
let (rawTests,ignoredTests,pubmod) =
(rawTests,ignoredTests,pubmod) <-
transformTests opts . renameCurryModule (modname++"_PUBLIC")
. makeAllPublic $ prog
(rawDetTests,ignoredDetTests,pubdetmod) =
let (rawDetTests,ignoredDetTests,pubdetmod) =
transformDetTests opts prooffiles
. renameCurryModule (modname++"_PUBLICDET")
. makeAllPublic $ prog
......@@ -816,10 +820,10 @@ createTestDataGenerator mainmodname qt@(mn,_) = do
ctvars = map (\i -> CTVar (i,"a"++show i)) tvars
cvars = map (\i -> (i,"a"++show i)) tvars
-- remove the generated files (except in Verbose-mode)
-- remove the generated files (except in highest verbose mode)
cleanup :: Options -> String -> [TestModule] -> IO ()
cleanup opts mainmodname modules =
unless (optVerb opts > 2) $ do
unless (optVerb opts > 3) $ do
removeCurryModule mainmodname
mapIO_ removeCurryModule (map testModuleName modules)
where
......
......@@ -2,6 +2,10 @@
TOOL=$(BINDIR)/currycheck
REWRITINGDIR = $(CURDIR)/../verification
# currycheck input path and dependencies:
CCPATH = $(REWRITINGDIR)
DEPS = *.curry $(LIBDIR)/Test/EasyCheck.curry $(LIBDIR)/AbstractCurry/*.curry
.PHONY: all compile install clean uninstall
......@@ -22,4 +26,4 @@ uninstall: clean
rm -f $(TOOL)
CurryCheck: $(DEPS)
$(REPL) $(REPL_OPTS) :l CurryCheck :save :q
$(REPL) $(REPL_OPTS) :set path $(CCPATH) :l CurryCheck :save :q
------------------------------------------------------------------------
--- The implementation of the "postcondition" reducer that simplifies
--- postconditions w.r.t. a given list of theorems.
--- This module contains the implementation of the "postcondition" reducer
--- which simplifies the postconditions in a list of function declarations
--- w.r.t. a given list of theorems.
---
--- Note that theorems are standard (EasyCheck) properties having the
--- prefix `theorem'`, as
---
--- theorem'sortlength xs = length xs <~> length (sort xs)
---
--- theorem'sorted xs = always (sorted (sort xs))
---
--- @author Michael Hanus
--- @version June 2016
--- @version August 2016
------------------------------------------------------------------------
module SimplifyPostConds(simplifyPostConditionWithTheorems) where
module SimplifyPostConds
( simplifyPostConditionsWithTheorems)
where
import AbstractCurry.Types
import AbstractCurry.Select
import AbstractCurry.Build
import ContractUsage
import List (last, maximum)
import Maybe (maybeToList)
import ReadShowTerm(readQTerm)
import List (last, maximum)
import Maybe (maybeToList)
import ReadShowTerm (readQTerm)
import Rewriting.Files
import Rewriting.Term
import Rewriting.Position
import Rewriting.Substitution
import Rewriting.Rules
simplifyPostConditionWithTheorems :: Int -> [CFuncDecl] -> [CFuncDecl]
-> IO [CFuncDecl]
simplifyPostConditionWithTheorems verb theofuncs postconds
| null theofuncs
= return postconds
| otherwise
= mapIO (simplifyPostCondition verb theofuncs) postconds >>= return . concat
simplifyPostCondition :: Int -> [CFuncDecl] -> CFuncDecl -> IO [CFuncDecl]
simplifyPostCondition verb theofuncs (CFunc qn ar vis texp rs) =
simplifyPostCondition verb theofuncs (CmtFunc "" qn ar vis texp rs)
simplifyPostCondition verb theofuncs (CmtFunc cmt qn ar vis texp rules) = do
when (verb>0) $ putStr $ unlines
["THEOREMS:", showTRS snd theoTRS,
"SIMPLIFICATION RULES:", showTRS snd simprules]
redrules <- mapIO (simplifyRule verb simprules qn) rules
return $ if all isTrivial redrules
then []
else [CmtFunc cmt qn ar vis texp redrules]
import ContractUsage
import TheoremUsage
-- Simplify the postconditions contained in the third argument w.r.t. a given
-- list of theorems (second argument).
-- If the verbosity (first argument) is greater than 1, the details
-- about the theorems, simplifcation rules, and reduced postconditions
-- are shown.
simplifyPostConditionsWithTheorems :: Int -> [CFuncDecl] -> [CFuncDecl]
-> IO [CFuncDecl]
simplifyPostConditionsWithTheorems verb theofuncs postconds = do
theoTRS <- mapIO safeFromFuncDecl theofuncs >>= return . concat
if null theoTRS
then return postconds
else do
let simprules = concatMap theoremToSimpRules theoTRS ++ standardSimpRules
when (verb>1) $ putStr $ unlines
[ "THEOREMS (with existing proof files):", showTRS snd theoTRS,
"SIMPLIFICATION RULES (for postcondition reduction):"
, showTRS snd simprules]
simppostconds <- mapIO (safeSimplifyPostCondition verb simprules) postconds
return (concat simppostconds)
where
theoTRS = concatMap (snd . fromFuncDecl) theofuncs
simprules = concatMap theoremToSimpRules theoTRS ++ standardSimpRules
safeFromFuncDecl fd =
catch (return $!! (snd (fromFuncDecl fd)))
(\e -> do
putStrLn $ showError e ++ "\nTheorem \"" ++
snd (funcName fd) ++
"\" not used for simplification (too complex)."
return [])
-- Simplify a single postcondition (third argument) w.r.t. a given
-- list of theorems (second argument):
safeSimplifyPostCondition :: Int -> TRS QName -> CFuncDecl -> IO [CFuncDecl]
safeSimplifyPostCondition verb simprules fundecl =
catch (simplifyPostCondition verb simprules fundecl)
(\e -> do putStrLn $ showError e ++ "\nPostcondition \"" ++
snd (funcName fundecl) ++
"\" not simplified (too complex)."
return [fundecl])
simplifyPostCondition :: Int -> TRS QName -> CFuncDecl -> IO [CFuncDecl]
simplifyPostCondition verb simprules (CFunc qn ar vis texp rs) =
simplifyPostCondition verb simprules (CmtFunc "" qn ar vis texp rs)
simplifyPostCondition verb simprules fdecl@(CmtFunc cmt qn ar vis texp rules) =
if isPostCondName (snd qn)
then do redrules <- mapIO (simplifyRule verb simprules qn) rules
return $ if all isTrivial redrules
then []
else [CmtFunc cmt qn ar vis texp redrules]
else return [fdecl]
theoremToSimpRules :: Rule QName -> [Rule QName]
theoremToSimpRules (_, TermVar _) =
......@@ -69,7 +107,8 @@ maxSimpSteps = 100
-- Simplify a rule of a postcondition.
simplifyRule :: Int -> TRS QName -> QName -> CRule -> IO CRule
simplifyRule verb simprules qn crule@(CRule rpats _) = do
when (verb > 0 ) $ putStrLn $ unlines
(id $!! (lhs,rhs)) `seq` done -- in order to raise a fromRule error here!
when (verb > 1 ) $ putStrLn $ unlines
["POSTCONDITION: " ++ showRule snd (lhs,rhs),
"POSTCONDEXP: " ++ showTerm snd postcondexp,
"SIMPLIFIEDEXP: " ++ showTerm snd simpterm,
......
......@@ -27,13 +27,15 @@
module TheoremUsage
( isTheoremFunc, isTheoremName, fromTheoremName, determinismTheoremFor
, getProofFiles, existsProofFor, isProofFileName, isProofFileNameFor
, getTheoremFunctions
) where
import AbstractCurry.Types
import AbstractCurry.Select
import Char
import Directory
import FilePath (dropExtension)
import Distribution (modNameToPath)
import FilePath (dropExtension, takeDirectory)
import List
------------------------------------------------------------------------
......@@ -89,3 +91,16 @@ deleteNonAlphanNum :: String -> String
deleteNonAlphanNum s = filter isAlphaNum (dropExtension s)
------------------------------------------------------------------------
-- Get all theorems which are contained in a given program
-- and for which proof files exist.
getTheoremFunctions :: CurryProg -> IO [CFuncDecl]
getTheoremFunctions (CurryProg mname _ _ functions _) = do
let dcltheofuncs = funDeclsWith isTheoremName functions -- declared theorems
prooffiles <- getProofFiles (takeDirectory (modNameToPath mname))
return $ filter (\fd -> existsProofFor (fromTheoremName (snd (funcName fd)))
prooffiles)
dcltheofuncs
where
funDeclsWith pred = filter (pred . snd . funcName)
------------------------------------------------------------------------
########################################################################
# Makefile for contract wrapping tool
# (only used for manual installation since it will be automatically
# installed via the ../Makefile of currypp)
#
# This makefile is only used if the tool should be installed manually
# (for testing). Usually, it will be automatically with currypp
# via the ../Makefile (of currypp).
########################################################################
TOOLDIR = ../..
# for determinism analysis and for module ContractUsage:
PPPATH = $(TOOLDIR)/analysis:$(TOOLDIR)/CASS:$(TOOLDIR)/currycheck
# additional imports for determinism analysis, for module ContractUsage,
# and rewriting libraries for contract optimization:
REWRITINGDIR = $(CURDIR)/../../verification
PPPATH = $(TOOLDIR)/analysis:$(TOOLDIR)/CASS:$(TOOLDIR)/currycheck:$(REWRITINGDIR)
.PHONY: all
all: cwrapper
# generate saved state for contract wrapper:
cwrapper: TransContracts.curry SimplifyPostConds.curry
pakcs :set path $(PPPATH) :l TransContracts :save :q && mv TransContracts cwrapper
curry :set path $(PPPATH) :l TransContracts :save :q && mv TransContracts cwrapper
.PHONY: clean
clean:
......
......@@ -4,7 +4,7 @@ assertion checking from pre/postconditions and specifications.
Sergio Antoy, Michael Hanus
May 3, 2016
August 12, 2016
------------------------------------------------------------------------
How to use the tool:
......@@ -13,7 +13,7 @@ The tool is integrated into the Curry Preprocessor (currypp). Hence,
to activate the transformation, put the following line into the
beginning of your Curry module:
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts --optF=-e #-}
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}
If postconditions or specifications are nondeterministic,
it is better that they will be evaluated via encapsulated search
......
......@@ -11,16 +11,11 @@
--- > Declarative Languages (PADL 2012), pp. 33-47, Springer LNCS 7149, 2012
---
--- @author Michael Hanus
--- @version May 2016
--- @version August 2016
------------------------------------------------------------------------
module TransContracts(main,transContracts) where
-- to use the determinism analysis:
import AnalysisServer (analyzeGeneric)
import GenericProgInfo (ProgInfo, lookupProgInfo)
import Deterministic (Deterministic(..), nondetAnalysis)
import AbstractCurry.Types
import AbstractCurry.Files
import AbstractCurry.Pretty
......@@ -31,17 +26,25 @@ import Char
import ContractUsage
import Directory
import Distribution
import FilePath (takeDirectory)
import FilePath (takeDirectory)
import List
import Maybe(fromJust)
import SimplifyPostConds
import Maybe (fromJust)
import System
-- in order to use the determinism analysis:
import AnalysisServer (analyzeGeneric)
import GenericProgInfo (ProgInfo, lookupProgInfo)
import Deterministic (Deterministic(..), nondetAnalysis)
import SimplifyPostConds
import TheoremUsage
------------------------------------------------------------------------
banner :: String
banner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText = "Contract Transformation Tool (Version of 01/06/16)"
bannerText = "Contract Transformation Tool (Version of 12/08/16)"
bannerLine = take (length bannerText) (repeat '=')
------------------------------------------------------------------------
......@@ -49,7 +52,7 @@ banner = unlines [bannerLine,bannerText,bannerLine]
--- The Curry program must be read with `readCurry` (and not
--- `readUntypedCurry`) in order to correctly process arities
--- based on function types!
--- The result is Nothing if no transformation was applied or Just the
--- The result is `Nothing` if no transformation was applied or `Just` the
--- transformed program.
transContracts :: Int -> [String] -> String -> CurryProg -> IO (Maybe CurryProg)
transContracts verb moreopts srcprog inputProg = do
......@@ -161,21 +164,16 @@ transformCProg verb opts srctxt orgprog outmodname = do
map (\ ((mn,fn),err) -> fn ++ " (module " ++ mn ++ "): " ++ err)
usageerrors)
error "Contract transformation aborted"
let funposs = linesOfFDecls srctxt prog
fdecls = functions prog
funspecs = getFunDeclsWith isSpecName prog
specnames = map (fromSpecName . snd . funcName) funspecs
preconds = getFunDeclsWith isPreCondName prog
prenames = map (fromPreCondName . snd . funcName) preconds
opostconds= getFunDeclsWith isPostCondName prog
dtheofuncs= getFunDeclsWith isTheoremName prog -- declared theorems
let funposs = linesOfFDecls srctxt prog
fdecls = functions prog
funspecs = getFunDeclsWith isSpecName prog
specnames = map (fromSpecName . snd . funcName) funspecs
preconds = getFunDeclsWith isPreCondName prog
prenames = map (fromPreCondName . snd . funcName) preconds
opostconds = getFunDeclsWith isPostCondName prog
-- filter theorems which have a proof file:
prooffiles <- getProofFiles (takeDirectory (modNameToPath (progName prog)))
let theofuncs = filter (\fd -> existsProofFor
(fromTheoremName (snd (funcName fd)))
prooffiles)
dtheofuncs
postconds <- simplifyPostConditionWithTheorems verb theofuncs opostconds
theofuncs <- getTheoremFunctions prog
postconds <- simplifyPostConditionsWithTheorems verb theofuncs opostconds
let postnames = map (fromPostCondName . snd . funcName) postconds
checkfuns = union specnames (union prenames postnames)
if null checkfuns
......
......@@ -141,10 +141,11 @@ usageText = unlines $
, "<OrgFileName> : name of original program source file"
, "<InputFilePath> : name of the actual input file"
, "<OutputFilePath>: name of the file where output should be written\n"
, "where <options> contain preprocessing targets\n"
, "where <options> contain preprocessing targets"
, "(if no target is given, 'foreigncode defaultrules contracts' are used)\n"
, "foreigncode : translate foreign code pieces in the source file"
, "--model:<ERD_Name>_UniSQLCode.info :"
, " data model to translate embedded sql requests."
, " data model to translate embedded SQL statements"
, "seqrules : implement sequential rule selection strategy"
, "defaultrules : implement default rules"
, "contracts : implement dynamic contract checking"
......@@ -155,16 +156,16 @@ usageText = unlines $
, "-v<n> : show more information about the preprocessor:"
, " <n>=0 : quiet"
, " <n>=1 : show some information (default)"
, " <n>=2 : show version and timing"
, " <n>=3 : show used file names"
, " <n>=4 : show transformed Curry program"
, " <n>=2 : show more information, e.g., version, timing"
, " <n>=3 : show much more information, e.g., used file names"
, " <n>=4 : show also transformed Curry program"
, "-h|-? : show help message and quit"
, ""
, "For 'defaultrules':"
, "For target 'defaultrules':"
, "specscheme : default translation scheme (as in PADL'16 paper)"
, "nodupscheme : translation scheme without checking conditions twice"
, ""
, "For 'contracts':"
, "For target 'contracts':"
, "-e : encapsulate nondeterminism of assertions"
, "-t : assert contracts only to top-level (not recursive) calls"
]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment