SB CSE 675Fall 2000 Program Transformation and Program Analysis Annie Liu Solution 10 Handout S10 Dec. 13, 2000

Problem 1.

```   rules:   dx, strict op.	\dE-

s := {}		E':= {}

s with:= y		E'(f(y)) +:= 1

s less:= y		E'(f(y)) -:= 1

f :={}		E':= {}

f(y):=om		if y in s then
E'(f(y)) -:=1

f(y):=z		if y in s then
E'(z) +:= 1

Note that, same as in rule M2 in paper, we assume that any use of
E'(z) for which z is outside the domain of E' has the value 0 and
that any assignment of 0 to E(z) removes z from the domain of E.

Otherwise, we just need to add the corresponding code, in particular,
for s with:=y, we have if E'(f(y))=om then E'(f(y))=1 else E'(f(y)) +:= 1.
for s less:=y, we have if E'(f(y))=1 then E'(f(y))=om else E'(f(y)) -:= 1.
```

Problem 2.

```   No.  Either way we get \dE2,E1 = \dE2<\dE1> \dE2<\dE1>
```

Problem 3.

```   Change the expression [[U,X],W] to [[U,W],X].
```

Problem 4.

```   It is easy to see how this cycle test problem is similar to the
tree center problem and the topological sort problem.

given:
program cycle1;
...
s := domain e;
while exists x in s| e{x} * s = {} loop
s less:= u;
end loop;
...
end;

canonical forms:
s*t --> {x in s| x in t}
s={} --> #s = 0
exists x in s --> exists x in {x in s}

B: while exists x in {x in s| #{y in e{x}| y in s} = 0}
s less:= x;

expensive computations:
E1 = {y in e{x}| y in s} nodes in s that are successors of x based on e
E2 = #E1 number of above
E3 = {x in s| E2=0} nodes in s that have no successors

auxiliary expressions:
E1 is needed for any x in s
E2 too
E4 = {[y,x]:[x,y] in e}

maintain:
for E1: succ = {[x,y] in e| y in s} so succ{x} = E1
for E2: nsucc= {[x,#succ{x}]: x in domain succ} so nsucc(x) = E2
for E3: tail = {x in s|nsucc(x)=0}
for E4: pred = {[y,x]:[x,y] in e}

FD:
\d succ, nsucc, tail, pred<B>
=\d nsucc, tail, pred<\d succ<B>> -- chain rule
1. insert \d-succ<s less:=x> before s less:=x
= for u in domain e| [u,x] in e -- rule D2
succ{u} less:= x;
= for u in pred{x} -- can be viewed \d pred
succ{u} less:= x;
2. replace {y in e{x}| y in s} by succ{x}
B1: while exists x in {x in s | #succ{x} = 0}
for u in pred{x}
succ{u} less:= x;
s less:= x;

=\d nsucc, tail<B1>
=\d tail<\d nsucc<B1>> -- chain rule
1. insert \d-nsucc<succ{u} less:=x> before succ{u} less:=x
= nsucc(u) -:= 1 -- rule M2
2. replace #succ{x} by nsucc(x)
B2: while exists x in {x in s| nsucc(x) = 0}
for u in pred{x}
nsucc(u) -:= 1;
succ{u} less:= x;
s less:= x;

=\d tail<B2>
1. insert \d-tail<nsucc(u) -:= 1> before nsucc(u) -:= 1
= if nsucc(u)=1 then
tail with:= u;
insert \d-tail<s less:= x> before s less:= x
= if nsucc(x)=0 then
tail less:= x;
2. replace {x in s| nsucc(x) = 0} by tail
B3: while exists x in tail
for u in pred{x}
if nsucc(u)=1 then
tail with:= u;
nsucc(u) -:= 1;
succ{u} less:= x; -- stmt and succ not needed (see later)
if nsucc(x)=0 then -- cond always true, since x in tail
tail less:= x;
s less:= x;
```