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:
There are two main entries in the main manual that explain the syntax and the semantics 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:
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:
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(int,L). % A2_too_strictRun-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(int,L). Because: ['L'=[_]]. ERROR: (lns 19-21) Failed in foo:len(L,N). }
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.
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:
The rtchecks_opt package provides three bacis assertion checking levels plus one optimization (see below):
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.
As an optimization for the safe_rt assertion checking level, a variant of it, safe_ctrt level, is available:
It is also available through the rtchecks_opt package:
:- use_package(library(rtchecks_opt/opt_rt_safe_ctrt)). % all + static analysisIf 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 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).
:- 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).
?- 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))]).
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].
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.
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:
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:
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):
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.
During run-time checks transformation the following changes will be made to the source code:
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:
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.