Run-time checking

Author(s): The Ciao Development Team.

Stability: [beta] Most of the functionality is there but it is still missing some testing and/or verification.


The rtchecks package provides a complete implementation of run-time checks of predicate assertions. The program is instrumented to capture violations of assertions at run time.

There are several main applications of run-time checks:

  • To improve debugging of certain predicates, specifying some expected behavior that is checked at run-time with the assertions.

  • To avoid manual implementation of run-time checks that should be done in some predicates, leaving the code clean and understandable.

Programs with assertions

There are two main entries in the main manual that explain the syntax and the semantics of assertions:

  • see "The Ciao assertion language" for general information on assertions and examples;
  • see "Types and properties related to assertions" for the formal definition of the syntax of several forms of assertions;

In Ciao assertions can be used to provide information on which properties should hold on predicate calls and successes. There can be several assertions for one predicate, e.g., in order to specify several possible calls and success patterns. Usually they are provided before the predicate definition in the source code:

% calculating length (as number of elements) N of a list L

:- pred len(L,N) : list(L)              => num(N) # "A1".
:- pred len(L,N) : (nnegint(N), var(L)) => list(L)# "A2".

len([],0).
len([_|T],N) :- len(T,M), N is M + 1.
The specification (assertions A1 and A2) for the len/2 predicate enumerates two possible ways for this predicate to be called:

  • A1: if called with its first argument L a list (basic_props:list/1) then on success its second argument N should be a number (basic_props:num/1). Here, as no property is specified to hald on calls for the second argument N, the most general property (basic_props:term/1) is assumed for it;
  • A2: if called with its second argument N a non-negavive integer (basic_props:nnegint/1), and the first argument L a free variable (term_typing:var/1), then on success its first argument L should be a list;

If no assertion status is specified explicitly, it is assumed that an assertion has a status check. By default, all assertions for a predicate with the check status are turned into run-time checks. This behavior may be modified either by setting Prolog flags (see Other run-time checks configuration with flags below) or performing source code analysis in one of the predefined Assertion checking levels.

There are several cases in which a run-time check may fail:

  1. a predicate was called with arguments that are outside of the acceptable call patterns (calls check failure); which can happen due to:

  2. a predicate succeeded with argument values that are incompatible with the expected success pattern (success check failure), which can happen due to:

    1. a bug in the implementation of the predicate (most often cause);
    2. a too restrictive specification;

Below we illustrate each of the cases mentioned above.

Case 1: suppose that we call len/2 with the wrong arguments, run-time checks will detect it and report this message:

?- len(a,z).
{In /tmp/foo.pl
ERROR: (lns 16-17) Run-time check failure in assertion for:
        foo:len(L,N).
In *calls*, unsatisfied property:
        list(L).
Because:
        ['L'=a].
ERROR: (lns 18-21) Failed in foo:len(L,N).
}

{In /tmp/foo.pl
ERROR: (lns 17-18) Run-time check failure in assertion for:
        foo:len(L,N).
In *calls*, unsatisfied property:
        nnegint(N).
Because:
        ['N'=z].
ERROR: (lns 18-21) Failed in foo:len(L,N).
}
Note how run-time checks report the first violated property: in the two error messages here for two pred assertions only one property violation is mentioned in each, although the var(L) from A2 is clearly violated too.

However, this situation might also occur when the initial call is made with the acceptable arguments, but the computation is performed in a way that is not compatible with the specification:

?- len(L,1).
{In /tmp/foo.pl
ERROR: (lns 16-17) Run-time check failure in assertion for:
        foo:len(L,N).
In *calls*, unsatisfied property:
        list(L).
Because:
        ['L'=L].
ERROR: (lns 18-21) Failed in foo:len(L,N).
ERROR: (lns 18-21) Failed during invocation of len(_,_)
}

{In /tmp/foo.pl
ERROR: (lns 17-18) Run-time check failure in assertion for:
        foo:len(L,N).
In *calls*, unsatisfied property:
        nnegint(N).
Because:
        ['N'=N].
ERROR: (lns 18-21) Failed in foo:len(L,N).
ERROR: (lns 18-21) Failed during invocation of len(_,_)
}
Notice, how in the recursive clause of the len/2 the unification for M happens after the evaluation of len(T,M) goal (due to the system-default left-to-right goal sequence reduction).

In this case we can re-write the len/2 predicate, making it left-recursive and fully complying with its specification:

len([],0).
len([_|T],N) :- M is N - 1, len(T,M).
Case 2.1: imagine that incidentally a bug was introduced in the first clause of len/2:

len(_,0).
len([_|T],N) :- M is N - 1, len(T,M).
Run-time checks will detect that now len/2 constructs not null-terminating lists:

?- len(L,1).
{In /tmp/foo.pl
ERROR: (lns 17-18) Run-time check failure in assertion for:
        foo:len(L,N).
In *success*, unsatisfied property:
        list(L).
ERROR: (lns 18-21) Failed in foo:len(L,N).
ERROR: (lns 18-21) Failed during invocation of len(_,_)
}

{In /tmp/foo.pl
ERROR: (lns 17-18) Run-time check failure in assertion for:
        foo:len(L,N).
In *success*, unsatisfied property:
        list(L).
Because:
        ['L'=[_|_]].
ERROR: (lns 18-21) Failed in foo:len(L,N).
}
Case 2.2: suppose the specification for len/2 instead of A2 contains A2_too_strict, which requires that on success L must be a list of integers, not just any terms.

:- pred len(L,N) : (nnegint(N), var(L)) => list(L,int). % A2_too_strict
Run-time checks will detect a failure of such assertion:

?- len(L,1).
{In /tmp/foo.pl
ERROR: (lns 17-19) Run-time check failure in assertion for:
        foo:len(L,N).
In *success*, unsatisfied property:
        list(L,int).
Because:
        ['L'=[_]].
ERROR: (lns 19-21) Failed in foo:len(L,N).
}
Bug: currently not all rtchecks* packages support interleaving assertions and predicate clauses. See rtchecks/rtchecks_tr.pl for details.

Note about performance: run-time checks usually affect the complexity of the program, which results in noticeable run-time overhead.

Consider a simplified specification of the len/2 predicate:

:- pred len(L,N) : list(L) => num(N).

len([],0).
len([_|T],N) :- M is N - 1, length(T,M).
Checking that the first argument of the len/2 predicate is a list at each recursive step turns the standard O(n) algorithm into O(n^2) one.

In Ciao the trade-offs between the thoroughness of the run-time checks and the associated run-time overhead are embodied into assertion checking levels. In the following we describe how to deal with the added complexity by run-time checks.

Assertion checking levels

There are several assertion checking levels availble in Ciao for different scenarios of run-time checking. They also represent different trade-offs between the number of run-time checks (overhead) and the respective code behavior guarantees (safety).

The rtchecks package provides two assertion checking levels, accessible through a package configuration flag:

  • rtchecks_level
    • exports: Only use rtchecks for external calls of the exported predicates.
    • inner : Use also rtchecks for internal calls. Default.

The rtchecks_opt package provides three bacis assertion checking levels plus one optimization (see below):

  • unsafe: no assertions are turned into run-time checks, zero run-time overhead added to program execution;

  • client_safe: only assertions for the exported predicates are turned into run-time checks, the rest are ignored;

  • safe_rt: all check assertions are turned into run-time checks;

Example of a module using run-time checks on one of the default checking levels:

:- module(ex_levels,[test/0,foo/2],[assertions,regtypes]).

:- use_module(engine(io_basic), [display/1,nl/0]).
:- use_package(library(rtchecks_opt/opt_rt_unsafe)).        % no checks
% :- use_package(library(rtchecks_opt/opt_rt_client_safe)). % interface
% :- use_package(library(rtchecks_opt/opt_rt_safe_rt)).     % all (interface + internal)

test :- foo(1,X), bar(X,Y), display(Y), nl.

:- pred foo(A,B) : int(A) => atm(B) # "A1".

foo(1,a).

:- pred bar(C,D) : atm(C) => atm(D) # "A2".

bar(a,z).
On the unsafe checking level no assertions will be checked, on the client_safe only A1 will be checked, and on safe_rt both A1 and A2 will be checked.

Check optimizations

Static checks optimization

As an optimization for the safe_rt assertion checking level, a variant of it, safe_ctrt level, is available:

  • safe_ctrt: the program is subjected to static analysis pass, remaining check assertions after it are turned into run-time checks. In any case, calls assertions for exported predicates will always be turned into checks.

It is also available through the rtchecks_opt package:

:- use_package(library(rtchecks_opt/opt_rt_safe_ctrt)). % all + static analysis
If the ex_levels module from the example above was compiled on this checking level, the analysis would be able to prove A2 to always hold, as well as the success part of A1, thus leaving only the calls part of A1 for run-time checking:

%% %% :- check pred foo(A,B)
%% %%    : int(A)
%% %%   => atm(B).

:- check calls foo(A,B)
         : int(A).

:- true success foo(A,B)
         : int(A)
        => atm(B).

%% %% :- check pred bar(C,D)
%% %%    : atm(C)
%% %%   => atm(D).

:- true success bar(C,D)
         : atm(C)
        => atm(D).

:- checked calls bar(C,D)
         : atm(C).
More details are available from the related publication [SMH18b].

Shallow run-time checking

Note: this is a new feature and under active development. The documentation may be partial/obsolete.

Shallow run-time checking is an optimization of run-time checks of regular types in predicate calls across module boundaries in presence of hidden functors (via :- hide declaration of the termhide package).

Bug: this syntax is currently not working properly, please use this feature through an appropriate assertion checking level of rtchecks_opt.
To enable property caching in run-time checks use a variant of the rtchecks package, namely rtchecks_shallow, together with the termhide package:
:- module(MOD, _, [assertions,termhide,rtchecks_shallow]).

More details are available from the related publication [SMH18a].

The main reason for performing shallow run-time checking is run-time overhead reduction, especially in the cases where run-time checks change complexity of predicate execution:

:- module(bintrees,[root/2],[assertions,regtypes,nativeprops]).
%:- use_package(library(rtchecks_opt/shallow_rt_unsafe)).     % no checks
:- use_package(library(rtchecks_opt/shallow_rt_client_safe)). % interface
%:- use_package(library(rtchecks_opt/shallow_rt_safe_rt)).    % all (interface + internal)
%:- use_package(library(rtchecks_opt/shallow_rt_safe_ctrt)).  % all + static analysis

:- hide(empty/0).
:- hide(tree/3).

:- regtype val_t/1.
val_t(X) :- int(X).

:- regtype tree/1.
tree(empty).
tree(tree(LC,X,RC)) :- tree(LC),val_t(X),tree(RC).

:- pred root/2 : tree * term => tree * val_t.

root(tree(_,X,_),X).
Here, the precondition checks for the root/1 predicate change its complexity from constant to linear in the size of the input argument, as the checking code will need to traverse the input tree term to verify that it is a well-formed tree.

In presence of hidden functor terms, however, it might be possible to infer data shapes produced by the module, and simplify run-time checks w.r.t. this information.

:- regtype 'tree$shallow'/1.
'tree$shallow'(empty).
'tree$shallow'(tree(LC,X,RC)) :- term(LC),term(X),term(RC).
Note: currently it is not possible to print/output the inferred shallow regular types, as it is implemented as an internal compiler pass. However, they can be viewed at the WAM level. To produce the MODULE.wam expansion of the target module, in the Ciao shell do:
?- use_module(library(compiler)).
Note: module compiler already in executable, just made visible

yes
?- make_wam(MODULE).
The resulting shallow regular types for the bintrees module from the example above will look like this:

clause('bintrees:tree$shallow/1/1',
   [ifshallow
   ,neck(1)
   ,else
   ,endif
   ,get_constant_x0('bintrees:empty')
   ,proceed]).

clause('bintrees:tree$shallow/1/2',
   [ifshallow
   ,neck(1)
   ,else
   ,endif
   ,get_structure_x0(/('bintrees:tree',3))
   ,unify_x_variable(0)
   ,allocate
   ,unify_y_variable(1)
   ,unify_y_variable(0)
   ,init([])
   ,call(/('basic_props:term',1),2)
   ,put_y_value(1,0)
   ,call(/('basic_props:term',1),1)
   ,put_y_value(0,0)
   ,deallocate
   ,execute(/('basic_props:term',1))]).

Check caching

This is a new feature and under active development. This documentation may be partial/obsolete.

To enable property caching in run-time checks use a variant of the rtchecks package, namely rtchecks_cached:

:- module(MOD, _, [assertions,rtchecks_cached]).
More details are available from the related publication [SMH15].

Bug: currently checks only for a limited subset of predefined regtypes can be cached. See rtchecks_cached/README for details.

Example of use:

:- module(amqueue,[enqueue/3],[assertions,regtypes,rtchecks_cached]).

:- def_impl(var/1,fast_var/2).
:- def_impl(term/1,fast_term/2).
:- def_impl(pair_list/1,fast_listpair_cached/2).

:- pred enqueue/3 :  pair_list * term * var
                  => pair_list * term * pair_list.

enqueue((Ins,Del),Elem,([Elem|Ins],Del)).

:- regtype pair_list/1.

pair_list((X,Y)) :- list(X), list(Y).
The def_impl/2 declaration is needed at the moment to relate the regtype definitions in the source code and the corresponding checks with caching.

See testsuite/rtchecks_cached/ for examples and benchmarks.

Run-time checking of trust assertions

By definition trust/1 assertions are trusted by the compiler and their information is taken to be true. To detect cases where these assertions may be erroneous we allow an additional run-time checking level in which all assertions (including trusts) are checked. It is controlled by setting the appropriate Prolog flag:

  • rtchecks_trust
    • no : Disable rtchecks for trust assertions.
    • yes : Enable rtchecks for trust assertions. Default.

Other run-time checks configuration with flags

These flags are currently being reviewed and might not be documented/working as described here.

Run-time checks (specifically, those of the rtchecks package) can be configured using Prolog flags. Below we itemize the valid Prolog flags with their values and a brief explanation of the effects:

  • rtchecks_entry
    • no : Disable rtchecks for entry assertions.
    • yes : Enable rtchecks for entry assertions. Default.

  • rtchecks_exit
    • no : Disable rtchecks for exit assertions.
    • yes : Enable rtchecks for exit assertions. Default.

  • rtchecks_asrloc Controls the usage of locators for the assertions in the error messages. The locator says the file and lines that contains the assertion that had failed. Valid values are:
    • no : Disabled.
    • yes : Enabled. Default.

  • rtchecks_predloc Controls the usage of locators for the predicate that caused the run-time check error. The locator says the first clause of the predicate that the violated assertion refers to.
    • no : Disabled.
    • yes : Enabled, Default.

  • rtchecks_callloc
    • no : Do not show the stack of predicates that caused the failure
    • predicate: Show the stack of predicates that caused the failure. Instrument it in the predicate. Default.
    • literal : Show the stack of predicates that caused the failure. Instrument it in the literal. This mode provides more information, because reports also the literal in the body of the predicate.

  • rtchecks_namefmt
    • long : Show the name of predicates, properties and the values of the variables
    • short : Only show the name of the predicate in a reduced format. Default.

  • rtchecks_abort_on_error Controls if run time checks must abort the execution of a program (by raising an exception), or if the execution of the program have to continue.

    Note that this option only affect the default handler and the predicate call_rtc/1, so if you use your own handler it will not have effect.

    • yes : Raising a run time error will abort the program.
    • no : Raising a run time error will not stop the execution, but a message will be shown. Default.

Custom property checks

This is a new feature and under active development. This documentation may be partial/obsolete.

In some cases declarative property definitions are not efficient enough to be used in the run-time checks instrumentation. In Ciao it is possible to write an alternative version of property that can be used specifically in run-time checks, while keeping the main version (which might be easier to read or is better understood by some static analyzer).

To provide the custom property implementation for run-time checking it is necessary to edit two files (suppose the original property is defined in a module foo.pl):

  • the foo_rtc.pl module that contains the custom property implementation and is placed in the same folder as foo.pl. Make sure the custom property implementation is exported from both modules.

  • $CIAOROOT/core/lib/rtchecks/rtchecks_rt_propimpl.pl, a database file that stores the links between different property implementations in the format of declarations ':- rtc_impl(ModOr:PropOr/ArityOr, ModRt:PropRt/ArityRt).' where ModOr and ModRt are names of the two modules that contain the original and the custom property definitions, PropOr and PropRt are the two different property implementations with respective arities ArityOr and ArityRt.

After these edits the rtchecks library needs to be rebuilt.

For an example of a system library that uses this feature see the assertions/native_props library.

Run-time checks implementation

During run-time checks transformation the following changes will be made to the source code:

  • assertions will be expanded into respective checkable calls and success assertion conditions;

  • for every instrumented predicate a wrapper clause will be generated;

Schematically, the run-time checks instrumentation looks as follows:

% original program source
:- pred P : Pre1 => Post1.
...
:- pred P : PreN => PostN.

P :- Body.
% instrumented program source
P :-    checkC(Pre1;...;PreN),
        Pnew,
        checkS(Pre1,Post1),...,checkS(PreN,PostN).

Pnew :- Body.
where:

  • checkC/1 is a simplified version of the preconditions check produced from the calls assertion condition, that checks if at least one calls pattern is satisfied in the predicate call, and emits a run-time error otherwise;

  • checkS/1 is a simplified version of the postcondition checks, produced from a success assertion condition, where each individual postcondition check is performed if the respective precondition held (with the possibility of emitting a run-time error if some property in a postcondition does not hold), or not performed if the precondition did not hold (and thus the postcondition is not applicable in the current predicate call).

  • P :- Pnew. is the wrapper clause that maintains all original calls to the predicate P in the program, while redirecting them to Pnew, so that run-time checks are executed during the execution of P.

For testing instructions of a specific run-time checks implementation (packages rtchecks, rtchecks_cached, rtchecks_opt, and rtchecks_shallow) see the README files of the respective testsuite/rtchecks* directory.


Usage and interface

Other information

Note: the assertions package must always be included together with the rtchecks package (see core/lib/compiler/global_module_options.pl for details).