diff --git a/backend/checkmach.ml b/backend/checkmach.ml index 3f14d6a0572..1fc0af94173 100644 --- a/backend/checkmach.ml +++ b/backend/checkmach.ml @@ -25,6 +25,8 @@ **********************************************************************************) [@@@ocaml.warning "+a-30-40-41-42"] +let debug = false + module String = Misc.Stdlib.String module Witness = struct @@ -72,9 +74,13 @@ module Witness = struct fprintf ppf "probe \"%s\" handler %s" name handler_code_sym let print ppf { kind; dbg } = - Format.fprintf ppf "%a %a" print_kind kind Debuginfo.print_compact dbg + Format.fprintf ppf "%a {%a}@," print_kind kind Debuginfo.print_compact dbg end +let take_first_n t n ~to_seq ~of_seq ~cardinal = + let len = cardinal t in + if len <= n then t else t |> to_seq |> Seq.take n |> of_seq + module Witnesses : sig type t @@ -98,6 +104,10 @@ module Witnesses : sig val compare : t -> t -> int + val size : t -> int + + val cutoff : t -> n:int -> t + type components = { nor : t; exn : t; @@ -108,10 +118,27 @@ module Witnesses : sig end = struct include Set.Make (Witness) - (* CR gyorsh: consider using Flambda_backend_flags.checkmach_details_cutoff to - limit the size of this set. The downside is that it won't get tested as - much. Only keep witnesses for functions that need checking. *) - let join = union + let print ppf t = Format.pp_print_seq Witness.print ppf (to_seq t) + + let size t = cardinal t + + let cutoff t ~n = take_first_n t n ~to_seq ~of_seq ~cardinal + + let join t1 t2 = + let res = union t1 t2 in + match !Flambda_backend_flags.checkmach_details_cutoff with + | Keep_all -> res + | No_details -> + if not (is_empty res) + then Misc.fatal_errorf "expected no witnesses got %a" print res; + res + | At_most n -> + (* CR-someday gyorsh: current implementation is naive: first compute the + union and then remove some elements. This can be optimized but should + preserve the property that we keep the smallest [n] witnesses from both + sets. This property makes user error messages more stable and + independent of iteration order. *) + cutoff res ~n let meet = inter @@ -121,8 +148,6 @@ end = struct let iter t ~f = iter f t - let print ppf t = Format.pp_print_seq Witness.print ppf (to_seq t) - type components = { nor : t; exn : t; @@ -139,36 +164,1071 @@ end = struct } end -module T = Zero_alloc_utils.Make (Witnesses) +module Tag = struct + type t = + | N + | E + | D + + let compare : t -> t -> int = fun t1 t2 -> Stdlib.compare t1 t2 + + let print = function N -> "nor" | E -> "exn" | D -> "div" +end + +module Var : sig + type t + + val create : string -> Tag.t -> t + + val name : t -> string + + val tag : t -> Tag.t + val print : Format.formatter -> t -> unit + + val compare : t -> t -> int + + val equal : t -> t -> bool + + module Map : Map.S with type key = t + + module Set : Set.S with type elt = t +end = struct + module T = struct + type t = + { name : string; + tag : Tag.t + } + + let compare { tag = tag1; name = name1 } { tag = tag2; name = name2 } = + let c = String.compare name1 name2 in + if c = 0 then Tag.compare tag1 tag2 else c + end + + include T + module Map = Map.Make (T) + module Set = Set.Make (T) + + let equal t1 t2 = compare t1 t2 = 0 + + let name t = t.name + + let tag t = t.tag + + let create name tag = { name; tag } + + let print ppf { name; tag } = + Format.fprintf ppf "%s.%s@ " name (Tag.print tag) +end + +(** Abstract value for each component of the domain. *) module V : sig - include module type of T.V + type t - val transform : Witnesses.t -> t -> t + (** order of the abstract domain *) + val lessequal : t -> t -> bool + + val join : t -> t -> t + + val meet : t -> t -> t + + val transform : t -> t -> t val replace_witnesses : Witnesses.t -> t -> t val diff_witnesses : expected:t -> actual:t -> Witnesses.t val get_witnesses : t -> Witnesses.t + + val print : witnesses:bool -> Format.formatter -> t -> unit + + val unresolved : Witnesses.t -> Var.t -> t + + val is_resolved : t -> bool + + val get_unresolved_names : t -> String.Set.t + + val apply : t -> env:(Var.t -> t option) -> t + + val bot : t + + val safe : t + + val top : Witnesses.t -> t + + (** [compare] is structural on terms (for the use of [V.t] as a key in sets and maps), + whereas [lessequal] is the order of the abstract domain (for fixed point checks). *) + val compare : t -> t -> int + + val match_with : + bot:'a -> + safe:'a -> + top:(Witnesses.t -> 'a) -> + unresolved:(unit -> 'a) -> + t -> + 'a end = struct - include T.V + let pp_w ~witnesses ppf w = + if witnesses then Format.fprintf ppf "@, (%a)" Witnesses.print w else () + + let pp_var ~witnesses ppf var w = + Format.fprintf ppf "(%a%a)@," Var.print var (pp_w ~witnesses) w + + let pp_top ~witnesses ppf w = Format.fprintf ppf "(top%a)" (pp_w ~witnesses) w + + (** Variables with witnesses *) + module Vars : sig + type t + + val empty : t + + val compare : t -> t -> int + + (** [same_vars] compares variables ignoring witnesses *) + val same_vars : t -> t -> bool + + val get_vars : t -> Var.Set.t + + val get_unresolved_name : t -> String.Set.t + + val join : t -> t -> t + + val update : t -> Var.t -> Witnesses.t -> t + + val singleton : Var.t -> Witnesses.t -> t + + val has_witnesses : t -> bool + + val replace_witnesses : t -> Witnesses.t -> t + + val print : witnesses:bool -> Format.formatter -> t -> unit + + val fold : + f:(Var.t -> Witnesses.t -> 'acc -> 'acc) -> init:'acc -> t -> 'acc + + val exists : (Var.t -> Witnesses.t -> bool) -> t -> bool + + val cutoff : t -> int -> t + + val cutoff_witnesses : t -> int -> t + end = struct + type t = Witnesses.t Var.Map.t + + let empty = Var.Map.empty + + let fold ~f ~init t = Var.Map.fold f t init + + let singleton var w = Var.Map.singleton var w + + let compare t1 t2 = Var.Map.compare Witnesses.compare t1 t2 + + let same_vars = Var.Map.equal (fun _ _ -> (* ignore witnesses *) true) + + let get_vars t = + (* CR-someday gyorsh: If this is called often, it may be better to store + the result of [get_vars t] in [t] instead of recomputing it. *) + t |> Var.Map.to_seq |> Seq.map fst |> Var.Set.of_seq + + let get_unresolved_name t = + t |> Var.Map.to_seq |> Seq.map fst |> Seq.map Var.name + |> String.Set.of_seq + + let exists p t = Var.Map.exists p t + + let has_witnesses vars = exists (fun _ w -> not (Witnesses.is_empty w)) vars + + let join t1 t2 = + Var.Map.union (fun _var w1 w2 -> Some (Witnesses.join w1 w2)) t1 t2 + + let update t var witnesses = + Var.Map.update var + (function + | None -> Some witnesses | Some w -> Some (Witnesses.join w witnesses)) + t + + let replace_witnesses t w = Var.Map.map (fun _ -> w) t + + let print ~witnesses ppf t = + Var.Map.iter (fun var w -> pp_var ~witnesses ppf var w) t + + let cutoff_witnesses t n = Var.Map.map (Witnesses.cutoff ~n) t + + let cutoff t n = + let t = cutoff_witnesses t n in + take_first_n t n ~to_seq:Var.Map.to_seq ~of_seq:Var.Map.of_seq + ~cardinal:Var.Map.cardinal + end + + (** Normal form of Transform. + [Transform] represents an abstract transformer of a primitive + such as a function call. *) + module Transform : sig + type t + + val var_with_top : Var.t -> var_witnesses:Witnesses.t -> Witnesses.t -> t + + val add_top : t -> Witnesses.t -> t + + val add_var : t -> Var.t -> Witnesses.t -> t + + val vars : var1:Var.t -> w1:Witnesses.t -> var2:Var.t -> w2:Witnesses.t -> t + + val print : witnesses:bool -> Format.formatter -> t -> unit + + val compare : t -> t -> int + + val equal : t -> t -> bool + + val has_witnesses : t -> bool + + val replace_witnesses : t -> Witnesses.t -> t + + val flatten : t -> t -> t + + val get_top : t -> Witnesses.t option + + val get_vars : t -> Vars.t + + (** [same_vars] compares variables ignoring witnesses *) + val same_vars : t -> t -> bool + + (** does not change the number of variables, only their witnesses. *) + val cutoff_witnesses : t -> n:int -> t + end = struct + type t = + | Args of Vars.t + | Args_with_top of + { w : Witnesses.t; + vars : Vars.t + } + + (* The binary "transform" is commutative and associative, so a nested + "transform" can be flattened in the normal form. The arguments are + represented as a set of variables and optionally top. if top is absent, + [vars] must contain at least two elements. if top is present, [vars] must + have at least one element. This is enforced by the available + constructors. + + We never need to represent other constants because these cases can be + simplified to either a constant or a variable. *) + + let compare t1 t2 = + match t1, t2 with + | Args a1, Args a2 -> Vars.compare a1 a2 + | Args _, Args_with_top _ -> -1 + | Args_with_top _, Args _ -> 1 + | ( Args_with_top { w = w1; vars = vars1 }, + Args_with_top { w = w2; vars = vars2 } ) -> + let c = Vars.compare vars1 vars2 in + if c <> 0 then c else Witnesses.compare w1 w2 + + let cutoff_witnesses t ~n = + match t with + | Args vars -> Args (Vars.cutoff_witnesses vars n) + | Args_with_top { w; vars } -> + Args_with_top + { w = Witnesses.cutoff w ~n; vars = Vars.cutoff_witnesses vars n } + + let equal t1 t2 = compare t1 t2 = 0 + + let var_with_top var ~var_witnesses w = + let vars = Vars.singleton var var_witnesses in + Args_with_top { w; vars } + + let vars ~var1 ~w1 ~var2 ~w2 = + assert (not (Var.equal var1 var2)); + let vars = Vars.(update (singleton var1 w1) var2 w2) in + Args vars + + let add_top t w = + match t with + | Args vars -> Args_with_top { w; vars } + | Args_with_top { w = w'; vars } -> + Args_with_top { w = Witnesses.join w w'; vars } + + let add_var t var witnesses = + (* CR gyorsh: future optimization is to return [t] when vars is phys equal + to (update vars).*) + match t with + | Args vars -> Args (Vars.update vars var witnesses) + | Args_with_top { w; vars } -> + Args_with_top { w; vars = Vars.update vars var witnesses } + + let flatten tr1 tr2 = + match tr1, tr2 with + | ( Args_with_top { w = w1; vars = vars1 }, + Args_with_top { w = w2; vars = vars2 } ) -> + Args_with_top { w = Witnesses.join w1 w2; vars = Vars.join vars1 vars2 } + | Args_with_top { w; vars }, Args vars' + | Args vars', Args_with_top { w; vars } -> + Args_with_top { w; vars = Vars.join vars vars' } + | Args vars1, Args vars2 -> Args (Vars.join vars1 vars2) + + let get_top t = + match t with Args_with_top { w; vars = _ } -> Some w | Args _ -> None + + let get_vars t = + match t with Args_with_top { w = _; vars } | Args vars -> vars + + let same_vars t1 t2 = Vars.same_vars (get_vars t1) (get_vars t2) + + let has_witnesses t = + match t with + | Args_with_top { w; vars } -> + Vars.has_witnesses vars || not (Witnesses.is_empty w) + | Args vars -> Vars.has_witnesses vars + + let replace_witnesses t w = + match t with + | Args vars -> Args (Vars.replace_witnesses vars w) + | Args_with_top { w = _; vars } -> + Args_with_top { w; vars = Vars.replace_witnesses vars w } + + let print ~witnesses ppf t = + match t with + | Args vars -> + Format.fprintf ppf "(transform:@.%a)@." (Vars.print ~witnesses) vars + | Args_with_top { w; vars } -> + Format.fprintf ppf "(transform:@.%a@.%a)@." (pp_top ~witnesses) w + (Vars.print ~witnesses) vars + end + + module Transforms : sig + type t + + val join : t -> t -> t + + val empty : t + + val add : Transform.t -> t -> t + + val compare : t -> t -> int + + val cutoff : t -> int -> t + + val iter : (Transform.t -> unit) -> t -> unit + + val map : (Transform.t -> Transform.t) -> t -> t + + val fold : (Transform.t -> 'a -> 'a) -> t -> 'a -> 'a + + val exists : (Transform.t -> bool) -> t -> bool + + val get_unresolved_names : t -> String.Set.t + + exception Widen + end = struct + (* Join of two Transform with the same set of vars: merged both sets of Vars + into one Transform in normal form, without loss of precision or + witnesses, even if one Transform has "Top" and the other does not. + + Naive implementation: map with key of type [Var.Set.t] to data of type + [Transform.t] *) + module M = Map.Make (Var.Set) + + type t = Transform.t M.t + + exception Widen + + let maybe_widen t = + match !Flambda_backend_flags.checkmach_join with + | Keep_all -> t + | Widen n -> if M.cardinal t > n then raise Widen else t + | Error n -> + if M.cardinal t > n + then + Misc.fatal_errorf + "Join with %d paths is too big, use -disable-precise-checkmach" + (M.cardinal t) + else t + + let empty = M.empty + + let get_key tr = tr |> Transform.get_vars |> Vars.get_vars + + let get_unresolved_names t = + (* collect the keys *) + t |> M.to_seq |> Seq.map fst |> Seq.map Var.Set.to_seq |> Seq.concat + |> Seq.map Var.name |> String.Set.of_seq + + let add tr t = + let res = M.add (get_key tr) tr t in + maybe_widen res + + let compare t1 t2 = M.compare Transform.compare t1 t2 + + let iter f t = M.iter (fun _key tr -> f tr) t + + let fold f t init = M.fold (fun _key tr acc -> f tr acc) t init + + let exists f t = M.exists (fun _key tr -> f tr) t + + let join t1 t2 = + let res = + M.union (fun _var tr1 tr2 -> Some (Transform.flatten tr1 tr2)) t1 t2 + in + maybe_widen res + + let map f t = M.fold (fun _key tr acc -> add (f tr) acc) t M.empty + + let cutoff t n = + let t = map (Transform.cutoff_witnesses ~n) t in + take_first_n t n ~to_seq:M.to_seq ~of_seq:M.of_seq ~cardinal:M.cardinal + end + + (* CR-someday gyorsh: treatment of vars and top is duplicated between Args and + Transform, is there a nice way to factor it out? + + For instance, Join.t could be defined as a record { args : Args.t; ... } + with the ellipsis encoding top/safe. It may simplify a couple of functions + in the Join module, and perhaps lead to a type like { args : Args.t; rest : + 'a; } that could then be used in other modules such as Transform. *) + + (** helper for Join *) + module Args : sig + type t + + val add_tr : t -> Transform.t -> t + + val add_var : t -> Var.t -> Witnesses.t -> t + + val empty : t + + val join : t -> t -> t + + val get : t -> Vars.t * Transforms.t + + (** [transform t tr] replace each element x of [t] with "transform x tr" *) + val transform : t -> Transform.t -> t + + (** [transform_var t var w] + replace each element x of [t] with "transfrom x var". *) + val transform_var : t -> Var.t -> Witnesses.t -> t + + (** [transform_top t w] replace each element x of [t] with + "transform t (Top w)" *) + val transform_top : t -> Witnesses.t -> t + + val transform_join : t -> t -> t + + val has_witnesses : t -> bool + + val replace_witnesses : t -> Witnesses.t -> t + + val cutoff : t -> int -> t + + val compare : t -> t -> int + + val print : witnesses:bool -> Format.formatter -> t -> unit + end = struct + type t = + { vars : Vars.t; + trs : Transforms.t + } + + let empty = { vars = Vars.empty; trs = Transforms.empty } - (** abstract transformer (backward analysis) for a statement that violates the property - but doesn't alter control flow. *) - let transform w = function - | Bot -> - (* if a return is unreachable from the program location immediately after - the statement, then return is unreachable from the program location - immediately before the statement. *) - Bot - | Safe -> Top w - | Top w' -> Top (Witnesses.join w w') + let get { vars; trs } = vars, trs - let replace_witnesses w t = match t with Top _ -> Top w | Bot | Safe -> t + let print ~witnesses ppf { vars; trs } = + let pp_trs ppf trs = + Transforms.iter (Transform.print ~witnesses ppf) trs + in + Format.fprintf ppf "vars=(%a)@.transforms=(%a)@," (Vars.print ~witnesses) + vars pp_trs trs + + let add_var t var witnesses = + (* Optimization to avoid allocation when the content hasn't changed. *) + let vars = Vars.update t.vars var witnesses in + if vars == t.vars then t else { t with vars } + + let add_tr t tr = + let trs = Transforms.add tr t.trs in + if trs == t.trs then t else { t with trs } + + let join ({ vars = v1; trs = trs1 } as t) ({ vars = v2; trs = trs2 } as t') + = + if debug + then + Format.fprintf Format.std_formatter "join@.%a@. %a@." + (print ~witnesses:true) t (print ~witnesses:true) t'; + let vars = Vars.join v1 v2 in + let trs = Transforms.join trs1 trs2 in + { vars; trs } + + let transform { vars; trs } tr = + let from_vars = + (* add each x from [vars] to [tr] *) + Vars.fold + ~f:(fun var w acc -> Transforms.add (Transform.add_var tr var w) acc) + vars ~init:Transforms.empty + in + let from_trs = Transforms.map (fun tr' -> Transform.flatten tr tr') trs in + { vars = Vars.empty; trs = Transforms.join from_vars from_trs } + + let transform_top { vars; trs } w = + let from_vars = + Vars.fold + ~f:(fun var var_witnesses acc -> + Transforms.add (Transform.var_with_top var ~var_witnesses w) acc) + vars ~init:Transforms.empty + in + let from_trs = Transforms.map (fun tr -> Transform.add_top tr w) trs in + { vars = Vars.empty; trs = Transforms.join from_vars from_trs } + + let transform_var { vars; trs } var witnesses = + let acc = + Vars.fold + ~f:(fun var1 w1 args -> + if Var.equal var1 var + then add_var args var witnesses + else + let tr = Transform.vars ~var1 ~w1 ~var2:var ~w2:witnesses in + add_tr args tr) + vars ~init:empty + in + let from_trs = + Transforms.map (fun tr -> Transform.add_var tr var witnesses) trs + in + { acc with trs = Transforms.join from_trs acc.trs } + + let transform_join t ({ vars; trs } as t') = + if debug + then + Format.fprintf Format.std_formatter "transform_join@.%a@. %a@." + (print ~witnesses:true) t (print ~witnesses:true) t'; + let acc = + Vars.fold vars ~init:empty ~f:(fun var witnesses acc -> + join acc (transform_var t var witnesses)) + in + Transforms.fold (fun tr acc -> join acc (transform t tr)) trs acc + + let has_witnesses { vars; trs } = + Vars.has_witnesses vars || Transforms.exists Transform.has_witnesses trs + + let replace_witnesses { vars; trs } w = + { vars = Vars.replace_witnesses vars w; + trs = Transforms.map (fun tr -> Transform.replace_witnesses tr w) trs + } + + let cutoff { vars; trs } n = + { vars = Vars.cutoff vars n; trs = Transforms.cutoff trs n } + + let compare { vars = vars1; trs = trs1 } { vars = vars2; trs = trs2 } = + let c = Vars.compare vars1 vars2 in + if c <> 0 then c else Transforms.compare trs1 trs2 + end + + (** normal form of join *) + module Join : sig + type t + + val tr_with_safe : Transform.t -> t + + val tr_with_top : Transform.t -> Witnesses.t -> t + + val var_with_top : Var.t -> var_witnesses:Witnesses.t -> Witnesses.t -> t + + val var_with_safe : Var.t -> Witnesses.t -> t + + val var_with_tr : Var.t -> Witnesses.t -> Transform.t -> t + + val vars : var1:Var.t -> w1:Witnesses.t -> var2:Var.t -> w2:Witnesses.t -> t + + val trs : Transform.t -> Transform.t -> t + + val add_top : t -> Witnesses.t -> t + + val add_safe : t -> t + + val add_var : t -> Var.t -> Witnesses.t -> t + + val add_tr : t -> Transform.t -> t + + val flatten : t -> t -> unit -> t + + val distribute_transform_over_join : t -> Transform.t -> unit -> t + + val distribute_transform_var_over_join : + t -> Var.t -> Witnesses.t -> unit -> t + + val distribute_transform_top_over_join : t -> Witnesses.t -> unit -> t + + val distribute_transform_over_joins : t -> t -> unit -> t + + val get_top : t -> Witnesses.t option + + val has_safe : t -> bool + + val get : t -> Vars.t * Transforms.t + + val print : witnesses:bool -> Format.formatter -> t -> unit + + val has_witnesses : t -> bool + + val replace_witnesses : t -> Witnesses.t -> t + + val compare : t -> t -> int + + val get_unresolved_names : t -> String.Set.t + end = struct + type t = + | Args_with_safe of Args.t + | Args_with_top of + { w : Witnesses.t; + args : Args.t + } + | Args of Args.t + + (* Tracks "top" to preserve witnesses. For example simplifying + * "join (Top w) (Var v w')" to "Top w" + * loses the witness w' when w' is non-empty and v resolved to Top at the end. + * Simplifying to "Top (join w w')" is wrong if v is resolved to Safe or Bot. *) + + (* Only Top or Safe are allowed not both. At least two elements must be + present in the join: if one of the constants is present then at least one + of vars or transforms must be non-empty. If no constants, then vars or + transforms have at least two elements between them. The following + constructor ensure it. *) + + (* [cutoff] is a heuristic to limit the size of the representation when + tracking witnesses. Adding [@zero_alloc] assert on a function has a + limited overhead on compilation time and memory. + + The representation may be resolved to more than [n] witnesses (e.g., + different variables from Args.vars and Args.trs) or less than [n] + witnesses (when some of the variables are not resolved to Top and + therefore don't contribute witnesses). + + Cutoff for "join with top" does not affect the precision of generated + summaries, only the number of witnesses reported. + + Termination of fixpoint: [Args] is sorted, [Arg.cutoff] keeps the least + [n], and [Arg.join] is used for fixpoint computation before applying the + cutoff. *) + let args_with_top w args = + if not (Args.has_witnesses args) + then + Misc.fatal_errorf "Join Top without witnesses in args:%a" + (Args.print ~witnesses:false) + args; + match !Flambda_backend_flags.checkmach_details_cutoff with + | Keep_all -> Args_with_top { w; args } + | No_details -> + Misc.fatal_errorf "unexpected: (Join (Top %a) %a) " Witnesses.print w + (Args.print ~witnesses:true) + args + | At_most n -> + (* Normal form after cutoff: args contains at least one element even + after cutoff because [n] is guaranteed to be positive. *) + let len = Witnesses.size w in + if len > n + then + Misc.fatal_errorf "expected at most %d witnesses, got %d: %a" n len + Witnesses.print w; + Args_with_top { w; args = Args.cutoff args n } + + let tr_with_safe tr = Args_with_safe Args.(add_tr empty tr) + + let tr_with_top tr w = args_with_top w Args.(add_tr empty tr) + + let var_with_top var ~var_witnesses w = + args_with_top w Args.(add_var empty var var_witnesses) + + let var_with_safe var w = Args_with_safe Args.(add_var empty var w) + + let trs tr1 tr2 = + assert (not (Transform.equal tr1 tr2)); + Args Args.(add_tr (add_tr empty tr1) tr2) + + let vars ~var1 ~w1 ~var2 ~w2 = + assert (not (Var.equal var1 var2)); + Args Args.(add_var (add_var empty var2 w2) var1 w1) + + let var_with_tr var w tr = Args Args.(add_var (add_tr empty tr) var w) + + let add_safe t = + match t with + | Args_with_top _ -> t + | Args_with_safe _ -> t + | Args args -> Args_with_safe args + + let add_top t witnesses = + match t with + | Args_with_top { w; args } -> + args_with_top (Witnesses.join w witnesses) args + | Args_with_safe args | Args args -> args_with_top witnesses args + + let add_var t var witnesses = + match t with + | Args_with_safe args -> Args_with_safe (Args.add_var args var witnesses) + | Args args -> Args (Args.add_var args var witnesses) + | Args_with_top { w; args } -> + args_with_top w (Args.add_var args var witnesses) + + let flatten t1 t2 () = + match t1, t2 with + | Args a1, Args a2 -> Args (Args.join a1 a2) + | Args_with_safe a1, Args_with_safe a2 -> Args_with_safe (Args.join a1 a2) + | Args_with_top { w; args = a1 }, (Args a2 | Args_with_safe a2) + | (Args a2 | Args_with_safe a2), Args_with_top { w; args = a1 } -> + args_with_top w (Args.join a1 a2) + | Args_with_top { w = w1; args = a1 }, Args_with_top { w = w2; args = a2 } + -> + args_with_top (Witnesses.join w1 w2) (Args.join a1 a2) + | Args args1, Args_with_safe args2 | Args_with_safe args1, Args args2 -> + Args_with_safe (Args.join args1 args2) + + let distribute_transform_over_join t tr () = + match t with + | Args_with_safe args -> + let args = Args.(add_tr (transform args tr) tr) in + Args args + | Args_with_top { w; args } -> + let tr' = Transform.add_top tr w in + let args = Args.(add_tr (transform args tr) tr') in + Args args + | Args args -> Args (Args.transform args tr) + + let distribute_transform_var_over_join t var witnesses () = + match t with + | Args_with_safe args -> + let args = + Args.add_var (Args.transform_var args var witnesses) var witnesses + in + Args args + | Args_with_top { w; args } -> + let tr' = Transform.var_with_top var ~var_witnesses:witnesses w in + let args = Args.(add_tr (transform_var args var witnesses) tr') in + Args args + | Args args -> Args (Args.transform_var args var witnesses) + + let distribute_transform_top_over_join t w () = + match t with + | Args_with_safe args -> + let args = Args.transform_top args w in + args_with_top w args + | Args_with_top { w = w'; args } -> + let args = Args.(transform_top args w) in + args_with_top (Witnesses.join w' w) args + | Args args -> Args (Args.transform_top args w) + + let distribute_transform_over_joins t1 t2 () = + match t1, t2 with + | Args a1, Args a2 -> Args (Args.transform_join a1 a2) + | Args_with_safe a1, Args_with_safe a2 -> + let new_args = Args.transform_join a1 a2 in + Args_with_safe (Args.join a1 (Args.join a2 new_args)) + | Args_with_safe a1, Args a2 | Args a2, Args_with_safe a1 -> + let new_args = Args.transform_join a1 a2 in + Args (Args.join a2 new_args) + | Args_with_top { w = w1; args = a1 }, Args_with_top { w = w2; args = a2 } + -> + if debug + then + Format.printf "distribute_transform_over_joins:@.%a@.%a@." + (Args.print ~witnesses:true) + a1 + (Args.print ~witnesses:true) + a2; + let new_args = Args.transform_join a1 a2 in + let args_top = + Args.join (Args.transform_top a1 w2) (Args.transform_top a2 w1) + in + args_with_top (Witnesses.join w1 w2) (Args.join new_args args_top) + | Args_with_top { w; args = a1 }, Args a2 + | Args a2, Args_with_top { w; args = a1 } -> + let new_args = Args.transform_join a1 a2 in + let args_top = Args.transform_top a2 w in + Args (Args.join new_args args_top) + | Args_with_top { w; args = a1 }, Args_with_safe a2 + | Args_with_safe a2, Args_with_top { w; args = a1 } -> + let new_args = Args.transform_join a1 a2 in + let args_top = Args.transform_top a2 w in + let args = Args.join new_args args_top in + args_with_top w args + + let add_tr t tr = + match t with + | Args_with_safe args -> Args_with_safe (Args.add_tr args tr) + | Args args -> Args (Args.add_tr args tr) + | Args_with_top { w; args } -> args_with_top w (Args.add_tr args tr) + + let get_top t = + match t with + | Args_with_top { w; args = _ } -> Some w + | Args _ | Args_with_safe _ -> None + + let has_safe t = + match t with + | Args_with_safe _ -> true + | Args _ | Args_with_top _ -> false + + let get t = + match t with + | Args_with_top { w = _; args } | Args args | Args_with_safe args -> + Args.get args + + let has_witnesses t = + match t with + | Args_with_safe args | Args args -> Args.has_witnesses args + | Args_with_top { w; args } -> + (not (Witnesses.is_empty w)) || Args.has_witnesses args + + let replace_witnesses t witnesses = + match t with + | Args_with_safe args -> + Args_with_safe (Args.replace_witnesses args witnesses) + | Args args -> Args (Args.replace_witnesses args witnesses) + | Args_with_top { w = _; args } -> + args_with_top witnesses (Args.replace_witnesses args witnesses) + + let compare t1 t2 = + match t1, t2 with + | Args a1, Args a2 | Args_with_safe a1, Args_with_safe a2 -> + Args.compare a1 a2 + | Args _, _ -> -1 + | _, Args _ -> 1 + | Args_with_safe _, _ -> -1 + | _, Args_with_safe _ -> 1 + | Args_with_top { w = w1; args = a1 }, Args_with_top { w = w2; args = a2 } + -> + let c = Witnesses.compare w1 w2 in + if c <> 0 then c else Args.compare a1 a2 + + let get_unresolved_names t = + match t with + | Args_with_safe args | Args_with_top { w = _; args } | Args args -> + let vars, trs = Args.get args in + String.Set.union + (Vars.get_unresolved_name vars) + (Transforms.get_unresolved_names trs) + + let print ~witnesses ppf t = + match t with + | Args_with_safe args -> + Format.fprintf ppf "(join:@.Safe@.%a)@." (Args.print ~witnesses) args + | Args_with_top { w; args } -> + Format.fprintf ppf "(join:@.%a@.%a)@." (pp_top ~witnesses) w + (Args.print ~witnesses) args + | Args args -> + Format.fprintf ppf "(join:@.%a)@." (Args.print ~witnesses) args + end + + type t = + | Top of Witnesses.t + | Safe + | Bot + (* unresolved *) + | Var of + { var : Var.t; + witnesses : Witnesses.t + } + | Transform of Transform.t + | Join of Join.t + + let unresolved witnesses var = Var { var; witnesses } + + let bot = Bot + + let safe = Safe + + let top w = Top w + + let is_resolved t = + match t with + | Top _ | Safe | Bot -> true + | Var _ | Join _ | Transform _ -> false + + let get_unresolved_names t = + match t with + | Bot | Safe | Top _ -> String.Set.empty + | Var { var; _ } -> String.Set.singleton (Var.name var) + | Transform tr -> Transform.get_vars tr |> Vars.get_unresolved_name + | Join j -> Join.get_unresolved_names j + + let print ~witnesses ppf t = + match t with + | Bot -> Format.fprintf ppf "bot" + | Safe -> Format.fprintf ppf "safe" + | Top w -> pp_top ~witnesses ppf w + | Var { var; witnesses = w } -> pp_var ~witnesses ppf var w + | Join j -> Format.fprintf ppf "(join %a)@," (Join.print ~witnesses) j + | Transform tr -> + Format.fprintf ppf "(transform %a)@," (Transform.print ~witnesses) tr + + let match_with ~bot ~safe ~top ~unresolved t = + match t with + | Bot -> bot + | Safe -> safe + | Top w -> top w + | Var _ | Join _ | Transform _ -> unresolved () let get_witnesses t = - match t with Top w -> w | Bot | Safe -> Witnesses.empty + match t with + | Top w -> w + | Bot | Safe -> Witnesses.empty + | Var _ | Transform _ | Join _ -> assert false + + (* structural *) + let compare t1 t2 = + match t1, t2 with + | Bot, Bot -> 0 + | Bot, _ -> -1 + | _, Bot -> 1 + | Safe, Safe -> 0 + | Safe, _ -> -1 + | _, Safe -> 1 + | Top w1, Top w2 -> Witnesses.compare w1 w2 + | Top _, (Var _ | Transform _ | Join _) -> -1 + | (Var _ | Transform _ | Join _), Top _ -> 1 + | Var { var = v1; witnesses = w1 }, Var { var = v2; witnesses = w2 } -> + let c = Var.compare v1 v2 in + if c = 0 then Witnesses.compare w1 w2 else c + | Var _, _ -> -1 + | _, Var _ -> 1 + | Transform tr1, Transform tr2 -> Transform.compare tr1 tr2 + | Transform _, _ -> -1 + | _, Transform _ -> 1 + | Join j1, Join j2 -> Join.compare j1 j2 + + let equal t1 t2 = compare t1 t2 = 0 + + (* This naive normal form is conceptually "dnf". Currently very inefficient, + does not guarantee sharing, and reallocates even if the input is already in + a normal form. Worst case exponential space (in the number of variables). + Someday it can be optimized using hash consing and bdd-like + representation. *) + + let bounded_join f = + try Join (f ()) with Transforms.Widen -> Top Witnesses.empty + + (* Keep [join] and [lessequal] in sync. *) + let join t1 t2 = + match t1, t2 with + | Bot, Bot -> Bot + | Safe, Safe -> Safe + | Top w1, Top w2 -> Top (Witnesses.join w1 w2) + | Safe, Bot | Bot, Safe -> Safe + | Top _, Bot | Top _, Safe -> t1 + | Bot, Top _ | Safe, Top _ -> t2 + | Bot, (Var _ | Transform _ | Join _) -> t2 + | (Var _ | Transform _ | Join _), Bot -> t1 + | Safe, Transform tr | Transform tr, Safe -> Join (Join.tr_with_safe tr) + | Safe, Var { var; witnesses } | Var { var; witnesses }, Safe -> + Join (Join.var_with_safe var witnesses) + | (Top w as top), Var { var; witnesses } + | Var { var; witnesses }, (Top w as top) -> + if Witnesses.is_empty witnesses + then top + else Join (Join.var_with_top var ~var_witnesses:witnesses w) + | Var { var = var1; witnesses = w1 }, Var { var = var2; witnesses = w2 } -> + if Var.equal var1 var2 + then Var { var = var1; witnesses = Witnesses.join w1 w2 } + else Join (Join.vars ~var1 ~w1 ~var2 ~w2) + | Var { var; witnesses }, Transform tr + | Transform tr, Var { var; witnesses } -> + Join (Join.var_with_tr var witnesses tr) + | Transform tr1, Transform tr2 -> + if Transform.equal tr1 tr2 + then t1 + else if Transform.same_vars tr1 tr2 + then Transform (Transform.flatten tr1 tr2) + else Join (Join.trs tr1 tr2) + | (Top w as top), Transform tr | Transform tr, (Top w as top) -> + (* [has_witnesses]: Don't simplify (join Top x) to x if there are any + witnesses in x. This makes the analysis more expensive because symbolic + summaries cannot be simplified as much. Finding out if there are + witnesses is also expensive (traverse the entire term). Someday, we can + make it cheap by passing [keep_witnesses] to all operations. Only + functions that need to be checked against a user-provided annotation at + the end keep witnesses, unless the analysis is used to visualize all + allocations. We can put a bound on the number of witnesses recorded, + but it would make the resulting error messages sensitive to iteration + order. *) + if Transform.has_witnesses tr then Join (Join.tr_with_top tr w) else top + | (Top w as top), Join j | Join j, (Top w as top) -> + if Join.has_witnesses j then Join (Join.add_top j w) else top + | Safe, Join j | Join j, Safe -> Join (Join.add_safe j) + | Var { var; witnesses }, Join j | Join j, Var { var; witnesses } -> + Join (Join.add_var j var witnesses) + | Join j, Transform tr | Transform tr, Join j -> Join (Join.add_tr j tr) + | Join j1, Join j2 -> bounded_join (Join.flatten j1 j2) + + (* CR gyorsh: Handling of constant cases here is an optimization, instead of + going directly to [join]. *) + let lessequal t1 t2 = + match t1, t2 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 + | Bot, (Var _ | Transform _ | Join _) -> true + | (Var _ | Transform _ | Join _), Bot -> false + | (Safe | Top _ | Var _ | Transform _ | Join _), _ -> + (* structural equality on the normal form *) + equal (join t1 t2) t2 + + (* Abstract transformer. Commutative and Associative. + + let transform t t' = if t = V.Bot || t' = V.Bot then V.Bot else (V.join t + t') + + The implementation is an optimized version of the above definition that + "inlines" and "specializes" join: efficiently handle definitive cases and + preserve normal form of unresolved. + + Soundness (intuitively): If a return is unreachable from the program + location immediately after the statement, or the statement does not return, + then return is unreachable from the program location immediately before the + statement. *) + let transform t t' = + match t, t' with + | Bot, _ -> Bot + | _, Bot -> Bot + | Safe, t' -> t' + | t, Safe -> t + | Top w, Top w' -> Top (Witnesses.join w w') + | Top w, Transform tr | Transform tr, Top w -> + Transform (Transform.add_top tr w) + | Top w, Var { var; witnesses } | Var { var; witnesses }, Top w -> + Transform (Transform.var_with_top var ~var_witnesses:witnesses w) + | Var { var; witnesses }, Transform tr + | Transform tr, Var { var; witnesses } -> + Transform (Transform.add_var tr var witnesses) + | Var { var = var1; witnesses = w1 }, Var { var = var2; witnesses = w2 } -> + if Var.equal var1 var2 + then Var { var = var1; witnesses = Witnesses.join w1 w2 } + else Transform (Transform.vars ~var1 ~w1 ~var2 ~w2) + | Transform tr1, Transform tr2 -> Transform (Transform.flatten tr1 tr2) + | Transform tr, Join j | Join j, Transform tr -> + bounded_join (Join.distribute_transform_over_join j tr) + | (Top w as top), Join j | Join j, (Top w as top) -> + if Join.has_safe j && not (Join.has_witnesses j) + then top + else bounded_join (Join.distribute_transform_top_over_join j w) + | Var { var; witnesses }, Join j | Join j, Var { var; witnesses } -> + bounded_join (Join.distribute_transform_var_over_join j var witnesses) + | Join j1, Join j2 -> + bounded_join (Join.distribute_transform_over_joins j1 j2) + + (* CR-soon xclerc for gyorsh: It may be valuable to gather the elements about + the "constructors" (e.g. join, transform above) in one place, with the + theoretical properties (e.g. neutral or absorbing elements, distribution), + while keeping the comments about implementation choices and/or imperatives + (e.g. why/how witnesses are tracked) next to the code. *) + + let replace_witnesses w t = + match t with + | Top _ -> Top w + | Bot | Safe -> t + | Join j -> Join (Join.replace_witnesses j w) + | Transform tr -> Transform (Transform.replace_witnesses tr w) + | Var { var; witnesses = _ } -> Var { var; witnesses = w } let diff_witnesses ~expected ~actual = (* If [actual] is Top and [expected] is not Top then return the [actual] @@ -180,25 +1240,128 @@ end = struct Witnesses.empty | Safe, Bot -> Witnesses.empty | Top w, (Bot | Safe) -> w + | (Var _ | Join _ | Transform _), _ | _, (Var _ | Join _ | Transform _) -> + assert false + + let meet t1 t2 = + match t1, t2 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 + | (Var _ | Transform _ | Join _), _ | _, (Var _ | Transform _ | Join _) -> + Misc.fatal_error + "Meet of unresolved is not implemented and shouldn't be needed." + + let apply t ~env = + let get env var w = + match env var with + | None -> unresolved w var + | Some v -> replace_witnesses w v + in + let contains_any env vars = + Vars.exists (fun var _w -> Option.is_some (env var)) vars + in + (* CR-someday gyorsh: This is a naive implementation that reallocates the + entire [t] whenever there is a change. Can be optimized to update the + underlying sets and maps instead of using [fold]. *) + let rec aux t = + match t with + | Bot | Safe | Top _ -> t + | Var { var; witnesses } -> ( + match env var with None -> t | Some v -> replace_witnesses witnesses v) + | Transform tr -> + let vars = Transform.get_vars tr in + if not (contains_any env vars) + then t + else + let init = + match Transform.get_top tr with None -> Safe | Some w -> Top w + in + Vars.fold + ~f:(fun var w acc -> transform (get env var w) acc) + ~init vars + | Join j -> + let vars, trs = Join.get j in + if (not (contains_any env vars)) + && not + (Transforms.exists + (fun tr -> contains_any env (Transform.get_vars tr)) + trs) + then t + else + let init = + match Join.get_top j with + | None -> if Join.has_safe j then Safe else Bot + | Some w -> Top w + in + let acc = + Vars.fold ~f:(fun var w acc -> join (get env var w) acc) ~init vars + in + Transforms.fold + (fun tr acc -> + let t = Transform tr in + join (aux t) acc) + trs acc + in + aux t end +module T = Zero_alloc_utils.Make_value (Witnesses) (V) + module Value : sig - include module type of T.Value + include module type of T - val transform : Witnesses.t -> t -> t + val transform : V.t -> t -> t val replace_witnesses : Witnesses.t -> t -> t + val get_unresolved_names : t -> String.Set.t + val get_witnesses : t -> Witnesses.components val diff_witnesses : expected:t -> actual:t -> Witnesses.components + + val unresolved : string -> Witnesses.t -> t + + val is_resolved : t -> bool + + val get_component : t -> Tag.t -> V.t + + val apply : t -> (Var.t -> V.t option) -> t end = struct - include T.Value + include T + + let unresolved name w = + { nor = Var.create name Tag.N |> V.unresolved w; + exn = Var.create name Tag.E |> V.unresolved w; + div = Var.create name Tag.D |> V.unresolved w + } + + let is_resolved t = + V.is_resolved t.nor && V.is_resolved t.exn && V.is_resolved t.div + + let get_unresolved_names t = + String.Set.( + union + (V.get_unresolved_names t.nor) + (union (V.get_unresolved_names t.exn) (V.get_unresolved_names t.div))) + + let get_component t (tag : Tag.t) = + match tag with N -> t.nor | E -> t.exn | D -> t.div + + let apply t env = + { nor = V.apply t.nor ~env; + exn = V.apply t.exn ~env; + div = V.apply t.div ~env + } - let transform w v = - { nor = V.transform w v.nor; - exn = V.transform w v.exn; - div = V.transform w v.div + let transform effect v = + { nor = V.transform effect v.nor; + exn = V.transform effect v.exn; + div = V.transform effect v.div } let replace_witnesses w t = @@ -274,7 +1437,7 @@ end = struct let get_loc t = t.loc let expected_value - { strict; never_returns_normally; assume = _; loc = _; never_raises } = + { strict; never_returns_normally; never_raises; assume = _; loc = _ } = Value.of_annotation ~strict ~never_returns_normally ~never_raises let valid t v = @@ -347,7 +1510,7 @@ end = struct always empty and the translation is trivial. Is there a better way to avoid duplicating [Zero_alloc_utils]? *) let transl w (v : Zero_alloc_utils.Assume_info.V.t) : V.t = - match v with Top _ -> Top w | Safe -> Safe | Bot -> Bot + match v with Top _ -> V.top w | Safe -> V.safe | Bot -> V.bot let transl w (v : Zero_alloc_utils.Assume_info.Value.t) : Value.t = { nor = transl w v.nor; exn = transl w v.exn; div = transl w v.div } @@ -360,7 +1523,7 @@ end = struct | None -> None | Some v -> let v = transl w v in - let v = if can_raise then v else { v with exn = V.Bot } in + let v = if can_raise then v else { v with exn = V.bot } in Some v end @@ -523,21 +1686,12 @@ module Func_info : sig { name : string; (** function name *) dbg : Debuginfo.t; (** debug info associated with the function *) mutable value : Value.t; (** the result of the check *) - annotation : Annotation.t option; + annotation : Annotation.t option (** [value] must be lessequal than the expected value if there is user-defined annotation on this function. *) - saved_body : Mach.instruction option - (** If the function has callees that haven't been analyzed yet, keep function body - so it can be reanalyzed when the callees are available. *) } - val create : - string -> - Value.t -> - Debuginfo.t -> - Annotation.t option -> - Mach.instruction option -> - t + val create : string -> Value.t -> Debuginfo.t -> Annotation.t option -> t val print : witnesses:bool -> msg:string -> Format.formatter -> t -> unit @@ -547,16 +1701,12 @@ end = struct { name : string; (** function name *) dbg : Debuginfo.t; (** debug info associated with the function *) mutable value : Value.t; (** the result of the check *) - annotation : Annotation.t option; + annotation : Annotation.t option (** [value] must be lessequal than the expected value if there is user-defined annotation on this function. *) - saved_body : Mach.instruction option - (** If the function has callees that haven't been analyzed yet, keep function body - so it can be reanalyzed when the callees are available. *) } - let create name value dbg annotation saved_body = - { name; dbg; value; annotation; saved_body } + let create name value dbg annotation = { name; dbg; value; annotation } let print ~witnesses ~msg ppf t = Format.fprintf ppf "%s %s %a@." msg t.name (Value.print ~witnesses) t.value @@ -597,18 +1747,16 @@ module Unit_info : sig val find_opt : t -> string -> Func_info.t option + val find_exn : t -> string -> Func_info.t + (** [recod t name v dbg a] name must be in the current compilation unit, and not previously recorded. *) val record : - t -> - string -> - Value.t -> - Debuginfo.t -> - Annotation.t option -> - Mach.instruction option -> - unit + t -> string -> Value.t -> Debuginfo.t -> Annotation.t option -> unit val iter : t -> f:(Func_info.t -> unit) -> unit + + val fold : t -> f:(Func_info.t -> 'a -> 'a) -> init:'a -> 'a end = struct (** map function name to the information about it *) type t = Func_info.t String.Tbl.t @@ -619,16 +1767,104 @@ end = struct let find_opt t name = String.Tbl.find_opt t name + let find_exn t name = String.Tbl.find t name + let iter t ~f = String.Tbl.iter (fun _ func_info -> f func_info) t - let record t name value dbg annotation saved_body = + let fold t ~f ~init = + String.Tbl.fold (fun _name func_info acc -> f func_info acc) t init + + let record t name value dbg annotation = match String.Tbl.find_opt t name with | Some _ -> Misc.fatal_errorf "Duplicate symbol %s" name | None -> - let func_info = Func_info.create name value dbg annotation saved_body in + let func_info = Func_info.create name value dbg annotation in String.Tbl.replace t name func_info end +module Unresolved_dependencies : sig + type t + + val create : unit -> t + + val reset : t -> unit + + val is_empty : t -> bool + + val contains : callee:string -> t -> bool + + val get_callers : callee:string -> t -> String.Set.t + + (** removes all association of the [callee] with its direct callers. [callee] must exist + and must not be associated with any callees of its own in [t]. *) + val remove : callee:string -> t -> unit + + (** adds a new caller. *) + val add : t -> caller:string -> callees:String.Set.t -> unit + + (** Ensure [caller] exists and is already associated with [callees], and remove + association of [caller] with any other callees. *) + val update : t -> caller:string -> callees:String.Set.t -> unit +end = struct + (** reverse dependencies: map from an unresolved callee to all its callers *) + type t = String.Set.t String.Tbl.t + + let create () = String.Tbl.create 2 + + let reset t = String.Tbl.reset t + + let is_empty t = String.Tbl.length t = 0 + + let contains ~callee t = String.Tbl.mem t callee + + let get_callers ~callee t = String.Tbl.find t callee + + let remove ~callee t = + assert (contains ~callee t); + String.Tbl.iter + (fun _ callers -> assert (not (String.Set.mem callee callers))) + t; + String.Tbl.remove t callee + + let add_one t ~caller callee = + let callers = + match String.Tbl.find_opt t callee with + | None -> String.Set.singleton caller + | Some callers -> + assert (not (String.Set.mem caller callers)); + String.Set.add caller callers + in + String.Tbl.replace t callee callers + + let add t ~caller ~callees = String.Set.iter (add_one t ~caller) callees + + let update t ~caller ~callees = + (* check that all callees are present *) + String.Set.iter + (fun callee -> + match String.Tbl.find_opt t callee with + | None -> + Misc.fatal_errorf "Unresolved dependencies: missing callee %s of %s" + callee caller + | Some callers -> + if not (String.Set.mem caller callers) + then + Misc.fatal_errorf + "Unresolved_dependencies: missing caller %s for callee %s in \ + unresolved " + caller callee) + callees; + (* remove resolved callees of this caller *) + let remove callee callers = + if String.Set.mem callee callees + then Some callers + else + let new_callers = String.Set.remove caller callers in + if String.Set.is_empty new_callers then None else Some new_callers + in + String.Tbl.filter_map_inplace remove t +end + (** The analysis involved some fixed point computations. Termination: [Value.t] is a finite height domain and [transfer] is a monotone function w.r.t. [Value.lessequal] order. @@ -639,22 +1875,20 @@ module Analysis (S : Spec) : sig Mach.fundecl -> future_funcnames:String.Set.t -> Unit_info.t -> + Unresolved_dependencies.t -> Format.formatter -> unit (** Resolve all function summaries, check them against user-provided assertions, and record the summaries in Compilenv to be saved in .cmx files *) - val record_unit : Unit_info.t -> Format.formatter -> unit + val record_unit : + Unit_info.t -> Unresolved_dependencies.t -> Format.formatter -> unit end = struct (** Information about the current function under analysis. *) type t = { ppf : Format.formatter; current_fun_name : string; future_funcnames : String.Set.t; - mutable approx : Value.t option; - (** Used for computing for self calls. *) - mutable unresolved : bool; - (** the current function contains calls to other unresolved functions (not including self calls) *) unit_info : Unit_info.t; (** must be the current compilation unit. *) keep_witnesses : bool } @@ -665,16 +1899,9 @@ end = struct | No_details -> false | At_most _ -> keep - let create ppf current_fun_name future_funcnames unit_info approx annot = + let create ppf current_fun_name future_funcnames unit_info annot = let keep_witnesses = should_keep_witnesses (Option.is_some annot) in - { ppf; - current_fun_name; - future_funcnames; - approx; - unresolved = false; - unit_info; - keep_witnesses - } + { ppf; current_fun_name; future_funcnames; unit_info; keep_witnesses } let analysis_name = Printcmm.property_to_string S.property @@ -689,16 +1916,8 @@ end = struct let report t v ~msg ~desc dbg = report' t.ppf v ~msg ~desc ~current_fun_name:t.current_fun_name dbg - let report_fail t d desc dbg = report t d ~msg:"failed" ~desc dbg - let is_future_funcname t callee = String.Set.mem callee t.future_funcnames - let check t (r : Value.t) msg dbg = - if V.is_not_safe r.nor then report_fail t r (msg ^ " nor") dbg; - if V.is_not_safe r.exn then report_fail t r (msg ^ " exn") dbg; - if V.is_not_safe r.div then report_fail t r (msg ^ " div") dbg; - r - let report_unit_info ppf unit_info ~msg = if !Flambda_backend_flags.dump_checkmach then @@ -711,7 +1930,7 @@ end = struct let msg = Printf.sprintf "%s %s:" analysis_name msg in Func_info.print ~witnesses:true ppf ~msg func_info - let record_unit ppf unit_info = + let check_and_save_unit_info ppf unit_info = let errors = ref [] in let record (func_info : Func_info.t) = (match func_info.annotation with @@ -765,6 +1984,7 @@ end = struct return ~msg v in let resolved v = + assert (Value.is_resolved v); let msg = Printf.sprintf "resolved %s" callee in return ~msg v in @@ -775,22 +1995,14 @@ end = struct (* Conservatively return Top. Won't be able to prove any recursive functions as non-allocating. *) unresolved (Value.top w) - "conservative handling of forward or recursive call or tailcall" + "conservative handling of forward or recursive call\nor tailcall" else if String.equal callee t.current_fun_name - then - (* Self call. *) - match t.approx with - | None -> - (* Summary is not computed yet. Conservative. *) - let v = Value.safe in - t.approx <- Some v; - unresolved v "self-call init" - | Some approx -> unresolved approx "self-call approx" - else ( + then (* Self call. *) + unresolved (Value.unresolved callee w) "self call" + else (* Call is defined later in the current compilation unit. Summary of this callee is not yet computed. *) - t.unresolved <- true; - unresolved Value.safe "forward or recursive call or tailcall") + unresolved (Value.unresolved callee w) "foward call" else (* CR gyorsh: unresolved case here is impossible in the conservative analysis because all previous functions have been conservatively @@ -801,22 +2013,24 @@ end = struct match S.get_value_opt callee with | None -> unresolved (Value.top w) - "(missing summary: callee compiled without checks)" + "missing summary: callee compiled without checks" | Some v -> resolved v) - | Some callee_info -> ( - (* Callee defined earlier in the same compilation unit. *) - match callee_info.saved_body with - | None -> resolved callee_info.value - | Some _ -> - (* callee was unresolved, mark caller as unresolved *) - t.unresolved <- true; - unresolved callee_info.value "unresolved callee") + | Some callee_info -> + (* Callee defined earlier in the same compilation unit. May have + unresolved dependencies. *) + if Value.is_resolved callee_info.value + then resolved callee_info.value + else + unresolved + (Value.unresolved callee w) + "defined earlier with unresolved dependencies" let transform_return ~(effect : V.t) dst = - match effect with - | V.Bot -> Value.bot - | V.Safe -> dst - | V.Top w -> Value.transform w dst + (* Instead of calling [Value.transform] directly, first check for trivial + cases to avoid reallocating [dst]. *) + V.match_with effect ~bot:Value.bot ~safe:dst + ~top:(fun _ -> Value.transform effect dst) + ~unresolved:(fun () -> Value.transform effect dst) let transform_diverge ~(effect : V.t) (dst : Value.t) = let div = V.join effect dst.div in @@ -831,7 +2045,7 @@ end = struct report t r ~msg:"transform join" ~desc dbg; let r = transform_diverge ~effect:effect.div r in report t r ~msg:"transform result" ~desc dbg; - check t r desc dbg + r let transform_top t ~next ~exn w desc dbg = let effect = @@ -847,7 +2061,9 @@ end = struct let v = find_callee t callee ~desc dbg w in let effect = match Metadata.assume_value dbg ~can_raise:true w with - | Some v' -> Value.meet v v' + | Some v' -> + assert (Value.is_resolved v'); + if Value.is_resolved v then Value.meet v v' else v' | None -> v in transform t ~next ~exn ~effect desc dbg @@ -885,14 +2101,15 @@ 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)); 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) + let effect = + match Metadata.assume_value dbg ~can_raise:false w with + | Some effect -> effect + | None -> Value.{ nor = V.top w; exn = V.bot; div = V.bot } + in + transform t ~effect ~next ~exn "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 @@ -977,75 +2194,209 @@ end = struct body |> fst - let analyze_body t body = - let rec fixpoint () = - let new_value = check_instr t body in - match t.approx with - | None -> new_value - | Some approx -> - (* Fixpoint here is only for the common case of "self" recursive - functions that do not have other unresolved dependencies. Other cases - will be recomputed simultaneously at the end of the compilation - unit. *) - if t.unresolved - then new_value - else if Value.lessequal new_value approx - then approx - else ( - t.approx <- Some (Value.join new_value approx); - fixpoint ()) - in - fixpoint () + module Env : sig + type t + + val empty : t + + val singleton : Func_info.t -> Value.t -> t + + val add : Func_info.t -> Value.t -> t -> t + + val get_value_exn : string -> t -> Value.t + + val iter : t -> f:(Func_info.t -> Value.t -> unit) -> unit + + val map : t -> f:(Func_info.t -> Value.t -> Value.t) -> t + + val print : msg:string -> Format.formatter -> t -> unit + + (** initialize [env] with Bot for all functions on normal and exceptional + return, and Safe for diverge component conservatively. *) + val init_val : Value.t + end = struct + type data = + { func_info : Func_info.t; + approx : Value.t + } + + type t = data String.Map.t + + let empty = String.Map.empty + + let add (func_info : Func_info.t) approx t = + assert (Value.is_resolved approx); + let d = { func_info; approx } in + String.Map.add func_info.name d t + + let singleton (func_info : Func_info.t) approx = add func_info approx empty - let fixpoint ppf unit_info = - report_unit_info ppf unit_info ~msg:"before fixpoint"; + let get_value_exn name t = + let d = String.Map.find name t in + d.approx + + let map t ~f = + String.Map.map + (fun d -> + let approx = f d.func_info d.approx in + assert (Value.is_resolved approx); + { d with approx }) + t + + let iter t ~f = String.Map.iter (fun _name d -> f d.func_info d.approx) t + + let print ~msg ppf t = + if !Flambda_backend_flags.dump_checkmach + then + iter t ~f:(fun func_info approx -> + Format.fprintf ppf "Env %s: %s: %a@." msg func_info.name + (Value.print ~witnesses:true) + approx) + + let init_val = Value.diverges + end + + (* CR gyorsh: do we need join in the fixpoint computation or is the function + body analysis/summary already monotone? *) + let fixpoint ppf init_env = (* CR gyorsh: this is a really dumb iteration strategy. *) - let change = ref true in - let analyze_func (func_info : Func_info.t) = - match func_info.saved_body with - | None -> () - | Some b -> - let t = - create ppf func_info.name String.Set.empty unit_info None - func_info.annotation - in - let new_value = analyze_body t b in - if not (Value.lessequal new_value func_info.value) - then ( - change := true; - report t new_value ~msg:"update" ~desc:"fixpoint" func_info.dbg; - Func_info.update func_info new_value) + let lookup env var = + let v = Env.get_value_exn (Var.name var) env in + Some (Value.get_component v (Var.tag var)) in - while !change do - change := false; - Unit_info.iter unit_info ~f:analyze_func; - report_unit_info ppf unit_info ~msg:"computing fixpoint" - done + let rec loop env = + Env.print ~msg:"computing fixpoint" ppf env; + let changed = ref false in + let env' = + Env.map + ~f:(fun func_info v -> + let v' = Value.apply func_info.value (lookup env) in + if !Flambda_backend_flags.dump_checkmach + then + Format.fprintf ppf "fixpoint after apply: %s %a@." func_info.name + (Value.print ~witnesses:true) + v'; + assert (Value.is_resolved v'); + if not (Value.lessequal v' v) + then ( + changed := true; + if !Flambda_backend_flags.dump_checkmach + then + Format.fprintf ppf "fixpoint update: %s %a@." func_info.name + (Value.print ~witnesses:true) + v'); + Value.join v v') + env + in + if !changed then loop env' else env' + in + let env = loop init_env in + Env.iter env ~f:(fun func_info v -> + assert (Value.is_resolved v); + Func_info.update func_info v); + Env.print ~msg:"after fixpoint" ppf env - let record_unit unit_info ppf = + let record_unit unit_info unresolved_deps ppf = Profile.record_call ~accumulate:true ("record_unit " ^ analysis_name) (fun () -> - fixpoint ppf unit_info; - record_unit ppf unit_info) + report_unit_info ppf unit_info ~msg:"before fixpoint"; + let found_unresolved = ref false in + let init_env = + Unit_info.fold unit_info ~init:Env.empty ~f:(fun func_info env -> + let v = + if Value.is_resolved func_info.value + then func_info.value + else ( + found_unresolved := true; + Env.init_val) + in + Env.add func_info v env) + in + if !found_unresolved + then ( + fixpoint ppf init_env; + report_unit_info ppf unit_info ~msg:"after fixpoint") + else assert (Unresolved_dependencies.is_empty unresolved_deps); + check_and_save_unit_info ppf unit_info) + + (* [fixpoint_self_rec] tries to resolve the common case of self-recursive + functions with no other unresolved dependencies, instead of waiting until + the end of the compilation unit to compute its fixpoint. Return the + unresolved callees of [func_info]. *) + let fixpoint_self_rec (func_info : Func_info.t) ppf = + let unresolved_callees = Value.get_unresolved_names func_info.value in + if String.Set.is_empty unresolved_callees + || not + (String.Set.equal unresolved_callees + (String.Set.singleton func_info.name)) + then unresolved_callees + else + let init_env = Env.singleton func_info Env.init_val in + fixpoint ppf init_env; + report_func_info ~msg:"after self-rec fixpoint" ppf func_info; + String.Set.empty + + (* [propagate] applies resolved values to transitive dependencies, but does + not resolve mutually recursive loops. *) + let rec propagate ~callee unit_info unresolved_deps ppf = + let callee_info = Unit_info.find_exn unit_info callee in + if Value.is_resolved callee_info.value + && Unresolved_dependencies.contains ~callee unresolved_deps + then ( + let callers = + Unresolved_dependencies.get_callers ~callee unresolved_deps + in + assert (not (String.Set.is_empty callers)); + Unresolved_dependencies.remove ~callee unresolved_deps; + let lookup var = + if String.equal (Var.name var) callee + then Some (Value.get_component callee_info.value (Var.tag var)) + else None + in + (* To avoid problems due to cyclic dependencies and sharing, first resolve + everything that directly depends on [callee_info] and update + dependencies, then propagate recursively. *) + String.Set.iter + (fun caller -> + let caller_info = Unit_info.find_exn unit_info caller in + let new_value = Value.apply caller_info.value lookup in + Func_info.update caller_info new_value; + let unresolved_callees = fixpoint_self_rec caller_info ppf in + Unresolved_dependencies.update ~caller:caller_info.name + ~callees:unresolved_callees unresolved_deps) + callers; + String.Set.iter + (fun caller -> propagate ~callee:caller unit_info unresolved_deps ppf) + callers) + + let add_unresolved_dependencies caller unit_info unresolved_deps ppf = + let caller_info = Unit_info.find_exn unit_info caller in + let unresolved_callees = fixpoint_self_rec caller_info ppf in + if not (String.Set.is_empty unresolved_callees) + then + Unresolved_dependencies.add ~caller ~callees:unresolved_callees + unresolved_deps; + propagate ~callee:caller unit_info unresolved_deps ppf - let fundecl (f : Mach.fundecl) ~future_funcnames unit_info ppf = + let fundecl (f : Mach.fundecl) ~future_funcnames unit_info unresolved_deps ppf + = let check () = let fun_name = f.fun_name in let a = Annotation.find f.fun_codegen_options S.property fun_name f.fun_dbg in - let t = create ppf fun_name future_funcnames unit_info None a in + let t = create ppf fun_name future_funcnames unit_info a in let really_check () = - let res = analyze_body t f.fun_body in - let saved_body = if t.unresolved then Some f.fun_body else None in + let res = check_instr t f.fun_body in report t res ~msg:"finished" ~desc:"fundecl" f.fun_dbg; - if not t.keep_witnesses + if (not t.keep_witnesses) && Value.is_resolved res then ( let { Witnesses.nor; exn; div } = Value.get_witnesses res in assert (Witnesses.is_empty nor); assert (Witnesses.is_empty exn); assert (Witnesses.is_empty div)); - Unit_info.record unit_info fun_name res f.fun_dbg a saved_body; + Unit_info.record unit_info fun_name res f.fun_dbg a; + add_unresolved_dependencies fun_name unit_info unresolved_deps t.ppf; report_unit_info ppf unit_info ~msg:"after record" in let really_check () = @@ -1055,14 +2406,14 @@ end = struct the summary is top. *) Unit_info.record unit_info fun_name (Value.top Witnesses.empty) - f.fun_dbg a None + f.fun_dbg a else really_check () in match a with | Some a when Annotation.is_assume a -> let expected_value = Annotation.expected_value a in report t expected_value ~msg:"assumed" ~desc:"fundecl" f.fun_dbg; - Unit_info.record unit_info fun_name expected_value f.fun_dbg None None + Unit_info.record unit_info fun_name expected_value f.fun_dbg None | None -> really_check () | Some a -> let expected_value = Annotation.expected_value a in @@ -1089,7 +2440,11 @@ module Spec_zero_alloc : Spec = struct in cmx and memory consumption Compilenv. Different components have different frequencies of Top/Bot. The most likely value is encoded as None (i.e., not stored). *) - let encode (v : V.t) = match v with Top _ -> 0 | Safe -> 1 | Bot -> 2 + let encode (v : V.t) = + V.match_with v + ~top:(fun _ -> 0) + ~safe:1 ~bot:2 + ~unresolved:(fun () -> assert false) (* Witnesses are not used across functions and not stored in cmx. Witnesses that appear in a function's summary are only used for error messages about @@ -1098,9 +2453,9 @@ module Spec_zero_alloc : Spec = struct let decoded_witness = Witnesses.empty let decode = function - | 0 -> V.Top decoded_witness - | 1 -> V.Safe - | 2 -> V.Bot + | 0 -> V.top decoded_witness + | 1 -> V.safe + | 2 -> V.bot | n -> Misc.fatal_errorf "Checkmach cannot decode %d" n let encode (v : Value.t) : Checks.value = @@ -1128,10 +2483,10 @@ module Spec_zero_alloc : Spec = struct let transform_specific w s = (* Conservatively assume that operation can return normally. *) - let nor = if Arch.operation_allocates s then V.Top w else V.Safe in - let exn = if Arch.operation_can_raise s then nor else V.Bot in + let nor = if Arch.operation_allocates s then V.top w else V.safe in + let exn = if Arch.operation_can_raise s then nor else V.bot in (* Assume that the operation does not diverge. *) - let div = V.Bot in + let div = V.bot in { Value.nor; exn; div } end @@ -1140,14 +2495,19 @@ module Check_zero_alloc = Analysis (Spec_zero_alloc) (** Information about the current unit. *) let unit_info = Unit_info.create () +let unresolved_deps = Unresolved_dependencies.create () + let fundecl ppf_dump ~future_funcnames fd = - Check_zero_alloc.fundecl fd ~future_funcnames unit_info ppf_dump; + Check_zero_alloc.fundecl fd ~future_funcnames unit_info unresolved_deps + ppf_dump; fd -let reset_unit_info () = Unit_info.reset unit_info +let reset_unit_info () = + Unit_info.reset unit_info; + Unresolved_dependencies.reset unresolved_deps let record_unit_info ppf_dump = - Check_zero_alloc.record_unit unit_info ppf_dump; + Check_zero_alloc.record_unit unit_info unresolved_deps ppf_dump; Compilenv.cache_checks (Compilenv.current_unit_infos ()).ui_checks type iter_witnesses = (string -> Witnesses.components -> unit) -> unit diff --git a/driver/flambda_backend_args.ml b/driver/flambda_backend_args.ml index 65a1b0582fc..7f0ab7813c1 100644 --- a/driver/flambda_backend_args.ml +++ b/driver/flambda_backend_args.ml @@ -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 @@ -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 @@ -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; @@ -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 *) @@ -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 diff --git a/driver/flambda_backend_args.mli b/driver/flambda_backend_args.mli index d6fbc04681f..9ead53e08cf 100644 --- a/driver/flambda_backend_args.mli +++ b/driver/flambda_backend_args.mli @@ -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 diff --git a/driver/flambda_backend_flags.ml b/driver/flambda_backend_flags.ml index 6ca998aa3d8..12f95345e46 100644 --- a/driver/flambda_backend_flags.ml +++ b/driver/flambda_backend_flags.ml @@ -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 diff --git a/driver/flambda_backend_flags.mli b/driver/flambda_backend_flags.mli index 6877de6d320..eba6ad4b66e 100644 --- a/driver/flambda_backend_flags.mli +++ b/driver/flambda_backend_flags.mli @@ -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 diff --git a/ocaml/utils/zero_alloc_utils.ml b/ocaml/utils/zero_alloc_utils.ml index 1893a82c1fa..f0043623416 100644 --- a/ocaml/utils/zero_alloc_utils.ml +++ b/ocaml/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/ocaml/utils/zero_alloc_utils.mli b/ocaml/utils/zero_alloc_utils.mli index a134fa6d668..5cabe367582 100644 --- a/ocaml/utils/zero_alloc_utils.mli +++ b/ocaml/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 diff --git a/tests/backend/checkmach/dune b/tests/backend/checkmach/dune index 876d4cafc01..4207a5413da 100644 --- a/tests/backend/checkmach/dune +++ b/tests/backend/checkmach/dune @@ -18,6 +18,19 @@ (alias runtest) (action (copy test_all_opt.ml test_all_opt3.ml))) + +(rule + (alias runtest) + (action (copy test_bounded_join.ml test_bounded_join2.ml ))) + +(rule + (alias runtest) + (action (copy test_bounded_join.ml test_bounded_join3.ml ))) + +(rule + (alias runtest) + (action (copy test_bounded_join.ml test_bounded_join4.ml ))) + ;; Tests whose outputs differ depending on stack_allocation configuration flag. ;; This condition is not expressible in "enable_if" clause ;; because dune does not support %{config:stack_allocation} yet. @@ -38,3 +51,4 @@ else cp test_assume_stub.heap_allocation.output test_assume_stub.output fi")))) + diff --git a/tests/backend/checkmach/dune.inc b/tests/backend/checkmach/dune.inc index ca7e5a7c015..411b0e29f74 100644 --- a/tests/backend/checkmach/dune.inc +++ b/tests/backend/checkmach/dune.inc @@ -997,3 +997,79 @@ (enabled_if (= %{context_name} "main")) (deps test_assume_stub.output test_assume_stub.output.corrected) (action (diff test_assume_stub.output test_assume_stub.output.corrected))) + +(rule + (enabled_if (= %{context_name} "main")) + (targets test_bounded_join.output.corrected) + (deps (:ml test_bounded_join.ml) filter_fatal_error.sh) + (action + (with-outputs-to test_bounded_join.output.corrected + (pipe-outputs + (with-accepted-exit-codes 2 + (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c + -zero-alloc-check default -checkmach-join -2 -checkmach-details-cutoff 20 -O3)) + (run "./filter_fatal_error.sh") + )))) + +(rule + (alias runtest) + (enabled_if (= %{context_name} "main")) + (deps test_bounded_join.output test_bounded_join.output.corrected) + (action (diff test_bounded_join.output test_bounded_join.output.corrected))) + +(rule + (enabled_if (= %{context_name} "main")) + (targets test_bounded_join2.output.corrected) + (deps (:ml test_bounded_join2.ml) filter.sh) + (action + (with-outputs-to test_bounded_join2.output.corrected + (pipe-outputs + (with-accepted-exit-codes 2 + (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c + -zero-alloc-check default -checkmach-join 2 -checkmach-details-cutoff 20 -O3)) + (run "./filter.sh") + )))) + +(rule + (alias runtest) + (enabled_if (= %{context_name} "main")) + (deps test_bounded_join2.output test_bounded_join2.output.corrected) + (action (diff test_bounded_join2.output test_bounded_join2.output.corrected))) + +(rule + (enabled_if (= %{context_name} "main")) + (targets test_bounded_join3.output.corrected) + (deps (:ml test_bounded_join3.ml) filter.sh) + (action + (with-outputs-to test_bounded_join3.output.corrected + (pipe-outputs + (with-accepted-exit-codes 2 + (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c + -zero-alloc-check default -checkmach-join 0 -checkmach-details-cutoff 20 -O3)) + (run "./filter.sh") + )))) + +(rule + (alias runtest) + (enabled_if (= %{context_name} "main")) + (deps test_bounded_join3.output test_bounded_join3.output.corrected) + (action (diff test_bounded_join3.output test_bounded_join3.output.corrected))) + +(rule + (enabled_if (= %{context_name} "main")) + (targets test_bounded_join4.output.corrected) + (deps (:ml test_bounded_join4.ml) filter.sh) + (action + (with-outputs-to test_bounded_join4.output.corrected + (pipe-outputs + (with-accepted-exit-codes 2 + (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c + -zero-alloc-check default -checkmach-join 0 -checkmach-details-cutoff 3 -O3)) + (run "./filter.sh") + )))) + +(rule + (alias runtest) + (enabled_if (= %{context_name} "main")) + (deps test_bounded_join4.output test_bounded_join4.output.corrected) + (action (diff test_bounded_join4.output test_bounded_join4.output.corrected))) diff --git a/tests/backend/checkmach/fail20.ml b/tests/backend/checkmach/fail20.ml index 8a8a7d67e9e..7465ee38a8f 100644 --- a/tests/backend/checkmach/fail20.ml +++ b/tests/backend/checkmach/fail20.ml @@ -4,7 +4,7 @@ let exn x = raise (Exn (x,x)) let rec div x : int list = x::(div (x+1)) let[@inline never] nor x = x+1 (* test detailed output for exceptions and diverge *) -let[@zero_alloc strict] foo x = +let[@zero_alloc strict] foo1 x = if x > 0 then exn (x+1) else if x < 0 then List.nth (div (x+2)) x diff --git a/tests/backend/checkmach/fail20.output b/tests/backend/checkmach/fail20.output index 032198a5ad6..65d3d22aebe 100644 --- a/tests/backend/checkmach/fail20.output +++ b/tests/backend/checkmach/fail20.output @@ -1,12 +1,9 @@ File "fail20.ml", line 7, characters 5-15: -Error: Annotation check for zero_alloc strict failed on function Fail20.foo (camlFail20.foo_HIDE_STAMP) +Error: Annotation check for zero_alloc strict failed on function Fail20.foo1 (camlFail20.foo1_HIDE_STAMP) File "fail20.ml", line 8, characters 16-25: Error: allocation of 32 bytes on a path to exceptional return (fail20.ml:8,16--25;fail20.ml:3,18--29) -File "fail20.ml", line 10, characters 13-24: -Error: called function may allocate on a path to exceptional return (direct call camlFail20.div_HIDE_STAMP) - File "fail20.ml", line 13, characters 5-15: Error: Annotation check for zero_alloc failed on function Fail20.foo (camlFail20.foo_HIDE_STAMP) diff --git a/tests/backend/checkmach/filter_fatal_error.sh b/tests/backend/checkmach/filter_fatal_error.sh new file mode 100755 index 00000000000..0cf2408a620 --- /dev/null +++ b/tests/backend/checkmach/filter_fatal_error.sh @@ -0,0 +1,3 @@ +#!/bin/sh + +grep "Fatal error" diff --git a/tests/backend/checkmach/gen/gen_dune.ml b/tests/backend/checkmach/gen/gen_dune.ml index 925a24b858f..9bf701e15ea 100644 --- a/tests/backend/checkmach/gen/gen_dune.ml +++ b/tests/backend/checkmach/gen/gen_dune.ml @@ -39,7 +39,8 @@ let () = |}; Buffer.output_buffer Out_channel.stdout buf in - let print_test_expected_output ?(extra_flags="-zero-alloc-check default") + let print_test_expected_output ?(filter="filter.sh") + ?(extra_flags="-zero-alloc-check default") ?output ~cutoff ~extra_dep ~exit_code name = let extra_deps = match extra_dep with @@ -59,6 +60,7 @@ let () = | "exit_code" -> string_of_int exit_code | "cutoff" -> string_of_int cutoff | "extra_flags" -> extra_flags + | "filter" -> filter | _ -> assert false in Buffer.clear buf; @@ -67,14 +69,14 @@ let () = (rule ${enabled_if} (targets ${output}.corrected) - (deps ${extra_deps} filter.sh) + (deps ${extra_deps} ${filter}) (action (with-outputs-to ${output}.corrected (pipe-outputs (with-accepted-exit-codes ${exit_code} (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c ${extra_flags} -checkmach-details-cutoff ${cutoff} -O3)) - (run "./filter.sh") + (run "./${filter}") )))) (rule @@ -183,4 +185,16 @@ let () = ~extra_dep:None ~exit_code:2 "test_assume_error"; print_test_expected_output ~cutoff:default_cutoff ~extra_dep:None ~exit_code:2 "test_assume_stub"; + print_test_expected_output ~cutoff:default_cutoff + ~extra_flags:"-zero-alloc-check default -checkmach-join -2" + ~extra_dep:None ~exit_code:2 ~filter:"filter_fatal_error.sh" "test_bounded_join"; + print_test_expected_output ~cutoff:default_cutoff + ~extra_flags:"-zero-alloc-check default -checkmach-join 2" + ~extra_dep:None ~exit_code:2 "test_bounded_join2"; + print_test_expected_output ~cutoff:default_cutoff + ~extra_flags:"-zero-alloc-check default -checkmach-join 0" + ~extra_dep:None ~exit_code:2 "test_bounded_join3"; + print_test_expected_output ~cutoff:3 + ~extra_flags:"-zero-alloc-check default -checkmach-join 0" + ~extra_dep:None ~exit_code:2 "test_bounded_join4"; () diff --git a/tests/backend/checkmach/test_bounded_join.ml b/tests/backend/checkmach/test_bounded_join.ml new file mode 100644 index 00000000000..f8abf20a7de --- /dev/null +++ b/tests/backend/checkmach/test_bounded_join.ml @@ -0,0 +1,29 @@ +type r = int + +type t = + A of r | B of r | C of r | D of r | E of r | F of r + +let[@inline never][@local never] next x y = Sys.opaque_identity (x + y) + +let[@zero_alloc] rec foo t x = + let + [@inline never][@local never] rec do_a x y = + if Sys.opaque_identity false then foo t (next x y) else x + and[@inline never][@local never] do_b x y= + if Sys.opaque_identity false then foo t (next x y) else x + and[@inline never][@local never] do_c x y = + if Sys.opaque_identity false then foo t (next x y) else x + and[@inline never][@local never] do_d x y = + if Sys.opaque_identity false then foo t (next x y) else x + and[@inline never][@local never] do_e x y = + if Sys.opaque_identity false then foo t (next x y) else x + and[@inline never][@local never] do_f x y = + if Sys.opaque_identity false then foo t (next x y) else x + in + match t with + | A y -> do_a x y + | B y -> do_b x y + | C y -> do_c x y + | D y -> do_d x y + | E y -> do_e x y + | F y -> do_f x y diff --git a/tests/backend/checkmach/test_bounded_join.output b/tests/backend/checkmach/test_bounded_join.output new file mode 100644 index 00000000000..b9ae5944af0 --- /dev/null +++ b/tests/backend/checkmach/test_bounded_join.output @@ -0,0 +1,2 @@ +>> Fatal error: Join with 3 paths is too big, use -disable-precise-checkmach +Fatal error: exception Misc.Fatal_error diff --git a/tests/backend/checkmach/test_bounded_join2.output b/tests/backend/checkmach/test_bounded_join2.output new file mode 100644 index 00000000000..f40022e02f2 --- /dev/null +++ b/tests/backend/checkmach/test_bounded_join2.output @@ -0,0 +1,2 @@ +File "test_bounded_join2.ml", line 8, characters 5-15: +Error: Annotation check for zero_alloc failed on function Test_bounded_join2.foo (camlTest_bounded_join2.foo_HIDE_STAMP) diff --git a/tests/backend/checkmach/test_bounded_join3.output b/tests/backend/checkmach/test_bounded_join3.output new file mode 100644 index 00000000000..82c1644b221 --- /dev/null +++ b/tests/backend/checkmach/test_bounded_join3.output @@ -0,0 +1,23 @@ +File "test_bounded_join3.ml", line 8, characters 5-15: +Error: Annotation check for zero_alloc failed on function Test_bounded_join3.foo (camlTest_bounded_join3.foo_HIDE_STAMP) + +File "test_bounded_join3.ml", lines 10-11, characters 43-61: +Error: allocation of 200 bytes + +File "test_bounded_join3.ml", line 24, characters 11-19: +Error: called function may allocate (direct tailcall camlTest_bounded_join3.do_a_HIDE_STAMP) + +File "test_bounded_join3.ml", line 25, characters 11-19: +Error: called function may allocate (direct tailcall camlTest_bounded_join3.do_b_HIDE_STAMP) + +File "test_bounded_join3.ml", line 26, characters 11-19: +Error: called function may allocate (direct tailcall camlTest_bounded_join3.do_c_HIDE_STAMP) + +File "test_bounded_join3.ml", line 27, characters 11-19: +Error: called function may allocate (direct tailcall camlTest_bounded_join3.do_d_HIDE_STAMP) + +File "test_bounded_join3.ml", line 28, characters 11-19: +Error: called function may allocate (direct tailcall camlTest_bounded_join3.do_e_HIDE_STAMP) + +File "test_bounded_join3.ml", line 29, characters 11-19: +Error: called function may allocate (direct tailcall camlTest_bounded_join3.do_f_HIDE_STAMP) diff --git a/tests/backend/checkmach/test_bounded_join4.output b/tests/backend/checkmach/test_bounded_join4.output new file mode 100644 index 00000000000..dea55bdbe00 --- /dev/null +++ b/tests/backend/checkmach/test_bounded_join4.output @@ -0,0 +1,11 @@ +File "test_bounded_join4.ml", line 8, characters 5-15: +Error: Annotation check for zero_alloc failed on function Test_bounded_join4.foo (camlTest_bounded_join4.foo_HIDE_STAMP) + +File "test_bounded_join4.ml", lines 10-11, characters 43-61: +Error: allocation of 200 bytes + +File "test_bounded_join4.ml", line 24, characters 11-19: +Error: called function may allocate (direct tailcall camlTest_bounded_join4.do_a_HIDE_STAMP) + +File "test_bounded_join4.ml", line 25, characters 11-19: +Error: called function may allocate (direct tailcall camlTest_bounded_join4.do_b_HIDE_STAMP)