Tool renamed, verification of user-defined data types added

README.md

-nonfailing: A tool for non-failing analysis
-===========================================
+failfree: A tool for verifying fail-free Curry programs
+=======================================================
 
 Objective: verify that all operations are non-failing, i.e.,
 does not result in a failure, if they are called with
@@ -92,5 +92,6 @@ Notes:
   For instance, the nonfail specification for `&>` can be named
   `op_x263E'nonfail`.
 
+- Operations defining contracts and properties are not verified.
 
 ---------------------------------------------------------------------------

examples/Peano.curry

+--- An example for verification with user-defined data types.
+
+--- Natural numbers defined in Peano representation.
+data Nat = Z | S Nat
+
+--- Transforms a natural number into a standard integer.
+fromNat :: Nat -> Int
+fromNat Z     = 0
+fromNat (S n) = 1 + fromNat n
+
+--- Addition on natural numbers.
+add :: Nat -> Nat -> Nat
+add Z     n = n
+add (S m) n = S(add m n)
+
+--- The predecessor operation is partially defined.
+pred :: Nat -> Nat
+pred (S m) = m
+
+pred'nonfail x = x/=Z
+
+main = pred (S Z)

examples/UserList.curry

+--- Test for verification with user-defined polymorphic lists.
+
+data MyList a = Nil | Cons a (MyList a)
+
+--- Defining head on these lists:
+head :: MyList a -> a
+head (Cons x _) = x
+
+head'nonfail xs = xs/=Nil
+
+main = head (Cons 1 Nil)

examples/test.sh

@@ -6,6 +6,8 @@ if [ "$1" = "-v" ] ; then
   VERBOSE=yes
 fi
 
+# Tool executable:
+TOOLBIN=curry-failfree
 # Tool options:
 OPTS=--contract
 
@@ -15,9 +17,9 @@ FAILEDTESTS=
 
 for p in *.curry ; do
   if [ $VERBOSE = yes ] ; then
-    curry-nonfail $OPTS $p | tee test.out
+    $TOOLBIN $OPTS $p | tee test.out
   else
-    curry-nonfail $OPTS $p > test.out
+    $TOOLBIN $OPTS $p > test.out
   fi
   if [ "`tail -1 test.out`" != "NON-FAILURE VERIFICATION SUCCESSFUL!" ] ; then
     echo "$p: FULL VERIFICATION FAILED!"

include/Integer_SPEC.curry

+------------------------------------------------------------------------------
+-- Non-failure conditions for operations of module Integer.
+
+-- Non-failure condition for `^`.
+op_x5E'nonfail :: Int -> Int -> Bool
+op_x5E'nonfail _ b = b >= 0
+
+pow'nonfail :: Int -> Int -> Bool
+pow'nonfail _ b = b >= 0
+
+ilog'nonfail :: Int -> Bool
+ilog'nonfail n = n > 0
+
+isqrt'nonfail :: Int -> Bool
+isqrt'nonfail n = n >= 0
+
+factorial'nonfail :: Int -> Bool
+factorial'nonfail n = n >= 0
+
+factorial'post :: Int -> Int -> Bool
+factorial'post _ f = f > 0
+
+binomial'nonfail :: Int -> Int -> Bool
+binomial'nonfail n m = m>0 && n>=m
+
+maxlist'nonfail :: [a] -> Bool
+maxlist'nonfail xs = not (null xs)
+
+minlist'nonfail :: [a] -> Bool
+minlist'nonfail xs = not (null xs)
+
+bitTrunc'nonfail :: Int -> Int -> Bool
+bitTrunc'nonfail n _ = n >= 0
+
+------------------------------------------------------------------------------
+

include/Nat_SPEC.curry

+------------------------------------------------------------------------------
+-- Non-failure conditions for operations of module Nat.
+
+toNat'nonfail :: Int -> Bool
+toNat'nonfail n = n >= 0
+
+sub'nonfail :: Nat -> Nat -> Bool
+sub'nonfail _ _ = False
+
+------------------------------------------------------------------------------
+

package.json

 {
-    "name": "nonfailing",
+    "name": "failfree",
     "version": "0.0.1",
     "author": "Michael Hanus <mh@informatik.uni-kiel.de>",
-    "synopsis": "A tool to analyze the non-failing behavior of Curry programs",
+    "synopsis": "A tool to verify whether a Curry program executes without failures",
     "category": [ "Programming", "Analysis", "Verification" ],
     "license": "BSD-3-Clause",
     "licenseFile": "LICENSE",
@@ -19,7 +19,7 @@
     },
     "configModule": "PackageConfig",
     "executable": {
-        "name"   : "curry-nonfail",
+        "name"   : "curry-failfree",
         "main"   : "Main",
         "options": { "kics2" : ":set rts -T" }
     },

src/BoolExp.curry

@@ -79,7 +79,7 @@ simpBE (Disj (bs1 ++ [Disj bs2] ++ bs3)) = simpBE (Disj (bs1 ++ bs2 ++ bs3))
 simpBE (Disj bs) = if null bs then bFalse else Disj (map simpBE bs)
 simpBE (Not (Not b)) = b
 simpBE (Binding _ [] e) = e
-simpBE (BTerm s args) = BTerm s (map simpBE args)
+simpBE (BTerm f args) = BTerm f (map simpBE args)
 simpBE'default be = be
 
 ---------------------------------------------------------------------------
@@ -93,6 +93,7 @@ smtBE :: BoolExp -> String
 smtBE (BVar i) = 'x' : show i
 smtBE (BTerm f args)
   | f == "="  = asLisp ["=", smtBE (head args), smtBE (args!!1)]
+  | f == "/=" = smtBE (Not (BTerm "=" args))
   | f == "let" = asLisp ["let", asLisp (map (\ (BTerm _ [v,e]) -> asLisp [smtBE v, smtBE e]) (tail args)), smtBE (head args)]
   | otherwise = if null args then f
                              else asLisp $ f : map smtBE args
@@ -118,6 +119,7 @@ prettyBE :: BoolExp -> String
 prettyBE (BVar i) = 'x' : show i
 prettyBE (BTerm f args)
   | f == "="  = prettyBE (head args) ++ " = " ++ prettyBE (args!!1)
+  | f == "/=" = prettyBE (Not (BTerm "=" args))
   | null args = f
   | not (isAlpha (head f)) && length args == 2
   = prettyBE (args!!0) ++ f ++ prettyBE (args!!1)

src/Curry2SMT.curry

@@ -2,13 +2,14 @@
 --- A tool to translate FlatCurry operations into SMT assertions.
 ---
 --- @author  Michael Hanus
---- @version September 2017
+--- @version April 2018
 ---------------------------------------------------------------------------
 
 module Curry2SMT where
 
 import IOExts
-import Maybe        ( fromMaybe )
+import List         ( isPrefixOf )
+import Maybe        ( fromJust, fromMaybe )
 
 -- Imports from dependencies:
 import FlatCurry.Annotated.Goodies ( argTypes, resultType )
@@ -31,8 +32,8 @@ funcs2SMT vstref qns = do
 ftype2SMT :: TAFuncDecl -> String
 ftype2SMT (AFunc qn _ _ texp _) =
   asLisp ["declare-fun", transOpName qn,
-          asLisp (map (smtBE . type2SMTExp) (argTypes texp)),
-          smtBE (type2SMTExp (resultType texp))]
+          asLisp (map (smtBE . polytype2SMTExp) (argTypes texp)),
+          smtBE (polytype2SMTExp (resultType texp))]
 
 -- Axiomatize a function rule as an SMT assertion.
 fdecl2SMT :: TAFuncDecl -> String
@@ -43,7 +44,7 @@ fdecl2SMT (AFunc qn _ _ _ rule) = unlines
   rule2SMT (AExternal _ s) =
     assertSMT $ bEqu (BTerm (transOpName qn) []) (BTerm ("External:" ++ s) [])
   rule2SMT (ARule _ vs exp) =
-    assertSMT $ forallBinding (map (\ (v,t) -> (v, type2SMTExp t)) vs)
+    assertSMT $ forallBinding (map (\ (v,t) -> (v, polytype2SMTExp t)) vs)
                               (if ndExpr exp
                                  then exp2SMT (Just lhs) exp
                                  else bEqu lhs (exp2SMT Nothing exp))
@@ -65,7 +66,7 @@ exp2SMT lhs exp = case exp of
   ALet   _ bs e -> letBinding (map (\ ((v,_),be) -> (v, exp2SMT Nothing be)) bs)
                               (exp2SMT lhs e)
   ATyped _ e _ -> exp2SMT lhs e
-  AFree  _ fvs e -> forallBinding (map (\ (v,t) -> (v, type2SMTExp t)) fvs)
+  AFree  _ fvs e -> forallBinding (map (\ (v,t) -> (v, polytype2SMTExp t)) fvs)
                                   (exp2SMT lhs e)
   AOr    _ e1 e2 -> Disj [exp2SMT lhs e1, exp2SMT lhs e2]
  where
@@ -92,39 +93,96 @@ patternTest (APattern ty (qf,_) _) be = constructorTest qf be ty
 --- Translates a constructor name and a BoolExp into a SMT formula
 --- implementing a test on the BoolExp for this constructor.
 constructorTest :: QName -> BoolExp -> TypeExpr -> BoolExp
-constructorTest qn  be vartype
+constructorTest qn be vartype
   | qn == pre "[]"
-  = bEqu be (BTerm "as" [BTerm "nil" [], type2SMTExp vartype])
+  = bEqu be (BTerm "as" [BTerm "nil" [], polytype2SMTExp vartype])
   | qn `elem` map pre ["[]","True","False","LT","EQ","GT","Nothing"]
   = bEqu be (BTerm (transOpName qn) [])
   | qn `elem` map pre ["Just","Left","Right"]
   = BTerm ("is-" ++ snd qn) [be]
-  | otherwise = error $ "Test for constructor " ++ showQName qn ++
-                        " not yet supported!"
+  | otherwise
+  = BTerm ("is-" ++ transOpName qn) [be]
 
+--- Computes the SMT selector names for a given constructor.
 selectors :: QName -> [String]
-selectors qf | qf == ("Prelude",":") = ["head","tail"]
-             | qf == ("Prelude","Left") = ["left"]
+selectors qf | qf == ("Prelude",":")     = ["head","tail"]
+             | qf == ("Prelude","Left")  = ["left"]
              | qf == ("Prelude","Right") = ["right"]
-             | qf == ("Prelude","Just") = ["just"]
-             | otherwise = error $ "Unknown selectors: " ++ snd qf
+             | qf == ("Prelude","Just")  = ["just"]
+             | otherwise = map (genSelName qf) [1..]
+
+--- Translates a FlatCurry type expression into a corresponding
+--- SMT expression.
+--- Polymorphic type variables are translated into the sort `TVar`.
+--- The types `TVar` and `Func` are defined in the SMT prelude
+--- which is always loaded.
+polytype2SMTExp :: TypeExpr -> BoolExp
+polytype2SMTExp = type2SMTExp [] False
 
 --- Translates a FlatCurry type expression into a corresponding
---- SMT expression. The types `TVar` and `Func` are defined
---- in the SMT prelude which is always loaded.
-type2SMTExp :: TypeExpr -> BoolExp
-type2SMTExp (TVar _) = BTerm "TVar" []
-type2SMTExp (FuncType dom ran) = BTerm "Func" (map type2SMTExp [dom,ran])
-type2SMTExp (TCons (mn,tc) targs)
-  | mn=="Prelude" && tc == "Char"      = BTerm "Int" []
+--- SMT expression. If the first argument is null, then type variables are
+--- translated into the sort `TVar`, otherwise we are in the translation
+--- of the types of selector operations and the first argument
+--- contains the currently defined data types. In this case, type variables
+--- are translated into  `Ti`, but further nesting of the defined data types
+--- are not allowed (since this is not supported by SMT).
+--- The types `TVar` and `Func` are defined in the SMT prelude
+--- which is always loaded.
+type2SMTExp :: [QName] -> Bool -> TypeExpr -> BoolExp
+type2SMTExp tdcl _  (TVar i) =
+  BTerm (if null tdcl then "TVar" else 'T':show i) []
+type2SMTExp tdcl _ (FuncType dom ran) =
+  BTerm "Func" (map (type2SMTExp tdcl True) [dom,ran])
+type2SMTExp tdcl nested (TCons qc@(mn,tc) targs)
+  | mn=="Prelude" && tc == "Char" -- Char is represented as Int:
+  = BTerm "Int" []
   | mn=="Prelude" && tc == "[]" && length targs == 1
-  = BTerm "List" [type2SMTExp (head targs)]
+  = BTerm "List" argtypes
   | mn=="Prelude" && tc == "(,)" && length targs == 2
-  = BTerm "Pair" (map type2SMTExp targs)
-  | mn=="Prelude" = BTerm tc (map type2SMTExp targs)
-  | otherwise = BTerm (mn ++ "." ++ tc) [] -- TODO: complete
+  = BTerm "Pair" argtypes
+  | mn=="Prelude" = BTerm tc argtypes
+  | null tdcl
+  = BTerm (tcons2SMT qc) argtypes
+  | otherwise -- we are in the selector definition of a datatype
+  = if qc `elem` tdcl
+      then if nested
+             then error $ "Type '" ++ showQName qc ++
+                          "': nested recursive types not supported by SMT!"
+             else BTerm (tcons2SMT qc) [] -- TODO: check whether arguments
+                            -- are directly recursive, otherwise emit error
+      else BTerm (tcons2SMT (mn,tc)) argtypes
+ where
+  argtypes = map (type2SMTExp tdcl True) targs
 --type2SMTExp (ForallType _ _) = error "type2SMT: cannot translate ForallType"
 
+--- Translates a FlatCurry type constructor name into SMT.
+tcons2SMT :: QName -> String
+tcons2SMT (mn,tc) = mn ++ "_" ++ tc
+
+----------------------------------------------------------------------------
+--- Translates a type declaration into an SMT datatype declaration.
+tdecl2SMT :: TypeDecl -> String
+tdecl2SMT (TypeSyn tc _ _ _) =
+  error $ "Cannot translate type synonym '" ++ showQName tc ++ "' into SMT!"
+tdecl2SMT (Type tc _ tvars consdecls) =
+  "(declare-datatypes (" ++ unwords (map (\v -> 'T':show v) tvars) ++ ") " ++
+  "((" ++ unwords (tcons2SMT tc : map tconsdecl consdecls) ++ ")))"
+ where
+  tconsdecl (Cons qn _ _ texps) =
+    let cname = transOpName qn
+    in if null texps
+         then cname
+         else "(" ++ unwords (cname : map (texp2sel qn) (zip [1..] texps))
+                  ++ ")"
+
+  texp2sel cname (i,texp) =
+    "(" ++ genSelName cname i ++ " " ++
+      smtBE (type2SMTExp [tc] False texp) ++ ")"
+
+--- Generates the name of the i-th selector for a given constructor.
+genSelName :: QName -> Int -> String
+genSelName qc i = "sel" ++ show i ++ transOpName qc
+
 ----------------------------------------------------------------------------
 
 --- Translates a pattern into an SMT expression.
@@ -132,7 +190,7 @@ pat2bool :: TAPattern -> BoolExp
 pat2bool (ALPattern _ l)    = lit2bool l
 pat2bool (APattern ty (qf,_) ps)
   | qf == pre "[]" && null ps
-  = BTerm "as" [BTerm "nil" [], type2SMTExp ty]
+  = BTerm "as" [BTerm "nil" [], polytype2SMTExp ty]
   | otherwise
   = BTerm (transOpName qf) (map (BVar . fst) ps)
 
@@ -153,9 +211,13 @@ transOpName (mn,fn)
 --- Translates an SMT string into qualified FlatCurry name.
 --- Returns Nothing if it was not a qualified name.
 untransOpName :: String -> Maybe QName
-untransOpName s = let (mn,ufn) = break (=='_') s in
- if null ufn
-   then Nothing
-   else Just (mn, tail ufn)
+untransOpName s
+ | "is-" `isPrefixOf` s
+ = Nothing -- selectors are not a qualified name
+ | otherwise
+ = let (mn,ufn) = break (=='_') s
+   in if null ufn
+        then Nothing
+        else Just (mn, tail ufn)
 
 ----------------------------------------------------------------------------

src/Main.curry

@@ -11,7 +11,7 @@ import Directory    ( doesFileExist )
 import FilePath     ( (</>) )
 import IOExts
 import List         ( (\\), elemIndex, find, isPrefixOf, isSuffixOf
-                    , maximum, minimum, splitOn )
+                    , maximum, minimum, splitOn, union )
 import Maybe        ( catMaybes )
 import Profile
 import ReadNumeric  ( readHex )
@@ -51,7 +51,7 @@ testv = test 3
 banner :: String
 banner = unlines [bannerLine,bannerText,bannerLine]
  where
-   bannerText = "Non-Failing Analysis Tool (Version of xx/04/18)"
+   bannerText = "Fail-Free Verification Tool for Curry (Version of 27/04/18)"
    bannerLine = take (length bannerText) (repeat '=')
 
 ---------------------------------------------------------------------------
@@ -101,13 +101,15 @@ verifyNonFailingMod opts modname = do
   pi1 <- getProcessInfos
   printWhenAll opts $ unlines $
     ["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg prog), line]
-  stats <- proveNonFailingFuncs opts siblingconsinfo tinfo (progFuncs prog) vstate
+  stats <- proveNonFailingFuncs opts siblingconsinfo tinfo (progFuncs prog)
+                                vstate
   pi2 <- getProcessInfos
   let tdiff = maybe 0 id (lookup ElapsedTime pi2) -
               maybe 0 id (lookup ElapsedTime pi1)
-  putStrLn $ "Total verification time  : " ++ show tdiff ++ " msec"
+  when (optTime opts) $ putStrLn $
+    "TOTAL VERIFICATION TIME  : " ++ show tdiff ++ " msec"
   when (optVerb opts > 0 || not (isVerified stats)) $
-    putStrLn (showStats stats)
+    putStr (showStats stats)
  where
   line = take 78 (repeat '-')
 
@@ -156,6 +158,13 @@ isContractOp (_,fn) =
   "'pre"     `isSuffixOf` fn ||
   "'post"    `isSuffixOf` fn
 
+--- Is a function declaration a property?
+isProperty :: TAFuncDecl -> Bool
+isProperty fdecl =
+  resultType (funcType fdecl)
+    `elem` map (\tc -> TCons tc [])
+               [("Test.Prop","Prop"),("Test.EasyCheck","Prop")]
+
 ---------------------------------------------------------------------------
 -- The state of the transformation process contains
 -- * the current assertion
@@ -194,7 +203,7 @@ proveNonFailingFuncs opts siblingconsinfo ti fdecls stats = do
 proveNonFailingFunc :: Options -> ProgInfo [(QName,Int)] -> TransInfo
                     -> IORef VState -> TAFuncDecl -> IO ()
 proveNonFailingFunc opts siblingconsinfo ti vstref fdecl =
-  unless (isContractOp (funcName fdecl)) $ do
+  unless (isContractOp (funcName fdecl) || isProperty fdecl) $ do
     printWhenIntermediate opts $
       "Operation to be analyzed: " ++ snd (funcName fdecl)
     modifyIORef vstref incNumAllInStats
@@ -344,14 +353,14 @@ exp2bool demanded ti (resvar,exp) = case exp of
   AVar _ i -> returnS $ if resvar==i then bTrue
                                      else bEquVar resvar (BVar i)
   ALit _ l -> returnS (bEquVar resvar (lit2bool l))
-  AComb ty _ (qf,_) args ->
+  AComb ty ct (qf,_) args ->
     if qf == ("Prelude","?") && length args == 2
       then exp2bool demanded ti (resvar, AOr ty (args!!0) (args!!1))
       else normalizeArgs args `bindS` \ (bs,nargs) ->
            -- TODO: select from 'bindexps' only demanded argument positions
            mapS (exp2bool (isPrimOp qf || optStrict (toolOpts ti)) ti)
                 bs `bindS` \bindexps ->
-           comb2bool qf nargs bs bindexps
+           comb2bool qf ct nargs bs bindexps
   ALet _ bs e ->
     mapS (exp2bool False ti)
          (map (\ ((i,_),ae) -> (i,ae)) bs) `bindS` \bindexps ->
@@ -371,17 +380,17 @@ exp2bool demanded ti (resvar,exp) = case exp of
   ATyped _ e _ -> exp2bool demanded ti (resvar,e)
   AFree _ _ _ -> error "Free variables not yet supported!"
  where
-   comb2bool qf nargs bs bindexps
+   comb2bool qf 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...
     = returnS (bEquVar resvar bTrue)
     | qf == pre "[]"
     = returnS (bEquVar resvar (BTerm "nil" []))
-    | qf == pre ":" && length nargs == 2
+    | ct == ConsCall
     = returnS (Conj (bindexps ++
-                     [bEquVar resvar (BTerm "insert" (map arg2bool nargs))]))
-    -- TODO: translate also other data constructors into SMT
+                     [bEquVar resvar (BTerm (transOpName qf)
+                                            (map arg2bool nargs))]))
     | isPrimOp qf
     = returnS (Conj (bindexps ++
                      [bEquVar resvar (BTerm (transOpName qf)
@@ -389,7 +398,6 @@ exp2bool demanded ti (resvar,exp) = case exp of
     | otherwise -- non-primitive operation: add contract only if demanded
     = preCondExpOf ti qf (map fst bs) `bindS` \precond ->
       postCondExpOf ti qf (map fst bs ++ [resvar]) `bindS` \postcond ->
-      -- TODO: use pre/postcondition only if explicitl
       returnS (Conj (bindexps ++
                      if demanded && optContract (toolOpts ti)
                        then [precond,postcond]
@@ -521,15 +529,16 @@ pred2bool exp = case exp of
  where
   comb2bool qf ar args
     | qf == pre "[]" && ar == 0
-    = returnS (BTerm "as" [BTerm "nil" [], type2SMTExp (annExpr exp)])
+    = returnS (BTerm "as" [BTerm "nil" [], polytype2SMTExp (annExpr exp)])
     | qf == pre "not" && ar == 1
     = pred2bool (head args) `bindS` \barg -> returnS (Not barg)
     | qf == pre "null" && ar == 1
     = let arg = head args
       in pred2bool arg `bindS` \barg ->
          getS `bindS` \tstate ->
-         returnS (bEqu barg (BTerm "as" [BTerm "nil" [],
-                                         type2SMTExp (typeOfVar tstate arg)]))
+         returnS (bEqu barg (BTerm "as"
+                               [BTerm "nil" [],
+                                polytype2SMTExp (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
@@ -628,7 +637,14 @@ addSuffix (mn,fn) s = (mn, fn ++ s)
 checkImplicationWithSMT :: Options -> IORef VState -> [(Int,TypeExpr)]
                         -> BoolExp -> BoolExp -> BoolExp -> IO (Maybe Bool)
 checkImplicationWithSMT opts vstref vartypes assertion impbindings imp = do
-  let smt = unlines
+  let usertypes = filter (\ (mn,_) -> mn /= "Prelude")
+                         (foldr union [] (map (tconsOfTypeExpr . snd) vartypes))
+  vst <- readIORef vstref
+  let decls = map (maybe (error "Internal error: some datatype not found!") id)
+                  (map (tdeclOf vst) usertypes)
+      smtdatatypes = unlines [ "; User-defined datatypes:"
+                             , unlines (map tdecl2SMT decls) ]
+      smt = unlines
               [ "; Free variables:"
               , typedVars2SMT vartypes
               , "; Boolean formula of assertion (known properties):"
@@ -651,9 +667,9 @@ checkImplicationWithSMT opts vstref vartypes assertion impbindings imp = do
     unwords (map showQName allqsymbols)
   smtfuncs   <- funcs2SMT vstref allqsymbols
   smtprelude <- readFile (packagePath </> "include" </> "Prelude.smt")
-  let smtinput = smtprelude ++ smtfuncs ++ smt
+  let smtinput = smtprelude ++ smtdatatypes ++ smtfuncs ++ smt
   printWhenAll opts $ unlines ["SMT SCRIPT:", line, smtinput, line]
-  printWhenAll opts $ "CALLING Z3..."
+  printWhenAll opts $ "CALLING Z3 (with options: -smt2 -T:5)..."
   (ecode,out,err) <- evalCmd "z3" ["-smt2", "-in", "-T:5"] smtinput
   when (ecode>0) $ printWhenAll opts $ "EXIT CODE: " ++ show ecode
   printWhenAll opts $ "RESULT:\n" ++ out
@@ -676,7 +692,14 @@ typedVars2SMT :: [(Int,TypeExpr)] -> String
 typedVars2SMT tvars = unlines (map tvar2SMT tvars)
  where
   tvar2SMT (i,te) = withBracket $ unwords
-    ["declare-const", smtBE (BVar i), smtBE (type2SMTExp te)]
+    ["declare-const", smtBE (BVar i), smtBE (polytype2SMTExp 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)
 
 ---------------------------------------------------------------------------
 -- Auxiliaries:
@@ -720,7 +743,12 @@ Verified system libraries:
 - AnsiCodes
 - Either
 - ErrorState
+- Integer
 - Maybe
 - State
+- Nat --> paper
+- ShowS
+- Socket
+- Array --> paper
 
 -}

src/ToolOptions.curry

@@ -28,10 +28,11 @@ data Options = Options
                          -- but not not be correct if some argument is not
                          -- demanded (TODO: add demand analysis to make it
                          -- safe and powerful)
+  , optTime    :: Bool   -- show elapsed verification time?
   }
 
 defaultOptions :: Options
-defaultOptions = Options 1 False False False False False
+defaultOptions = Options 1 False False False False False False
 
 --- Process the actual command line argument and return the options
 --- and the name of the main program.
@@ -48,25 +49,35 @@ processOptions banner argv = do
 
 -- Help text
 usageText :: String
-usageText = usageInfo ("Usage: curry-ctopt [options] <module names>\n") options
-  
+usageText =
+  usageInfo ("Usage: curry-failfree [options] <module names>\n") options
+
 -- Definition of actual command line options.
 options :: [OptDescr (Options -> Options)]
 options =
-  [ Option "h?" ["help"]  (NoArg (\opts -> opts { optHelp = True }))
+  [ Option "h?" ["help"]
+           (NoArg (\opts -> opts { optHelp = True }))
            "print help and exit"
-  , Option "q" ["quiet"] (NoArg (\opts -> opts { optVerb = 0 }))
+  , 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 status messages (default)\n2: show intermediate results (same as `-v')\n3: show all intermediate results and more details"
-  , Option "e" ["error"] (NoArg (\opts -> opts { optError = True }))
+            "verbosity level:\n0: quiet (same as `-q')\n1: show status messages (default)\n2: show intermediate results (same as `-v')\n3: show all details (e.g., SMT scripts)"
+  , Option "e" ["error"]
+           (NoArg (\opts -> opts { optError = True }))
            "consider 'Prelude.error' as a failing operation"
-  , Option "r" ["recursive"] (NoArg (\opts -> opts { optRec = True }))
+  , Option "r" ["recursive"]
+           (NoArg (\opts -> opts { optRec = True }))
            "recursive, i.e., verify imported modules first"
-  , Option "c" ["contract"] (NoArg (\opts -> opts { optContract = True }))
+  , Option "c" ["contract"]
+            (NoArg (\opts -> opts { optContract = True }))
            "consider contract (pre/postcondition) for verification"
-  , Option "s" ["strict"] (NoArg (\opts -> opts { optStrict = True }))
+  , Option "s" ["strict"]
+           (NoArg (\opts -> opts { optStrict = True }))
+           "check contracts w.r.t. strict evaluation strategy"
+  , Option "t" ["time"]
+           (NoArg (\opts -> opts { optTime = True }))
            "check contracts w.r.t. strict evaluation strategy"
   ]
  where

src/TypedFlatCurryGoodies.curry

@@ -156,6 +156,7 @@ isPrimOp (mn,fn) = mn=="Prelude" && fn `elem` map fst preludePrimOps
 preludePrimOps :: [(String,String)]
 preludePrimOps =
   [("==","=")
+  ,("/=","/=")  -- will be translated as negated '='
   ,("+","+")
   ,("-","-")
   ,("negate","-")

src/VerifierState.curry

 module VerifierState where
 
+import List ( find )
+
 import FlatCurry.Annotated.Types
+import FlatCurry.Annotated.Goodies
 
 ---------------------------------------------------------------------------
 -- The global state of the verification process keeps some
@@ -22,20 +25,20 @@ initVState = VState [] 0 0 0 0 []
 
 --- Shows the statistics in human-readable format.
 showStats :: VState -> String
-showStats vstate =
-  "\nTESTED OPERATIONS        : " ++ show (numAllFuncs vstate) ++
-  "\nNONFAIL CONDITIONS       : " ++ show (numNFCFuncs vstate) ++
-  "\nTESTS OF MISSING PATTERNS: " ++ show (numPatTests vstate) ++
-  "\nTESTS OF NON-FAIL CALLS  : " ++ show (numFailTests vstate) ++
-  showStat "\nPOSSIBLY FAILING OPERATIONS" (failedFuncs vstate) ++
-  (if isVerified vstate then "\nNON-FAILURE VERIFICATION SUCCESSFUL!" else "")
+showStats vstate = unlines $
+  [ "TESTED OPERATIONS        : " ++ show (numAllFuncs vstate)
+  , "NONFAIL CONDITIONS       : " ++ show (numNFCFuncs vstate)
+  , "TESTS OF MISSING PATTERNS: " ++ show (numPatTests vstate)
+  , "TESTS OF NON-FAIL CALLS  : " ++ show (numFailTests vstate) ] ++
+  showStat "POSSIBLY FAILING OPERATIONS" (failedFuncs vstate) ++
+  if isVerified vstate then ["NON-FAILURE VERIFICATION SUCCESSFUL!"] else []
  where
   showStat t fs =
     if null fs
-      then ""
-      else "\n" ++ t ++ ":\n" ++
-           unlines (map (\ (fn,reason) -> fn ++ " (" ++ reason ++ ")")
-                        (reverse fs))
+      then []
+      else (t ++ ":") :
+           map (\ (fn,reason) -> fn ++ " (" ++ reason ++ ")")
+               (reverse fs)
 
 --- Are all non-failing properties verified?
 isVerified :: VState -> Bool
@@ -67,3 +70,11 @@ addProgToState :: AProg TypeExpr -> VState -> VState
 addProgToState prog vstate = vstate { currTAProgs = prog : currTAProgs vstate }
 
 ---------------------------------------------------------------------------
+--- Selects the type declaration of a type constructor from the state.
+tdeclOf :: VState -> QName -> Maybe TypeDecl
+tdeclOf vst tcons@(mn,tc) =
+  maybe Nothing
+        (\p -> find (\td -> typeName td == tcons) (progTypes p))
+        (find (\p -> progName p == mn) (currTAProgs vst))
+
+---------------------------------------------------------------------------