|Did you know ...||Search Documentation:|
|Packs (add-ons) for SWI-Prolog|
|Title:||Runtime determinacy checker|
|Rating:||Not rated. Create the first rating!|
|Author:||Raivo Laanemets http://rlaanemets.com/|
No reviews. Create the first review!.
Many predicates dealing with databases and external systems are deterministic. Deterministic (det) predicates have the following properties:
This library attempts to provide runtime check for these conditions.
rdet/1 to annotate predicates that are supposed to be
When annotated predicate call fails, an error is thrown:
Where Module refers to module in which the call was made and Line the location of the call inside the module.
:- use_module(library(rdet)). :- rdet(insert_sort/2). :- rdet(i_sort/3). :- rdet(insert/3). insert_sort(List, Sorted):- i_sort(List, , Sorted). i_sort(, Acc, Acc). i_sort([H|T], Acc, Sorted):- insert(H,Acc,NAcc), i_sort(T,NAcc,Sorted). insert(X,[Y|T],[Y|NT]):- X>Y, insert(X,T,NT). insert(X,[Y|T],[X,Y|T]):- X=<Y. insert(X,[a],[X]).
Running the sorting procedure will throw an error (the last clause of
intentionally made to fail with numbers):
?- insert_sort([2,4,1,3], Sorted). ERROR: Unhandled exception: Goal insert/3 failed in module user on line 11.
The checker is not compatible with all extensions based on
call/N. This means that calls in some
places are not enhanced and determinism errors is not reported
As goal expansion is not called for terms inside (dynamic)
call/1 and such, the predicate calls as
are not checked.
Checks work for DCG predicates, except on direct
phrase/3. It seems likely that
goal_expansion is not applied for those. DCG calls in body
of another DCG predicate are suitable. Example:
:- rdet(one_c//0). top --> one_c. one_c --> `c`. wrap:- phrase(top, ``).
wrap on the console will produce an error:
ERROR: Unhandled exception: Goal one_c/2 failed in module user on line 5.
Dict functions are not supported.
goal_expansion is not run on
the expanded calls.
PlUnit does its own term expansion and goals inside test bodies
cannot be enhanced. This seems to have effect on everything between
Checks works together with
rdf_meta declarations and prefix
Lambda bodies use
call/1 and calls inside there are thus not supported.
Supports (tests run and checks are done) with
Overhead on tight code is can be interesting. On the insert_sort benchmark it makes the code run about 40%-50% faster.
insert/3 fixed and
with annotations commented out:
?- findall(X, between(1, 1000, X), Xs), time(insert_sort(Xs, Sorted)). % 1,001,001 inferences, 0.386 CPU in 0.391 seconds (98% CPU, 2596612 Lips) Xs = Sorted, Sorted = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] .
with annotations enabled:
?- findall(X, between(1, 1000, X), Xs), time(insert_sort(Xs, Sorted)). % 1,001,002 inferences, 0.217 CPU in 0.218 seconds (100% CPU, 4613383 Lips) Xs = Sorted, Sorted = [1, 2, 3, 4, 5, 6, 7, 8, 9|...].
These numbers were obtained with SWI 7.3.10 on a 2.4Ghz Q6600 CPU.
Every annotated predicate call in predicate bodies gets wrapped into an if-then-else.
... somepred(Args), ...
... ( somepred(Args) -> true ; throw(error(goal_failed(...)))),
List of predicate calls that get enhanced:
See if some predicate body has enhanced call:
rdet debug statements (before loading code to be enhanced):
?- debug(rdet). Warning: rdet: no matching debug topic (yet) true. ?- [insert]. % rdet: adding goal: user:insert_sort/2 % rdet: adding goal: user:i_sort/3 % rdet: adding goal: user:insert/3 % rdet: rewriting goal i_sort/3 at user:7 % rdet: rewriting goal insert/3 at user:11 % rdet: rewriting goal insert/3 at user:15 true.
user usually contains the code that is not explicitly
put into a module.
Good luck building a static analysis system that includes the following:
And has all of this optional: you can combine your code easily with 3rd party untyped/unmoded libraries.
To install as a package:
Tested with SWI-Prolog 7.x but should work with earlier versions too.
In the package root, insert into swipl:
Or if you cloned the repo:
Please send bug reports/feature request through the GitHub project page.
The MIT license. See the LICENSE file.
Pack contains 11 files holding a total of 12.1K bytes.