Commit 1965d1d7 authored by Michael Hanus's avatar Michael Hanus
Browse files

Some improvements to enable verification of complete prelude.

parent b80ccc2a
nonfailing
==========
Notes:
------
- Contracts and nonfail specifications can also be stored in a separate
file. When checking a module `m`, if there is a Curry module `m_SPEC`
in the load path, the contents of `m_SPEC` is added to `m` before
it is checked.
- nonfail specifications for operators can be also specified by
operations named by `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, the nonfail specification for `&>` can be named
`op_x263E'nonfail`.
-- To detect the non-failure of the following operation,
-- reasoning over integers is required:
abs :: Int -> Int
abs x | x>=0 = x
| x<0 = 0 - x
-- It must be proved that the guards are complete since the definition
-- above is translated into the following definition:
absif x = if x>=0 then x
else if x<0 then (0 - x)
else failed
faci n = if n==0 then 1 else n * faci (n-1)
facg'nonfail n = n>=0
facg n | n==0 = 1
| n>0 = n * facg (n-1)
\ No newline at end of file
--- Accumulates a non-empty list from right to left:
foldr1'nonfail :: (a -> a -> a) -> [a] -> Bool
foldr1'nonfail _ xs = not (null xs)
--- Accumulates a non-empty list from right to left:
foldr1 :: (a -> a -> a) -> [a] -> a
foldr1 _ [x] = x
foldr1 f (x:xs@(_:_)) = f x (foldr1 f xs)
--- Accumulates all list elements by applying a binary operator from
--- left to right.
foldl :: (a -> b -> a) -> a -> [b] -> a
foldl _ z [] = z
foldl f z (x:xs) = foldl f (f z x) xs
--- Accumulates a non-empty list from left to right.
foldl1'nonfail :: (a -> a -> a) -> [a] -> Bool
foldl1'nonfail _ xs = not (null xs)
foldl1 :: (a -> a -> a) -> [a] -> a
foldl1 f (x:xs) = foldl f x xs
--- Computes the first element of a list.
head'nonfail xs = not (null xs)
head :: [a] -> a
head (x:_) = x
main = head "12"
--- Returns the last element of a non-empty list.
last'nonfail xs = not (null xs)
last :: [a] -> a
last [x] = x
last (_ : xs@(_:_)) = last xs
--- Returns the input list with the last element removed.
init'nonfail xs = not (null xs)
init :: [a] -> [a]
init [_] = []
init (x:xs@(_:_)) = x : init xs
--- Is a list empty?
null :: [_] -> Bool
null [] = True
null (_:_) = False
lastOr :: [a] -> a -> a
lastOr xs x = if null xs then x
else last xs
--- Accumulates a non-empty list from right to left:
foldr1'nonfail :: (a -> a -> a) -> [a] -> Bool
foldr1'nonfail _ xs = not (null xs)
--- Accumulates a non-empty list from right to left:
foldr1 :: (a -> a -> a) -> [a] -> a
foldr1 _ [x] = x
foldr1 f (x:xs@(_:_)) = f x (foldr1 f xs)
unwords :: [String] -> String
unwords ws = if ws==[] then []
else foldr1 (\w s -> w ++ ' ':s) ws
#!/bin/sh
# Script to test the set of current examples
VERBOSE=no
if [ "$1" = "-v" ] ; then
VERBOSE=yes
fi
# Tool options:
OPTS=
/bin/rm -rf .curry
ECODE=0
FAILEDTESTS=
for p in *.curry ; do
if [ $VERBOSE = yes ] ; then
curry-nonfail $OPTS $p | tee test.out
else
curry-nonfail $OPTS $p > test.out
fi
if [ "`tail -1 test.out`" != "NON-FAILURE VERIFICATION SUCCESSFUL!" ] ; then
echo "$p: FULL VERIFICATION FAILED!"
FAILEDTESTS="$FAILEDTESTS $p"
ECODE=1
fi
rm test.out
done
if [ $ECODE -gt 0 ] ; then
echo "FAILURES OCCCURRED IN SOME TESTS:$FAILEDTESTS"
exit $ECODE
elif [ $VERBOSE = yes ] ; then
echo "All tests successfully executed!"
fi
......@@ -4,6 +4,9 @@
; For polymorphic types:
(declare-sort TVar)
; Pair type:
(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
; For functional types:
(declare-datatypes (T1 T2) ((Func (mk-func (argument T1) (result T2)))))
......@@ -17,5 +17,14 @@
"pakcs": ">= 1.14.0, < 2.0.0",
"kics2": ">= 0.5.0, < 2.0.0"
},
"configModule": "PackageConfig"
"configModule": "PackageConfig",
"executable": {
"name": "curry-nonfail",
"main": "Main"
},
"testsuite": {
"src-dir": "examples",
"script": "test.sh",
"options": "-v"
}
}
......@@ -99,6 +99,8 @@ type2SMTExp (TCons (mn,tc) targs)
| mn=="Prelude" && length targs == 0 = BTerm tc []
| mn=="Prelude" && tc == "[]" && length targs == 1
= BTerm "List" [type2SMTExp (head targs)]
| mn=="Prelude" && tc == "(,)" && length targs == 2
= BTerm "Pair" (map type2SMTExp targs)
| otherwise = BTerm (mn ++ "." ++ tc) [] -- TODO: complete
--type2SMTExp (ForallType _ _) = error "type2SMT: cannot translate ForallType"
......
......@@ -3,9 +3,10 @@ module Main where
import Directory ( doesFileExist )
import FilePath ( (</>) )
import IOExts
import List ( (\\), elemIndex, find, isSuffixOf
import List ( (\\), elemIndex, find, isPrefixOf, isSuffixOf
, maximum, minimum, splitOn )
import Maybe ( catMaybes )
import ReadNumeric ( readHex )
import State
import System
......@@ -62,7 +63,7 @@ main = do
analyzeNonFailing :: Options -> String -> IO ()
analyzeNonFailing opts modname = do
prog <- readTypedFlatCurry modname
prog <- readTypedFlatCurryWithSpec modname
siblingconsinfo <- loadAnalysisWithImports siblingCons prog
printWhenAll opts $ unlines $
["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg prog), line]
......@@ -159,6 +160,7 @@ verifyNonFailing :: Options -> ProgInfo [(QName,Int)] -> TransInfo -> TAProg
-> VState -> IO VState
verifyNonFailing opts siblingconsinfo ti prog stats = do
vstref <- newIORef stats
modifyIORef vstref (addProgToState prog)
mapIO_ (proveNonFailingFunc opts siblingconsinfo ti vstref) (progFuncs prog)
readIORef vstref
......@@ -225,12 +227,13 @@ proveNonFailingRule opts siblingconsinfo ti (mn,fn)
proveNonFailExp pts e
maybe
(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 = (freshvar, annExpr e) : varTypes pts1 }
, varTypes = freshtypedvar : varTypes pts1 }
misscons = missingConsInBranch siblingconsinfo brs
in do mapIO_ (verifyMissingCons pts2 freshvar (annExpr e)) misscons
mapIO_ (proveNonFailBranch pts2 freshvar) brs
in do mapIO_ (verifyMissingCons pts2 freshtypedvar) misscons
mapIO_ (proveNonFailBranch pts2 freshtypedvar) brs
)
(\ (fe,te) ->
let (be,pts1) = pred2bool e pts
......@@ -248,11 +251,11 @@ proveNonFailingRule opts siblingconsinfo ti (mn,fn)
ATyped _ e _ -> proveNonFailExp pts e
_ -> done
verifyMissingCons pts dvar dvartype (cons,_) = do
verifyMissingCons pts typedvar (cons,_) = do
printWhenIntermediate opts $
fn ++ ": checking missing constructor case '" ++ snd cons ++ "'"
valid <- checkImplicationWithSMT opts vstref (varTypes pts) (preCond pts)
bTrue (bNot (constructorTest cons dvar dvartype))
bTrue (bNot (constructorTest cons typedvar))
unless (valid == Just True) $ do
let reason = if valid == Nothing
then "due to SMT error"
......@@ -262,15 +265,17 @@ proveNonFailingRule opts siblingconsinfo ti (mn,fn)
putStrLn $ "POSSIBLY FAILING BRANCH in function '" ++ fn ++
"' with constructor " ++ snd cons
proveNonFailBranch pts dvar branch = do
proveNonFailBranch pts (var,vartype) branch = do
let (ABranch p e, pts1) = renamePatternVars pts branch
let npts = pts1 { preCond = Conj [preCond pts1, bEquVar dvar (pat2bool p)] }
-- set pattern type correctly (important for [] pattern)
bpat = pat2bool (setAnnPattern vartype p)
npts = pts1 { preCond = Conj [preCond pts1, bEquVar var bpat] }
proveNonFailExp npts e
--- Translates a constructor name and a variable into a SMT formula
--- implementing a test for this constructor.
constructorTest :: QName -> Int -> TypeExpr -> BoolExp
constructorTest qn var vartype
constructorTest :: QName -> (Int,TypeExpr) -> BoolExp
constructorTest qn (var,vartype)
| qn == pre "[]"
= bEquVar var (BTerm "as" [BTerm "nil" [], type2SMTExp vartype])
| qn `elem` [pre "[]", pre "True", pre "False"]
......@@ -364,25 +369,47 @@ exp2bool demanded ti (resvar,exp) = case exp of
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 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 (returnS bTrue)
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 -> funcName fd == qnpre) (nfConds ti))
(find (\fd -> transSpecialName (funcName fd) == qnpre) (nfConds ti))
where
qnpre = addSuffix qf "'nonfail"
predefs qn | qn `elem` [pre "failed", pre "=:="]
= 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.
......@@ -450,9 +477,10 @@ pred2bool exp = case exp of
= pred2bool (head args) `bindS` \barg -> returnS (Not barg)
| qf == pre "null" && ar == 1
= let arg = head args
argtype = annExpr arg
in pred2bool (head args) `bindS` \barg ->
returnS (bEqu barg (BTerm "as" [BTerm "nil" [], type2SMTExp argtype]))
in pred2bool arg `bindS` \barg ->
getS `bindS` \tstate ->
returnS (bEqu barg (BTerm "as" [BTerm "nil" [],
type2SMTExp (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
......@@ -460,10 +488,23 @@ pred2bool exp = case exp of
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)
| 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
......
solve'nonfail :: Bool -> Bool
solve'nonfail x = x
doSolve'nonfail :: Bool -> Bool
doSolve'nonfail x = x
head'nonfail :: [a] -> Bool
head'nonfail xs = not (null xs)
tail'nonfail :: [a] -> Bool
tail'nonfail xs = not (null xs)
foldr1'nonfail :: (a -> a -> a) -> [a] -> Bool
foldr1'nonfail _ xs = not (null xs)
foldl1'nonfail :: (a -> a -> a) -> [a] -> Bool
foldl1'nonfail _ xs = not (null xs)
anyOf'nonfail :: [a] -> Bool
anyOf'nonfail xs = not (null xs)
-- Non-failure condition for `&>`.
op_x263E'nonfail :: Bool -> a -> Bool
op_x263E'nonfail x _ = x
-- Non-failure condition for `!!`.
op_x2121'nonfail :: [a] -> Int -> Bool
op_x2121'nonfail xs n = n >= 0 && length (take (n+1) xs) == n+1
---------------------------------------------------------------------------
-- External operations:
-- Non-failure condition for `=:=`.
op_x3D3A3D'nonfail :: a -> a -> Bool
op_x3D3A3D'nonfail _ _ = False
-- Non-failure condition for `=:<=`.
op_x3D3A3C3D'nonfail :: a -> a -> Bool
op_x3D3A3C3D'nonfail _ _ = False
-- Non-failure condition for `=:<<=`.
op_x3D3A3C3C3D'nonfail :: a -> a -> Bool
op_x3D3A3C3C3D'nonfail _ _ = False
-- Non-failure condition for `&`.
op_x26'nonfail :: Bool -> Bool -> Bool
op_x26'nonfail x y = x && y
chr'nonfail :: Int -> Bool
chr'nonfail n = n>=0
{-
div'nonfail :: Int -> Int -> Bool
div'nonfail x y = y/=0
mod'nonfail :: Int -> Int -> Bool
mod'nonfail x y = y/=0
divMod'nonfail :: Int -> Int -> Bool
divMod'nonfail x y = y/=0
quot'nonfail :: Int -> Int -> Bool
quot'nonfail x y = y/=0
rem'nonfail :: Int -> Int -> Bool
rem'nonfail x y = y/=0
quotRem'nonfail :: Int -> Int -> Bool
quotRem'nonfail x y = y/=0
-}
......@@ -7,9 +7,10 @@
module TypedFlatCurryGoodies where
import FlatCurry.Files
import Directory ( doesFileExist )
import Distribution ( lookupModuleSourceInLoadPath )
import IOExts
import List ( find, nub )
import List ( find, nub, union )
import Maybe ( fromJust )
import Pretty ( pPrint )
import System ( exitWith )
......@@ -20,6 +21,7 @@ import FlatCurry.Annotated.Goodies
import FlatCurry.Annotated.Pretty ( ppExp )
import FlatCurry.Annotated.Types
import FlatCurry.Annotated.TypeInference ( inferProg )
import FlatCurry.Files
import VerificationState
......@@ -32,7 +34,7 @@ type TABranchExpr = ABranchExpr TypeExpr
type TAPattern = APattern TypeExpr
----------------------------------------------------------------------------
--- Reads a type FlatCurry program or exit with a failure message
--- Reads a typed FlatCurry program or exits with a failure message
--- in case of some typing error.
readTypedFlatCurry :: String -> IO TAProg
readTypedFlatCurry mname = do
......@@ -42,17 +44,36 @@ readTypedFlatCurry mname = do
exitWith 1)
return
--- Reads a typed FlatCurry program together with a possible `_SPEC` program
--- (containing further contracts) or exits with a failure message
--- in case of some typing error.
readTypedFlatCurryWithSpec :: String -> IO TAProg
readTypedFlatCurryWithSpec mname = do
prog <- readTypedFlatCurry mname
fspec <- lookupModuleSourceInLoadPath specName
if fspec == Nothing
then return prog
else do specprog <- readTypedFlatCurry specName
return (unionTAProg prog (rnmProg mname specprog))
where
specName = mname ++ "_SPEC"
--- Returns the union of two typed FlatCurry programs.
unionTAProg :: TAProg -> TAProg -> TAProg
unionTAProg (AProg name imps1 types1 funcs1 ops1)
(AProg _ imps2 types2 funcs2 ops2) =
AProg name (union imps1 imps2) (types1++types2) (funcs1++funcs2) (ops1++ops2)
----------------------------------------------------------------------------
--- Extract all user-defined typed FlatCurry functions that might be called
--- by a given list of functions.
getAllFunctions :: IORef VState -> [TAFuncDecl] -> [QName]
-> IO [TAFuncDecl]
getAllFunctions vstref currfuns newfuns = do
getAllFunctions :: IORef VState -> [TAFuncDecl] -> [QName] -> IO [TAFuncDecl]
getAllFunctions vstref currfuncs newfuns = do
currmods <- readIORef vstref >>= return . currTAProgs
getAllFunctions' currfuns currmods newfuns
getAllFuncs currmods newfuns
where
getAllFunctions' currfuncs _ [] = return (reverse currfuncs)
getAllFunctions' currfuncs currmods (newfun:newfuncs)
getAllFuncs _ [] = return (reverse currfuncs)
getAllFuncs currmods (newfun:newfuncs)
| newfun `elem` standardConstructors ++ map funcName currfuncs
|| isPrimOp newfun
= getAllFunctions vstref currfuncs newfuncs
......@@ -106,6 +127,11 @@ ndExpr = trExpr (\_ _ -> False)
ppTAExpr :: TAExpr -> String
ppTAExpr e = pPrint (ppExp e)
--- Sets the top annotation of a pattern.
setAnnPattern :: TypeExpr -> TAPattern -> TAPattern
setAnnPattern ann (ALPattern _ lit) = ALPattern ann lit
setAnnPattern ann (APattern _ aqn vars) = APattern ann aqn vars
----------------------------------------------------------------------------
--- Is a qualified FlatCurry name primitive?
isPrimOp :: QName -> Bool
......@@ -129,7 +155,8 @@ preludePrimOps =
,("not","not")
,("&&","and")
,("||","or")
,("apply","") -- SMT name not used
,("otherwise","true")
,("apply","apply") -- TODO...
]
--- Primitive constructors from the prelude and their SMT names.
......@@ -139,6 +166,7 @@ primCons =
,("False","false")
,("[]","nil")
,(":","insert")
,("(,)","mk-pair")
]
-- Some standard constructors from the prelude.
......
Supports Markdown
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