`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;
}

[karoliineh]

This causes a spurious NullPointerDereference in SV-COMP task ldv-regression/nested_structure-2.i.

The program location for the warning: [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (./ldv-regression/nested_structure-2.i:17:3-17:9)
is the return statement of __VERIFIER_assert:

void __VERIFIER_assert(int cond) {
  if (!(cond)) {
    ERROR: {reach_error();abort();}
  }
  return;
}

[sim642]

Turns out this is not so easy to do due to how var_eq performs interprocedural analysis. It actually relies on the caller state being passed through the callee to be used in combine_env. Doing it differently requires the use of taintPartialContexts analysis to know what the caller didn't modify and reuse that from callee's old state.

This is also what relation analysis does, except it has one more useful optimization: it records which caller locals were not reachable to the callee and thus remain unchanged even without the taintPartialContexts analysis. I think this is usually the case, so relation analysis can get away without taintPartialContexts quite well.