A tool to verify Curry operations as non-failing

This package contains a tool to verify that all operations in a given Curry module are non-failing, i.e., their evaluation does not result in a failure, if they are called with appropriate arguments. The tool automatically infers abstract call types and non-fail conditions specifying supersets of appropriate arguments.

As an example, consider the following operation to compute the last element of a given list:

last :: [a] -> a
last [x]            = x
last (_ : xs@(_:_)) = last xs

In the default mode (where types are abstracted into a set of allowed top-level constructors), the inferred call type is

last: {:}

specifying that last does not fail if the argument is a non-empty list, i.e., evaluable to some data term rooted by the list constructor “:”.

When an operation with such a restricted call type is used, the tool checks whether it is used in a context which ensures its call type. For instance, the operations

head (x:xs) = x

and

tail (x:xs) = xs

have the inferred call types

head: {:}
tail: {:}

When these operations are applied, it should be ensured (in a top-level functional computation) that the actual arguments are non-empty lists, as in the following operation:

readCommand :: IO ()
readCommand = do
  putStr "Input a command:"
  s <- getLine
  let ws = words s
  case null ws of True  -> readCommand
                  False -> processCommand (head ws) (tail ws)

The tool automatically verifies that the operation readCommand is non-failing.

The ideas of the implementation of this tool are described in:

M. Hanus: Inferring Non-Failure Conditions for Declarative Programs, Proc. of the 17th International Symposium on Functional and Logic Programming (FLOPS 2024), Springer LNCS 14659, pp. 167-187, 2024, DOI: 10.1007/978-981-97-2300-3_10,

Arithmetic non-fail conditions

If the SMT solver Z3 is installed and the executable z3 can be found in the path, the tool can also infer and verify arithmetic non-fail conditions. For instance, it infers for the factorial function defined by

fac :: Int -> Int
fac n | n == 0 = 1
      | n > 0  = n * fac (n - 1)

the non-fail condition

fac'nonfail :: Int -> Bool
fac'nonfail v1 = (v1 == 0) || (v1 > 0)

specifying that the argument must be non-negative in order to ensure that fac does not fail. With this information, it also proves that the following I/O operation does not fail (where the operation readInt reads a line until it is an integer):

printFac :: IO ()
printFac = do
  putStr "Factorial computation for: "
  n <- readInt
  if n<0 then putStrLn "Negative number, try again" >> printFac
         else print (fac n)

Installation

If you downloaded the sources of this package, then the tool can be installed via the command

> cypm install

in the main directory of this package. Otherwise, the tool can also be downloaded and installed by the command

> cypm install verify-non-fail

This installs the executable curry-calltypes in the bin-directory of CPM.

If one uses KiCS2 to install this tool, one should use version 3.1.0 of April 11, 2024 (or newer) due to a memory leak in an older version of KiCS2.

Web Demo Installation

If you want to try this tool on simple programs via a web interface, you can use a Web Demo Installation of this tool.

Files

In order to support a modular analysis of applications consisting of several modules, the tool caches already computed analysis results of modules in under the directory ~/.curry_verify_cache. This path is defined in Verify.Files.getVerifyCacheDirectory. To store the analysis results for different Curry systems and abstract domains separately, the analysis results for a Curry module which is stored in a file with path MODULEPATH.curry are contained in

~/.curry_verify_cache/CURRYSYSTEMID/DOMAINID/MODULEPATH-*

For instance, the call types of the prelude for KiCS2 Version 3.1.0 w.r.t. the abstract domain Values are stored in

~/.curry_verify_cache/kics2-3.1.0/Values/opt/kics2/lib/Prelude-CALLTYPES

provided that KiCS2 is installed at /opt/kics2 so that the prelude is contained in the file /opt/kics2/lib/Prelude.curry.

All cache files (for the Curry system used to install this tool) can be deleted by the command

curry-calltypes --delete