New domains for CiaoPP and how to add new properties #93
Replies: 3 comments 4 replies
-
|
Hi Gianluca, |
Beta Was this translation helpful? Give feedback.
-
|
Hi Manuel, 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. or Bagnara, R., Zaffanella, E., and Hill, P. M. 2005. 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. |
Beta Was this translation helpful? Give feedback.
-
|
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, |
Beta Was this translation helpful? Give feedback.
-
|
Thanks Manuel, 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:
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 Thanks again for your support! --gianluca |
Beta Was this translation helpful? Give feedback.
-
|
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 |
Beta Was this translation helpful? Give feedback.
-
|
Hi, 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: I tried to change the configuration of Ciao with I think I am doing something fundamentally wrong. --gianluca |
Beta Was this translation helpful? Give feedback.
-
|
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) |
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
-
Hi all,
I am developing new abstract domains for the PLAI analyzer. In particular, I am working on:
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
Beta Was this translation helpful? Give feedback.
All reactions