diff --git a/utils/zero_alloc_utils.ml b/utils/zero_alloc_utils.ml index 1893a82c1fa..f0043623416 100644 --- a/utils/zero_alloc_utils.ml +++ b/utils/zero_alloc_utils.ml @@ -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 @@ -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 diff --git a/utils/zero_alloc_utils.mli b/utils/zero_alloc_utils.mli index a134fa6d668..5cabe367582 100644 --- a/utils/zero_alloc_utils.mli +++ b/utils/zero_alloc_utils.mli @@ -19,76 +19,97 @@ module type WS = sig val compare : t -> t -> int end -module Make (Witnesses : WS) : sig +module type Component = sig (** 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. *) + type t - val lessequal : t -> t -> bool + type witnesses - val join : t -> t -> t + (** Property may not hold on some paths. *) + val top : witnesses -> t - val meet : t -> t -> t + (** Property holds on all paths. *) + val safe : t - val is_not_safe : t -> bool + (** Not reachable. *) + val bot : t - val print : witnesses:bool -> Format.formatter -> t -> unit - end + (** Order of the abstract domain *) + val lessequal : t -> t -> bool + + val join : t -> t -> t + + val meet : t -> t -> t + + (** Use [compare] for structural comparison of terms, for example to store them in a + set. Use [lessequal] for checking fixed point of the abstract domain. *) + val compare : t -> t -> int + + val print : witnesses:bool -> Format.formatter -> t -> unit +end +module Make_component (Witnesses : WS) : sig + type t = + | Top of Witnesses.t + | Safe + | Bot + + include Component with type witnesses := Witnesses.t and type t := t +end + +module Make_value + (Witnesses : WS) + (V : Component with type witnesses := Witnesses.t) : sig (** Abstract value associated with each program location in a function. *) - module Value : sig - type t = - { nor : V.t; - (** Property about + 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 + 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. *) - } + div : V.t + (** Property about all paths from this program point that may diverge. *) + } - val lessequal : t -> t -> bool + val lessequal : t -> t -> bool - val join : t -> t -> t + val join : t -> t -> t - val meet : t -> t -> t + val meet : t -> t -> t - val top : Witnesses.t -> t + val top : Witnesses.t -> t - val bot : t + val bot : t - (** [normal_return] means property holds on paths to normal return, exceptional return + (** [normal_return] means property holds on paths to normal return, exceptional return is not reachable and execution will not diverge. *) - val normal_return : t + val normal_return : t - (** [exn_escape] means the property holds on paths to exceptional return, normal + (** [exn_escape] means the property holds on paths to exceptional return, normal return is not reachable and execution will not diverge. *) - val exn_escape : t + val exn_escape : t - (** [diverges] means the execution may diverge without violating the property, but + (** [diverges] means the execution may diverge without violating the property, but normal and exceptional return are not reachable (i.e., [div] is Safe, `nor` and `exn` are Bot). *) - val diverges : t + val diverges : t - (** [safe] means the property holds on all paths (i.e., all three components are set + (** [safe] means the property holds on all paths (i.e., all three components are set to Safe). *) - val safe : t + val safe : t - (** [relaxed] means the property holds on paths that lead to normal returns only + (** [relaxed] means the property holds on paths that lead to normal returns only (i.e., [nor] component is Safe, others are Top. *) - val relaxed : Witnesses.t -> t + val relaxed : Witnesses.t -> t - (** Constructs a value from a user annotation. The witness will be empty. *) - val of_annotation : - strict:bool -> never_returns_normally:bool -> never_raises:bool -> t + (** Constructs a value from a user annotation. The witness will be empty. *) + val of_annotation : + strict:bool -> never_returns_normally:bool -> never_raises:bool -> t - val print : witnesses:bool -> Format.formatter -> t -> unit + val print : witnesses:bool -> Format.formatter -> t -> unit - (** Use [compare] for structural comparison of terms, for example + (** Use [compare] for structural comparison of terms, for example to store them in a set. Use [lessequal] for checking fixed point of the abstract domain. @@ -100,8 +121,7 @@ module Make (Witnesses : WS) : sig does not always imply [compare t1 t2 <= 0]. In particular, [compare] distinguishes between two "Top" values with different witnesses. *) - val compare : t -> t -> int - end + val compare : t -> t -> int end (** The [Assume_info] module contains an instantiation of the abstract domain @@ -147,7 +167,9 @@ module Assume_info : sig val compare : t -> t -> int end - include module type of Make (Witnesses) + module V : module type of Make_component (Witnesses) + + module Value : module type of Make_value (Witnesses) (V) val get_value : t -> Value.t option end