Skip to content
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

Open
vicuna opened this issue Jun 17, 2018 · 8 comments
Open

Wraparound in %caml_fresh_oo_id leads to incorrect %caml_equal results #7809

vicuna opened this issue Jun 17, 2018 · 8 comments

Comments

@vicuna
Copy link

vicuna commented Jun 17, 2018

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:

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 reproduce

type '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 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.

@vicuna
Copy link
Author

vicuna commented Jun 20, 2018

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.

@vicuna
Copy link
Author

vicuna commented Jun 21, 2018

Comment author: @alainfrisch

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).

@vicuna
Copy link
Author

vicuna commented Jun 21, 2018

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)?

@vicuna
Copy link
Author

vicuna commented Jun 22, 2018

Comment author: @whitequark

Sounds good to me.

@github-actions
Copy link

github-actions bot commented May 7, 2020

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.

@github-actions github-actions bot added the Stale label May 7, 2020
@whitequark
Copy link
Member

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.

@nojb nojb removed the Stale label May 15, 2020
@github-actions
Copy link

github-actions bot commented Oct 4, 2021

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.

@github-actions github-actions bot added the Stale label Oct 4, 2021
@gasche gasche removed the Stale label Oct 4, 2021
@github-actions
Copy link

github-actions bot commented Oct 7, 2022

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.

@github-actions github-actions bot added the Stale label Oct 7, 2022
@alainfrisch alainfrisch removed the Stale label Oct 7, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

5 participants