[CakeML-dev] Pathological modLang programs

[Scott Owens]

> On 2017/03/26, at 03:09, Yong Kiam <tanyongkiam at gmail.com> wrote:
> 
> Hi dev,
> 
> I've been stuck on mod_live for awhile, the main problem seems to be that this is a legitimate modLang program:
> 
> val 0 = fn () => Global 1
> val 1 = ...
> val 2 = (Global 0) ()
> ... Global 1 never read here ...
> 
> In my current set up, I pass a set of live globals from back to front through the list of decs, tracking all the globals that could have been read.
> 
> In the above fragment, this approach would delete the val 1 = ... line because it was never read from back to front. I think only focusing on deleting Dletrecs does not solve the problem either.
> 
> I have two ways around this:
> 
> 1) fallback to a more naive analysis, i.e. walk through all the declarations and keep every global that is ever read. This would not be able to catch chains of dead globals:
> 
> val 0 = ...
> val 1 = Global 0
> val 2 = Global 1
> ... (0,1,2 all dead, but only 2 would be removed)
> 

You could always run the naive analysis multiple times. But this is probably not a good idea.

> 2) go to a more complicated one. Not only do I go back to front, but I also go front to back and track for each global, the set of globals that it can transitively reference. When a global gets added, this analysis would have to add all the globals that can be transitively read via that global. (so when 0 gets added above, it transitively adds 1).
> 
> I didn't particularly like 1 or 2 because 1) seems too naive and 2) seems to difficult (having to deal with termination of the transitive addition).

2 starts to sound more like a traditional dead code elimination pass where you iterate to a fixed point.

> 
> A potential 3rd approach is to essentially type check the entire program and only apply the removal [ass if all the globals happen to point in the right way. i.e. any dec at position n must only mention globals < n. I think that still works in modLang before any complicated knot tying is done.
> 
> Does anyone have better suggestions? Or am I missing something important?

The transition into modLang does the knot typing for top-level mutually recursive functions, so you can have cycles. But since the Dletrecs are still around, it is conveniently marked where the cycles can appear, i.e., they have to be inside of Dletrecs. It’s probably ok to treat each Dletrec atomically, and not worry about missing out on removing part of the Dletrec when the functions weren’t actually mutually recursive.

Scott