Re: Interpreted Basic control-flow analysis
- From: "Gene" <gene.ressler@xxxxxxxxx>
- Date: 4 Jul 2006 20:44:00 -0700
Arthur J. O'Dwyer wrote:
On Tue, 3 Jul 2006, Gene wrote:
Arthur J. O'Dwyer wrote:
I've thought of recursively simulating a run through the program,
taking both branches at each decision point, and keeping control
stacks for each thread so I always know where each "End" goes. But
that needs a way to detect and avoid infinite loops. The only way
I've thought of is to avoid duplicating any (line number, control
stack) state; but that involves keeping arbitrarily large amounts
of data [...]
(Trim, please!)
Unfortunately this problem is undecidable. You can't write a program
that will give the right successors in all cases. But you can get a
useful approximation.
Yes; as I said, I'm looking for an approximation that's "as conservative
[read: sloppy] as possible" without being outrageously sloppy. Mainly
because expression-parsing is really hard, and so I'm trying not to
do it; but also because I realize that the Halting Problem is
undecidable. ;)
[snip explanation of what to do once I know how to find successors]
The problem as you say is the successors of "End." You can make a big
approximation by saying the first statement in every While body
succeeds every End.. Probably not good enough.
Right. /Too/ sloppy.
You can do better by
making your program prove a theorem. One approach is an analysis
pre-pass to determine which While statements can "reach" each End.
This will be roughly similar to "reaching definitions," which is a
standard compiler dataflow algorithm. It's just interpreting the
program in a different way, attaching sets of reaching Whiles to each
End. Check Aho, Sethi, and Ulman, Principles of Compiler Design.
I'm probably missing or misunderstanding at least half of the
critical part here, but I don't see how reaching definitions are
the right tool here. AIUI, applying reaching definitions to the
following program gives:
1. A no whiles encountered, therefore {}
2. If X:Then gen(If) on line 2, therefore {2:If}
3. B {2:If}
4. While Y {2:If, 4:While}
5. End {2:If, 4:While}
6. End {2:If, 4:While}
That is, we're being too sloppy with the "reaching set" of line 6.
But in order to make that set just {2:If}, we'd need line 5 to know
that it could remove {4:While} --- which implies that we're keeping
the reaching sets in some kind of stack, which means we're not really
doing the textbook kind of "reaching definitions", but something very
close to just "simulating" the program by maintaining a (number of)
control stack(s).
In short, I think you're proposing the same thing I did, but may
not know it. :)
-Arthur
Sorry I should have been clearer about "roughly similar." Here's what
I was thinking. First form the "conservative" control graph with Ends
connected only to the following statement. Associate with each
statement a set of augmented natural numbers for each While in the
program. Initially all sets are empty. The numbers are going to
represent the depth in the stack of the respective while context (stack
top is 0) when the statement is reached. It's a set because (as you
have shown), a single While can have multiple contexts in the stack at
the same time. The augmented naturals are { 0, 1, 2, ... N, <top> }.
Choose N to be any value you like. The higher it is, the more precise
the approximation. <top> is a distinguished value encoding information
about stack elements beyond N.
Now traverse the control graph with a queue of nodes remaining to be
explored in the usual way for flow analysis (breadth first). The rules
for updating the sets after traversing an edge A->B would be
A = If:Then, B = line following Then ->
Let I be a copy of A.sets with all elements incremented by 1; B.sets
:= B.sets merge I
[ model pushing the If context on the stack ]
A = If:Then, B = line following next End ->
B.sets = B.sets merge A.sets
A = Goto L, B = Lbl L ->
B.sets = B.sets merge A.sets
A = While: B = first line of body
Let I be a copy of A.sets with all elements incremented by 1;
B.sets := B.sets merge I and also insert 0 into the set for this
While.
A = While: B = first line following next End
B.sets = B.sets merge A.sets
A = any statement, B = End ->
For any set in A.sets containing a zero, add an edge (if not already
there)
to the graph from End to respective While (and queue the While for
further search). Remove these zeros. Let D be a copy of A.sets
decremented by 1. B.sets := B.sets merge D
By "merge" I mean form the union of respective While sets. "Increment"
is generalized with N + 1 = <top>. Decrementing <top> adds N to the
respective set, but <top> remains in the set. I.e. <top> in a set
means that there's an unknown set of contexts (though perhaps none) for
the respective While in positions N+1 and deeper in the stack.
Keep traversing the graph until you dequeue and visit a node the second
time with no changes to any set or to the graph.
The traversal must terminate because the sets can't grow forever; nor
can the graph. I have not worked through a proof of correctness (or
even an example!), but this representation of all possible stack
configs seems powerful enough to get a sound algorithm even if what
I've written above is not.
Happy to discuss further.
.
- References:
- Interpreted Basic control-flow analysis
- From: Arthur J. O'Dwyer
- Re: Interpreted Basic control-flow analysis
- From: Gene
- Re: Interpreted Basic control-flow analysis
- From: Arthur J. O'Dwyer
- Interpreted Basic control-flow analysis
- Prev by Date: Re: Deleting every mth element
- Next by Date: About implementing RegEx & pattern-match using finite automata
- Previous by thread: Re: Interpreted Basic control-flow analysis
- Next by thread: Re: Interpreted Basic control-flow analysis
- Index(es):
Relevant Pages
|
