Lecture 3: Galois Connection A. Pnueli Foundations of Abstract Interpretation, Lecture 3 Taken from Lecture II of David Schmidt. Program Analysis, NYU, Spring, 2004 6 Lecture 3: Galois Connection A. Pnueli Galois Insertion A Galois connection is called a Galois insertion, if . Every Galois connection can be lifted to a Galois insertion, by identifying every two abstract elements which have the same concretization. is a Galois connection which is not an insertion. In Assume that this case, there must exists two distinct abstract elements , such that . Composing to both sides of the equality, we obtain . Thus, a non-insertion connection is possible only if we have two distinct abstract elements with the same -mapping. be a non-insertion connection. Define to be a new abstract Let where 2 -elements are domain whose elements are equivalence sets over equivalent if they have the same -mapping. For each , we define , where is any member of . . For every is defined by Ordering over the adjunct mapping can be defined by , % % $ $ ! is a Galois insertion. Program Analysis, NYU, Spring, 2004 & " # " ! It is not difficult to show that 7 Lecture 3: Galois Connection A. Pnueli Subset Structured Abstract Domains Earlier, we restricted our attention to the case that the concrete domain has the . For such a case, it is possible to specify a Galois connection by a structure relation , provided it satisfies: and & % $ ! An additional useful restriction is the case that the abstract domain also has the structure , where is an unordered domain of individuals. In this case, it in order to obtain a is sufficient to specify an abstraction function Galois connection. Such a function induces a relation given by . The above two closure requirements are translated into the following valid properties: % $ gives rise to the Galois It follows that the specification of a structure connection , where ! and , for every . % $ ! , for every . % $ ! Program Analysis, NYU, Spring, 2004 8 Concrete and abstract operations by , we must model , by abstract computation Now that we know how to model concrete computation steps, . steps, , and concrete operation, . , and abstract operation, , defined as We have abstract domain, Example: We have concrete domain, , defined as : must be consistent (sound) with respect to if , then #" ! #" ! % $ & ' #" ! #" ! , where relates numbers to their parities (e.g., , etc.). 4 )*+, 0 2 201 /-. ( #" ! #" ! , for implies We want soundness: and all . , we ! #" Since we have the Galois connection, know that . So, soundness is stated equivalently as , , for all for all and this is equivalent to saying, $ #" ! , for all that is, $ #" ! . is , where for all This is interesting, because it states a commutative, “semi-homorphism” property.... 4 )*+, 2 201 /-. ( Definition: For Galois connection, , and functions , is a sound approximation of iff for all iff for all This slightly abstract presentation exposes that is a “semi-homomorphism” with respect to and : α(c ) f# f f( c ) c α α α ( f( c ) ) f #( α ( c ) ) , 4 4 )*+, 2 201 /-. ( #" ! succ # succ * any any {3,4} α any α {2,3} : We have that #" ! where Galois connection: implies Example 1: 4 )*+, 1 2 201 /-. ( & & #" ! & & & & & & & & & & & & & & # " div2 # div2 * any odd {3} α even {6} α : We have that #" ! where Galois connection: implies Example 2: 4 )*+, 2 201 /-. ( Lecture 3: Galois Connection A. Pnueli Lifting Functions For Subset Structured Domains Consider a subset-structured abstraction . With each operation , we associate a corresponding abstract operation . Both are extended point-wise to set arguments. and , for all is a sound approximation of The abstract operation iff iff Program Analysis, NYU, Spring, 2004 , for all 9 Synthesizing from acts as a “semi-homomorphism” The previous slides show how between and . Given the Galois connection, , and operation, that is sound with respect to is most precise , the . is sound with respect to iff Proposition: $ # $ # .) ! ! , " iff for all ! (Note: Of course, has a mathematical definition — not an algorithmic might not be finitely computable ! one — , (+ (* $ (+ ' %&' $ # (*)# ' %&' , + 210 / 3 .+- ' %&' Parity example continued: $ # + 6 7 7 120 45 / .+ 3 D 9:;< E BB@A ?)=> 8 One more example: . ! ! *7 ! $ ! # ! $ # $ ! # *7 , . , . . " 3 - # / +$ + *7 *7 *7 # $ . . . *7 *7 , . The operation loses precision: Hence, , we have and Given , 3 . *7 # $ 3 . (* (+ , but , . (+ $ $ $ # # )(*# *7 *7 )(*# (+ $ . 3 $ - # . . *7 , 1 +! 5 - . 3 Nonetheless, this is the best we can do, given the crude structure of the abstract domain, Parity . D 9:;< BB@A ?)=> 8 Lecture 3: Galois Connection A. Pnueli The Best Sound Approximation Claim 5. The function smallest sound approximation. is a sound approximation of and is the . Observe is sound, we have to show To show that Proof: that . since we are considering insertions in which be any (other) sound abstraction. Being sound, it satisfies Let , we obtain Composing both sides with on the left and canceling . . . is given by For the case of subset-structured abstractions, Program Analysis, NYU, Spring, 2004 10 Completeness with respect to as is forwards ( ) complete with respect to iff , we state soundness of iff Given Definition: is backwards ( ) complete with respect to iff Definition: The two completeness notions are not equivalent! For an to be (forwards or backwards) complete, it must equal . Indeed, the structure of the Galois connection and determines whether is complete. ) * ' '%& #$!" Forwards ( ) completeness: is forwards-complete iff maps image points of to image points of — . f f Backwards ( ) completeness: is backwards-complete iff maps all points in the same -equivalence class to points in the same -equivalence class — implies . f ) ' '%& #$!" Lecture 3: Galois Connection A. Pnueli Illustrating Forwards and Backwards Completeness div2 even is forwards complete, because div2 odd any. even. div2 maps image is not forwards complete, because succ odd succ is forwards-complete iff Forwards ( ) Completeness: points of to image points. Backwards ( ) Completeness: is backwards-complete iff maps all points in the same -equivalence class to points in the same -equivalence class maps individuals in to individuals. iff odd even and is backwards complete, because succ even odd. succ succ div2 is not backwards complete, because odd div2 Program Analysis, NYU, Spring, 2004 even even though div2 even. 11 Transfer functions generate computation steps to has an ), which This defines a computation step of the form, Each program transition from program point associated transfer function, (or describes the associated computation. . has the transfer . For example, Example: Assignment function, . For modelling multiple transitions in conditional/nondeterministic choice, we attach a transfer function to each possible transition. # " !" , * % + ( % ) & '&% $ $ Example: For * ( , % % / .# < 1234 = ::89 756 0 For we have these functions: if $ % # " !" , + * % ( % ) $ &'% otherwise * ( & $ , $ - if % % % - / .# otherwise , because , but , because . The transfer functions “filter” the data that arrives at a program point. % $ For example, % % - % % $ , that produce “no data” ( ). We ignore computation steps, An execution trace is a (possibly infinite) sequence, , such that, for all : . equals no 1234 8 9 ::89 756 0 s to build sound, abstract trace trees Using the 0 /01 . . - , + "! abbreviates p4 : exit Note: } p0 : while (x != 1) { p1 : if Even(x) p2 : then x = x div2; p3 : else x = 3*x + 1; 2 #$ #% #$ #% #$ #% &% ' Each concrete transition is generated by an ; each abstract transition is generated by the corresponding . &% ' ) ) ( ) ) ( * 39 1234 ::89 756 0 , is reproduced by a , where . / - - - - - is interpreted concretely by and is interpreted abstractly by . - For example, Each concrete transition, corresponding abstract transition, The traces embedded in the abstract trace tree “cover” (simulate) the concrete traces, e.g., this concrete trace, - is simulated by this abstract trace, which is extracted from the abstract computation tree: - - , are , and indeed, all concrete traces starting with simulated by the abstract tree in this manner. <9 1234 ::89 756 0 Proof of soundness of trace construction implies iff . iff iff iff , say that Lemma: and For ' . , there exists an , . Theorem: For every concrete trace, , such that for all abstract trace, Proof: We use the Lemma and induction to assemble this diagram: & & & & & & (Note: each in the diagram is more precisely stated as , because .) Due to imprecision of the s, the abstract , but there trace tree may possess many traces that begin with is always one trace in the tree that simulates the concrete trace. ' 1234 9 9 ::89 756 0 When all the operations, , are complete with respect to the previous result is strengthened: s, the .) iff . (Similarly, say that iff Say that In both cases, the lemma holds: . .) implies implies ' iff iff ' Lemma: (Similarly, Theorem ( -completeness): When iff , then for every , there exists an abstract trace, , concrete trace, such that for all , . , , , there exists an , . iff Theorem ( -completeness): When then for every trace on sets of stores, , such that for all abstract trace, 1234 9 ::89 756 0 References P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. ACM POPL 1977. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. ACM POPL, 1979. P. Cousot. Slides for invited lecture at VMCAI 2003, New York City. R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. Journal ACM 47(2) 2000. R. Giacobazzi and E. Quinterelli. Incompleteness, counterexamples, and refinements in abstract model-checking. SAS 2001, Springer LNCS 2126. D. Schmidt. Structure-preserving binary relations for program abstraction. In The Essence of Computation: Complexity, Analysis, Transformation. Springer LNCS 2566, 2002. 1234 9 ::89 756 0