La lecture à portée de main
29
pages
English
Documents
Écrit par
Patrick Cousot1
Publié par
chaeh
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe en t'inscrivant gratuitement
Découvre YouScribe en t'inscrivant gratuitement
29
pages
English
Ebook
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Comparing the Galois Connection
and Widening/Narrowing Approaches
to Abstract Interpretation
1 2PatrickCousot andRadhiaCousot
1 LIENS,DMI,ÉcoleNormaleSupérieure,45,rued’Ulm,75230Pariscedex05
(France)
cousot@dmi.ens.fr
2 LIX,ÉcolePolytechnique,91128Palaiseaucedex(France)
radhia@polytechnique.fr
Abstract. The use of infinite abstract domains with widening and -
narrowing for accelerating the convergence of abstract interpretations
is shown to be more powerful than the Galois connection approach re
stricted to finite lattices (or lattices satisfying the chain condition).
1 Introduction
Awidely-heldopinionisthatfinitelattices(orlatticessatisfyingthechaincondi
tion,i.e.,suchthatallstrictlyincreasingchainsarefinite)canbeusedinsteadof
wideningsandnarrowingstoensuretheterminationofabstractinterpretations
ofprogramsoninfinitelattices.Weshowthat,ingeneral,thiscanonlybetothe
detrimentofprecisionandprovethattheuseofinfiniteabstractdomainswith
wideningsandnarrowingsismorepowerfulthantheGaloisconnectionapproach
forfinitelattices(orlatticessatisfyingthechaincondition).Bywayofexample,
variouswideningsaresuggestedforsolvingnon-convergenceproblemsleftopen
intheliterature.
2 Upper Approximation of the Collecting Semantics
Following[CC76,CC77a,CC79b],theabstractinterpretationofaprogramcan
beformalizedastheeffectivecomputationofanupperapproximationAofthe
collecting semanticsoftheprogram.
This collecting semantics can often be specified as the least fixed point
con1lfp (F) of a continuous operator F ∈ L −→ L on a cpo L(, )greater⊥-
2thana basis⊥- satisfying⊥- F(⊥-).ByKleenefixpointtheorem(Prop. 23in
nthe appendix), lfp (F) is the least upper bound F (⊥-)ofthe iterates⊥- n∈IN
def defn 0 n+1 nF (⊥-)definedbyF (x)= xandF (x)= F(F (x))forallx∈L.
This work was supported in part by Esprit BRA action 3124 “Sémantique”.
1 Monotony is sufficient by considering transfinite iterations [CC79a].
2 -The basis⊥ is often the infimum⊥ of the cpo, in which case lfp F is written lfpF.⊥-270
3ThisapproximationAmustbe soundinthesensethatlfp(F)A .
Example 1 ((Imperative programs)). Assumethatthecollectingsemanticsofthe
following Pascalprogram:
program P;
var I : integer ;
begin
I := 1;
while I <= 100 do
begin
{I ∈ [1, 100] }
I := I + 1;
end;
{I=101 }
end.
isthesetofpossiblevaluesofintegervariable Iwhenstartingexecutionofthe
loopbody.Itistheleastfixedpointlfp(F)=lfp (F)={i∈ZZ|1≤i≤100}∅
ofthecontinuous(andevenadditive)operator:
con .F ∈L −→L = λX ({1}∪{i+1|i∈X})∩{i∈ZZ|i≤100} (1)
onthecompletelatticeL=℘(ZZ)(⊆,∅,ZZ,∩,∪)whereZZisthesetofintegers
and℘(S)isthepowersetofthesetS.
Asound upper approximationisthe loopinvariantA= {i ∈ ZZ | i ≥0}
specifyingthat Iisnon-negative.
Example 2 ((Logic programs)). Let Pbealogicprogram(containingatleast
none constant), B be its Herbrand universe over a family F = F ofP n∈IN
nn-ary functors f∈F and ground(P) be the set of all ground instances of
con
clausesin P.The immediate consequence operator is T ∈℘(B ) −→℘(B )P P P
suchthat:
.T =λX {A |A←B,...,B ∈ground(P)∧∀i=1,...,n:B ∈X} .P 1 n i
A modelofPisasetI⊆B ,suchthatT (I)⊆I.ThecharacterizationtheoremP P
ofvanEmdenandKowalski[vEK76]showsthatP hasaleastmodelM intheP n
completelattice℘(B )(⊆,∅,∪)suchthatM =lfp T = T (∅). P P P P∅ n∈IN
Example 3 ((Functional programs)). Following [CC92c], the relational seman
ticsofthefunctionalfactorialprogram:
f(n) ≡ if n = 0 then 1 else n ∗ f(n − 1);
def
isf ∈℘(IN ×IN ),whereIN =IN∪{⊥}and⊥representsnon-termination,⊥ ⊥ ⊥
suchthat:f ={ ⊥ , ⊥ }∪{ n, ⊥ | n<0}∪{ n, n! | n≥0}.Itistheleast
con
fixpointlfp F ofF ∈℘(IN ×IN ) −→℘(IN ×IN )suchthat:⊥ ⊥ ⊥ ⊥⊥-
F(f)={ ⊥ ,⊥ }∪{ 0,1 }∪{ n,n∗ρ | n−1,ρ ∈ f}
3 Although commonly satisfied, these hypotheses on the definition of the collecting
semantics and the specification of the approximation are stronger than strictly nec
essary, see a discussion of various weaker hypotheses in [CC92b].
271
where⊥−ρ=ρ−⊥=⊥and⊥∗ρ=ρ∗⊥=⊥.Thesemanticdomain℘(IN ×⊥
-IN )(,⊥-,,)isacompletelattice,where:⊥
def
⊥- =IN ×{⊥}⊥
def-=IN ×IN⊥
def - -f f =(f∩ )⊆(f ∩ ) ∧ (f∩⊥-)⊇(f ∩⊥-)
def - f = ∪ (f ∩ )∪∩ (f ∩⊥-) .i∈ i i∈ i i∈ i
Observethatff ifandonlyiff producesmoreoutputresultsinINthatf
foragiventerminatingornon-terminatingargumentinIN andf terminates⊥
morefrequentlythanf.
3TheGaloisConnectionApproachtoAbstract
Interpretation
Principle ofthe Approach. TheGalois connectionapproachtoabstractinter
pretation[CC76,CC77a]formalizestheideathattheequationX =F(X)can
mon
befirstsimplifiedintoX=F(X),whereF ∈L −→LandL(,)isaposet,
-andthensolvediterativelystartingfromthebasis ⊥.Thetechniqueconsistsin
understandingLasadiscreteapproximationofLandinextendingthisnotion
ofapproximation,invariousways,tosemanticdomainssuchasproductsL×L,
powersets℘(L)andfunctionspacesL −→L[CC77b,CC79b].
Galois Connection. ThecorrespondencebetweenthesemanticdomainLandits
abstractversionLcanbeformalizedbyaGaloisconnection(alsocalled pair of
adjoined functions).
Definition 4.*IfL()andL()areposets,thenα,γisa Galois connec
γ
−tion,writtenL−L,ifandonlyifα∈L −→Landγ∈L −→Larefunctionsα
suchthat:
∀x∈L,y∈L: α(x)y ⇐⇒ (xγ(y)) . (2)
α(x)isthe abstractionofx,i.e.,themostpreciseapproximationofx∈LinL.
γ(y)isthe concretizationofy,i.e.,themostimpreciseelementofLwhichcan
besoundlyapproximatedbyy∈L.
Example 5 ((Intervals)). In[CC76],℘(ZZ)orderedby⊆isapproximatedusing
the abstract lattice of intervals L = {⊥}∪{[ , u ] | ∈ ZZ∪{−∞}∧u ∈
ZZ∪{+∞}∧≤u}orderedby,suchthat:
def
⊥ [ ,u ] =true
(3)def
[,u ][,u ] = ≤ ≤u ≤u .0 0 1 1 1 0 0 1
ThisapproximationisformalizedbytheGaloisconnectiondefinedby:
γ(⊥)=∅ α(∅)=⊥
γ([ ,u ])={x∈ZZ|≤x≤u} α(X)=[minX,maxX] .
Forexampletheset{1,2,5}∈℘(ZZ)issoundlyapproximatedby[1,5]∈L. 272
Soundness and Precision. Here,theconcreteandabstractnotionsofsoundness
andprecisionareformalizedinthesameway,bytherespectivepartialorders
on Land on L. x y is interpretedas “y is asound approximationof
x”, “xisamorepreciseconcreteassertionthany”or“xlogicallyimplies y”.
Thesamewayxy z meansthaty andz aresoundapproximationsofx
butyismoreprecisethanz.Wemayhavexyandxzbutneitheryz
nor z y in which case y and z are non-comparable sound approximations
of x.Equation(2)statesthattheconcreteandabstractnotionsofsoundness
andprecisioncoincide,uptoanapproximation,whichconsistsinrepresenting
severalconcreteassertions{x|α(x)=x}bythesameabstractassertionx.
Example 6 ((Intervals, continued)). For intervalsconsidered in Ex.5, the con
creteapproximationrelationissubsetinclusion ⊆whereastheabstractap
proximationrelation is definedby(3).For example, {1,2,5}⊆{i ∈ ZZ |
i≥1}and{1,2,5}⊆{i∈ZZ|i≤5}sincetheassertionthatthevalueofa
variablecanonlybe1,2or5duringexecutionismoreprecisethansayingthat
itisstrictlypositive.Theseassertionsarerespectivelyabstractedby[1,5][1,
+∞]and[1,5][−∞,5]buttheseapproximationsarenotcomparablesince
[1,+∞][−∞,5]and[−∞,5][1,+∞].[1,5]isthebestpossibleabstract
approximationoftheconcreteassertion{1,2,5}.
Extension to Function Spaces.Theconcreteapproximationrelation ∈ ℘(L×L)
defcan be extended to the function space L −→ L pointwise, i.e., F F =
∀x∈L:F(x)F (x).TheintuitionisthatF ismoreprecisethanF ifand
onlyifF alwaysyieldsmorepreciseresultsthanF .
Then,theapproximationofLbyLcanbeextendedtotheapproximationof
thefunctionspaceL −→LbyL −→Lusingthefunctionalabstractionαand
concretizationγdefined,asin[CC77b],by:
α∈(L −→L) −→(L −→L) γ∈(L −→L) −→(L −→L)
(4)def def
◦ ◦ ◦ ◦α(ϕ)=α ϕ γ γ(ϕ)=γ ϕ α
suchthat,byProp.25intheappendix:
γmon mon−(L