Reconsider not writing to known addresses if a pointer contains an unknown element

[michael-schwarz]

We currently do completely ignore the possibility that any of the known pointers are written as soon as we have ? in the points-to set. This seems like it is philosophically the wrong thing to do to me.

In my opinion, we should at least potentially update the targets which we have identified.

analyzer/src/analyses/base.ml

Lines 1730 to 1748 in a84e07d

	let update_one x store =
	match Addr.to_mval x with
	| Some x -> update_one_addr x store
	| None -> store
	in try
	(* 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
	(* If any of the addresses are unknown, we ignore it!?! *)
	| SetDomain.Unsupported x ->
	(* if M.tracing then M.tracel "set" ~var:firstvar "set got an exception '%s'" x; *)
	M.info ~category:Unsound "Assignment to unknown address, assuming no write happened."; st

[sim642]

I suspect the SetDomain.Unsupported code is some legacy thing that never even happens now. AddressSet.top isn't a lifted Top but a normal (foldable-over) set with UnknownPtr in it. And update_one there just ignores that one when doing Addr.to_mval.