Skip to content

zero alloc: assume on calls #2165

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 11 commits into from
Mar 26, 2024
Merged

zero alloc: assume on calls #2165

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
967acd5
Consume [@zero_alloc assume] attribute on Texp_apply
gretay-js Oct 25, 2023
804705c
Fix [test_never_returns_normally]
gretay-js Mar 25, 2024
6311033
Improve comment about "assume never_return_normally" on allocations
gretay-js Mar 25, 2024
af26beb
bug fix: use [Assume_info.is_none] in [Debginfo.is_none]
gretay-js Mar 25, 2024
553b98b
Provide Value.compare for use in Debuginfo.compare in middle end.
gretay-js Mar 25, 2024
3fa8488
Update comment
gretay-js Mar 25, 2024
f363d78
Cleanup
gretay-js Mar 25, 2024
22463bd
Update comment
gretay-js Mar 25, 2024
8cb0ffa
Add a test for "assume" annotation dropped without warning
gretay-js Mar 25, 2024
5dd7684
Document the interface of Value
gretay-js Mar 26, 2024
3d590cb
Update ocaml/utils/zero_alloc_utils.mli
gretay-js Mar 26, 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
204 changes: 68 additions & 136 deletions backend/checkmach.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,12 +91,16 @@ module Witnesses : sig

val join : t -> t -> t

val meet : t -> t -> t

val create : Witness.kind -> Debuginfo.t -> t

val print : Format.formatter -> t -> unit

val elements : t -> Witness.t list

val compare : t -> t -> int

type components =
{ nor : t;
exn : t;
Expand All @@ -112,6 +116,8 @@ end = struct
much. Only keep witnesses for functions that need checking. *)
let join = union

let meet = inter

let create kind dbg = singleton (Witness.create dbg kind)

let iter t ~f = iter f t
Expand All @@ -134,16 +140,10 @@ end = struct
}
end

(** Abstract value for each component of the domain. *)
module V : sig
type t =
| Top of Witnesses.t (** Property may not hold on some paths. *)
| Safe (** Property holds on all paths. *)
| Bot (** Not reachable. *)

val lessequal : t -> t -> bool
module T = Zero_alloc_utils.Make (Witnesses)

val join : t -> t -> t
module V : sig
include module type of T.V

val transform : Witnesses.t -> t -> t

Expand All @@ -152,34 +152,8 @@ module V : sig
val diff_witnesses : expected:t -> actual:t -> Witnesses.t

val get_witnesses : t -> Witnesses.t

val is_not_safe : t -> bool

val print : witnesses:bool -> Format.formatter -> t -> unit
end = 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 lessequal v1 v2 =
match v1, v2 with
| Bot, Bot -> true
| Safe, Safe -> true
| Top _, Top _ -> true
| Bot, Safe -> true
| Bot, Top _ -> true
| Safe, Top _ -> true
| Top _, (Bot | Safe) -> false
| Safe, Bot -> false
include T.V

(** abstract transformer (backward analysis) for a statement that violates the property
but doesn't alter control flow. *)
Expand All @@ -203,49 +177,10 @@ end = struct
else (
assert (expected = Safe);
match actual with Bot | Safe -> assert false | Top w -> w)

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

(** Abstract value associated with each program location in a function. *)
module Value : sig
type t =
{ nor : V.t;
(** Property about
all paths from this program location that may reach a Normal Return *)
exn : V.t;
(** Property about all paths from this program point that may reach a Return with
Exception *)
div : V.t
(** Property about all paths from this program point that may diverge. *)
}

val lessequal : t -> t -> bool

val join : t -> t -> t

val top : Witnesses.t -> t

val bot : t

val normal_return : t

val exn_escape : t

val diverges : t

val safe : t

val relaxed : Witnesses.t -> t

val print : witnesses:bool -> Format.formatter -> t -> unit
include module type of T.Value

val transform : Witnesses.t -> t -> t

Expand All @@ -255,24 +190,7 @@ module Value : sig

val diff_witnesses : expected:t -> actual:t -> Witnesses.components
end = struct
(** Lifts V to triples *)
type t =
{ nor : V.t;
exn : V.t;
div : V.t
}

let bot = { nor = V.Bot; exn = V.Bot; div = V.Bot }

let lessequal v1 v2 =
V.lessequal v1.nor v2.nor && V.lessequal v1.exn v2.exn
&& V.lessequal 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
}
include T.Value

let transform w v =
{ nor = V.transform w v.nor;
Expand All @@ -297,22 +215,6 @@ end = struct
Witnesses.exn = V.get_witnesses t.exn;
Witnesses.div = V.get_witnesses t.div
}

let normal_return = { bot with nor = V.Safe }

let exn_escape = { bot with exn = V.Safe }

let diverges = { bot with div = V.Safe }

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

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

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
end

(** Representation of user-provided annotations as abstract values *)
Expand All @@ -324,7 +226,7 @@ module Annotation : sig
val find :
Cmm.codegen_option list -> Cmm.property -> string -> Debuginfo.t -> t option

val expected_value : t -> Value.t
val expected_value : t -> Witnesses.t -> Value.t

val is_assume : t -> bool

Expand Down Expand Up @@ -360,9 +262,12 @@ end = struct

let get_loc t = t.loc

let expected_value t =
let res = if t.strict then Value.safe else Value.relaxed Witnesses.empty in
if t.never_returns_normally then { res with nor = V.Bot } else res
let expected_value t w =
let res = if t.strict then Value.safe else Value.relaxed w in
let res =
if t.never_returns_normally then { res with nor = V.Bot } else res
in
res

let is_assume t = t.assume

Expand Down Expand Up @@ -412,6 +317,35 @@ end = struct
List.exists is_enabled Cmm.all_properties
end

module Metadata : sig
(* CR-someday gyorsh: propagate assert of arbitrary expressions. *)
val assume_value :
Debuginfo.t -> can_raise:bool -> Witnesses.t -> Value.t option
end = struct
(* CR gyorsh: The return type of [Assume_info.get_value] is
[Assume_info.Value.t]. It is not the same as [Checkmach.Value.t], because
[Witnesses] in [Checkmach] depend on Debuginfo and cannot be used in
Assume_info due to cyclic dependencies. The witnesses in Assume_info are
always empty and the translation is trivial. Is there a better way to avoid
duplicating [Zero_alloc_utils]? *)
let transl w (v : Assume_info.V.t) : V.t =
match v with Top _ -> Top w | Safe -> Safe | Bot -> Bot

let transl w (v : Assume_info.Value.t) : Value.t =
{ nor = transl w v.nor; exn = transl w v.exn; div = transl w v.div }

let assume_value dbg ~can_raise w =
(* [loc] can be obtained by [Debuginfo.to_location dbg], For now just return
[Location.none] because it is not used. *)
let a = Debuginfo.assume_zero_alloc dbg in
match Assume_info.get_value a with
| None -> None
| Some v ->
let v = transl w v in
let v = if can_raise then v else { v with exn = V.Bot } in
Some v
end

module Report : sig
type t =
{ a : Annotation.t;
Expand Down Expand Up @@ -864,7 +798,7 @@ end = struct
| Some a ->
Builtin_attributes.mark_property_checked analysis_name
(Annotation.get_loc a);
let expected_value = Annotation.expected_value a in
let expected_value = Annotation.expected_value a Witnesses.empty in
if (not (Annotation.is_assume a))
&& S.enabled ()
&& not (Value.lessequal func_info.value expected_value)
Expand Down Expand Up @@ -992,17 +926,19 @@ end = struct

let transform_top t ~next ~exn w desc dbg =
let effect =
if Debuginfo.assume_zero_alloc dbg then Value.relaxed w else Value.top w
match Metadata.assume_value dbg ~can_raise:true w with
| Some v -> v
| None -> Value.top w
in
transform t ~next ~exn ~effect desc dbg

let transform_call t ~next ~exn callee w ~desc dbg =
report t next ~msg:"transform_call next" ~desc dbg;
report t exn ~msg:"transform_call exn" ~desc dbg;
let effect =
if Debuginfo.assume_zero_alloc dbg
then Value.relaxed w
else
match Metadata.assume_value dbg ~can_raise:true w with
| Some v -> v
| None ->
let callee_value, new_dep = find_callee t callee dbg in
update_deps t callee_value new_dep w desc dbg;
(* Abstract witnesses of a call to the single witness for the callee
Expand Down Expand Up @@ -1045,14 +981,14 @@ end = struct
| Ialloc { mode = Alloc_local; _ } ->
assert (not (Mach.operation_can_raise op));
next
| Ialloc { mode = Alloc_heap; bytes; dbginfo } ->
| Ialloc { mode = Alloc_heap; bytes; dbginfo } -> (
assert (not (Mach.operation_can_raise op));
if Debuginfo.assume_zero_alloc dbg
then next
else
let w = create_witnesses t (Alloc { bytes; dbginfo }) dbg in
let w = create_witnesses t (Alloc { bytes; dbginfo }) dbg in
match Metadata.assume_value dbg ~can_raise:false w with
| Some effect -> transform t ~next ~exn ~effect "heap allocation" dbg
| None ->
let r = Value.transform w next in
check t r "heap allocation" dbg
check t r "heap allocation" dbg)
| Iprobe { name; handler_code_sym; enabled_at_init = __ } ->
let desc = Printf.sprintf "probe %s handler %s" name handler_code_sym in
let w = create_witnesses t (Probe { name; handler_code_sym }) dbg in
Expand Down Expand Up @@ -1088,15 +1024,11 @@ end = struct
| Ispecific s ->
let effect =
let w = create_witnesses t Arch_specific dbg in
if Debuginfo.assume_zero_alloc dbg
then
(* Conservatively assume that operation can return normally. *)
let nor = V.Safe in
let exn = if Arch.operation_can_raise s then V.Top w else V.Bot in
(* Assume that the operation does not diverge. *)
let div = V.Bot in
{ Value.nor; exn; div }
else S.transform_specific w s
match
Metadata.assume_value dbg ~can_raise:(Arch.operation_can_raise s) w
with
| Some v -> v
| None -> S.transform_specific w s
in
transform t ~next ~exn ~effect "Arch.specific_operation" dbg
| Idls_get -> Misc.fatal_error "Idls_get not supported"
Expand Down Expand Up @@ -1183,12 +1115,12 @@ end = struct
in
match a with
| Some a when Annotation.is_assume a ->
let expected_value = Annotation.expected_value a in
let expected_value = Annotation.expected_value a Witnesses.empty in
report t expected_value ~msg:"assumed" ~desc:"fundecl" f.fun_dbg;
Unit_info.join_value unit_info fun_name expected_value
| None -> really_check ~keep_witnesses:false
| Some a ->
let expected_value = Annotation.expected_value a in
let expected_value = Annotation.expected_value a Witnesses.empty in
report t expected_value ~msg:"assert" ~desc:"fundecl" f.fun_dbg;
(* Only keep witnesses for functions that need checking. *)
really_check ~keep_witnesses:true
Expand Down
Loading
Loading