New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Wraparound in %caml_fresh_oo_id leads to incorrect %caml_equal results #7809
Comments
Comment author: @xavierleroy Concerning the undefined behavior: the OCaml runtime system is compiled with C compiler options that make overflow in signed integer arithmetic defined as wrapping around. Signed arithmetic overflows occurs in the bytecode interpreter, in particular, and is nothing to worry about. I took the liberty to fix the summary of this problem report to de-emphasize this point. The problem remains that because of overflow two different objects or first-class modules can end up with the same identifier. |
Comment author: @alainfrisch
I believe this impacts objects, and extension constructors (such as exceptions), not first-class modules (it would make sense indeed to attach such an id to them, but this is not currently the case). |
Comment author: @alainfrisch As a quick and partial fix, what about at least returning UNORDERED in do_compare_val when total==0, oid1==oid2, but v1!=v2. As far as I can tell, this would already fix equality comparison (with (=), not Pervasives.compare = 0)? |
Comment author: @whitequark Sounds good to me. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Yes, this is still a soundness bug. Also, the idea of having a bot that auto-closes soundness issues is idiotic and you should turn it off on such issues. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Original bug ID: 7809
Reporter: @whitequark
Status: acknowledged (set by @xavierleroy on 2018-06-20T14:19:49Z)
Resolution: open
Priority: normal
Severity: minor
Platform: 32-bit
Version: 4.08.0+dev/beta1/beta2
Category: runtime system and C interface
Monitored by: @gasche
Bug description
caml_fresh_oo_id looks like:
Since
value
isintnat
, calling it 2**30 times results in a signed overflow, which is undefined in C. In addition, it can make polymorphic equality function return an incorrect result, as demonstrated by the code below.Steps to reproduce
Additional information
I am explicitly asking to NOT make overflow in this function a trap. The code above is perfectly legitimate and could be used when an unbounded amount of fresh concrete types is needed at runtime.
In fact it was extracted from a real module I wrote for Coq, where such an overflow is indeed possible at runtime. (That module is not affected by the bug.)
I am not sure what can be done about this overflow other than fixing the undefined behavior in C by adding an appropriate cast. It does not affect 64-bit systems and the only thing it ever affects is polymorphic equality on objects and extensible variants. It might make sense to document that.
The text was updated successfully, but these errors were encountered: