Deadcode elimination in boot is not conservative

[elegios]

This is an issue I ran into working on #738 where calls to a (side-effecting) function for marking files to run or not were being removed. I think this is a minimal case that shows the issue:

let testMain = lam f. f dprint in
testMain (lam call. call 1; ())

which when running boot --debug-dead-code-elim pprints as (modulo whitespace)

let testMain = lam f. f dprint in
testMain (lam call. ())

Note that call 1; is removed. The important factor seems to be that we have a function bound via lambda parameter or pattern match, that we then call it, and that we're not in the right-hand side of a let or recursive let.

I'm not entirely sure what an appropriate fix would be. Two options/possible causes:

• miking/src/boot/lib/deadcode.ml

  Lines 10 to 36 in e1cba70

  	(* Checks if a term _may_ have a side effect. It is conservative
  	and returns only false if it is _sure_ to not have a side effect.
  	The 'nmap' contains information (third element of the tuple) if
  	a symbol may contain a side effect. *)
  	let tm_has_side_effect nmap tm =
  	let rec work nmap (acc_se, acc_prerun) = function
  	| TmVar (_, _, s, _, _) -> (
  	if acc_se then (true, acc_prerun)
  	else
  	match SymbMap.find_opt s nmap with
  	| Some (_, _, effect, _) ->
  	(effect, acc_prerun)
  	| None ->
  	(false, acc_prerun) (* In case of lambda or pattern variables *)
  	)
  	| TmConst (_, c) ->
  	if acc_se then (true, acc_prerun)
  	else (const_has_side_effect c, acc_prerun)
  	| TmRef (_, _) | TmTensor (_, _) ->
  	(true, acc_prerun)
  	| TmPreRun (_, _, _) ->
  	(true, true)
  	| t ->
  	if acc_se then (true, acc_prerun)
  	else sfold_tm_tm (work nmap) (acc_se, acc_prerun) t
  	in
  	work nmap (false, false) tm

  , in particular line 23, seems to assume that a variable bound in lambda or pattern match cannot contribute to a side-effect, which is true until it happens to be a function that we call, in which case it might be false. However, just saying true here means that the mere act of referencing a parameter is treated as a side-effect, which might be an issue.
• I think the code is supposed to only prune top-level definitions, i.e., it should only traverse the spine of the program, which isn't what the final, default, sfold case does (it descends into anything, in this case a function-call. This could be assisted by something like Refactoring inexpr #826, which would make spine-traversal easy.

---

Addendum: I found a smaller case, but I'm not sure it's truly illustrative. The program lam f. f 1; () is deadcode eliminated to lam f. (), but of course the two are not observably different since they're never called.