Debugging PLAI analyses

Author(s): Isabel Garcia-Contreras.

This module is intended for debugging fixpoints and abstract domains. The debugging modes are sorted by difficulty and knowledge required by the programmer.

General comments. To discard errors related with not cleaning properly internal databases it is better not to debug in the ciao/ciaopp toplevel, but rather use the ciaopp command line if possible.

Debug raw analysis result

Output the analysis result without postprocessing. This is using internal clause representation of ciaopp and internal representation of the abstract domain. For this, simply set the flag output_lang to raw.

For every reachable program point there is one or more true annotations, one for every inferred call pattern. In the body, annotations with the same number correspond to the execution of the abstract call with that number. A raw assertion will appear with the same id for such abstract call and success.

Note that this option is specially useful when developing a new abstract domain. If the predicates asub_to_info/5, asub_to_native/6, etc are not defined, no useful information appears in the usual.

Inspect analysis graphs

Dump the analysis graph in some <file>:

ciaopp ?- use_module(ciaopp(p_dump)).
ciaopp ?- dump(<file>).

Use the command ciaopp-dump to inspect:

$ ciaopp-dump show <file>
     # Print info of the dump <file>.
$ ciaopp-dump fmt <file>
     # Outputs the analysis result in dot format.
$ dot -Tpdf <file>.dot -o <file>.pdf
     # Generates a graph in pdf of the dot analysis format.

Trace fixpoint operations

Output steps to reach fixpoint. It is useful to combine this option with the raw output, as it shows the steps to generate the graphs using the same numbers for ids.

In file src/plai/fixpoint_options.pl, uncomment :- use_package(.(notrace))., and recompile:

$ ciao build --bin ciaopp

A clean may be necessary, due to some undetected changes in incremental compilation of programs with included files.

$ ciao clean ciaopp

Then set flag trace_fixp to trace in the ciaopp toplevel or activate it in the command line:

$ ciaopp -A <file> -ftrace_fixp=trace

Additionally, if the flag timestamp_trace is set to on (can only be set in the ciaopp toplevel) a timestamp is printed when tracing. This can help finding perfomance issues.

Activate run-time checks

Go to any module, add :- use_package(rtchecks). and recompile by

$ ciao build --bin ciaopp

Modules recommended:

Generic domain interface src/plai/domains.pl.
Any specific domain. of src/domains/* (check that it has assertions!).
Fixpoints: src/plai/fixpoint_options.pl.
Generic fixpoint operations: src/plai/fixpo_ops.pl.
Modular analysis: src/plai/intermod_options.pl.
Incremental analysis: src/plai/incanal/incanal_options.pl.
Assertions during fixpoint: src/plai/apply_assertions.pl/src/plai/apply_assertions_old.pl.

In domains.pl the assertions were written by looking only at some domains, not all of them. It could happen that they are too restrictive. If you find that an assertion does not hold in run-time, please open an issue.

Debug fixpoint step by step

For this, it is recommended to deactivate run-time checks, as the debugger shows also the code for RT checking.

Write :- use_package(trace). in src/plai/fixpoint_options.pl and recompile:

$ ciao build --bin ciaopp

In an emacs shell buffer do M-x ciao-inferior-mode. Then execute the ciaopp command to debug

$ ciaopp -A <file>

Access PLAI databases directly

ciaopp ?- use_module(ciaopp(plai/plai_db)).
ciaopp ?- complete(SgKey,AbsInt,Sg,Proj,Prime,Id,Parents).
ciaopp ?- memo_table(LitKey,AbsInt,Id,Child,Vars_u,Call).