BaseAnalysis: Investigate why join over alternatives for non-definite AD target does not work

[michael-schwarz]

For #1458 I also attempted to replace this snippet

analyzer/src/analyses/base.ml

Lines 1735 to 1743 in 5cd8650

	(* We start from the current state and an empty list of global deltas,
	* and we assign to all the the different possible places: *)
	let nst = AD.fold update_one lval st in
	(* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *)
	(* If the address was definite, then we just return it. If the address
	* was ambiguous, we have to join it with the initial state. *)
	let nst = if AD.cardinal lval > 1 then { nst with cpa = CPA.join st.cpa nst.cpa } else nst in
	(* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *)
	nst

with

AD.fold (fun addr acc -> D.join (update_one addr st) acc) lval (D.bot ())

but that lead to some strange test failures where I really have no idea what's going on:

3 test(s) failed: ["04/35 trylock_rc", "04/36 trylock_nr", "41/05 more"]

This would be the cleaner solution, so we should investigate it.

Originally posted by @michael-schwarz in #1458 (comment)

[michael-schwarz]

That's odd indeed. I'm fine with the current improvement then because it fixes the issue and doesn't break anything else.
The naive implementation failing some tests deserves an issue though. I had a quick tracing look and somehow there seemed to be CPA maps with many variables missing or Uninitialized (i.e. superbot) values, so something odd happens. Maybe when the address set is somehow empty, the new D.bot () comes into play?

Originally posted by @sim642 in #1458 (comment)

[karoliineh]

The tests pass when we replace it with:

if AD.is_empty lval then
  st
else
  AD.fold (fun addr acc -> D.join (update_one addr st) acc) lval (D.bot ())

1. In "04/35 trylock_rc", and "04/36 trylock_nr", lval becomes empty because of the call time (NULL), where in LibFuns we try to write to the argument (("time", unknown [drop "arg" [w]]);) that is then a NullPointer, which is removed by collect_invalidate.
2. In "41/05 more" the same happens because of the call strtol("bla", 0, 8), where we try to write to the second argument ("strtol", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []]); that is also a NullPointer.

I tried to catch all cases where lval might be empty with assert (not @@ AD.is_empty lval);. Then one more test ("05/21 race-null-type") crashes, but that also contains a call to time (NULL).