FrNecas
commented
2 years ago Thanks for finding time for a review, Peter! We have already discussed how we could integrate incremental solving, our idea was however quite different from your proposed approach (at least as far as I can understand from your description) so it would be nice to discuss the approach to go with in the future. I see this PR as a more of a transition state, it demonstrates the advantages of GOTO unwinding and improves capabilities of 2LS, though it's far from ideal.
This PR introduces a new unwinder which unwinds on GOTO level, makes necessary transformations (mainly related to dynamic object handling) and then computes a new SSA with correct points-to analysis. So far, we have not managed to integrate this solution with incremental SAT solving but this already shows promising results.
The GOTO unwinding itself is slower due to not making use of incremental SAT solver. To overcome this, the current implementation uses both the old unwinder (by default) and then the new unwinder only in cases where dynamic objects are used with unwinding (or k-induction). Such approach combines the best of both worlds -- it is sound when the old approach was not but it is quick where the overhead would not bring any advantages. This is achieved by the unwinders implementing a general interface.
Experiments show promising results so far, we've compared the old and new solution on a subset of SV-COMP benchmarks (most of reach-safety was included, the whole memsafety and part of termination) with a 5 minute timeout:
All of these improvements come from proper use of k-induction in benchmarks with dynamic memory. The 3 new failing tests in memsafety are a bit unfortunate, these are:
In order to make memory leak analysis sound with unwinding, I had to introduce a workaround which duplicates assignments to
__CPROVER_memory_leakvariable for each malloc/free. I initially expected that some of the new failing benchmarks will be caused by the same problem but with__CPROVER_deallocatedso I tried implementing a "split" of this variable as well (present ondeallocated-fixbranch on my fork), however it introduced more incorrect results and slowed 2LS down significantly. I assume there will be differrent reasons for the 3 incorrect benchmarks, haven't figured it out just yet.This PR also re-labels some of our old regression tests since they now work properly with the new unwinder and adds some new tests where the upsides of this solution are demonstrated.