Run-time checking of assertions

Author(s): Edison Mera, Nataliia Stulova.

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

This package provides a complete implementation of run-time checks of predicate assertions. The program is instrumented to check such assertions at run time, and in case a property does not hold, the error is reported. Note that there is also an older package called rtchecks, by David Trallero. The advantage of this one is that it can be used independently of CiaoPP and also has updated functionality.

There are two 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.

Run-time checks configuration with flags

The run-time checks 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
- no : Disable rtchecks for trust assertions.
- yes : Enable rtchecks for trust assertions. Default.
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_test
- no : Disable rtchecks for test assertions. Default.
- yes : Enable rtchecks for test assertions. Used for debugging purposes, but is better to use the unittest library.
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.

Custom implementation for property checks

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

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

Usage and interface

Library usage:
:- module(...,...,[...,rtchecks]).
Implicit imports:
- Internal (engine) modules:
  term_basic, arithmetic, atomic_basic, basiccontrol, exceptions, term_compare, term_typing, debugger_support, basic_props.
- Packages:
  prelude, initial, condcomp, assertions, assertions/assertions_basic.

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