☰

depth-k (abstract domain)

Author(s): Francisco Bueno, Daniel Jurjo Rivas (improvements and bug fixes).

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


This tutorials aims to explain how depthk analysis works.

The abstract substitution

The abstract substitution of this domains consists in a sorted list of idempotent unification equations (or bottom). For example:

[X=_, Y=g(X)]
is not a proper abstract substitution since X appears both in the left and the right side. The correct abstract substitution would be:

[X = A, Y = g(A)]
Notice that X = A does not means that X is a variable. It means that we do not know anything about X (i.e. is top)

How to run the analysis

We can run this analysis as we do with others. In that case the depth is set to one. If we want to change the depth of the analysis we have to type in the CiaoPP top-level:

?- set_pp_flag(depthk_k, N).
with N a natural number (and this excludes the 0).

Some examples

Example 1

Consider this dummy predicate:

ex1(X) :- 
    X = f(a, Y), 
    Y = g(h(k(a, b, c))).
the results of the analysis with K = 1 is:

:- true pred ex1(X)
   => instance(X,f(_A,_B)).
Let us check the results with another values of K:

  1. K = 2 we obtain: instance(X,f(a,g(_A))).
  2. K = 3 we obtain: instance(X,f(a,g(h(_A)))).
  3. K = 4 we obtain: instance(X,f(a,g(h(k(_A,_B,_C))))).
  4. K = 5 we obtain: instance(X,f(a,g(h(k(a,b,c))))).

This analysis is quite more useful when recursion arises:

Example 2

Consider the following example:

ex(X) :-
    li(Y),
    X = g(s(a, Y), Z).

li(f(a, a, f(b,b, f(c,c, nil)))).
li(f(a, a, f(b,b,T))) :-
    li(T).
in this case with the default depth we obtain:

:- true pred ex(X)
   => instance(X,g(_A,_B)).
Let us check the results with another values of K:

  1. K = 2 we obtain: instance(X,g(s(_B,_C),_A)).
  2. K = 3 we obtain: instance(X,g(s(a,f(_B,_C,_D)),_A)).
  3. K = 4 we obtain: instance(X,g(s(a,f(a,a,f(_B,_C,_D))),_A)).
  4. K = 5 we obtain: instance(X,g(s(a,f(a,a,f(b,b,f(_B,_C,_D)))),_A)).

More in depth

Consider the following example:

r(Y, Z) :-
    Y = g(L),
    M = f(K), 
    Z = f(Y).
If we execute the analysis with a raw output (that can be activated typing set_pp_flag(output_lang, raw). in the toplevel) we get:

r(Y,Z) :-
    true(2,[[Y=_,Z=_,L=_,M=_,K=_]]),
    'term_basic:='(Y,g(L)),
    true(2,[[Y=g(F),Z=_,L=F,M=_,K=_]]),
    'term_basic:='(M,f(K)),
    true(2,[[Y=g(G),Z=_,L=G,M=f(H),K=H]]),
    'term_basic:='(Z,f(Y)),
    true(2,[[Y=g(I),Z=f(g(I)),L=I,M=f(J),K=J]]).
In this case we can see that all the program variables are represented in the abstract substitution. Moreover each variables in the left side of a unification is a program variable. Notice that we do not know if they are free or not with the given information.

Documentation on exports

PREDICATEvariables_are_variables/2
No further documentation available for this predicate.

Documentation on multifiles

PREDICATEaidomain/1
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.init_abstract_domain/2
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.amgu/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.augment_asub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.augment_two_asub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.call_to_entry/10
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.exit_to_prime/8
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.project/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.widencall/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.needs/2
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.widen/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.compute_lub/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.compute_clauses_lub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.compute_clauses_glb/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.fixpoint_covered/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.fixpoint_covered_gfp/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.identical_abstract/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.abs_sort/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.extend/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.less_or_equal/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.glb/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.eliminate_equivalent/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.abs_subset/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.call_to_success_fact/10
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.special_builtin/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.combined_special_builtin0/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.body_succ_builtin/9
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.split_combined_domain/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.success_builtin/7
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.call_to_success_builtin/7
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.obtain_info/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.input_interface/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.input_user_interface/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.asub_to_native/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.concrete/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.unknown_call/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.unknown_entry/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.empty_entry/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.part_conc/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.multi_part_conc/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.collect_auxinfo_asub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.rename_auxinfo_asub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.dom_statistics/2
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.contains_parameters/2
No further documentation available for this predicate. The predicate is multifile.

Documentation on imports

This module has the following direct dependencies:
Generated with LPdoc using Ciao