silicon
silicon copied to clipboard
viperproject
Examples testHistogram.sil and testHistogramFull.sil don't terminate
Created by @mschwerhoff on 2015-06-08 10:07 Last updated on 2019-08-28 09:52
After Silicon-QP commit https://github.com/viperproject/silicon/commit/9776220f35d135dba62de1b4bb277fc3dd9fcff0, quantifiedpermissions\third_party\testHistogram.sil and quantifiedpermissions\third_party\testHistogramFull.sil no longer terminate (in reasonable time).
It is not clear what the reason could be. The examples contain integer division and modulo, which could be a problem. Z3 also consumes a lot of memory, so there could be a matching loop as well. The memory consumption only increases somewhat slowly, though, which is different from other examples that (potentially or confirmedly) contain matching loops.
A forall that could give rise to a matching loop is
forall k_fresh_rw_0: Int ::
(k_fresh_rw_0 in [0..M * N)) && (k_fresh_rw_0 % N < N)
==> (matrix[k_fresh_rw_0].Ref__Integer_value in [0..P))
@mueller55 on 2015-06-11 15:31:
- changed the assignee from (none) to @mschwerhoff
@mschwerhoff commented on 2015-07-27 09:52
I looked at the two long-running/non-terminating check-sats that I found in the SMT file generated by Silicon, and judging by Z3's statistics, it looked as if the non-linear arithmetic solver went crazy. Fortunately, these check-sats were due to branch feasibility checks (which were doomed to yield unknown anyway).
After adding short time-outs to branch feasibility checks (Silicon-QP commit https://github.com/viperproject/silicon/commit/64461e0e4aa93f689760bce17208369c3f7c6c73), and after adding a rewriter that rewrites expressions of the shape x in [a..b) into a <= x && x < b (commit https://github.com/viperproject/silicon/commit/97c4e14575b0dbf2dcd3cd0e01adb14625f36d05), both examples now verify in about 9s.
@mschwerhoff commented on 2015-11-26 10:51
The non-termination problem resurfaced with Silicon-QP commit https://github.com/viperproject/silicon/commit/961117ec3c783cf67743c2dac684c72aac1cbe4d. third_party\stefan_recent\testHistogramFull.sil is currently being ignored.
@alexanderjsummers commented on 2019-08-28 09:52
Does the code contain non-linear arithmetic? If so, I suppose we can chalk this up to that (and mark the issue as invalid). It would be helpful to attach a version of the code.
Come to think of it, there should be something in the tutorial about non-linear arithmetic pitfalls…