search

boogie-org / boogie

Boogie
http://research.microsoft.com/en-us/projects/boogie/
MIT License
510 stars 112 forks source link

:rlimit value multiplied by 1000 when passed to prover #795

Closed robin-aws closed 1 year ago

robin-aws commented 1 year ago

This looks like a simple case of Checker.SetRLimit imitating the Checker.SetTimeout method. The difference is that the latter is converting between seconds and milliseconds, whereas there seems to be no reason to apply the same transformation on resource units, which are totally abstract. This gets really confusing if you then read the current rlimit value, as Dafny does, because that value is not similarly adjusted.

I don't think we should just "fix" this in place since it will break existing projects. I think we should instead document this behavior more explicitly, and add a parallel option with a different name that does not alter the value. I'd suggest something like "reproducible-resource-limit" to align with the concept in SMT-LIB: https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf (p. 4.1.7)

shazqadeer commented 1 year ago

I am not in favor of two different names for roughly the same concept. It might break behavior but in the long run I prefer to keep Boogie less confusing overall. I don't have any preference for the chosen name. If you think it is better to align with the SMTLIB concept, let us converge on that.

cc: @atomb

atomb commented 1 year ago

I think that's a reasonable argument, especially given that I think Dafny is the only Boogie client to widely use this feature, and therefore the only thing likely to break if the behavior changes. We can implement some backward compatibility mechanism at the Dafny level while keeping Boogie simple.