CIS 905, Program Analysis, Spring 2003.

Exercise 2.21 from PPA

Design choices

If a shape graph contains some n_X and x in X then (x,n_X) in S (apparently, this does not follow from the invariants 1-5).
Consider the claim made in Example 2.47: that Fig 2.15 denotes the case where x has length >= 2. In order for that claim to make sense, we must assume
1. if (n_V,sel,n_W) in H with V != @ then there must exist a concrete heap pointer from the location represented by n_V to a location represented by n_W;
2. if (n_@,sel,n_W) in H then there may exist a concrete heap pointer from a location represented by n_@ to a location represented by n_W.
Unlike the book (p.114), we use shape graphs to predict the outcomes of tests.

Graph notation

Since all selectors are "cdr", and since it turns out that nothing is shared, we can compactly represent a shape graph as a set of columns of the form

        V           V
             or
        V'

with V ranging over sets of variables.

From this information, we can construct (S,H,is) as follows:

S = {(x,n_V) | exists V occuring in the columns such that x in V}
H = {(n_V,cdr,n_V') | V' is in the bottom of a column with V at the top}
is = {}

We can now iterate the transfer functions, reaching the following fixed point:

Initial configuration (Fig 2.15)

x @ @ @
x is a list with at least two elements

1: y := nil

x @ @ @

Merge with the end of loop body (that is, output from 6)

x @ @ @

y x @ @ @

y x @ @

y x @ z @ @

x y @ z @

y @ z @

z y x @ @ z @ @

z y @ x @ z @

y z @ z @ @

2: not is-nil(x) (true-branch)

x @ @ @

y x @ @ @

y x @ @

y x @ z @ @

x y @ z @

z y x @ @ z @ @

z y @ x @ z @

3: z := y

x @ @ @

yz x @ @ @

zy x @ @

zy x @ @ @ @

zy @ x @ @
identical to previous

4: y := x

xy @ @ @

z yx @ @ @

z yx @ @

z xy @ @ @ @

z @ yx @ @

Realigning the above

xy @ @ @

z yx @ @ @

z yx @ @

z xy @ @ @ @

z @ yx @ @

5.1: t := x.cdr

xy t @ t @ @

xy @ t @

z yx t @ t @ @

z yx @ t @

z yx @ @

z xy t @ @ t @ @

z xy @ @ t @

z @ xy @ @

5.2: x := t

y xt @ xt @ @

y xt @ xt @

z y xt @ xt @ @

z y @ xt @

z y @ @

z y xt @ @ xt @ @

z y @ @ xt @

z @ y @ @

5.3: t := nil

y x @ x @ @

y x @ x @

z y x @ x @ @

z y @ x @

z y @ @

z y x @ @ x @ @

z y @ @ x @

z @ y @ @

6: y.cdr := z

y x @ @ @

y x @ @

y x @ z @ @

x y @ z @

y @ z @

z y x @ @ z @ @

z y @ x @ z @

y z @ z @ @

End of loop (false-branch of 2):

y @ z @

y z @ z @ @

7: z := nil

y @ @ @
y is a list with at least two elements

Torben Amtoft

Initial configuration (Fig 2.15)
x @ @ @		`x` is a list with at least two elements
1: y := nil
x @ @ @
Merge with the end of loop body (that is, output from 6)
x @ @ @	y x @ @ @	y x @ @	y x @ z @ @	x y @ z @	y @ z @	z y x @ @ z @ @	z y @ x @ z @	y z @ z @ @
2: not is-nil(x) (true-branch)
x @ @ @	y x @ @ @	y x @ @	y x @ z @ @	x y @ z @		z y x @ @ z @ @	z y @ x @ z @
3: z := y
x @ @ @	yz x @ @ @	zy x @ @	zy x @ @ @ @	zy @ x @ @		identical to previous
4: y := x
xy @ @ @	z yx @ @ @	z yx @ @	z xy @ @ @ @	z @ yx @ @
Realigning the above
xy @ @ @		z yx @ @ @		z yx @ @	z xy @ @ @ @		z @ yx @ @
5.1: t := x.cdr
xy t @ t @ @	xy @ t @	z yx t @ t @ @	z yx @ t @	z yx @ @	z xy t @ @ t @ @	z xy @ @ t @	z @ xy @ @
5.2: x := t
y xt @ xt @ @	y xt @ xt @	z y xt @ xt @ @	z y @ xt @	z y @ @	z y xt @ @ xt @ @	z y @ @ xt @	z @ y @ @
5.3: t := nil
y x @ x @ @	y x @ x @	z y x @ x @ @	z y @ x @	z y @ @	z y x @ @ x @ @	z y @ @ x @	z @ y @ @
6: y.cdr := z
y x @ @ @	y x @ @	y x @ z @ @	x y @ z @	y @ z @	z y x @ @ z @ @	z y @ x @ z @	y z @ z @ @
End of loop (false-branch of 2):
y @ z @	y z @ z @ @
7: z := nil
y @ @ @		`y` is a list with at least two elements