cps & contification

[Matthew Fluet]

  This message is in MIME format.  The first part should be readable text,
  while the remaining parts are likely unreadable without MIME-aware tools.
  Send mail to mime@docserver.cac.washington.edu for more info.

---559023410-851401618-980348335=:1072
Content-Type: TEXT/PLAIN; charset=US-ASCII


> So the upshot is that on all the examples, the new analysis is at least as
> precise as call based, continuation based, or both, right?  

Correct.

> And we believe that
> will always hold, right?

Yes.  The theorems below show that A will always match or improve upon a
safe analysis B whenever B(f) = Uncalled or B(f) = j in Jump.  So A will
always match the continuation based analysis (modulo some of the
implementation details; e.g., the current continuation based analaysis
doesn't distinguish between nontail calls with uncalled callers and
nontail calls with called callers, so the new analysis can make more
functions Uncalled). 

Likewise, it should be trivial to show that a function f matching the
criteria for the call based analysis will have A(f) <> Unknown. 

> > On the other hand, there are some interesting properties that can be
> > shown.  If B is a safe analysis and B(f) = Uncalled, then A'(f) =
> > Uncalled and A(f) = Uncalled.  Likewise, if B is a safe analysis and B(f)
> > = j in Jump, then A'(f) <= j and A(f) <= j.
> 
> I like these, and would like to add one more.
> 	If B is safe and B(f) = g then A(f) <> Unknown

Nice.  I'll think about it a little more.

> > Here's an updated contify.fun with the new analysis.  I checked into logic
> > a little more (tweaking checkDominators to run just before contify and
> > print out the call graph was useful, rather than tracing 47 functions by
> > hand), and it looks pretty clear that the mutual recursion can't be
> > moved into the local functions.
> 
> Can you send the graph?  You know about dot, right?

Sure.  I'm also including call-graph.{sig, fun} which is a modified
version of checkDominators which creates the call graph with nontail call
edges labeled with the continuation.  This makes it a little easier to
think about what the contification analysis is doing on particular
functions.  Of course, it results in many more edges on the graph.

In all three passes, all of the functions which are contifiable by the new
analysis want to be contified in x_49.  Probably the easiest example is to
look at x_0, x_1, and x_49.  We have
(x_49, x_0), (x_49, x1), (x_0, x_1), (x_1, x_0), (x_1, x_49) in T
The problem is that x_0 and x_1 are mutually recursive, but there are
outside calls from x_49 to each of them.


---559023410-851401618-980348335=:1072
Content-Type: APPLICATION/octet-stream; name="call.tgz"
Content-Transfer-Encoding: BASE64
Content-ID: <Pine.SOL.3.95.1010124095855.1072A@yodel.cs.cornell.edu>
Content-Description: 

H4sIAHDsbjoAA+1cbY8buZHer9av6Ew+ZAaYKE0WX7odeIFg4+Ry8NmL9V4+7GJgKBqNrY0sTWY0
t7tw5r9fN4uUqiiy9vaDvbdAE7BH7IeserpYfC1Ky8Vm8/u3d4vbd/Obh+1nHyWptnXGNJ81jQIP
9G9IrtVt03gNYJ3V2g2wBms/a9qPQ4enh/v94q5pPrvZPKz2Qrmfwn+laWj05X5313wx+MFfRzdo
zl8/bb7404sXb/761Z++/I83r7/+6r+/+Pr1BX3YPGtm9/u7h+V+NtvdrrbN61nMP9ytGhTzrPnz
+m613K+uQ3622S0Xm9nQ3KECPltvxwfHmi9316uh4viHA8+v347A+Ge22l7PZv+z2DTBa18+vH/a
rLf75m51M5QY/29ns+Gtms3ix93DPr7T28tmu3i/Gv4fZL8Mn1aDsPHTRfNsVLa+aW4Wm/ugeEj7
dwPL84sxtzo+/ct6s5p/v96/e/Wwj4/Ol7vtcrFvvj37w/797R++Obts/rbdz/e71/u79fZtc/6b
xPPisjmbnyUiZ/Pr3f7s6rKJcpqbbTPwbZ59nh5sVvvZE2qv+YvwSn/eJd3Di48l8PF8+Hc7CDjH
F28+vI3t8PZy9mRIzX6934xWDPrx0e52v95t74eH317FR6NZXh0eD6SGKp+PXJDI8wMcig8VEpNm
ubhfHazarCIeCuxumpevXj4fJX17RYHm383rV//1vPmOPRyLvVj8Y7VpvrviaobGjzzHhmQ8t4zn
ywNc5pn8oNl+LJ6PgejYphdjI/2xGXxmvl19v1lvV+PT2bHoBXrs8t1q+c/m/LZZ3Ddf3u2G9ns/
/7r5ELro+J6XzfvFenvZzOfzx+i1o4+gmLFHvBksMTrfers89A4CJ4dAZxqojA5O8A9vB+s9C6b5
2/Zm9zQYcb5vfv9582F0mqfNXwYq8/3j4LTji96H4sP/L2ONx4HUk5H67epu/+N8EPd6tX+1Xa6a
8yDqdrO+36NZQjqUXG/X+68W66Fdzs+S+rNRS7RpqI1+fXFxynh0OmQ8uidj/J8P72/n++joY5NQ
3s9jPYF3EPh/4p1IVHg3u0hud1Ey+tjI+ApoY3yFoXpqhcdTks15KHtg1xTYDSWOyPnQTW5iN5lF
bx05bKlThEE4uAot8oa3dHM++GEw8cj98SIUHfpWoDz60GN4Mvo2ba/xLeMg/9tQcnd48Rn34+FV
/74aZ6b5ze5utVgOZAb6h54wtuPNFhlcNv/YXf+I3SK07+EFg8q73fto36B5rDF7chw+nzz/4Tbp
GCfB4cl5kDeabVQx1rxshlF+P/bLcXhIqp4QVc2R/X5H9Y0fOL7CyexDYjb8uUymDnX3u8dUY01a
b5ihXgwtPV/9MPx/j96I/er+Yblc3d/v7u6P0nBGCYN3KLP618MwvZ1HH2wGqw2eeHTpkBbb66HM
btb8dDoPo+hvgwecJ9dvVhez4yBIBtNhIl8R5DCa/m4Ew7R7gVzStBtmouHxwVOD4Q5uuri+DkuC
8+CnOJeTl1njoE56+MDx6K8jq0dSfFxRxM/p47/zdke+U8v/3JbHNVWt6cPoHPkNxv3udxef0g+Q
SN0TLmbHxxfZ+JQtL1F9FHQ2rHQ3Z4dsWpvgcmT+fnF7fh5U76IVd4cp96LZokNExTgXxKXkRd66
VGCSlBrkolkxSTgPJklhTMbVd9PczuKbj/9+6f3IlD5tWh73//frtx9Hx0/s/xvQ6rj/hzbs/3U7
7f8/Rdr/eLsK+2fcOYTdxGzwhO0ibLxPDwLGvf9QZigyS4PscvMwTHdffPn6zddfPX+eRpOilHrt
E0WxABl2w/7o6WFrFNbIh0xS+0sb9FeWvlHzcQgYDyM+mg65/yvnrT32fzue/ymnpv7/SdL1Gk8F
RidoPsw24TTjWVzCzLZt8+3h0Wa3u33Tnl2NT4eeN2LDZ5WXUGfh6VhChRI6L6HPwtMo44C9QOEI
6FAVCLxb3mMBCAUMq6mOAISaNqsZCthQwLGa+gjYUNNnNUMBHwp0rCYcAR9q9lnNUKBHS/AXNUek
RyuqrG4ooaIZNatsKYQmZiV2S7ST0lmRJGvMtbwCNlpLGbUH4kOu48WDTTry6l2yz/DZ8bLBCo4Y
2KVWGD4bXja8tSHNaFJbj4yoN/wQ3xHbXMUShpXAl0IRyqYSIedYzrNcx3I9zemW5RTLaZYDljMs
x7hoxkUzLppx0YwLMC7AuADjAoyLYjlgzIAxA8YMGDNgzIAxM4yZYcwMY2YYF8O4GMbFMC6GcTGM
i2FcLONiGRfLuFjGxfLxxZ1VIU8h5AzcD0NvgVjCpRIh51kO3wO4n4f+A1BS3dWhnkKRlWVyQ18D
y1hZxsoyVprVDoMQ6JJq1QqYoljk5ZjkYGpwjJdjvBzjpVjt0Bqgirq1gAHFIi/PJKOxPePlGS/P
eLWsNrZHW9RtBMxSLPLq+CiH5u4YsY4R6ygx3fPqoUV0X9TuBMxTLDLLRKPBe8asZ8x6xix7sdAm
uitq7wSspxgyM7w10OSmpcxSzrNcZMZdAVtF+5J23QqYolhkxv0XTW4UY6YYM8WY8c4TW8UVtWsB
A4pFZrzHo8mNZsw0Y6YZMz7cxFaxRe1GwCzFIjM+QqLJDTBmwJgBY5YNz9gqxcFdOwHzFIvMMtHB
5IYN/YYN/YYN/Tp7MWyV4gCvOwHrKRaZ8eZAkxs2/Bs2/Bs2/GvuDLFVimM8tAKmKBaZcRdGk5vo
in0qQpnFFSRO7Zp3oNgqxVEetIABxSIz3u2jyflQEm1dHL3BCJilWNTHB0A0pCkOcuAEzFMMRVv+
KtgOFkciF1dFfPRGYykcoR0ulUxWJNjMFOcH6ASsp1gkyL0ATWdjS8c9XaY9WNAygiqzIK7bOiaF
tx8ayxbbyLQCpigW3yHTHkxgmXbH+xFawhX7itECBhSzHDMEc1k9K8h0AuYFfZ2gT3g/2wqYquuz
uq7PgiDTCJgV9DlBnxdkdgLW1/W5tq7PqbpMJ/iLE/zFCf7iBH9xgr84wV+c4C9O8Bcv+IsX/MUL
/uIFf/GCv3jBX7zgL17wFy/4ixf8pRP8pRP8pRP8pRP8pRP8pRP8pRP8pcv9ZczxgRoHY9fS4d7x
9RKOya68V+4ErKdYPHfgEyYOxsqzmYSvPHBMtsXVRd8KmKJY1M5nQxzSVXHp3msBA4rxZuypzKwZ
eyvIdALmBX2doK+vy1RtK4Eq0ziaks+xOOfZylmFlkCgYGyZ7BQFrVHcuqjWSKClYHR5WuZh+/16
e/1mf7dYb/C005mD8cZc5n7YhcrHG62TQFbTZmBHQJfX7AWxeDBRA1WmczR01ptx+QR0jcrEXK/u
VjdoGXvcoY25rI0CS4uWzg7TFR5SJLDNQCBgl2GGVjwoDmSzkpaUzO3gqBRLpcRD6pTzLNexXE9z
8ZA65RTLaZYDlmPvoBkXzbhoxkUzLppxAcYFGBdgXIBxUSwHjBkwZsCYAWMGjBkwZoYxM4yZYcwM
42IYF8O4GMbFMC6GcTGMi2VcLONiGZd4SO2og4eYGs7X0f3iYOLyQjhxxxEYuTqfF8IZPE50+Aqu
ywvhcFI+fsMzqBrYUTAba/CMKIIuRpPopm/1w3qPHd7Tnvpusb3erO4OSPAgLlpTLBsC8AAoYkzf
CGL8j4obb2FHXepgcFYHKJiNBnjykkCfgZaC2YiDJyMJzHl6AvpsHAsnF4+luxHf6F88/m/1kDnG
/32I/7dmiv9/ivQz4v8pPkuj/4fP1NvCuoZXxCVc6pj0M90UhxMxXhHPC1OvpZ/pKcNYiN8ViEE3
HPgx1pA+04OocA7FK8Znca6mn0nFeGuArjJwHZLm/yseB4/BaBx646CaFhWHzz35HOPuMaNoRtMM
0IyhGRpsV45mqH5FCSjKQFMGmjLQlIGmDDRloCkD+llTNpqy0ZSNpmyAsgHKBigboGyAsgHKACgD
oAyAMgDKwFAGhjIwlIGhDAxlYCgDw2cFd1ZDPEGQaBbyoVEdcwgKkUVGiurE43LutXjqbUuauzpE
YzmJVbZfPrs6RLrMIYhGWXnGisdNcCQwJdW4q6hgNJKTePEzWYzndIxXx3h1jBffkmBsAYq6tYDR
OE7ixQ+z0dg949UzXj3jxbe42B66qNsIGI3iRF5Z3DpGl1tKLOV6mrPFaExsEVXU7gSMRnESs0w0
DecnZooxU4xZ9mLYJm1ReydgNN6TmGWRUpyPNGOmGTNNmWWBF2yVGHjJtOMytoIpikVm3H/R5PFa
SGIGjBkwZllEHo93uqJ2LWBAscOdFyYar1ewCz3ALvQAv9CTReR7cjyXazcCZil2uPfCxlfsAWwX
B2wXB2wXlx3daXpAlWt3AkaP0hKzTDT2ADb0Axv6gQ392dFVbJXiAI+hzgrWU+xw94WJxh7Ahn9g
wz+w4T+7uBdbpTjGY1C0gtEbf4kZd2E0eboRo1IRyixiMaCYReSxVYqjfAyYljGg2OHyCxONJs/i
7H18WJJpBMxS7HClhc38GF0uDnIxulzGPMWi6CwyG9ohxXfjvTo+ekdjHQ8Hr06uwsTocnF+iNHl
MtZTLBLMIrN4+4FHyDPteGjHCKrMgth9eQg/i++isYpthAGNCqYoFg+SMu14PMoD0LwfoSVssa9g
QKOCAcX4EQWGIuzxSgvFrCDTCZgX9HWCPuH9bCtgqq7P6ro+C4JMI2BW0OcEfV6Q2QlYX9fn2ro+
p+oyneAvTvAXJ/iLE/zFCf7iBH9xgr84wV+84C9e8Bcv+IsX/MUL/uIFf/GCv3jBX7zgL17wl07w
l07wl07wl07wl07wl07wl07wly73l6vTICG+5jEOeHUaRsK3Le+VOwGj4Sdz+lWRFFxm16GyK444
Ipvi2qJvBUxRLH1Xg0kO9i4u23tdh4BAvAF7IjBrPwwrlwW6OuTrurq6rr4qMEaUK5ji2q5OLnXi
LGcqpxNaAoGCKDw7NsEj/nJtI2CWYNHBaZHTWLJlN+zz0Ct2mPJhBsaSayCrmUU3WhrRtXnNXhCL
xxA1UGU6r06uu+IqwrAgGhNDYsnmuB+7OrkDiksOg5bOo8WOYFn8CU8rIpaHoIFgkGGGYAdGgV9W
0JKCnhbsaKanmXjInHKK5TTLAcsZlrMsx0gqxkQxKopx0YyLZlw046IZF824aMaFZTQjphkxzYhp
RgwYMWDEgBEDRgwYMWBcgHEBxgUYF2BcDONiGBfDuBjGxTAuKWhNPfsYWWWXWI+hTnv8Sgl1O9wQ
2/JYqkSQ3o7NRwo8z6npHPtSMZo5pZ+bvoFfOv6r9TBpHOO/bvz9B2W9muK/nyJN8d//v/FfatN4
sbaMkejhryZUzALC1bAxCxWfvLcXbNIJWF/HcDNVwZSAaQEDATMCJrR5T9qchdCzgq4qghhPF799
RoOWWd2uDtGvniW5ha8Ox6Bj/lqtgNGvjiXJhS//xqBhXlsLGP3qV5Jc+Pqubou1jYDRL3mlL/OX
vn+rij8TgRuKCuYJlkSXvkAbw24nnUDAeoIl0aVvwCpfqh5jlGVMESyJzgZKGvjKq2sBo3fdk+jS
d1BV8a6vNgJGr2off5OBitbsxyay6k7A6M8HJNGlb4GqYm+LQaMy1hMsiS59jVMV+xu0AqYIFkVn
IaD+eKSV//iJrkPkJ1PYxY0Ud+gPGzQK2bpAV4d8XVdX11V/L4w4lCFV1WV1VZet/4CMNXXI1nW5
ui5fF9jVob6qy7VVXU5VBbq6b7i6b7i6b7i6b7i6b7i6b7i6b7i6b/i6b/i6b/i6b/i6b/i6b/i6
b/i6b/i6b/i6b/i6b3R13+jqvtHVfaOr+0ZX942u7htd3Te6zDeuTm/k4cUmtrbVdImfxcLjHFBc
m7A4eY4BwRKVUsxCF2e1rhMwesMvic6Cy/Sy3ckKwktgR8CsuRSe2yeQN5hu27pY3QqENJ7LazbP
1gMh+ZpW1yESCMlehQZCshehgZBcoKtDvq6rq+vqqwJZIOQEU1zblRSrOKlsBIzEKpJrUcqnsQp9
7L5XpzdN0ZsqS1GQQHpJNTOobulvvJz4oZPEegnsMp1X2bUSEojgP8GWXWQ19FduTrRIYNxkVUAl
gVoCQQKNBFoJdBLoJbCTQMlCWrKQliykJQtpyUJaspCWLKQlC2nJQlqykJYsBJKFQLIQUAsVA2i1
ipL1QLIeSNYDUadkPZCsB5L1jGQ9I1nPSP5lJAsZyUJGspCRLGQkCxnJQuIAZiULWclCVrKQlSxk
JQtZyUKWWSjzaZGPZD0rWc9K1nOS9ZxkPSexdZL1nGQ9J1nPSf7lJAs5yUJOspCXLOQlC3nJQl6y
kJcs5CULeclCXrKQlyzkJQt11ELFCwu1ipL1Osl6nShWsl4nWa+TrNdJ1usk63WS9XrJv3rJQr1k
oV6yUC9ZqJcs1EsW6iUL9ZKFesFC0AoWglawELSChaAVLAQttVDxok2tomA9aAXrQStYD1rBeiCt
4UFaw4O0hgdpPgKpY4NoIWkND2xd59JuplhSMpe0oAdpQQ/Sgh6kBT1IC3qQFvQgLehBWtCDtKAH
aUEPbEFfvCBWqyhZT1rsg7TYB5CsJy3oQVrQg7SgB2lBD9KCHqQFPUgLemALek8dnH3FtJdcX1r3
A1/3KyZHsxywnGE5y3K8IzLWitFWjHcM9qcc46IZF824MOWaEdMcE0cIaZMD0iYHpE0OSJsckDY5
IG1yQNrkgLTJAWmTA2yTo1lj6cLXeI+3+KAcpsZhtwZ2BNT5ryCNLzjdxZvSlKY0pSlNaUpTmtKU
pjSlKU1pSlOa0pSmNKUpTWlKU5rSlKY0pSlNaUpTmtKUpjSlKU3pk6b/Bf/a45oAoAAA

---559023410-851401618-980348335=:1072--