Skip to content

Remove integer comparison involving nonconstant polymorphic variants#854

Merged
mshinwell merged 1 commit intooxcaml:mainfrom
lthls:poly-variant-isint
Oct 3, 2022
Merged

Remove integer comparison involving nonconstant polymorphic variants#854
mshinwell merged 1 commit intooxcaml:mainfrom
lthls:poly-variant-isint

Conversation

@lthls
Copy link
Copy Markdown
Contributor

@lthls lthls commented Sep 29, 2022

This hopefully means that we will be able to revert #729.

@lthls lthls requested a review from mshinwell as a code owner September 29, 2022 16:46
@mshinwell
Copy link
Copy Markdown
Collaborator

mshinwell commented Sep 30, 2022

For context, this relates to examples like the following:

type simple = [ `Black | `Blue | `Red | `Green | `Yellow ]

let[@inline never] compare_simple s1 s2 = Sys.opaque_identity 0

type t = [ simple | `RGB of int ]

let compare t1 t2 =
  match t1, t2 with
  | #simple as s1, #simple as s2 -> compare_simple s1 s2
  | `RGB i1, `RGB i2 -> Int.compare i1 i2
  | x, y -> compare x y

let example = `RGB 12345

let compare_spec t = (compare [@inlined]) t example

where currently the pattern matching compiler is generating integer ordered comparisons between pointers and integers, which we wish to disallow:

(let
  (compare_simple/262 = (function s1/264 s2/265 never_inline : int (opaque 0))
   compare/335 =
     (function t1/336 t2/337 : int
       (catch
         (catch
           (if (isint t1/336)
             (if (>= t1/336 82908052) (if (!= t1/336 737308346) (if (!= t1/336 756711075) (if (>= t1/336 82908053) (exit 1) (exit 2)) (exit 2)) (exit 2))
               (if (!= t1/336 -937474657) (if (!= t1/336 4100401) (exit 1) (exit 2)) (exit 2)))
             (if (!= (field 0 t1/336) 4093677) (exit 1) (if (isint t2/337) (exit 1) (if (!= (field 0 t2/337) 4093677) (exit 1) (apply (field 8 (global Stdlib__Int!)) (field 1 t1/336) (field 1 t2/337))))))
          with (2)
           (catch
(* --> *)      (if (>= t2/337 82908052) (if (!= t2/337 737308346) (if (!= t2/337 756711075) (if (>= t2/337 82908053) (exit 1) (exit 3)) (exit 3)) (exit 3))
               (if (!= t2/337 -937474657) (if (!= t2/337 4100401) (exit 1) (exit 3)) (exit 3)))
            with (3) (apply compare_simple/262 t1/336 (makeblock 0 t1/336 t2/337))))
        with (1) (caml_compare t1/336 t2/337)))
   example/371 = [0: 4093677 12345]
   compare_spec/372 = (function t/374 : int (apply compare/335 t/374 example/371 always_inline)))
  (makeblock 0 compare_simple/262 compare/335 example/371 compare_spec/372))

@lthls
Copy link
Copy Markdown
Contributor Author

lthls commented Sep 30, 2022

I think this also fixes a bug.
Looking at the generated lambda:

(if (>= t1/336 82908052) ... (if (>= t1/336 82908053) ...

The last test checks whether t1/336 is equal to 82908052. It assumes the there is no valid input between 82908052 and 82908053. But after taking tagging into account, these become tests against 165816105 and 165816107 respectively. So there could be a pointer represented as 165816106 hiding in between (in this particular case, alignment forbids it, but it could happen for different hashes).
For this reason, I think we could upstream the fix.

@mshinwell
Copy link
Copy Markdown
Collaborator

mshinwell commented Sep 30, 2022

Wow that is very subtle. We should upstream this.

@mshinwell mshinwell added the to upstream PR should be sent to upstream OCaml label Sep 30, 2022
@lthls lthls mentioned this pull request Sep 30, 2022
Merged
@lthls
Copy link
Copy Markdown
Contributor Author

lthls commented Sep 30, 2022

I've created a PR upstream (ocaml/ocaml#11587).

@mshinwell
Copy link
Copy Markdown
Collaborator

mshinwell commented Oct 3, 2022

I'm going to approve this based on the upstream approval.

@mshinwell mshinwell merged commit d77351a into oxcaml:main Oct 3, 2022
mshinwell added a commit to mshinwell/oxcaml that referenced this pull request Oct 24, 2022
@mshinwell
Squashed 'ocaml/' changes from 2118848..25188da
db559ae 
25188da flambda-backend: Missed comment from PR802 (oxcaml#887)
9469765 flambda-backend: Improve the semantics of asynchronous exceptions (new simpler version) (oxcaml#802)
d9e4dd0 flambda-backend: Fix `make runtest` on NixOS (oxcaml#874)
4bbde7a flambda-backend: Simpler symbols (oxcaml#753)
ef37262 flambda-backend: Add opaqueness to Obj.magic under Flambda 2 (oxcaml#862)
a9616e9 flambda-backend: Add build system hooks for ocaml-jst (oxcaml#869)
045ef67 flambda-backend: Allow the compiler to build with stock Dune (oxcaml#868)
3cac5be flambda-backend: Simplify Makefile logic for natdynlinkops (oxcaml#866)
c5b12bf flambda-backend: Remove unnecessary install lines (oxcaml#860)
ff12bbe flambda-backend: Fix unused variable warning in st_stubs.c (oxcaml#861)
c84976c flambda-backend: Static check for noalloc: attributes (oxcaml#825)
ca56052 flambda-backend: Build system refactoring for ocaml-jst (oxcaml#857)
39eb7f9 flambda-backend: Remove integer comparison involving nonconstant polymorphic variants (oxcaml#854)
c102688 flambda-backend: Fix soundness bug by using currying information from typing (oxcaml#850)
6a96b61 flambda-backend: Add a primitive to enable/disable the tick thread (oxcaml#852)
f64370b flambda-backend: Make Obj.dup use a new primitive, %obj_dup (oxcaml#843)
9b78eb2 flambda-backend: Add test for oxcaml#820 (include functor soundness bug) (oxcaml#841)
8f24346 flambda-backend: Add `-dtimings-precision` flag (oxcaml#833)
65c2f22 flambda-backend: Add test for oxcaml#829 (oxcaml#831)
7b27a49 flambda-backend: Follow-up PR#829 (comballoc fixes for locals) (oxcaml#830)
ad7ec10 flambda-backend: Use a custom condition variable implementation (oxcaml#787)
3ee650c flambda-backend: Fix soundness bug in include functor (oxcaml#820)
2f57378 flambda-backend: Static check noalloc (oxcaml#778)
aaad625 flambda-backend: Emit begin/end region only when stack allocation is enabled (oxcaml#812)
17c7173 flambda-backend: Fix .cmt for included signatures (oxcaml#803)
e119669 flambda-backend: Increase delays in tests/lib-threads/beat.ml (oxcaml#800)
ccc356d flambda-backend: Prevent dynamic loading of the same .cmxs twice in private mode, etc. (oxcaml#784)
14eb572 flambda-backend: Make local extension point equivalent to local_ expression (oxcaml#790)
487d11b flambda-backend: Fix tast_iterator and tast_mapper for include functor. (oxcaml#795)
a50a818 flambda-backend: Reduce closure allocation in List (oxcaml#792)
96c9c60 flambda-backend: Merge ocaml-jst
a775b88 flambda-backend: Fix ocaml/otherlibs/unix 32-bit build (oxcaml#767)
f7c2679 flambda-backend: Create object files internally to avoid invoking GAS (oxcaml#757)
c7a46bb flambda-backend: Bugfix for Cmmgen.expr_size with locals (oxcaml#756)
b337cb6 flambda-backend: Fix build_upstream for PR749 (oxcaml#750)
8e7e81c flambda-backend: Differentiate is_int primitive between generic and variant-only versions (oxcaml#749)

git-subtree-dir: ocaml
git-subtree-split: 25188da
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mshinwell mshinwell mshinwell approved these changes

Assignees

No one assigned

Labels

accepted upstream middle end to upstream PR should be sent to upstream OCaml

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@lthls @mshinwell