`var_eq` doesn't remove unreachable variables in `enter`

[sim642]

Here's enter for var_eq analysis:

analyzer/src/analyses/varEq.ml

Lines 412 to 430 in 5614dd3

	(* First assign arguments to parameters. Then join it with reachables, to get
	rid of equalities that are not reachable. *)
	let enter ctx lval f args =
	let rec fold_left2 f r xs ys =
	match xs, ys with
	| x::xs, y::ys -> fold_left2 f (f r x y) xs ys
	| _ -> r
	in
	let assign_one_param st lv exp =
	let rm = remove (Analyses.ask_of_ctx ctx) (Var lv, NoOffset) st in
	add_eq (Analyses.ask_of_ctx ctx) (Var lv, NoOffset) exp rm
	in
	let nst =
	try fold_left2 assign_one_param ctx.local f.sformals args
	with SetDomain.Unsupported _ -> (* ignore varargs fr now *) D.top ()
	in
	match D.is_bot ctx.local with
	| true -> raise Analyses.Deadcode
	| false -> [ctx.local,nst]

The comment claims it tries to remove unreachable variables but nowhere does it actually do that.

This means that the analysis keeps around equalities from the entire call stack, which makes them large (and thus less efficient to manipulate). It also means more unnecessary contexts for the called function because it can in no way observe those variables. Finally, in my unassume benchmarking and tracing, I've noticed it can cause extra widening iterations in the called function due to equations on unreachable variables being invalidated.

Example

// PARAM: ---set ana.activated[+] "'var_eq'"
void foo() {
  // var_eq has x == y here
}

int main() {
  int x;
  int y;
  y = x;
  foo();
  return 0;
}