Comparing the Galois Connection and Widening Narrowing Approaches

Patrick Cousot1

Description

Niveau: Supérieur
Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation Patrick Cousot1 and Radhia Cousot2 1 LIENS, DMI, École Normale Supérieure, 45, rue d'Ulm, 75230 Paris cedex 05 (France) 2 LIX, École Polytechnique, 91128 Palaiseau cedex (France) 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 A widely-held opinion is that finite lattices (or lattices satisfying the chain condi? tion, i.e., such that all strictly increasing chains are finite) can be used instead of widenings and narrowings to ensure the termination of abstract interpretations of programs on infinite lattices. We show that, in general, this can only be to the detriment of precision and prove that the use of infinite abstract domains with widenings and narrowings is more powerful than the Galois connection approach for finite lattices (or lattices satisfying the chain condition). By way of example, various widenings are suggested for solving non-convergence problems left open in the literature. 2 Upper Approximation of the Collecting Semantics Following [CC76,CC77a,CC79b] , the abstract interpretation of a program can be formalized as the e?ective computation of an upper approximation A of the collecting semantics of the program.

• abstract interpretation


• con?? ?


• precise than


• strictly nec?


• approximation relation


• no strictly


• galois connection


• upper approximation

Sujets

• Esprit
• École polytechnique
• Abstract interpretation
• Galois connection

Informations

• Publié par: chaeh
• Nombre de lectures: 21
• Langue: English

Extrait

Comparing the Galois Connection
and Widening/Narrowing Approaches
to Abstract Interpretation
1 2PatrickCousot andRadhiaCousot
1 LIENS,DMI,ÉcoleNormaleSupérieure,45,rued’Ulm,75230Pariscedex05
(France)
[e-mail]
2 LIX,ÉcolePolytechnique,91128Palaiseaucedex(France)
[e-mail]
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