Skip to content

zero alloc: symbolic values (all changes in one PR) #2524

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.

Sign up for GitHub

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

Merged
merged 4 commits into from
May 9, 2024
Merged

zero alloc: symbolic values (all changes in one PR) #2524

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
580df7f
Symbolic values
gretay-js May 2, 2024
509704b
regenerate dune.inc after rebase
gretay-js May 7, 2024
4971d73
Fix [meet] after rebase: now we use it, handle conservatively
gretay-js May 7, 2024
d183cd0
Remove a stray comment
gretay-js May 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1,716 changes: 1,538 additions & 178 deletions backend/checkmach.ml
View file
Open in desktop

Large diffs are not rendered by default.

28 changes: 28 additions & 0 deletions driver/flambda_backend_args.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,17 @@ let mk_checkmach_details_cutoff f =
| No_details -> 0
| At_most n -> n)


let mk_checkmach_join f =
"-checkmach-join", Arg.Int f,
Printf.sprintf " How many abstract paths before losing precision \
(default %d, negative to fail instead of widening, \
0 to keep all)"
(match Flambda_backend_flags.default_checkmach_join with
| Keep_all -> 0
| Widen n -> n
| Error n -> -n)

let mk_function_layout f =
let layouts = Flambda_backend_flags.Function_layout.(List.map to_string all) in
let default = Flambda_backend_flags.Function_layout.(to_string default) in
Expand Down Expand Up @@ -665,6 +676,7 @@ module type Flambda_backend_options = sig
val disable_checkmach : unit -> unit
val disable_precise_checkmach : unit -> unit
val checkmach_details_cutoff : int -> unit
val checkmach_join : int -> unit

val function_layout : string -> unit
val disable_poll_insertion : unit -> unit
Expand Down Expand Up @@ -783,6 +795,7 @@ struct
mk_disable_checkmach F.disable_checkmach;
mk_disable_precise_checkmach F.disable_precise_checkmach;
mk_checkmach_details_cutoff F.checkmach_details_cutoff;
mk_checkmach_join F.checkmach_join;

mk_function_layout F.function_layout;
mk_disable_poll_insertion F.disable_poll_insertion;
Expand Down Expand Up @@ -956,6 +969,14 @@ module Flambda_backend_options_impl = struct
in
Flambda_backend_flags.checkmach_details_cutoff := c

let checkmach_join n =
let c : Flambda_backend_flags.checkmach_join =
if n < 0 then Error (-n)
else if n = 0 then Keep_all
else Widen n
in
Flambda_backend_flags.checkmach_join := c

let function_layout s =
match Flambda_backend_flags.Function_layout.of_string s with
| None -> () (* this should not occur as we use Arg.Symbol *)
Expand Down Expand Up @@ -1245,6 +1266,13 @@ module Extra_params = struct
| None -> ()
end;
true
| "checkmach-join" ->
begin match Compenv.check_int ppf name v with
| Some i ->
Flambda_backend_options_impl.checkmach_join i
| None -> ()
end;
true
| "function-layout" ->
(match Flambda_backend_flags.Function_layout.of_string v with
| Some layout -> Flambda_backend_flags.function_layout := layout; true
Expand Down
1 change: 1 addition & 0 deletions driver/flambda_backend_args.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ module type Flambda_backend_options = sig
val disable_checkmach : unit -> unit
val disable_precise_checkmach : unit -> unit
val checkmach_details_cutoff : int -> unit
val checkmach_join : int -> unit

val function_layout : string -> unit
val disable_poll_insertion : unit -> unit
Expand Down
8 changes: 8 additions & 0 deletions driver/flambda_backend_flags.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,14 @@ type checkmach_details_cutoff =
let default_checkmach_details_cutoff = At_most 20
let checkmach_details_cutoff = ref default_checkmach_details_cutoff
(* -checkmach-details-cutoff n *)
type checkmach_join =
| Keep_all
| Widen of int (* n > 0 *)
| Error of int (* n > 0 *)

let default_checkmach_join = Widen 100
let checkmach_join = ref default_checkmach_join
(* -checkmach-precise-join-threshold n *)
module Function_layout = struct
type t =
| Topological
Expand Down
8 changes: 8 additions & 0 deletions driver/flambda_backend_flags.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,14 @@ type checkmach_details_cutoff =
val checkmach_details_cutoff : checkmach_details_cutoff ref
val default_checkmach_details_cutoff : checkmach_details_cutoff

type checkmach_join =
| Keep_all
| Widen of int (* n > 0 *)
| Error of int (* n > 0 *)

val checkmach_join : checkmach_join ref
val default_checkmach_join : checkmach_join

module Function_layout : sig
type t =
| Topological
Expand Down
226 changes: 127 additions & 99 deletions ocaml/utils/zero_alloc_utils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,118 +43,145 @@ module type WS = sig
val compare : t -> t -> int
end

module Make (Witnesses : WS) = struct
(** Abstract value for each component of the domain. *)
module V = struct
type t =
| Top of Witnesses.t
| Safe
| Bot

let join c1 c2 =
match c1, c2 with
| Bot, Bot -> Bot
| Safe, Safe -> Safe
| Top w1, Top w2 -> Top (Witnesses.join w1 w2)
| Safe, Bot | Bot, Safe -> Safe
| Top w1, Bot | Top w1, Safe | Bot, Top w1 | Safe, Top w1 -> Top w1

let meet c1 c2 =
match c1, c2 with
| Bot, Bot -> Bot
| Safe, Safe -> Safe
| Top w1, Top w2 -> Top (Witnesses.meet w1 w2)
| Safe, Bot | Bot, Safe -> Bot
| Top _, Bot | Bot, Top _ -> Bot
| Top _, Safe | Safe, Top _ -> Safe

let lessequal v1 v2 =
match v1, v2 with
| Bot, Bot -> true
| Safe, Safe -> true
| Top w1, Top w2 -> Witnesses.lessequal w1 w2
| Bot, Safe -> true
| Bot, Top _ -> true
| Safe, Top _ -> true
| Top _, (Bot | Safe) -> false
| Safe, Bot -> false

let compare t1 t2 =
match t1, t2 with
| Bot, Bot -> 0
| Safe, Safe -> 0
| Top w1, Top w2 -> Witnesses.compare w1 w2
| Bot, (Safe | Top _) -> -1
| (Safe | Top _), Bot -> 1
| Safe, Top _ -> -1
| Top _, Safe -> 1

let is_not_safe = function Top _ -> true | Safe | Bot -> false

let print ~witnesses ppf = function
| Bot -> Format.fprintf ppf "bot"
| Top w ->
Format.fprintf ppf "top";
if witnesses then Format.fprintf ppf " (%a)" Witnesses.print w
| Safe -> Format.fprintf ppf "safe"
end
module type Component = sig
type t

type witnesses

val top : witnesses -> t

val safe : t

val bot : t

val lessequal : t -> t -> bool

val join : t -> t -> t

val meet : t -> t -> t

module Value = struct
(** Lifts V to triples *)
type t =
{ nor : V.t;
exn : V.t;
div : V.t
}
val compare : t -> t -> int

val print : witnesses:bool -> Format.formatter -> t -> unit
end

module Make_component (Witnesses : WS) = struct
(* keep in sync with "resolved" values in Checkmach. *)
type t =
| Top of Witnesses.t
| Safe
| Bot

let bot = Bot

let top w = Top w

let safe = Safe

let join c1 c2 =
match c1, c2 with
| Bot, Bot -> Bot
| Safe, Safe -> Safe
| Top w1, Top w2 -> Top (Witnesses.join w1 w2)
| Safe, Bot | Bot, Safe -> Safe
| Top w1, Bot | Top w1, Safe | Bot, Top w1 | Safe, Top w1 -> Top w1

let meet c1 c2 =
match c1, c2 with
| Bot, Bot -> Bot
| Safe, Safe -> Safe
| Top w1, Top w2 -> Top (Witnesses.meet w1 w2)
| Safe, Bot | Bot, Safe -> Bot
| Top _, Bot | Bot, Top _ -> Bot
| Top _, Safe | Safe, Top _ -> Safe

let lessequal v1 v2 =
match v1, v2 with
| Bot, Bot -> true
| Safe, Safe -> true
| Top w1, Top w2 -> Witnesses.lessequal w1 w2
| Bot, Safe -> true
| Bot, Top _ -> true
| Safe, Top _ -> true
| Top _, (Bot | Safe) -> false
| Safe, Bot -> false

let compare t1 t2 =
match t1, t2 with
| Bot, Bot -> 0
| Safe, Safe -> 0
| Top w1, Top w2 -> Witnesses.compare w1 w2
| Bot, (Safe | Top _) -> -1
| (Safe | Top _), Bot -> 1
| Safe, Top _ -> -1
| Top _, Safe -> 1

let print ~witnesses ppf = function
| Bot -> Format.fprintf ppf "bot"
| Top w ->
Format.fprintf ppf "top";
if witnesses then Format.fprintf ppf " (%a)" Witnesses.print w
| Safe -> Format.fprintf ppf "safe"
end

let bot = { nor = V.Bot; exn = V.Bot; div = V.Bot }
module Make_value
(Witnesses : WS)
(V : Component with type witnesses := Witnesses.t) =
struct
(** Lifts V to triples *)
type t =
{ nor : V.t;
exn : V.t;
div : V.t
}

let lessequal v1 v2 =
V.lessequal v1.nor v2.nor && V.lessequal v1.exn v2.exn
&& V.lessequal v1.div v2.div
let bot = { nor = V.bot; exn = V.bot; div = V.bot }

let join v1 v2 =
{ nor = V.join v1.nor v2.nor;
exn = V.join v1.exn v2.exn;
div = V.join v1.div v2.div
}
let lessequal v1 v2 =
V.lessequal v1.nor v2.nor && V.lessequal v1.exn v2.exn
&& V.lessequal v1.div v2.div

let meet v1 v2 =
{ nor = V.meet v1.nor v2.nor;
exn = V.meet v1.exn v2.exn;
div = V.meet v1.div v2.div
}
let join v1 v2 =
{ nor = V.join v1.nor v2.nor;
exn = V.join v1.exn v2.exn;
div = V.join v1.div v2.div
}

let normal_return = { bot with nor = V.Safe }
let meet v1 v2 =
{ nor = V.meet v1.nor v2.nor;
exn = V.meet v1.exn v2.exn;
div = V.meet v1.div v2.div
}

let exn_escape = { bot with exn = V.Safe }
let normal_return = { bot with nor = V.safe }

let diverges = { bot with div = V.Safe }
let exn_escape = { bot with exn = V.safe }

let safe = { nor = V.Safe; exn = V.Safe; div = V.Safe }
let diverges = { bot with div = V.safe }

let top w = { nor = V.Top w; exn = V.Top w; div = V.Top w }
let safe = { nor = V.safe; exn = V.safe; div = V.safe }

let relaxed w = { nor = V.Safe; exn = V.Top w; div = V.Top w }
let top w = { nor = V.top w; exn = V.top w; div = V.top w }

let of_annotation ~strict ~never_returns_normally ~never_raises =
let res = if strict then safe else relaxed Witnesses.empty in
let res = if never_raises then { res with exn = V.Bot } else res in
if never_returns_normally then { res with nor = V.Bot } else res
let relaxed w = { nor = V.safe; exn = V.top w; div = V.top w }

let print ~witnesses ppf { nor; exn; div } =
let pp = V.print ~witnesses in
Format.fprintf ppf "{ nor=%a; exn=%a; div=%a }" pp nor pp exn pp div
let of_annotation ~strict ~never_returns_normally ~never_raises =
let res = if strict then safe else relaxed Witnesses.empty in
let res = if never_raises then { res with exn = V.bot } else res in
if never_returns_normally then { res with nor = V.bot } else res

let compare { nor = n1; exn = e1; div = d1 }
{ nor = n2; exn = e2; div = d2 } =
let c = V.compare n1 n2 in
if c <> 0
then c
else
let c = V.compare e1 e2 in
if c <> 0 then c else V.compare d1 d2
end
let print ~witnesses ppf { nor; exn; div } =
let pp = V.print ~witnesses in
Format.fprintf ppf "{ nor=%a;@ exn=%a;@ div=%a }@," pp nor pp exn pp div

let compare { nor = n1; exn = e1; div = d1 } { nor = n2; exn = e2; div = d2 }
=
let c = V.compare n1 n2 in
if c <> 0
then c
else
let c = V.compare e1 e2 in
if c <> 0 then c else V.compare d1 d2
end

module Assume_info = struct
Expand All @@ -174,7 +201,8 @@ module Assume_info = struct
let compare _ _ = 0
end

include Make (Witnesses)
module V = Make_component (Witnesses)
module Value = Make_value (Witnesses) (V)

type t =
| No_assume
Expand Down
Loading
Loading