Skip to content

Commit 22c805d

Browse files
authored
flambda-backend: Take into account witnesses when computing [lessequal] on values (#2402)
otherwise we lose witnesses sometimes
1 parent fc7bf14 commit 22c805d

File tree

4 files changed

+7
-1
lines changed

4 files changed

+7
-1
lines changed

lambda/assume_info.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ module Witnesses = struct
3434
type t = unit
3535

3636
let join _ _ = ()
37+
let lessequal _ _ = true
3738
let meet _ _ = ()
3839
let print _ _ = ()
3940
let empty = ()

lambda/assume_info.mli

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ module Witnesses : sig
1515

1616
val join : t -> t -> t
1717
val meet : t -> t -> t
18+
val lessequal : t -> t -> bool
1819
val print : Format.formatter -> t -> unit
1920
val compare : t -> t -> int
2021
end

utils/zero_alloc_utils.ml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@ module type WS = sig
55

66
val meet : t -> t -> t
77

8+
val lessequal : t -> t -> bool
9+
810
val print : Format.formatter -> t -> unit
911

1012
val compare : t -> t -> int
@@ -39,7 +41,7 @@ module Make (Witnesses : WS) = struct
3941
match v1, v2 with
4042
| Bot, Bot -> true
4143
| Safe, Safe -> true
42-
| Top _, Top _ -> true
44+
| Top w1, Top w2 -> Witnesses.lessequal w1 w2
4345
| Bot, Safe -> true
4446
| Bot, Top _ -> true
4547
| Safe, Top _ -> true

utils/zero_alloc_utils.mli

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ module type WS = sig
1010

1111
val meet : t -> t -> t
1212

13+
val lessequal : t -> t -> bool
14+
1315
val print : Format.formatter -> t -> unit
1416

1517
val compare : t -> t -> int

0 commit comments

Comments
 (0)