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

Fix lsl overflow detection #8865

Merged
merged 4 commits into from Aug 9, 2019

Conversation

@lthls
Copy link
Contributor

commented Aug 8, 2019

A left shift by Sys.word_size - 1 should be considered an overflow.

Fixes #8864

lthls added 3 commits Aug 8, 2019
Copy link
Contributor

left a comment

The revised check for overflow is correct, I checked it in Coq.

I'll merge in trunk and in 4.09.

@xavierleroy xavierleroy merged commit 0557f07 into ocaml:trunk Aug 9, 2019
0 of 2 checks passed
0 of 2 checks passed
continuous-integration/appveyor/pr Waiting for AppVeyor build to complete
Details
continuous-integration/travis-ci/pr The Travis CI build is in progress
Details
xavierleroy added a commit that referenced this pull request Aug 9, 2019
The formula for Misc.no_overflow_lsl a k is sound only if k < width of type int.
@xavierleroy

This comment has been minimized.

Copy link
Contributor

commented Aug 9, 2019

Cherry-pick to 4.09: bd31ecb

This might deserve backporting to 4.07 and 4.08 one way or another.

@hhugo

This comment has been minimized.

Copy link
Contributor

commented Aug 9, 2019

This PR fixes the implementation to match the documentation

(** [n lsl m] shifts [n] to the left by [m] bits.
    The result is unspecified if [m < 0] or [m > Sys.int_size].
    Right-associative operator at precedence level 8/11. *)

but makes Int.(lsl) not longer behave like Int64.shift_left (resp Int32.shift_left) where the behavior is unspecified when y >= 64 (resp. 32)

external shift_left : int32 -> int -> int32 = "%int32_lsl"
(** [Int32.shift_left x y] shifts [x] to the left by [y] bits.
   The result is unspecified if [y < 0] or [y >= 32]. *)

external shift_left : int64 -> int -> int64 = "%int64_lsl"
(** [Int64.shift_left x y] shifts [x] to the left by [y] bits.
   The result is unspecified if [y < 0] or [y >= 64]. *)

Should other implementations be fixed as well ?

@xavierleroy

This comment has been minimized.

Copy link
Contributor

commented Aug 9, 2019

Should other implementations be fixed as well ?

No. It would be costly to make [Int64.shift_left x 64] defined and always equal to 0. On the other hand, [x lsl 63 = 0] (on a 64-bit platform) falls out of the natural implementation of left shift over tagged integers, and is occasionally useful. For example, you can safely normalize the shift amount by keeping only bits 0 to 5: [x lsl (n land 0x3f)]. This would be more complicated if [x lsl 63] was undefined.

Here I'm speaking of the non-optimized implementation of lsl over tagged integers, [((x - 1) << n) + 1]. The bug that this PR fixes is in an optimized implementation, [(x << n) - (1 << n) + 1].

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.