Investigate all "Excellent: ignored check"-s

[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!

update_suite #1428

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

update_suite group apron #1428

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

update_suite group apron2 #1428

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

update_suite group termination #1428

• [x] Excellent: ignored check on tests/regression/78-termination/25-leave-loop-goto-terminating.c for term is now passing!
• [x] 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. d09998584d1a38f7a8baab033af4331b692e05e7 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 711d37bb0584e69bbf1c5881013af0006b1c5fba, but somehow was added back without use later). Surely, we must be comparing them somewhere, right? /cc @stilscher

[michael-schwarz]

https://github.com/goblint/analyzer/commit/d09998584d1a38f7a8baab033af4331b692e05e7 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 https://github.com/goblint/analyzer/commit/711d37bb0584e69bbf1c5881013af0006b1c5fba, 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.

https://github.com/goblint/analyzer/blob/ac1225aa1242ceb2022dd18ffc35f4a4f6544232/src/solver/td3.ml#L702-L717

[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.