silicon
silicon copied to clipboard
viperproject
Incompleteness when unrolling a loop too many times
Created by bitbucket user robinsierra on 2019-06-04 17:45 Last updated on 2019-07-29 12:58
When doing loop unrolling both Silicon and Carbon hit a limit after which they can’t prove the postcondition anymore.
- 99 iterations: ok for both Silicon and Carbon (SyCy.vpr)
- 100 iterations: ok for Silicon, but not Carbon (SyCn.vpr)
- 101 iterations: neither Silicon nor Carbon (SnCn.vpr)
Attachments:
@marcoeilers commented on 2019-07-29 12:58
Similar to the Carbon issue, this can be worked around by calling Silicon with the command line argument
--z3Args "smt.qi.lazy_threshold=N"
(where the quotation marks have to be part of the argument string and might have to be escaped) with an appropriate N>100.
@marcoeilers I'm tempted to close this as "won't fix" because it doesn't really seem to be a Silicon bug, and the solution/work-around you provided sounds not too hacky to me. What do you think?
I'm wondering what the options are.
- Is there an actual fix, can one set this to infinity or 1000000000, and if yes, would that be a good idea?
- I guess one option would be to give Silicon a command line parameter for this. That would have the advantage that it would make it explicit that this bound exists and what value Silicon chooses for it by default.
- If it's not a good idea to increase the default value to something super high and there's a reason to not add a Silicon parameter (probably that we don't do this for other Z3 options either) then I'd think it's okay to just use this workaround, yes. Although I'd still think it'd be good if it was documented somewhere which defaults Silicon chooses for various Z3 parameters (maybe that documentation exists and I'm just not aware of it?)
Silicon's Z3 configuration can be found here: https://github.com/viperproject/silicon/blob/master/src/main/resources/z3config.smt2. For option qi.lazy_threshold, Z3's default value is used. According to z3 -pd, the default is 20.0.
You could locally change the value in Silicon's Z3 config and run the test suite with, e.g. 1000000000. The script https://github.com/viperproject/silicon/blob/master/utils/scripts/benchmark.sh creates a CSV file with timings, which makes it easy to compare two different runs of Silicon.
I'm not thrilled to add a dedicated Silicon option for this: for the reason you mentioned, and because the need of configuring this Z3 option seems to arise rather rarely.
I'll check the timings with the changed value. For what it's worth, Silicon does use a non-default value for the other apparently-relevant parameter,
(set-option :smt.qi.eager_threshold 100)
I'm not really sure what eager and lazy do in this case, I'll just try different combinations.
So this took forever, sorry, but here are the results. I ran the Silicon test suite, minus the graphs folder that contained examples that don't parse, three times, four repetions each. Here are the results for
- the current version (eager_threshold 100, lazy_threshold default)
- a super high (I put a billion or trillion or something) eager threashold (lazy_threshold default)
- a super high lazy treshold (eager_threshold default)
Unfortunately Github doesn't let me attach files with the extention csv, so I renamed them to txt.
current.txt eager_large.txt lazy_large.txt
Sorry for the late reply. Thanks for running the experiments! How do the runtimes compare?
I compared the benchmarks: 2020-05-27_issue-368.xlsx.
| Current | Eager | Lazy | |
|---|---|---|---|
| Files | 1096 | 1094 | 1095 |
| Minutes | 16:04 | 39:34 | 16:00 |
| Inconsistencies | - | 7 | 0 |
Inconsistencies means that the number of outputs (= errors) obtained for a test case differs relative to Current.
Not sure why Lazy contains one file less, but that aside, Lazy seems acceptable :-)
Great, thanks! I added the parameter commit 83ec94d2ee317991239ec4022461398e43b73da9.
Well, I don't know how that happened, but setting the lazy threshold to a high value did slow things down on the build server to the point that the build times out (build number 2280). No idea why that happened on the server but not on my machine. I changed the parameter back again.