NetNews Usenet Archive 1992 #20/NN_1992_20.iso/spool/comp/compiler/1553

Internet Message Format | 1992-09-15 | 4.1 KB

Path: sparky!uunet!zaphod.mps.ohio-state.edu!pacific.mps.ohio-state.edu!cis.ohio-state.edu!rutgers!faatcrl!iecc!compilers-sender
From: [e-mail] (P.T. Breuer)
Newsgroups: comp.compilers
Subject: re: Abstract Interpretation Query
Keywords: functional, logic
Message-ID: <[e-mail]>
Date: 14 Sep 92 11:58:11 GMT
References: <[e-mail]> <[e-mail]>
Sender: [e-mail]
Reply-To: P.T. Breuer <[e-mail]>
Organization: Compilers Central
Lines: 81
Approved: [e-mail]

[e-mail] (Steve Masticola) writes:
>[e-mail] (Vugranam Chakravarthy Sreedhar) writes:
>>AI, although nice, is expensive in terms of time and space. I doubt if the
>>concept is being used in any production compilers.
>
>I don't believe that this generalization holds. As I understand it,
>abstract interpretation (please forgive me if I don't use the prejudicial
>term "AI" :-) is a theoretical framework for connecting a program to an
>abstraction of that program, or for generating the abstraction given some
>particular information you'd like to estimate.  The abstraction is
>supposed to have properties that make it nice for data flow analysis
>(monotonic edge functions, etc.)
>
>Standard problems like reaching definitions can be cast in an abstract
>interpretation framework, and it costs nothing in terms of analysis
>time to do so.
>
> If anyone knows differently, please jump in...

I can understand hardly a word of the above, and I have written at least
one paper on A-I, and probably four (it's hard to tell what is and what
ain't A-I). If anyone else feels the same, here's the 2c I owe. I may not
actually know what it is, but I know what I think it is:

I believe A-I is just the interpretation of a program text as something
other than a program. As a type, for example. Or as a control flow graph.
Fin.  That's the end of the mystery.

There are especially nice consequences for the proper treatment of
recursion if the following square diagram appears anywhere:

    thing -AI---> other thing
     |              |
     |              |
     |              |
     V   -AI---> >  V
   one more        yet another thing
   thing


The `'>' (in some sense) at the bottom is important.  For example, I have
often used:

    seq of   ---AI--> seq of
    programs          numbers
    |                  |
    | limit            | limit
    V                  V
    program  ---AI-> > number

and this diagram tells me that my A-I allows me to take limits of numbers
instead of solving for limits of programs. What I get is a lower bound for
the number that I would have got as the A-I of the limiting program.

In my case, the number was associated with a nontermination estimate, and
the sequence of programs was a loop expanded out various numbers of times.

To make the diagrams `make sense', one has to have the right settings
(computational domains, categories, or whatever you prefer as the semantic
substrate) and the right conditions within that setting (here that the seq
is directed and increasing in a limit-complete structure - boy, wouldn't
you just love infinite programs to be meaningless?) But I don't see any
need for jargon or obfuscation! Cognoscenti will see from this that I was
using the lest fixed point semantics for ptograms, and therefore must have
been dealing with a lazy language, but that's by and by. People who use
strict semantics wil talk about `<' where I have `>', and be trying to
prove finite termination, not infinite extension (I was interested in the
program that never stops, because it never hangs).

Now will someone please explain to me what all this has to do with
compilation? Static analysis, I can understand the connection with.
Compilers no. Optimisation, yes.

Peter
-----------------------------
Peter T. Breuer
Oxford University Computing Laboratory <[e-mail]>
Cambridge University Engineering Department <[e-mail]>
--
Send compilers articles to [e-mail] or
{ima | spdcc | world}!iecc!compilers.  Meta-mail to compilers-request.