Show_coverage/1 and incremental tabling resulting in odd behavior?

General
1

I am trying to extract coverage information for a project. Without going into too many details, I am trying to use the coverage information to provide feedback to a grey-box fuzzer (AFL).

My application (OOAnalyzer) uses incremental tabling quite heavily, and the results from using show_coverage/1 have been strange. I am not sure if I’m doing something wrong with my hook, or if show_coverage/1 does not support tabled code.

Here is a small program that demonstrates the problem:

% This seems to be needed to force prolog_cover to load.
:- show_coverage(true).

my_file_coverage(Succeeded, Failed, Options) :-
    forall(member(Cl, Succeeded),
           (prolog_cover:clause_source(Cl, File, Line),
            prolog_cover:clause_pi(Cl, Name),
            format('~w ~w ~w~n', [Name, File, Line]))).

prolog_cover:report_hook(Succ, Fail) :- my_file_coverage(Succ, Fail, []).

:- table iamtabled/1 as incremental.
iamtabled(X) :- what(X).

iamnottabled(X) :- what(X).

what(X) :- X = 4.

test :-
    % This will display the default "Coverage by File" table...
    show_coverage(iamtabled(X)),
    writeln('The first call has ended.'),
    % This will not
    show_coverage(iamnottabled(X)).

To see the problem, query test. Here I will print out the results separately so it is easier to see.

First, the expected behavior:

?- show_coverage(iamnottabled(X)).
user:what/1 /tmp/test.pl 17
user:iamnottabled/1 /tmp/test.pl 15
system:once/1 /home/ed/Documents/swipl-devel/build/home/boot/init.pl 537
X = 4.

My hook is used as desired.

Next, the unexpected behavior:

?- show_coverage(iamtabled(X)).
$tabling:reset_delays/0 /home/ed/Documents/swipl-devel/build/home/boot/tabling.pl 926
system:call/1 /home/ed/Documents/swipl-devel/build/home/boot/init.pl 501

==============================================================================
                               Coverage by File                               
==============================================================================
File                                                     Clauses    %Cov %Fail
==============================================================================
/tmp/test.pl                                                   8    25.0   0.0
...uments/swipl-devel/build/home/library/test_cover.pl        65     1.5   1.5
==============================================================================
X = 4.

My hook is used a bit, but then the non-hooked summary is printed?

What is going on?!

2

Hi Ed,

First of all, you do not need :- show_coverage(true)., but you need to define the hook as multifile as otherwise loading the library (lazily) will wipe the clause. We can see the problem if we do

4 ?- trace(my_file_coverage, fail).
%         my_file_coverage/3: [fail]
true.

5 ?- test.
 ...
$tabling:activate/3 /home/janw/src/swipl-devel/build.pgo/home/boot/tabling.pl 584
 T [19] Fail: my_file_coverage([<clause>(0x55dbe8db0000), <clause>(0x55dbe8d71900), <clause>(0x55dbe8da4800), <clause>(0x55dbe8d76e00), <clause>(0x55dbe8d17d10), <clause>(0x55dbe8a98310), <clause>(0x55dbe8c0a630), <clause>(0x55dbe8aa2240)|...], [<clause>(0x55dbe8ac4400), <clause>(0x55dbe8f6fb80)], [])

I’ll try to have a look soon. I think the issue is that the predicate wrappers as used by tabling upset one of the predicates that is required to do the reporting. In itself, the coverage analysis is pretty unrelated to tabling, although the suspend/resume actions may make the outcome a little hard to interpret. Never tried it.

3

Actually, it is simpler. Despite the docs, prolog_cover:clause_source(+Cl, -File, -Line) is semidet rather than det as not all clauses have a related source location. So you need to report something else than a file:line. Note that the coverage analysis itself only reports calls to clauses that are related to files.

You may try the dir(SomeDir) option to get a detailed dump of the behavior of your code.

4

Thanks Jan! I got thrown off because the problem was only occurring during tabling. I suppose tabling must create a clause that does not have a source location.