Incremental TD3: optimize write-only unknown restarting#634
Incremental TD3: optimize write-only unknown restarting#634sim642 merged 26 commits intointeractivefrom
Conversation
|
This somehow screws with |
This checks that race warnings don't all disappear.
This caused them to be incorrectly pruned.
One read access disappears due to broken rho_write relift.
Turns out the precision differences were related to severe issues. In particular, the two issues I now fixed caused all or some accesses to disappear even when incrementally analyzing the unchanged program. This is what happens if all the incremental tests only try to get rid of warnings (which you can do by simply forgetting all of them) and don't check if they are introduced or remain. I added the corresponding Precision comparisons on the incremental bench look fine again as well: https://goblint.cs.ut.ee/simmo-results/bench_result-write-only-fixed/. For a couple of basic incremental cases it even fixes the spurious precision difference that came just from a removed access, so the idea seems to work. |
On top of #391. This should be a saner version of #633.
This adds a
rho_write: S.Dom.t HM.t HM.tdata structure, which is used likevar_messages, but to retrigger write-only side-effects from superstable unknowns. Ideally, this would also allow collecting all unknown-related messages inrho_writeand getting rid of the specialvar_messagesaltogether.To know which unknowns may be treated specially, a
is_write_only: t -> boolfunction is added to the unknowns. This is true for write-only unknowns that are only collected during postsolving, e.g. accesses, but also others.