Inconsistent behavior for startstate in incremental analysis based on whether AST or CFG comparison is used

[sim642]

Extracted from #1392:

Remove TODO only if passing thanks to analysis improvement. Otherwise improvement is unsound from a bug.

update_suite incremental ast

• Excellent: ignored check on ../11-restart/13-changed_start_state2.c:10 is now passing!
• Excellent: ignored check on ../11-restart/13-changed_start_state2.c:11 is now passing!

---

Resolved

update_suite #1428

• Excellent: ignored check on tests/regression/04-mutex/58-pthread-lock-return.c:73 is now passing!: OSX difference
• Excellent: ignored check on tests/regression/04-mutex/58-pthread-lock-return.c:82 is now passing!: OSX difference
• Excellent: ignored check on tests/regression/04-mutex/58-pthread-lock-return.c:87 is now passing!: OSX difference
• Excellent: ignored check on tests/regression/57-floats/15-more-library.c:42 is now passing!: OSX difference
• Excellent: ignored check on tests/regression/57-floats/15-more-library.c:56 is now passing!: OSX difference
• Excellent: ignored check on tests/regression/57-floats/17-other.c:18 is now passing!: OSX difference

update_suite group apron #1428

• Excellent: ignored check on tests/regression/36-apron/21-traces-cluster-based.c:48 is now passing!
• Excellent: ignored check on tests/regression/36-apron/21-traces-cluster-based.c:66 is now passing!
• Excellent: ignored check on tests/regression/36-apron/21-traces-cluster-based.c:69 is now passing!
• Excellent: ignored check on tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c:25 is now passing!
• Excellent: ignored check on tests/regression/36-apron/34-large-bigint.c:18 is now passing!
• Excellent: ignored check on tests/regression/36-apron/38-branch-global.c:13 is now passing!
• Excellent: ignored check on tests/regression/36-apron/42-threadenter-arg.c:6 is now passing!
• Excellent: ignored check on tests/regression/36-apron/91-mine14-5b-no-threshhold.c:49 is now passing!

update_suite group apron2 #1428

• Excellent: ignored check on tests/regression/46-apron2/75-mutex_with_ghosts.c:56 is now passing!

update_suite group termination #1428

• Excellent: ignored check on tests/regression/78-termination/25-leave-loop-goto-terminating.c for term is now passing!
• Excellent: ignored check on tests/regression/78-termination/28-do-while-continue-terminating.c for term is now passing!

[sim642]

11-restart/13-changed_start_state2.c confuses me a lot:

1. d099985 put the TODOs there, but I don't really understand why. /cc @michael-schwarz
2. I cannot find anywhere were global variable initializers are even compared for incremental. There is CompareAST.eq_init but it is dead code (it was even removed in 711d37b, but somehow was added back without use later). Surely, we must be comparing them somewhere, right? /cc @stilscher

[michael-schwarz]

d099985 put the TODOs there, but I don't really understand why

I think the TODOs are to ensure that the test passes, and checks that g !=1 and g == 2 are considered possible, i.e., the incremental analysis is not unsound. There seems to have been some imprecision at some point, but now the //TODOs should be safe to remove.

[sim642]

Soundness checks would've had to use UNKNOWN! though (or at least UNKNOWN if it's just our own intended imprecision from joins). I'm not sure if they're supposed to be passing though: the configuration only restarts write-only globals (as opposed to 00-basic/03-changed_start_state2 which does all), so it seems like we shouldn't be getting this extra precision now. Otherwise the two versions of this test would be identical.

[stilscher]

I cannot find anywhere were global variable initializers are even compared for incremental. There is CompareAST.eq_init but it is dead code (it was even removed in 711d37b, but somehow was added back without use later). Surely, we must be comparing them somewhere, right? /cc @stilscher

I discussed this with @jerhard and @michael-schwarz and we found that in the solver, side is called for all start variables. We think that this should be sufficient to propagate possible changes in the initializers, such that there is no need for the eq_init comparison.

analyzer/src/solver/td3.ml

Lines 702 to 717 in ac1225a

	(* Call side on all globals and functions in the start variables to make sure that changes in the initializers are propagated.
	* This also destabilizes start functions if their start state changes because of globals that are neither in the start variables nor in the contexts *)
	List.iter (fun (v,d) ->
	if should_restart_start then (
	match GobList.assoc_eq_opt S.Var.equal v data.st with
	| Some old_d when not (S.Dom.equal old_d d) ->
	Logs.debug "Destabilizing and restarting changed start var %a" S.Var.pretty_trace v;
	restart_and_destabilize v (* restart side effect from start *)
	| _ ->
	(* don't restart unchanged start global *)
	(* no need to restart added start global (implicit bot before) *)
	(* restart removed start global below *)
	()
	);
	side v d
	) st;

[sim642]

When I looked into different logs (out vs inside of dune, full suite vs one test) I saw different results: sometimes the incremental run was success, sometimes unknown.
Apparently there's a difference between AST and CFG comparison:

• With AST comparison, the TODOs pass, because old values of globals are somehow forgotten.
• With CFG comparison, the TODOs don't pass, because old values of globals somehow stay around.