Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007809OCamlruntime system and C interfacepublic2018-06-17 12:062018-06-22 17:10
Assigned To 
Platform32-bitOSOS Version
Product Version4.08.0+dev/beta1 
Target VersionFixed in Version 
Summary0007809: Wraparound in %caml_fresh_oo_id leads to incorrect %caml_equal results
Descriptioncaml_fresh_oo_id looks like:

  CAMLprim value caml_fresh_oo_id (value v) {
    v = oo_last_id;
    oo_last_id += 2;
    return v;

Since `value` is `intnat`, 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 Reproducetype 'a typ = ..

type value = { get: 'k. 'k typ -> 'k }

type box = Box : 'a typ -> box

let create : type v. v -> v typ * value =
  fun value ->
  let module M = struct
    type _ typ += Typ : v typ

    let typ = Typ

    let get : type k. k typ -> k =
      fun typ ->
      match typ with
      | Typ -> value
      | _ -> assert false
  end in
  M.typ, { get = M.get }

let eid : 'a -> int = fun v ->
  Obj.extension_id (Obj.extension_constructor v)

let () =
  let ta, fa = create 1 in
  Printf.printf "ta : %d\n%!" (eid ta);
  Printf.printf "a = %d\n%!" (fa.get ta);
  for i = 0 to 2 lsl 29 - 1 do ignore (create "x"); done;
  for i = 0 to 2 lsl 29 - 2 do ignore (create "x"); done;
  let tb, fb = create "y" in
  Printf.printf "tb : %d\n%!" (eid tb);
  Printf.printf "ta = tb => %b\n%!" ((Box ta) = (Box tb));
  Printf.printf "a = %s\n%!" (fa.get tb);
Additional InformationI 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
xleroy (administrator)
2018-06-20 16:19
edited on: 2018-06-20 17:09

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.

frisch (developer)
2018-06-22 00:15

> The problem remains that because of overflow two different objects or first-class modules can end up with the same identifier.

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).
frisch (developer)
2018-06-22 00:29

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 = 0)?
whitequark (developer)
2018-06-22 17:10

Sounds good to me.

- Issue History
Date Modified Username Field Change
2018-06-17 12:06 whitequark New Issue
2018-06-20 16:19 xleroy Note Added: 0019199
2018-06-20 16:19 xleroy Status new => acknowledged
2018-06-20 16:19 xleroy Summary Wraparound in %caml_fresh_oo_id has undefined behavior and leads to incorrect %caml_equal results => Wraparound in %caml_fresh_oo_id leads to incorrect %caml_equal results
2018-06-20 17:09 xleroy Note Edited: 0019199 View Revisions
2018-06-20 17:09 xleroy Note Edited: 0019199 View Revisions
2018-06-22 00:15 frisch Note Added: 0019201
2018-06-22 00:29 frisch Note Added: 0019202
2018-06-22 17:10 whitequark Note Added: 0019206

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker