- The CiaoPP Program Processor »
- PART I - Using CiaoPP »
- Available abstract domains »
- depth-k (abstract domain)
ON THIS PAGE
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 tutorial aims to explain how depthk analysis works.
The abstract substitution
The abstract substitution of this domain 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 mean that X is a variable. It means that we do not know anything about X (i.e., it is top).
How to run the analysis
We can run this analysis by simply calling analyze(depthk) as usual. In that case the depth is set to one. If we want to change the depth paramemter we have to type the follwoing in the CiaoPP top level:
?- set_pp_flag(depthk_k, N). with N a natural number (but not 0).Some examples
Example 1
Consider this predicate:
ex1(X) :- X = f(a, Y), Y = g(h(k(a, b, c))).the result of the analysis with K = 1 is:
:- true pred ex1(X) => instance(X,f(_A,_B)).Let us check the results with other values of K:
- K = 2 we obtain: instance(X,f(a,g(_A))).
- K = 3 we obtain: instance(X,f(a,g(h(_A)))).
- K = 4 we obtain: instance(X,f(a,g(h(k(_A,_B,_C))))).
- K = 5 we obtain: instance(X,f(a,g(h(k(a,b,c))))).
Larger depths can be more useful when recursion arises (but not to the point of covering the complete recursiomn, as, e.g., a regular type analysis will):
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 other values of K:
- K = 2 we obtain: instance(X,g(s(_B,_C),_A)).
- K = 3 we obtain: instance(X,g(s(a,f(_B,_C,_D)),_A)).
- K = 4 we obtain: instance(X,g(s(a,f(a,a,f(_B,_C,_D))),_A)).
- 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 variable 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.
Usage and interface
- Library usage:
:- use_module(domain(depthk)). - Exports:
- Predicates:
variables_are_variables/2. - Multifiles:
aidomain/1, aidom.init_abstract_domain/2, aidom.amgu/5, aidom.augment_asub/4, aidom.augment_two_asub/4, aidom.call_to_entry/10, aidom.exit_to_prime/8, aidom.project/6, aidom.widencall/4, aidom.needs/2, aidom.widen/4, aidom.compute_lub/3, aidom.compute_clauses_lub/4, aidom.compute_clauses_glb/4, aidom.fixpoint_covered/3, aidom.fixpoint_covered_gfp/3, aidom.identical_abstract/3, aidom.abs_sort/3, aidom.extend/6, aidom.less_or_equal/3, aidom.glb/4, aidom.eliminate_equivalent/3, aidom.abs_subset/3, aidom.call_to_success_fact/10, aidom.special_builtin/6, aidom.combined_special_builtin0/3, aidom.body_succ_builtin/9, aidom.split_combined_domain/4, aidom.success_builtin/7, aidom.call_to_success_builtin/7, aidom.obtain_info/5, aidom.input_interface/5, aidom.input_user_interface/6, aidom.asub_to_native/6, aidom.concrete/4, aidom.unknown_call/5, aidom.unknown_entry/4, aidom.empty_entry/4, aidom.part_conc/5, aidom.multi_part_conc/4, aidom.collect_auxinfo_asub/4, aidom.rename_auxinfo_asub/4, aidom.dom_statistics/2, aidom.contains_parameters/2.
- Predicates:
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:- Application modules:
preprocess_flags, domains, s_eqs. - System library modules:
sets, sort, lists, terms_check, terms_vars, write. - Internal (engine) modules:
term_basic, arithmetic, atomic_basic, basiccontrol, exceptions, term_compare, term_typing, debugger_support, basic_props, hiord_rt. - Packages:
prelude, initial, condcomp, assertions, assertions/assertions_basic, modes_extra, modes, aidomain.