Skip to content

Commit db1fc1e

Browse files
gretay-jsgretay-js
authored
zero alloc: symbolic values (all changes in one PR) (#2524)
* Symbolic values * regenerate dune.inc after rebase * Fix [meet] after rebase: now we use it, handle conservatively * Remove a stray comment
1 parent 9c308a3 commit db1fc1e

18 files changed

+1955
-329
lines changed

‎backend/checkmach.ml

Lines changed: 1538 additions & 178 deletions
Large diffs are not rendered by default.

‎driver/flambda_backend_args.ml

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,17 @@ let mk_checkmach_details_cutoff f =
132132
| No_details -> 0
133133
| At_most n -> n)
134134

135+
136+
let mk_checkmach_join f =
137+
"-checkmach-join", Arg.Int f,
138+
Printf.sprintf " How many abstract paths before losing precision \
139+
(default %d, negative to fail instead of widening, \
140+
0 to keep all)"
141+
(match Flambda_backend_flags.default_checkmach_join with
142+
| Keep_all -> 0
143+
| Widen n -> n
144+
| Error n -> -n)
145+
135146
let mk_function_layout f =
136147
let layouts = Flambda_backend_flags.Function_layout.(List.map to_string all) in
137148
let default = Flambda_backend_flags.Function_layout.(to_string default) in
@@ -665,6 +676,7 @@ module type Flambda_backend_options = sig
665676
val disable_checkmach : unit -> unit
666677
val disable_precise_checkmach : unit -> unit
667678
val checkmach_details_cutoff : int -> unit
679+
val checkmach_join : int -> unit
668680

669681
val function_layout : string -> unit
670682
val disable_poll_insertion : unit -> unit
@@ -783,6 +795,7 @@ struct
783795
mk_disable_checkmach F.disable_checkmach;
784796
mk_disable_precise_checkmach F.disable_precise_checkmach;
785797
mk_checkmach_details_cutoff F.checkmach_details_cutoff;
798+
mk_checkmach_join F.checkmach_join;
786799

787800
mk_function_layout F.function_layout;
788801
mk_disable_poll_insertion F.disable_poll_insertion;
@@ -956,6 +969,14 @@ module Flambda_backend_options_impl = struct
956969
in
957970
Flambda_backend_flags.checkmach_details_cutoff := c
958971

972+
let checkmach_join n =
973+
let c : Flambda_backend_flags.checkmach_join =
974+
if n < 0 then Error (-n)
975+
else if n = 0 then Keep_all
976+
else Widen n
977+
in
978+
Flambda_backend_flags.checkmach_join := c
979+
959980
let function_layout s =
960981
match Flambda_backend_flags.Function_layout.of_string s with
961982
| None -> () (* this should not occur as we use Arg.Symbol *)
@@ -1245,6 +1266,13 @@ module Extra_params = struct
12451266
| None -> ()
12461267
end;
12471268
true
1269+
| "checkmach-join" ->
1270+
begin match Compenv.check_int ppf name v with
1271+
| Some i ->
1272+
Flambda_backend_options_impl.checkmach_join i
1273+
| None -> ()
1274+
end;
1275+
true
12481276
| "function-layout" ->
12491277
(match Flambda_backend_flags.Function_layout.of_string v with
12501278
| Some layout -> Flambda_backend_flags.function_layout := layout; true

‎driver/flambda_backend_args.mli

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ module type Flambda_backend_options = sig
5555
val disable_checkmach : unit -> unit
5656
val disable_precise_checkmach : unit -> unit
5757
val checkmach_details_cutoff : int -> unit
58+
val checkmach_join : int -> unit
5859

5960
val function_layout : string -> unit
6061
val disable_poll_insertion : unit -> unit

‎driver/flambda_backend_flags.ml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,14 @@ type checkmach_details_cutoff =
4646
let default_checkmach_details_cutoff = At_most 20
4747
let checkmach_details_cutoff = ref default_checkmach_details_cutoff
4848
(* -checkmach-details-cutoff n *)
49+
type checkmach_join =
50+
| Keep_all
51+
| Widen of int (* n > 0 *)
52+
| Error of int (* n > 0 *)
53+
54+
let default_checkmach_join = Widen 100
55+
let checkmach_join = ref default_checkmach_join
56+
(* -checkmach-precise-join-threshold n *)
4957
module Function_layout = struct
5058
type t =
5159
| Topological

‎driver/flambda_backend_flags.mli

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,14 @@ type checkmach_details_cutoff =
4949
val checkmach_details_cutoff : checkmach_details_cutoff ref
5050
val default_checkmach_details_cutoff : checkmach_details_cutoff
5151

52+
type checkmach_join =
53+
| Keep_all
54+
| Widen of int (* n > 0 *)
55+
| Error of int (* n > 0 *)
56+
57+
val checkmach_join : checkmach_join ref
58+
val default_checkmach_join : checkmach_join
59+
5260
module Function_layout : sig
5361
type t =
5462
| Topological

‎ocaml/utils/zero_alloc_utils.ml

Lines changed: 127 additions & 99 deletions
Original file line numberDiff line numberDiff line change
@@ -43,118 +43,145 @@ module type WS = sig
4343
val compare : t -> t -> int
4444
end
4545

46-
module Make (Witnesses : WS) = struct
47-
(** Abstract value for each component of the domain. *)
48-
module V = struct
49-
type t =
50-
| Top of Witnesses.t
51-
| Safe
52-
| Bot
53-
54-
let join c1 c2 =
55-
match c1, c2 with
56-
| Bot, Bot -> Bot
57-
| Safe, Safe -> Safe
58-
| Top w1, Top w2 -> Top (Witnesses.join w1 w2)
59-
| Safe, Bot | Bot, Safe -> Safe
60-
| Top w1, Bot | Top w1, Safe | Bot, Top w1 | Safe, Top w1 -> Top w1
61-
62-
let meet c1 c2 =
63-
match c1, c2 with
64-
| Bot, Bot -> Bot
65-
| Safe, Safe -> Safe
66-
| Top w1, Top w2 -> Top (Witnesses.meet w1 w2)
67-
| Safe, Bot | Bot, Safe -> Bot
68-
| Top _, Bot | Bot, Top _ -> Bot
69-
| Top _, Safe | Safe, Top _ -> Safe
70-
71-
let lessequal v1 v2 =
72-
match v1, v2 with
73-
| Bot, Bot -> true
74-
| Safe, Safe -> true
75-
| Top w1, Top w2 -> Witnesses.lessequal w1 w2
76-
| Bot, Safe -> true
77-
| Bot, Top _ -> true
78-
| Safe, Top _ -> true
79-
| Top _, (Bot | Safe) -> false
80-
| Safe, Bot -> false
81-
82-
let compare t1 t2 =
83-
match t1, t2 with
84-
| Bot, Bot -> 0
85-
| Safe, Safe -> 0
86-
| Top w1, Top w2 -> Witnesses.compare w1 w2
87-
| Bot, (Safe | Top _) -> -1
88-
| (Safe | Top _), Bot -> 1
89-
| Safe, Top _ -> -1
90-
| Top _, Safe -> 1
91-
92-
let is_not_safe = function Top _ -> true | Safe | Bot -> false
93-
94-
let print ~witnesses ppf = function
95-
| Bot -> Format.fprintf ppf "bot"
96-
| Top w ->
97-
Format.fprintf ppf "top";
98-
if witnesses then Format.fprintf ppf " (%a)" Witnesses.print w
99-
| Safe -> Format.fprintf ppf "safe"
100-
end
46+
module type Component = sig
47+
type t
48+
49+
type witnesses
50+
51+
val top : witnesses -> t
52+
53+
val safe : t
54+
55+
val bot : t
56+
57+
val lessequal : t -> t -> bool
58+
59+
val join : t -> t -> t
60+
61+
val meet : t -> t -> t
10162

102-
module Value = struct
103-
(** Lifts V to triples *)
104-
type t =
105-
{ nor : V.t;
106-
exn : V.t;
107-
div : V.t
108-
}
63+
val compare : t -> t -> int
64+
65+
val print : witnesses:bool -> Format.formatter -> t -> unit
66+
end
67+
68+
module Make_component (Witnesses : WS) = struct
69+
(* keep in sync with "resolved" values in Checkmach. *)
70+
type t =
71+
| Top of Witnesses.t
72+
| Safe
73+
| Bot
74+
75+
let bot = Bot
76+
77+
let top w = Top w
78+
79+
let safe = Safe
80+
81+
let join c1 c2 =
82+
match c1, c2 with
83+
| Bot, Bot -> Bot
84+
| Safe, Safe -> Safe
85+
| Top w1, Top w2 -> Top (Witnesses.join w1 w2)
86+
| Safe, Bot | Bot, Safe -> Safe
87+
| Top w1, Bot | Top w1, Safe | Bot, Top w1 | Safe, Top w1 -> Top w1
88+
89+
let meet c1 c2 =
90+
match c1, c2 with
91+
| Bot, Bot -> Bot
92+
| Safe, Safe -> Safe
93+
| Top w1, Top w2 -> Top (Witnesses.meet w1 w2)
94+
| Safe, Bot | Bot, Safe -> Bot
95+
| Top _, Bot | Bot, Top _ -> Bot
96+
| Top _, Safe | Safe, Top _ -> Safe
97+
98+
let lessequal v1 v2 =
99+
match v1, v2 with
100+
| Bot, Bot -> true
101+
| Safe, Safe -> true
102+
| Top w1, Top w2 -> Witnesses.lessequal w1 w2
103+
| Bot, Safe -> true
104+
| Bot, Top _ -> true
105+
| Safe, Top _ -> true
106+
| Top _, (Bot | Safe) -> false
107+
| Safe, Bot -> false
108+
109+
let compare t1 t2 =
110+
match t1, t2 with
111+
| Bot, Bot -> 0
112+
| Safe, Safe -> 0
113+
| Top w1, Top w2 -> Witnesses.compare w1 w2
114+
| Bot, (Safe | Top _) -> -1
115+
| (Safe | Top _), Bot -> 1
116+
| Safe, Top _ -> -1
117+
| Top _, Safe -> 1
118+
119+
let print ~witnesses ppf = function
120+
| Bot -> Format.fprintf ppf "bot"
121+
| Top w ->
122+
Format.fprintf ppf "top";
123+
if witnesses then Format.fprintf ppf " (%a)" Witnesses.print w
124+
| Safe -> Format.fprintf ppf "safe"
125+
end
109126

110-
let bot = { nor = V.Bot; exn = V.Bot; div = V.Bot }
127+
module Make_value
128+
(Witnesses : WS)
129+
(V : Component with type witnesses := Witnesses.t) =
130+
struct
131+
(** Lifts V to triples *)
132+
type t =
133+
{ nor : V.t;
134+
exn : V.t;
135+
div : V.t
136+
}
111137

112-
let lessequal v1 v2 =
113-
V.lessequal v1.nor v2.nor && V.lessequal v1.exn v2.exn
114-
&& V.lessequal v1.div v2.div
138+
let bot = { nor = V.bot; exn = V.bot; div = V.bot }
115139

116-
let join v1 v2 =
117-
{ nor = V.join v1.nor v2.nor;
118-
exn = V.join v1.exn v2.exn;
119-
div = V.join v1.div v2.div
120-
}
140+
let lessequal v1 v2 =
141+
V.lessequal v1.nor v2.nor && V.lessequal v1.exn v2.exn
142+
&& V.lessequal v1.div v2.div
121143

122-
let meet v1 v2 =
123-
{ nor = V.meet v1.nor v2.nor;
124-
exn = V.meet v1.exn v2.exn;
125-
div = V.meet v1.div v2.div
126-
}
144+
let join v1 v2 =
145+
{ nor = V.join v1.nor v2.nor;
146+
exn = V.join v1.exn v2.exn;
147+
div = V.join v1.div v2.div
148+
}
127149

128-
let normal_return = { bot with nor = V.Safe }
150+
let meet v1 v2 =
151+
{ nor = V.meet v1.nor v2.nor;
152+
exn = V.meet v1.exn v2.exn;
153+
div = V.meet v1.div v2.div
154+
}
129155

130-
let exn_escape = { bot with exn = V.Safe }
156+
let normal_return = { bot with nor = V.safe }
131157

132-
let diverges = { bot with div = V.Safe }
158+
let exn_escape = { bot with exn = V.safe }
133159

134-
let safe = { nor = V.Safe; exn = V.Safe; div = V.Safe }
160+
let diverges = { bot with div = V.safe }
135161

136-
let top w = { nor = V.Top w; exn = V.Top w; div = V.Top w }
162+
let safe = { nor = V.safe; exn = V.safe; div = V.safe }
137163

138-
let relaxed w = { nor = V.Safe; exn = V.Top w; div = V.Top w }
164+
let top w = { nor = V.top w; exn = V.top w; div = V.top w }
139165

140-
let of_annotation ~strict ~never_returns_normally ~never_raises =
141-
let res = if strict then safe else relaxed Witnesses.empty in
142-
let res = if never_raises then { res with exn = V.Bot } else res in
143-
if never_returns_normally then { res with nor = V.Bot } else res
166+
let relaxed w = { nor = V.safe; exn = V.top w; div = V.top w }
144167

145-
let print ~witnesses ppf { nor; exn; div } =
146-
let pp = V.print ~witnesses in
147-
Format.fprintf ppf "{ nor=%a; exn=%a; div=%a }" pp nor pp exn pp div
168+
let of_annotation ~strict ~never_returns_normally ~never_raises =
169+
let res = if strict then safe else relaxed Witnesses.empty in
170+
let res = if never_raises then { res with exn = V.bot } else res in
171+
if never_returns_normally then { res with nor = V.bot } else res
148172

149-
let compare { nor = n1; exn = e1; div = d1 }
150-
{ nor = n2; exn = e2; div = d2 } =
151-
let c = V.compare n1 n2 in
152-
if c <> 0
153-
then c
154-
else
155-
let c = V.compare e1 e2 in
156-
if c <> 0 then c else V.compare d1 d2
157-
end
173+
let print ~witnesses ppf { nor; exn; div } =
174+
let pp = V.print ~witnesses in
175+
Format.fprintf ppf "{ nor=%a;@ exn=%a;@ div=%a }@," pp nor pp exn pp div
176+
177+
let compare { nor = n1; exn = e1; div = d1 } { nor = n2; exn = e2; div = d2 }
178+
=
179+
let c = V.compare n1 n2 in
180+
if c <> 0
181+
then c
182+
else
183+
let c = V.compare e1 e2 in
184+
if c <> 0 then c else V.compare d1 d2
158185
end
159186

160187
module Assume_info = struct
@@ -174,7 +201,8 @@ module Assume_info = struct
174201
let compare _ _ = 0
175202
end
176203

177-
include Make (Witnesses)
204+
module V = Make_component (Witnesses)
205+
module Value = Make_value (Witnesses) (V)
178206

179207
type t =
180208
| No_assume

0 commit comments

Comments
 (0)