Program Specialisation and Abstract Interpretation Reconciled Michael Leuschel1
Department of Computer Science,K.U.Leuven,Belgium
DIKU,University of Copenhagen,Denmark
Abstract
We clarify the relationship between abstract interpretation and program specialisation in the context of logic programming.We prent a generic top-down abstract specialisation framework,along with a generic correctness result,into which a lot of the existing specialisation techniques can be cast. The framework also shows how the techniques can be further improved by moving to more refined abstract domains.It,however,also highlights inherent limitations shared by all the approaches.In order to overcome them,and to fully unify program specialisation with abstract interpretation, we also develop a generic combined bottom-up/top-down framework,which allows specialisation and analysis outside the reach of existing techniques.
1Introduction郑德雁
Atfirst sight abstract interpretation(,[5,3])and program special-isation(,[7])might appe
ar to be completely unrelated techniques: abstract interpretation focuss on correct and preci analysis,while the main goal of program specialisation is to produce more efficient residual code(for a given task at hand).Nonetheless,it is often felt that there is a clo relationship between abstract interpretation and program specialisa-tion and,recently,there has been a lot of interest in the integration of the two techniques(,[16,11,22].
Indeed,for good specialisation to take place,program specialirs have to perform some form of analysis.For instance,the incomplete SLD-trees produced by partial deduction[20,7]can be en as complete(given the clodness condition of[20])description of the top-down computation-flow.
爱上西雅图In this paper we want to substantiate this intuition and make the link to abstract interpretation fully explicit.We therefore prent a generic(aug-mented)top-down abstract interpretation framework in which most of the specialisation techniques(such as partial deduction[20,7],ecological partial deduction[18,13],constrained partial deduction[15],conjunctive partial deduction[17,10])can be cast.It also paves the way for more refined and 1The work was done while the author was Post-doctoral Fellow of the Belgian Fund for Scientific Rearch(F.W.O.-Vlaanderen).and visiting DIKU,University of Copenhagen. The author’s prent address is:Dept.of Electronics and Computer Science,University of Southampton,Southampton SO171BJ,UK.E-mail:mal@ecs.soton.ac.uk
powerful specialisation,by allowing more refined abstract domains and more refined“abstract unfolding”rules.
However,we will not stop there.The above formalisation will actually make two(additional)shortcomings of most earlier specialisation techniques apparent(already identified ,[16,13]):the lack of side-ways infor-mation passing and of inference of global success information.Recent tech-niques[16,23,22](as well as some earlier attempts such as[21]and[9,6]) have tried to overcome the limitations by incorporating bottom-up abstract interpretation techniques.However,we feel that a fully satisfactory inte-gration of program specialisation with abstract interpretation has not been achieved yet,and we strive to do so in this paper.
培训的目的和意义This integration is not solely beneficial for specialisation purpos.In-deed,as shown in[16,13](for one particular abstract domain),a full integra-tion of abstract interpretation with program specialisation can yield analysis outside the reach of either method alone(and can even be ud to perform inductive theorem proving or infinite model checking).
We thus prent an augmented,combined top-down/bottom-up abstract specialisation framework in which all the earlier techniques(and more)can be cast,and provide thefirst“full-blown”integration of
abstract interpreta-tion and program specialisation,leading towards powerful specialisation and analysis beyond the reach of existing techniques.
2Top-Down Abstract Partial Deduction
In this paper,we restrict ourlves to definite programs and goals(but pos-sibly with declarative built-in’s such as is,call,functor,arg,\==;this allows to express a very large number of interesting,practical programs;one can even implement and u certain higher-order features such as map/3).
An expression is either a term,an atom or a conjunction.We u E1 E2 to denote that the expression E1is an instance of the expression E2.By mgu(E1,E2)we denote a most general unifier and by msg(E1,E2)a most specific generalisation of E1and E2.Also,as common in partial deduction, the notion of SLD-trees is extended to allow incomplete SLD-trees which may contain leaves where no literal has been lected for further derivation.
2.1The Abstract Domain
We denote by Q the t of all conjunctions.Our abstract domain AQ is then a t of abstract conjunctions equipped with a concretisation function γ:AQ→2Q,providing the link between the abstra
ct and the concrete domain.We suppo thatγ(A)is always downwards clod(Q∈γ(A)⇒Qθ∈γ(A)),i.e.we restrict ourlves to“declarative”properties.Also,for reasons that will become clear below,we suppo that all conjunctions in γ(A)have the same number of conjuncts and with the same predicates at
the same position.Obrve that this still admits the possibility of a bottom element⊥who concretisation is empty.
We will denote the fact thatγ(A1)⊆γ(A2)by A1 A2.We also sometimes uγon ts of abstract conjunctions:γ(S)={Q|Q∈γ(A)∧A∈S}.One particular abstract domain,which will often rve for illustration purpos,is the PD-domain where AQ=he abstract conjunctions are the concrete ones)andγ(Q)={Q |Q Q}(i.e.an abstract conjunction denotes all its instances).
2.2Abstract Unfolding
Program specialisation can achieve more efficient residual code—amongst others—by pre-computing certain operations at compile time(which then no longer have to be performed at run-time).In other words,one computa-tion step in the residual program may actually reprent an entire quence of computation steps within the original program.
In the context of logic programming,this can be en as producing a residual clau which,when resolved against,has the same effect as a -quence of resolution steps in the original program.Partial deduction,for example,produces the claus by unfolding an atom A,thereby producing an SLD-treeτfor P∪{←A}.Every non-failing branch ofτis translated into a residual clau by taking the resultant of the derivation.2The resultants can then be ud in a sound manner for any concretisation of ,any instance of A)in the n that resolution will lead to computed answers and resolvents which can also be obtained in the original program.But actually the u by partial deduction algorithms of the resultants is not limited to code generation.,the resultant p(f(X))←q(f(X)).When resolving a particular runtime call p(¯t)with that resultant we will obtain resolvents which are instances of←q(f(X)).Partial deduction therefore also analys(and specialis)the atom q(f(X)).In other words,the body of the residual clau is ud for theflow analysis as a reprentative of all possible resolvents.This multiple u of the residual claus relies on using an abstract domain identical to the concrete domain.
In the more general tting we endeavour to develop,the two roles of unfolding will have to be parated out(as the residual program has to be expresd in the concrete domain).In other words,to speciali an abstract conjunction A we generate:
–resultants H i←B i,totally correct for the calls inγ(A)and
爱不释手意思–for each resultant H i←B i an abstract conjunction A i approximat-ing all the possible resolvent goals which can occur after resolving an element ofγ(A)with H i←B i.
This leads to Definition2.1of abstract unfolding and resolution below.(Ob-rve that the resultants H i←B i below are not necessarily Horn claus. We will discuss the generation of Horn clau programs later in Section2.4.) 2A resultant is a formula H←B where H and B are conjunctions of literals.
First,we introduce the following notations.Given an SLD-treeτfor P∪{←Q}we denote by Q YθτL the fact that a leaf goal L ofτcan be reached via c.a.s.θ.Given a resultant C i=H i←B i and a conjunction Q we denote by
L the fact that mgu(Q,H i)=θ withθ |vars(Q)=θand L=B iθ .3 Q YθC
i
学会减压>减弱Definition2.1An abstract unfolding operation aunf(.)maps abstract con-junctions tofinite ts of resultants and has the property that for all A∈AQ and Q∈γ(A)there exists an SLD-treeτfor P∪{←Q}su
ch that:
L(1) Q YθτL⇔∃C i∈aunf(Q YθC
i
An abstract resolution operation ares(.)maps an abstract conjunction A and a concrete resultant C i to another abstract conjunction such that for all Q∈γ(A):Q YθC
L⇒L∈γ(ares(A,C i)).
i雅思小作文
The⇒part of point1requests that the code generated by aunf(.)is complete while the⇐part additionally requests soundness(as we want to have residual code which is totally correct and not just a safe approximation). We call an abstract unfolding rule conrvative if the⇐part of point1holds for all Q(and not just for Q∈γ(A)).
Example2.2Let P be the following program:
eq([],[])←
eq([H|X],[H|Y])←eq(X,Y)
Let A=eq([a|T],Z)in the PD-domain.aunf(A)={H←B}and ares(A,H←B)=eq(T,Y)where H=eq(X,[a|Y])and B=eq(X,Y) are correct.Also,both remain correct with H=eq(H,[H|Y])but not with H=eq(X,[b|Y]).H=eq([H],[H|Y])and B=eq([],Y)is also incorrect.
Obrve,that in Definition2.1above,nothing forces one to u the same same lected literal positions,same claus)for all the con-cretisations of A.Indeed,this enables some very powerful optimisations not achievable within existing“classical”specialisation frameworks.For in-stance,in the example below we are able to completely eliminate a type-like check from the residual program.
Example2.3Let P be the program from Example2.2and A reprent the t of all calls eq(L,L)where L is a bounded(nil-terminated)list(this can obviously not be reprented in the PD-domain).Then aunf(A)=C1 ={eq(X,Y)←}and ares(A,C1)=P are correct according to the above definition!One can thus generate the residual code:
eq(X,Y)←
Obrve that this abstract unfolding is,in contrast to Example2.2,not con-rvative.In other words the residual code is only sound for concretisations of A but ,for the call eq(a,[]).
3If Q and H
are atoms this is equivalent to saying that←Q resolves with the clau i
H i←B i via c.a.s.θyielding←L as resolvent.Also obrve that for any Q,C i and there is at most one choice ofθand L such that Q;θC
L.
i
Example2.4Let P be the following program:
(C1)p(a)←
(C2)p(f(X))←p(X)
(C3)p(g(X))←p(X)
养生灸Let A reprent all calls p(X)where X has typeτ::=a|g(τ).Then aunf(A)={C1,C3},ares(A,C1)=P and ares(A,C3)=A is correct and by abstract unfolding we are able to safely remove the redundant clau C2.
To more concily express theflow analysis,we extend aunf(.)so that it maps ts of abstract conjunctions to ts of abstract conjunctions in the following way:aunf∗(S)={ares(A,C)|C∈aunf(A)}.
2.3Widening by Splitting
The computationflow aspect of program specialisation could now be per-formed by calculating U↑∞,where U(S)=S∪aunf∗(S).However,it is obvious that,for but the simplest abstract domains,this construction will not terminate and that generalisation is required.
As usual in abstract interpretation,one could imagine to reprent gen-eralisation by a widening functionω:AQ→AQ such that∀A∈AQ: A ω(A).Unfortunately,this is not enough to be able to ensure termina-tion of abstract interpretation in the prent tting,becau all concretisa-tions of an abstract conjunction must have the same number of conjuncts.In other words,no terminating analysis could be produced ,a program containing the clau p←p,p.This is why we need a more refined notion of widening,which involves splitting conjunctions into subconjunctions:
Definition2.5A quence A1,...,A n of abstract conjunctions is an ab-straction of an abstract conjunction A iffγ(A)⊆{Q1∧...∧Q n|Q i∈γ(A i)}.
Obrve that for i=1this condition is equivalent to A A1.Also obrve that this splitting operation does not allow re-ordering of conjunc-tions.It is,however,straightforward to do so.One just has to be careful to u the same reordering for all concretisations(otherwi it will be impos-sible to synchroni the code generation with theflow analysis,cf.the next subction).
We extend the abstraction concept to ts:
Definition2.6A t A is called an abstraction of another t of abstract conjunctions A,denoted by A split A,ifffor all A∈A there exists an abstraction A1,...,A n of A such that all A i∈A .
For example,in the PD-domain, p(X)∧q(X),p(b) is an abstraction of p(b)∧q(b)∧p(b)and we have thus,for example,{p(X)∧q(X),p(b)} split {p(b)∧q(b)∧p(b),p(c)∧q(c)}.
We can now define a more refined widening operator to be a function4ω:2AQ→2AQ satisfying thatω(A) split A for all A.
By using appropriate widening operators it is now possible to ensure termination for any program(we
refer the ,to[18,10,13]on how to deviωin the context of partial deduction).
We also say that a t A of abstract conjunctions is covered iffA split aunf∗(A).Intuitively,this means that A is a complete description of the computationflow(induced by aunf(.))for all concretisations of A.
2.4Generating Residual Code
Generating residual code from the resultants H i←B i produced by the abstract unfolding involves transforming them into Horn claus.This can be achieved by mapping the abstract conjunctions produced by theflow analysis to atoms and then appropriately renaming the heads H i and the bodies B i.
Wefirst introduce the following concepts.A concrete dominator of an abstract conjunction A is a concrete conjunction which is more general than all the concretisations of A.A skeleton for an abstract conjunction A is a maximally general concrete dominator of A.By our earlier assumption that all conjunctions inγ(A)have the same predicates at the same position we know that a concrete dominator(and thus skeleton)exists for all abstract conjunctions.By A we denote some skeleton for A.
We also require that for all A∈AQ and H i←B i∈aunf(A)we have H i A .The requirement prevents gar
bage code(any H i A can never unify with a concretisation of A)and simplifies the construction below.
Definition2.7An atomic renamingρA for an abstract conjunction A is an atom A such that vars( A )=vars(A).Also,for any Q A we define ρA(Q)=Aθwhereθis such that Q= A θ.
In the PD-domain,we might have A=p(f(X))∧q(Z), A =p(X)∧q(Y),ρA=pq(X,Y)and Q=p(f(a))∧q(b).In that caρA(Q)= pq(f(a),b).
Obrve that for all Q A we haveρA(Qθ)=ρA(Q)θ.Also,to avoid name clashes,we will always suppo that for any A=A the predicate symbols ud byρA andρ A are different.
Given a resultant H i←B i∈aunf(A)we can now produce an actual Horn clau by renaming H i and B i.Renaming H i is easy:we just calculate ρA(H i)(which is always defined).If ourflow analysis also contains A i= ares(A,H i←B i)(and thus code for A i will be generated)then renaming
B i is just as easy:we just calculateρA
i (B i).However,suppo that we
have applied a widening step and that we actually did not analy A i but an abstraction G1,...,G n of it.In that ca B i has to be chopped up
4It is of cour possible to give extra parameters toω,e.g.,to take the specialisation history into account.
