Run-time checking of assertions

Examples of using run-time checks to detect program errors

As described in "The Ciao assertion language" and "Types and properties related to assertions", Ciao assertions can be used to provide predicate specifications, and in particular, 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.

• 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 hold 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 (see Controlling 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 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 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).
}

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 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 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(_,_)
}

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).

len(_,0).
len([_|T],N) :- M is N - 1, len(T,M).

?- len(L,1).
{In 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 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).
}

:- pred len(L,N) : (nnegint(N), var(L)) => list(int,L). % A2_too_strict

?- len(L,1).
{In foo.pl
ERROR: (lns 17-19) Run-time check failure in assertion for:
    foo:len(L,N).
In *success*, unsatisfied property:
    list(int,L).
Because:
    ['L'=[_]].
ERROR: (lns 19-21) Failed in foo:len(L,N).
}

Note on 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).

Controlling assertion checking levels

The rtchecks package supports several assertion checking levels for different scenarios, which allow controlling the trade-offs between the number of run-time checks (overhead) and the respective code behavior guarantees (safety).

The run-time checking level can be configured using prolog flags. Below we itemize the valid prolog flags with its values and a brief explanation of the meaning:

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

• rtchecks_trust: By definition trust/1 assertions are trusted by the compiler and analyzer and their information is taken to be true. Enable to detect cases where these assertions may be erroneous).
  • no : Disable rtchecks for trust assertions.
  • yes : Enable rtchecks for trust assertions. Default.

• rtchecks_entry (deprecated in rtchecks_opt)
  • no : Disable rtchecks for entry assertions.
  • yes : Enable rtchecks for entry assertions. Default.

• rtchecks_exit (deprecated in rtchecks_opt)
  • no : Disable rtchecks for exit assertions.
  • yes : Enable rtchecks for exit assertions. Default.

Custom implementation for property checks

The run-time check instrumentation can use custom property checks implementations. This is useful when defining native properties (without a clause-based definition supported by the default instrumentation) or when the generic run-time checks are not efficient enough. The custom implementation can be used specifically in run-time checks, while keeping a declarative 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 recommended 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.
• 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.

Other run-time checks configuration flags

• rtchecks_test (internal flag, used in test case generation)
  • no : Disable rtchecks for test assertions. Default.
  • yes : Enable rtchecks for test assertions.

• 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. Default.
  • short : Only show the name of the predicate in a reduced format.

Usage and interface

Other information

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

• Currently not all rtchecks* packages support interleaving assertions and predicate clauses. See rtchecks/rtchecks_tr.pl for details.

• The interaction of custom implementation of property checks with other user-defined properties like regular types is buggy.

:- 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).

:- use_package(library(rtchecks_opt/opt_rt_safe_ctrt)). % all + static analysis

%% %% :- 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).

:- module(MOD, _, [assertions,termhide,rtchecks_shallow]).

:- 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).

:- regtype 'tree$shallow'/1.
'tree$shallow'(empty).
'tree$shallow'(tree(LC,X,RC)) :- term(LC),term(X),term(RC).

?- use_module(library(compiler)).
Note: module compiler already in executable, just made visible

yes
?- make_wam(MODULE).

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))]).

:- module(..., ..., [...,assertions,rtchecks_cached]).

:- 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).

% 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.