Francisco Bueno Carrillo wrote:
The only thing that I'm still confused about is all of the different options for analysis / specialisation but I've found a few references to papers that I can check.
Amoss, maybe the current manual page on the subject is of some help: most options are now briefly documented. Please, find it enclosed.
Paco
I've found that section of the manual, some of the descriptions are helpful but there are some missing. For instance, the unfolding rules for local control don't have any descriptions or even full names to google for papers describing them. I've moved on to trying to specialise our target program now which is an interpreter and although ciaopp seems to unfold some of the predicates as I would expect it leaves others as residuals. Any arithmetic expression, or control flow dependant on arthimetic comparisons seems to stay in the residual. For example:
:- entry mem(X,[1,2,3]) : (ground(X)). mem(X,[X|_]). mem(X,[_|Y]) :- member(X,Y).
This code specialises to what I would expect, namely three clauses, one for each success case. If I try a similar code that uses some basic arithmetic then I don't get the same results :
:- entry loop(1,10). loop(X,L) :- X>=L. loop(X,L) :- X<L, write(dude), X2 is X+1, loop(X2,L).
This code specialises to:
:- entry loop(1,10). loop(1,10) :- user:write(dude), A is 1+1, user:loop(A,10).
This isn't actually correct as it will write 'dude' once and then fail, where-as the original will write 'dude' nine times and then succeed. But also, I would expect the loop to be unfolded to yield something (close to):
loop(1,10) :- write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude).
How can I get ciaopp to unfold arithmetic expressions like this? Is it a different set of menu options to the one that I am using to select a different type of analysis, or is it a different local-control rule?
Amoss ============================================================================== Message: Address: Action: help majordomo(a)clip.dia.fi.upm.es Info. on useful commands subscribe ciaopp-users-request(a)clip.dia.fi.upm.es Subscribe to this list unsubscribe ciaopp-users-request(a)clip.dia.fi.upm.es Unsubscribe from list <whatever> ciaopp-users(a)clip.dia.fi.upm.es Send message to list ----------------------------------------------------------------------------- Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciaopp-users/ -----------------------------------------------------------------------------
Hi Amoss,
:- entry mem(X,[1,2,3]) : (ground(X)). mem(X,[X|_]). mem(X,[_|Y]) :- member(X,Y).
This code specialises to what I would expect, namely three clauses, one for each success case.
Good!
If I try a similar code that uses some basic arithmetic then I don't get the same results :
:- entry loop(1,10). loop(X,L) :- X>=L. loop(X,L) :- X<L, write(dude), X2 is X+1, loop(X2,L).
This code specialises to:
:- entry loop(1,10). loop(1,10) :- user:write(dude), A is 1+1, user:loop(A,10).
This isn't actually correct as it will write 'dude' once and then fail, where-as the original will write 'dude' nine times and then succeed. But also, I would expect the loop to be unfolded to yield something (close to):
loop(1,10) :- write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude).
How can I get ciaopp to unfold arithmetic expressions like this? Is it a different set of menu options to the one that I am using to select a different type of analysis, or is it a different local-control rule?
I am afraid the problem is not in the arithmetic predicates but rather on the predicate write/1. Since it has side effects, it cannot be executed at specialization time. Then the only solution is to perform non-leftmost unfolding. For this you have to select
Select Computation Rule: [leftmost, local_builtin, local_emb, jump_builtin] (leftmost) ? jump_builtin
all the other flags you can leave with the default value.
This will generate your expected output:
%%%%%%%%%%%%% :- module( _loop, [loop/2], [assertions] ).
:- entry loop(1,10).
loop(1,10) :- write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude), write(dude). %%%%%%%%
German
P.S. I have added your program to CVS, under CVS:Projects/Asap/Deliverables/Tests/loop.pl so that we always speak about exactly the same code. Note I have added a module declaration.
I am afraid the problem is not in the arithmetic predicates but rather on the predicate write/1. Since it has side effects, it cannot be executed at specialization time. Then the only solution is to perform non-leftmost unfolding. For this you have to select
Select Computation Rule: [leftmost, local_builtin, local_emb, jump_builtin] (leftmost) ? jump_builtin
all the other flags you can leave with the default value.
This is perfect, the interpreter now unfolds exactly as we unexpected and we end up with a residual that is isomorphic to our target language. Now I need to control what is left in the residual, currently I just have some dummy predicates for the PIC instructions like:
movf(F) :- write(movf),nl,write(F),nl.
These are are unfolded in the body of the interpreter, in logen we marked these as rescall so that the calls would stay in the residual program. How do I apply a similar assertion / property in ciaopp?
In the residual program that is generated there is a lot of dead code that is not reachable from the entry points. Is there an option to remove this code automatically or should I perform slicing on the generated code afterwards?
Amoss
============================================================================== Message: Address: Action: help majordomo(a)clip.dia.fi.upm.es Info. on useful commands subscribe ciaopp-users-request(a)clip.dia.fi.upm.es Subscribe to this list unsubscribe ciaopp-users-request(a)clip.dia.fi.upm.es Unsubscribe from list <whatever> ciaopp-users(a)clip.dia.fi.upm.es Send message to list ----------------------------------------------------------------------------- Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciaopp-users/ -----------------------------------------------------------------------------
This is perfect, the interpreter now unfolds exactly as we unexpected and we end up with a residual that is isomorphic to our target language.
Great!
Now I need to control what is left in the residual, currently I just have some dummy predicates for the PIC instructions like:
movf(F) :- write(movf),nl,write(F),nl.
These are are unfolded in the body of the interpreter, in logen we marked these as rescall so that the calls would stay in the residual program. How do I apply a similar assertion / property in ciaopp?
The easiest thing is that you move the definition of this predicates to a separate module, say dummy_defs.pl and write in your main module :- use_module(dummy_defs).
In the residual program that is generated there is a lot of dead code that is not reachable from the entry points. Is there an option to remove this code automatically or should I perform slicing on the generated code afterwards?
Hmm, partial deduction should already eliminate dead-code.
Where are your programs? Are they in CVS so that we can take a look?
German
The easiest thing is that you move the definition of this predicates to a separate module, say dummy_defs.pl and write in your main module :- use_module(dummy_defs).
Ah, I had a hunch that would do it. This is fine for now but later we may need to specialise predicates that are in other modules, is there an easy way to do this?
In the residual program that is generated there is a lot of dead code that is not reachable from the entry points. Is there an option to remove this code automatically or should I perform slicing on the generated code afterwards?
Hmm, partial deduction should already eliminate dead-code.
Where are your programs? Are they in CVS so that we can take a look?
I've checked the latest copy into /Projects/Deliverables/Case_Studies/Precision_Interpreter. There are only two important source files, exec.pl contains the rough outline of the interpreter for a single operation. pic.pl contains the necessary PIC instructions to implement it. pic.pl is just a place-holder for now, the pic-interpreter will perform this task properly, and be an executable definition. I'm currently specialising exec.pl like this:
ciaopp ?- customize_and_exec( 'exec.pl' ).
(Press h for help)
Select Menu Level: [naive, expert] (expert) ? Select Action Group: [analyze, check_assertions, optimize] (optimize) ? Select Optimize: [none, spec, parallelize] (spec) ? Select Abs Specialization: [off, mono, poly] (off) ? Select Analysis Domain: [none, pd, pdb, def, gr, share, shareson, shfr, shfrson, shfrnv, son, aeq, depth, path, difflsign, fr, frdef, lsign, eterms, ptypes, svterms, terms] (shfr) ? Select Local Control: [off, orig, inst, det, det_la, depth, first_sol, first_sol_d, all_sol, hom_emb, hom_emb_anc, hom_emb_as, df_hom_emb_as, df_tree_hom_emb, df_hom_emb] (df_hom_emb_as) ? Select Computation Rule: [leftmost, local_builtin, local_emb, jump_builtin] (jump_builtin) ? Select Partial Concretization: [off, mono, multi] (off) ? Perform Argument Filtering: [off, on] (off) ? Select Global Control: [off, id, inst, hom_emb] (off) ? Abstract Spec Definitions: [off, rem, exec, all] (off) ? Remove Useless Clauses: [off, pre, post, both] (off) ? Note: Current Saved Menu Configurations: [] Menu Configuration Name: (none) ? {Loading current module from /home/staff/moss/common/asap/precision/exec.pl {Reading /home/staff/moss/common/asap/precision/exec.pl WARNING: (lns 28-31) [L,Len,Rep,Start,U] - singleton variables in addr/5 WARNING: (lns 39-44) predicate addr/6 is already defined with arity 5 WARNING: (lns 45-47) [VL] - singleton variables in addr/6 WARNING: (lns 62-66) [Len,U,VU] - singleton variables in partAddr/4 WARNING: (lns 84-96) [Au,Bu,Ol] - singleton variables in addvals/3 } {loaded in 4210.0 msec.} } {Analyzing /home/staff/moss/common/asap/precision/exec.pl {preprocessed for plai in 0.0 msec.} {unfolded in 220.0 msec.} {total transformation time 240.0 msec.} {In /home/staff/moss/common/asap/precision/exec.pl WARNING (fixpo_ops): (lns 78-83) Unknown predicate pic:movf/2 } {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/3} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/4} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/5} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/6} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/7} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/8} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/9} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/10} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/11} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/12} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/13} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/14} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/15} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/16} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:addmodloop_1/5/17} {unfolded in 30.0 msec.} {total transformation time 40.0 msec.} {In /home/staff/moss/common/asap/precision/exec.pl WARNING (fixpo_ops): (lns 67-74) Unknown predicate pic:movf/2 } {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:add8_1/5/2} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:add8_1/5/3} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:add8_1/5/4} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:add8_1/5/5} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:add8_1/5/6} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:add8_1/5/7} {WARNING (fixpo_ops): Unknown predicate pic:movf/2 in clause exec:add8_1/5/8} {unfolded in 0.0 msec.} {total transformation time 0.0 msec.} {unfolded in 0.0 msec.} {total transformation time 0.0 msec.} {unfolded in 10.0 msec.} {total transformation time 10.0 msec.} {unfolded in 0.0 msec.} {total transformation time 10.0 msec.} {unfolded in 0.0 msec.} {total transformation time 0.0 msec.} {unfolded in 0.0 msec.} {total transformation time 0.0 msec.} {unfolded in 0.0 msec.} {total transformation time 10.0 msec.} {unfolded in 0.0 msec.} {total transformation time 0.0 msec.} {unfolded in 0.0 msec.} {total transformation time 0.0 msec.} {unfolded in 0.0 msec.} {total transformation time 0.0 msec.} {unfolded in 10.0 msec.} {total transformation time 10.0 msec.} {unfolded in 0.0 msec.} {total transformation time 0.0 msec.} {unfolded in 20.0 msec.} {total transformation time 20.0 msec.} {In /home/staff/moss/common/asap/precision/exec.pl WARNING (fixpo_ops): (lns 84-96) Unknown predicate pic:movf/2 } {analyzed by di using shfr in 2320.0 msec.} } {Transforming /home/staff/moss/common/asap/precision/exec.pl {transformed by codegen in 60.0 msec.} } {written file /home/staff/moss/common/asap/precision/exec_shfr_codegen_co.pl}
In the resulting file the body of addvals/3 is exactly what we wanted:
addvals(x,y,x) :- movf(10,0), addwf(13,0), movwf(10), movf(11,0), addwf(14,0), movwf(11), movf(12,0), addwf(15,0), movwf(12).
But all of the code above it is dead-code that cannot be reached from the entry point. We could slice it away but this seems a bit of a heavy approach.
Amoss
Dear Amoss,
I have got the following specialized program:
%%%%%%%%%%%%%%%%%% :- module( _exec, [addvals/3], [assertions] ).
:- entry addvals(x,y,x).
addvals(x,y,x) :- movf(10,0), addwf(13,0), movwf(10), movf(11,0), addwf(14,0), movwf(11), movf(12,0), addwf(15,0), movwf(12). %%%%%%%%%%%%%%%%%%%
which is, I believe, what you want.
I have done a couple of changes to your initial program, though.
- I have uncommented the use_module(pic), which is needed - I have replaced the initial module declaration:
:- module(_,_).
with
:- module(_,[addvals/3]).
The difference is that the first declaration means that all predicates in the module are exported (regardless of whether you later add entry declarations for them or not).
If you only want to specialize the program for predicate addvals, then the second declaration is what you want. Note that otherwise the rest of predicates in the module cannot be safely considered dead code because they are exported and they are potentially used from outside.
Ah, I had a hunch that would do it. This is fine for now but later we may need to specialise predicates that are in other modules, is there an easy way to do this?
There are two ways. One is to add "eval" assertions for exported predicates which allow the partial evaluator to fully compute calls to predicates in other modules.
Another possibility is to ask ciaopp to generate a monolithic program from a set of modules. In that program, all predicate names are module qualified an all code can live in a single module.
German
-
Amoss -
German Puebla