New domains for CiaoPP and how to add new properties

[amato-gianluca]

Hi all,
I am developing new abstract domains for the PLAI analyzer. In particular, I am working on:

• a new implementation of Sharing which incorporates the optimizations in https://dx.doi.org/10.1017/S1471068409990111;
• the reduced product Sharing x Lin which incorporates the optimizations in https://dx.doi.org/10.1017/S1471068409990160
• a domain originally due to Andy King (https://dx.doi.org/10.1007/3-540-57880-3_24) with optimizations in http://dx.doi.org/10.1017/S1471068409990160

All the development is happening in my fork of CiaoPP (https://github.com/amato-gianluca/ciaopp). Once development is over, I would be glad to merge the changes in the original repository, in case you are interested.

For the moment, I have a problem with the last domain. The properties which can be expressed with King's domain are quite sophisticated, and cannot be simulated using a combination of mshare, linear and other builtin assertions of CiaoPP. Therefore, in order to provide precise input to the analyzer, I would like to introduce a new property (let's call it shlin2) for use in entry assertions, such as:

:- entry example(U, V): shlin2([ ([U,V],[]), ([U], [U]) ])

is there a way to introduce the new property by only changing CiaoPP, without touching the core Ciao Prolog ?

Thanks,
--gianluca

[mherme]

Hi Gianluca,
that sounds very exciting, we are interested of course! This issue has several facets and possible answers. A first question is: are you interested fundamentally in performing analysis with these domains or also in other parts of the system such as verifying assertions, abstract executability, run-time checking of properties, etc.?
Cheers,
Manuel

[amato-gianluca]

Hi Manuel,
thanks for the quick reply.

In the short term, I am only interested in performing analysis with these domains. Together with Francesca Scozzari, we are trying to make a comparison similar to

Codish, M., Mulkers, A., Bruynooghe, M., de la Banda, M. G., and Hermenegildo, M. 1995.
Improving abstract interpretations by combining domains.

or

Bagnara, R., Zaffanella, E., and Hill, P. M. 2005.
Enhanced sharing analysis techniques: A comprehensive evaluation.

explicitly focused on the hypothetical costs and benefits of using optimal abstract operators (increase in precision versus decrease in performance). So, let's say that, at this moment, I am only interested in a quick hack for adding a new entry assertion to PLAI (a hack less dirty than the one I am using now, which is abusing the nonvar assertion).

Later on, I would like to complete the implementation of the domains with the things that it is missing now (predicates not used in PLAI, implementation of all builtins, and so on), and in this phase it seems plausible to extend the new assertion to cover all the other use cases.

[mherme]

Hi again Gianlucca, and sorry for the delay. If you are for now only interested in running the analysis then that simplifies things and it should indeed possible to modify only the code inside the domain definitions. Of course the analysis will want to use any new properties inferred by the domain in the output, but this is OK if the source program includes the definition of the property already, e.g.:

:- module(_,[p/2],[assertions]).

:- prop foo(X) + native.
:- impl_defined(foo/1).
% Alternatively, one can add code defining the property, but this is
% not necessary for analysis if the domain already 'understands' the
% property.  
% Note that these two declarations can be put in a file that is 
% then included in all examples!

:- entry p(X,Y) : foo(X).

p(1,a).
p(2,b).

The property can be used, e.g., in an entry declaration in the source program, and the output can now include it also because it will include as well the property definition in the original program:

:- module(_,[p/2],[assertions]).

:- prop foo(X) + native.
:- impl_defined(foo/1).

:- entry p(X,Y) : foo(X).

:- true pred p(X,Y) : foo(X) => foo(Y).

p(1,a) :-
    true(foo(1)),
    true(foo(a)). 

Both of these files should be fine as input and output, and the entry declaration should be visible to the new domain. Please let us know if this works for you or if you have any problems.

Btw, my original question was because in CiaoPP the domains and their associated properties are used in many places (assertion checking, abstract partial evaluation, run-time checking). While most of this functionality lives inside CiaoPP, a few things are outside CiaoPP in the Ciao libraries. This is something we plan on improving. Also, we have been working for quite a while on making the addition of domains simpler and more flexible, in particular that domains can be added dynamically. We also hope to duistribute that soon.

We will be happy to help out with any other questions you may have and with the merge of the new domains!

Cheers,
Manuel and the rest of the Ciao team

[amato-gianluca]

Thanks Manuel,
it was exactly what I was trying to achieve without success !

I will take profit from your kindness and ask you another question. From what I have understood, in PLAI the exit substitution of a clause is transformed into the success substitution of the calling goal in a two way process:

1. First, exit_to_prime transform the exit substitution into the prime substitution (which is like the success substitution, but restricted to the variables of the atom which caused the execution of the clause);
2. Later, extend extends the prime to the full success substitution.

For several reasons, I would like to do the opposite: first compute the success substitution from the exit one, and later, if it is needed, project the success substitution onto a subset of the variables to obtain the Prime. This is possible in the special case in which the clause is a fact, when PLAI calls the predicate call_to_success_fact. Is it possible to do the same also for clauses with bodies (without having to rewrite too large portions of the PLAI fixpoint algorithm) ?

Thanks again for your support!

--gianluca

[amato-gianluca]

I forgot to say in the previous comment that in some papers (such as "JOAQUÍN ARIAS and MANUEL CARRO. Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP", https://doi.org/10.1017/S1471068419000383) there is a reference to the exit_to_success predicate, which does not seem to exist in practice.

[amato-gianluca]

Hi,
we've mostly completed the development of the new domains, and we presented some preliminary results at CSV 2024:

Now, I am doing some refinements and optimizations, and I would like to use the Ciao Profiler to test alternative implementations of some operations. However, I don't understand how to enable it. Just as an example, I wrote the following module:

:- module(a, [], [profiler]).
:- cost_center pippo/2.
:- export(pippo/2).
pippo(2,3).

Whenever I try to load it in Ciao, I always get the error:

{ERROR: absolute_file_name/7, arg 1 - existence error: source_sink:library(profiler) does not exist}

I tried to change the configuration of Ciao with ciao configure --interactive (run by the ~/.ciaoroot/v1.23.0-m1/ folder), setting thedebug_level configuration parameter to profile, but the change seems to be ignored. If immediately after I give the command ciao configure, the debug_level settings is again set to nodebug. Nonethless, I tried to build a new version of the core bundle with ciao build core, but still the profiler does not work.

I think I am doing something fundamentally wrong.

--gianluca

[jfmc]

Great news on the excellent progress on the domains and the results at CSV!

(I've transferred the ciaodbg issue to #95 to keep there the discussion regarding profiling CiaoPP code)