From bc7a71d413e57d45ae92e2b9a6113409d5d96a8a Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 1 Mar 2018 10:11:00 -0800 Subject: [PATCH] [IR] add API for Sil and Exp.FreeVar Summary: `Sequence` API to walk over free variables in expressions, instead of computing lists with uniqueness constraints that make them have linear complexity for insertion. Switch to a Set representation when we don't care about the order of elements, otherwise to a `Hash_queue`: https://ocaml.janestreet.com/ocaml-core/113.33/doc/core/Std/Hash_queue.mod/S.modt/ Often, we don't even need to compute the sequence of free variables, as we are just testing membership/emptiness/... Reviewed By: mbouaziz Differential Revision: D7099294 fbshipit-source-id: e96f84b --- infer/src/IR/Exp.ml | 33 ++++- infer/src/IR/Exp.mli | 8 + infer/src/IR/Ident.ml | 20 +++ infer/src/IR/Ident.mli | 6 + infer/src/IR/Sil.ml | 241 +++++++++++-------------------- infer/src/IR/Sil.mli | 79 ++-------- infer/src/backend/Attribute.ml | 4 +- infer/src/backend/BuiltinDefn.ml | 4 +- infer/src/backend/abs.ml | 89 ++++++------ infer/src/backend/absarray.ml | 30 ++-- infer/src/backend/dom.ml | 45 +++--- infer/src/backend/interproc.ml | 28 ++-- infer/src/backend/match.ml | 17 +-- infer/src/backend/paths.ml | 3 +- infer/src/backend/prop.ml | 229 +++++++++++++++-------------- infer/src/backend/prop.mli | 38 ++--- infer/src/backend/prover.ml | 28 ++-- infer/src/backend/rearrange.ml | 41 +++--- infer/src/backend/specs.ml | 43 +++--- infer/src/backend/specs.mli | 3 +- infer/src/backend/state.ml | 3 +- infer/src/backend/symExec.ml | 17 +-- infer/src/backend/tabulation.ml | 81 +++++------ infer/src/base/ISequence.ml | 14 ++ infer/src/base/ISequence.mli | 15 ++ infer/src/istd/IList.ml | 14 -- infer/src/istd/IList.mli | 4 - 27 files changed, 528 insertions(+), 609 deletions(-) create mode 100644 infer/src/base/ISequence.ml create mode 100644 infer/src/base/ISequence.mli diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml index 20c1d2222..9a0ed9d6b 100644 --- a/infer/src/IR/Exp.ml +++ b/infer/src/IR/Exp.ml @@ -292,6 +292,31 @@ let is_objc_block_closure = function false +let rec gen_free_vars = + let open Sequence.Generator in + function + | Var id -> + yield id + | Cast (_, e) + | Exn e + | Lfield (e, _, _) + (* do nothing since we only count non-program variables *) + | UnOp (_, e, _) -> + gen_free_vars e + | Closure {captured_vars} -> + ISequence.gen_sequence_list captured_vars ~f:(fun (e, _, _) -> gen_free_vars e) + | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _) + | Lvar _ + | Sizeof _ (* TODO: Sizeof length expressions may contain variables, do not ignore them. *) -> + return () + | BinOp (_, e1, e2) | Lindex (e1, e2) -> + gen_free_vars e1 >>= fun () -> gen_free_vars e2 + + +let free_vars e = Sequence.Generator.run (gen_free_vars e) + +let ident_mem e id = free_vars e |> Sequence.exists ~f:(Ident.equal id) + let rec gen_program_vars = let open Sequence.Generator in function @@ -304,13 +329,7 @@ let rec gen_program_vars = | BinOp (_, e1, e2) | Lindex (e1, e2) -> gen_program_vars e1 >>= fun () -> gen_program_vars e2 | Closure {captured_vars} -> - let rec aux = function - | (_, p, _) :: tl -> - yield p >>= fun () -> aux tl - | [] -> - return () - in - aux captured_vars + ISequence.gen_sequence_list captured_vars ~f:(fun (_, p, _) -> yield p) let program_vars e = Sequence.Generator.run (gen_program_vars e) diff --git a/infer/src/IR/Exp.mli b/infer/src/IR/Exp.mli index b3b4ee398..bdd83e950 100644 --- a/infer/src/IR/Exp.mli +++ b/infer/src/IR/Exp.mli @@ -119,6 +119,14 @@ val lt : t -> t -> t val get_vars : t -> Ident.t list * Pvar.t list (** Extract the ids and pvars from an expression *) +val free_vars : t -> Ident.t Sequence.t +(** all the idents appearing in the expression *) + +val gen_free_vars : t -> (unit, Ident.t) Sequence.Generator.t + +val ident_mem : t -> Ident.t -> bool +(** true if the identifier appears in the expression *) + val program_vars : t -> Pvar.t Sequence.t (** all the program variables appearing in the expression *) diff --git a/infer/src/IR/Ident.ml b/infer/src/IR/Ident.ml index 5be340562..f43ba6203 100644 --- a/infer/src/IR/Ident.ml +++ b/infer/src/IR/Ident.ml @@ -236,3 +236,23 @@ let pp f id = F.fprintf f "%s" (to_string id) (** pretty printer for lists of identifiers *) let pp_list = Pp.comma_seq pp + +module HashQueue = Hash_queue.Make (struct + type nonrec t = t + + let compare = compare + + let hash = Hashtbl.hash + + let sexp_of_t id = Sexp.of_string (to_string id) +end) + +let hashqueue_of_sequence ?init s = + let q = match init with None -> HashQueue.create () | Some q0 -> q0 in + Sequence.iter s ~f:(fun id -> + let _ : [`Key_already_present | `Ok] = HashQueue.enqueue q id () in + () ) ; + q + + +let set_of_sequence ?(init= Set.empty) s = Sequence.fold s ~init ~f:(fun ids id -> Set.add id ids) diff --git a/infer/src/IR/Ident.mli b/infer/src/IR/Ident.mli index 4ca8e4338..20ec8d69e 100644 --- a/infer/src/IR/Ident.mli +++ b/infer/src/IR/Ident.mli @@ -39,6 +39,8 @@ module Hash : Caml.Hashtbl.S with type key = t (** Map with ident as key. *) module Map : Caml.Map.S with type key = t +module HashQueue : Hash_queue.S with type Key.t = t + module NameGenerator : sig type t @@ -134,3 +136,7 @@ val to_string : t -> string val pp_list : Format.formatter -> t list -> unit (** Pretty print a list of identifiers. *) + +val hashqueue_of_sequence : ?init:unit HashQueue.t -> t Sequence.t -> unit HashQueue.t + +val set_of_sequence : ?init:Set.t -> t Sequence.t -> Set.t diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index 1141291f3..5e4ddbaa9 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -1015,144 +1015,61 @@ let hpred_entries hpred = hpred_get_lexp [] hpred (** {2 Functions for computing free non-program variables} *) -(** Type of free variables. These include primed, normal and footprint variables. - We keep a count of how many types the variables appear. *) -type fav = Ident.t list ref - -let fav_new () = ref [] - -(** Emptyness check. *) -let fav_is_empty fav = match !fav with [] -> true | _ -> false - -(** Check whether a predicate holds for all elements. *) -let fav_for_all fav predicate = List.for_all ~f:predicate !fav - -(** Check whether a predicate holds for some elements. *) -let fav_exists fav predicate = List.exists ~f:predicate !fav - -(** flag to indicate whether fav's are stored in duplicate form. - Only to be used with fav_to_list *) -let fav_duplicates = ref false - -(** extend [fav] with a [id] *) -let ( ++ ) fav id = - if !fav_duplicates || not (List.exists ~f:(Ident.equal id) !fav) then fav := id :: !fav - - -(** extend [fav] with ident list [idl] *) -let ( +++ ) fav idl = List.iter ~f:(fun id -> fav ++ id) idl - -(** add identity lists to fav *) -let ident_list_fav_add idl fav = fav +++ idl - -(** Convert a list to a fav. *) -let fav_from_list l = - let fav = fav_new () in - let _ = List.iter ~f:(fun id -> fav ++ id) l in - fav - - -(** Convert a [fav] to a list of identifiers while preserving the order - that the identifiers were added to [fav]. *) -let fav_to_list fav = List.rev !fav - -(** Pretty print a fav. *) -let pp_fav f fav = Pp.seq Ident.pp f (fav_to_list fav) - -(** Turn a xxx_fav_add function into a xxx_fav function *) -let fav_imperative_to_functional f x = - let fav = fav_new () in - let _ = f fav x in - fav - - -(** [fav_filter_ident fav f] only keeps [id] if [f id] is true. *) -let fav_filter_ident fav filter = fav := List.filter ~f:filter !fav - -(** Like [fav_filter_ident] but return a copy. *) -let fav_copy_filter_ident fav filter = ref (List.filter ~f:filter !fav) - -let fav_mem fav id = List.exists ~f:(Ident.equal id) !fav - -let rec exp_fav_add fav e = - match (e : Exp.t) with - | Var id -> - fav ++ id - | Exn e -> - exp_fav_add fav e - | Closure {captured_vars} -> - List.iter ~f:(fun (e, _, _) -> exp_fav_add fav e) captured_vars - | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _) -> - () - | Cast (_, e) | UnOp (_, e, _) -> - exp_fav_add fav e - | BinOp (_, e1, e2) -> - exp_fav_add fav e1 ; exp_fav_add fav e2 - | Lvar _ -> - () - | Lfield (e, _, _) (* do nothing since we only count non-program variables *) -> - exp_fav_add fav e - | Lindex (e1, e2) -> - exp_fav_add fav e1 ; exp_fav_add fav e2 - (* TODO: Sizeof length expressions may contain variables, do not ignore them. *) - | Sizeof _ -> - () - - -let exp_fav = fav_imperative_to_functional exp_fav_add - -let exp_fav_list e = fav_to_list (exp_fav e) - -let ident_in_exp id e = - let fav = fav_new () in - exp_fav_add fav e ; fav_mem fav id - - -let atom_fav_add fav = function - | Aeq (e1, e2) | Aneq (e1, e2) -> - exp_fav_add fav e1 ; exp_fav_add fav e2 - | Apred (_, es) | Anpred (_, es) -> - List.iter ~f:(fun e -> exp_fav_add fav e) es - - -let atom_fav = fav_imperative_to_functional atom_fav_add - -let rec strexp_fav_add fav = function - | Eexp (e, _) -> - exp_fav_add fav e - | Estruct (fld_se_list, _) -> - List.iter ~f:(fun (_, se) -> strexp_fav_add fav se) fld_se_list - | Earray (len, idx_se_list, _) -> - exp_fav_add fav len ; - List.iter ~f:(fun (e, se) -> exp_fav_add fav e ; strexp_fav_add fav se) idx_se_list - - -let hpred_fav_add fav = function - | Hpointsto (base, sexp, te) -> - exp_fav_add fav base ; strexp_fav_add fav sexp ; exp_fav_add fav te - | Hlseg (_, _, e1, e2, elist) -> - exp_fav_add fav e1 ; - exp_fav_add fav e2 ; - List.iter ~f:(exp_fav_add fav) elist - | Hdllseg (_, _, e1, e2, e3, e4, elist) -> - exp_fav_add fav e1 ; - exp_fav_add fav e2 ; - exp_fav_add fav e3 ; - exp_fav_add fav e4 ; - List.iter ~f:(exp_fav_add fav) elist +let atom_gen_free_vars = + let open Sequence.Generator in + function + | Aeq (e1, e2) | Aneq (e1, e2) -> + Exp.gen_free_vars e1 >>= fun () -> Exp.gen_free_vars e2 + | Apred (_, es) | Anpred (_, es) -> + ISequence.gen_sequence_list es ~f:Exp.gen_free_vars -let hpred_fav = fav_imperative_to_functional hpred_fav_add +let atom_free_vars a = Sequence.Generator.run (atom_gen_free_vars a) -(** This function should be used before adding a new - index to Earray. The [exp] is the newly created - index. This function "cleans" [exp] according to whether it is - the footprint or current part of the prop. - The function faults in the re - execution mode, as an internal check of the tool. *) +let rec strexp_gen_free_vars = + let open Sequence.Generator in + function + | Eexp (e, _) -> + Exp.gen_free_vars e + | Estruct (fld_se_list, _) -> + ISequence.gen_sequence_list fld_se_list ~f:(fun (_, se) -> strexp_gen_free_vars se) + | Earray (len, idx_se_list, _) -> + Exp.gen_free_vars len + >>= fun () -> + ISequence.gen_sequence_list idx_se_list ~f:(fun (e, se) -> + Exp.gen_free_vars e >>= fun () -> strexp_gen_free_vars se ) + + +let hpred_gen_free_vars = + let open Sequence.Generator in + function + | Hpointsto (base, sexp, te) -> + Exp.gen_free_vars base + >>= fun () -> strexp_gen_free_vars sexp >>= fun () -> Exp.gen_free_vars te + | Hlseg (_, _, e1, e2, elist) -> + Exp.gen_free_vars e1 + >>= fun () -> + Exp.gen_free_vars e2 >>= fun () -> ISequence.gen_sequence_list elist ~f:Exp.gen_free_vars + | Hdllseg (_, _, e1, e2, e3, e4, elist) -> + Exp.gen_free_vars e1 + >>= fun () -> + Exp.gen_free_vars e2 + >>= fun () -> + Exp.gen_free_vars e3 + >>= fun () -> + Exp.gen_free_vars e4 >>= fun () -> ISequence.gen_sequence_list elist ~f:Exp.gen_free_vars + + +let hpred_free_vars h = Sequence.Generator.run (hpred_gen_free_vars h) + +(** This function should be used before adding a new index to Earray. The [exp] is the newly created + index. This function "cleans" [exp] according to whether it is the footprint or current part of + the prop. The function faults in the re - execution mode, as an internal check of the tool. *) let array_clean_new_index footprint_part new_idx = - if footprint_part && not !Config.footprint then assert false ; - let fav = exp_fav new_idx in - if footprint_part && fav_exists fav (fun id -> not (Ident.is_footprint id)) then ( + assert (not (footprint_part && not !Config.footprint)) ; + if footprint_part + && Exp.free_vars new_idx |> Sequence.exists ~f:(fun id -> not (Ident.is_footprint id)) + then ( L.d_warning ( "Array index " ^ Exp.to_string new_idx ^ " has non-footprint vars: replaced by fresh footprint var" ) ; @@ -1164,28 +1081,37 @@ let array_clean_new_index footprint_part new_idx = (** {2 Functions for computing all free or bound non-program variables} *) -let hpara_shallow_av_add fav para = - List.iter ~f:(hpred_fav_add fav) para.body ; - fav ++ para.root ; - fav ++ para.next ; - fav +++ para.svars ; - fav +++ para.evars - +(** Variables in hpara, excluding bound vars in the body *) +let hpara_shallow_gen_free_vars {body; root; next; svars; evars} = + let open Sequence.Generator in + ISequence.gen_sequence_list ~f:hpred_gen_free_vars body + >>= fun () -> + yield root + >>= fun () -> + yield next + >>= fun () -> + ISequence.gen_sequence_list ~f:yield svars + >>= fun () -> ISequence.gen_sequence_list ~f:yield evars -let hpara_dll_shallow_av_add fav para = - List.iter ~f:(hpred_fav_add fav) para.body_dll ; - fav ++ para.cell ; - fav ++ para.blink ; - fav ++ para.flink ; - fav +++ para.svars_dll ; - fav +++ para.evars_dll - -(** Variables in hpara, excluding bound vars in the body *) -let hpara_shallow_av = fav_imperative_to_functional hpara_shallow_av_add +let hpara_shallow_free_vars h = Sequence.Generator.run (hpara_shallow_gen_free_vars h) (** Variables in hpara_dll, excluding bound vars in the body *) -let hpara_dll_shallow_av = fav_imperative_to_functional hpara_dll_shallow_av_add +let hpara_dll_shallow_gen_free_vars {body_dll; cell; blink; flink; svars_dll; evars_dll} = + let open Sequence.Generator in + ISequence.gen_sequence_list ~f:hpred_gen_free_vars body_dll + >>= fun () -> + yield cell + >>= fun () -> + yield blink + >>= fun () -> + yield flink + >>= fun () -> + ISequence.gen_sequence_list ~f:yield svars_dll + >>= fun () -> ISequence.gen_sequence_list ~f:yield evars_dll + + +let hpara_dll_shallow_free_vars h = Sequence.Generator.run (hpara_dll_shallow_gen_free_vars h) (** {2 Functions for Substitution} *) @@ -1200,7 +1126,6 @@ type subst = [`Exp of exp_subst | `Typ of Typ.type_subst_t] [@@deriving compare] type subst_fun = [`Exp of Ident.t -> Exp.t | `Typ of (Typ.t -> Typ.t) * (Typ.Name.t -> Typ.Name.t)] -(** Equality for substitutions. *) let equal_exp_subst = [%compare.equal : exp_subst] let sub_no_duplicated_ids sub = not (List.contains_dup ~compare:compare_ident_exp_ids sub) @@ -1308,11 +1233,13 @@ let extend_sub sub id exp : exp_subst option = if mem_sub id sub then None else Some (List.merge ~cmp:compare sub [(id, exp)]) -(** Free auxilary variables in the domain and range of the - substitution. *) -let sub_fav_add fav (sub: exp_subst) = - List.iter ~f:(fun (id, e) -> fav ++ id ; exp_fav_add fav e) sub +(** Free auxilary variables in the domain and range of the substitution. *) +let exp_subst_gen_free_vars sub = + let open Sequence.Generator in + ISequence.gen_sequence_list sub ~f:(fun (id, e) -> yield id >>= fun () -> Exp.gen_free_vars e) + +let exp_subst_free_vars sub = Sequence.Generator.run (exp_subst_gen_free_vars sub) let rec exp_sub_ids (f: subst_fun) exp = let f_typ x = match f with `Exp _ -> x | `Typ (f, _) -> f x in diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index de5906130..5e2476b6e 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -405,81 +405,22 @@ val hpred_list_get_lexps : (Exp.t -> bool) -> hpred list -> Exp.t list val hpred_entries : hpred -> Exp.t list -(** {2 Function for computing lexps in sigma} *) +val atom_free_vars : atom -> Ident.t Sequence.t -(** Type of free variables. These include primed, normal and footprint variables. - We remember the order in which variables are added. *) -type fav +val atom_gen_free_vars : atom -> (unit, Ident.t) Sequence.Generator.t -val fav_duplicates : bool ref -(** flag to indicate whether fav's are stored in duplicate form. - Only to be used with fav_to_list *) +val hpred_free_vars : hpred -> Ident.t Sequence.t -val pp_fav : F.formatter -> fav -> unit [@@warning "-32"] -(** Pretty print a fav. *) +val hpred_gen_free_vars : hpred -> (unit, Ident.t) Sequence.Generator.t -val fav_new : unit -> fav -(** Create a new [fav]. *) +val hpara_shallow_free_vars : hpara -> Ident.t Sequence.t -val fav_is_empty : fav -> bool -(** Emptyness check. *) - -val fav_for_all : fav -> (Ident.t -> bool) -> bool -(** Check whether a predicate holds for all elements. *) - -val fav_exists : fav -> (Ident.t -> bool) -> bool -(** Check whether a predicate holds for some elements. *) - -val fav_mem : fav -> Ident.t -> bool -(** Membership test fot [fav] *) - -val fav_from_list : Ident.t list -> fav -(** Convert a list to a fav. *) - -val fav_to_list : fav -> Ident.t list -(** Convert a [fav] to a list of identifiers while preserving the order - that identifiers were added to [fav]. *) - -val fav_imperative_to_functional : (fav -> 'a -> unit) -> 'a -> fav -(** Turn a xxx_fav_add function into a xxx_fav function *) - -val fav_filter_ident : fav -> (Ident.t -> bool) -> unit -(** [fav_filter_ident fav f] only keeps [id] if [f id] is true. *) - -val fav_copy_filter_ident : fav -> (Ident.t -> bool) -> fav -(** Like [fav_filter_ident] but return a copy. *) - -val ident_list_fav_add : Ident.t list -> fav -> unit -(** add identifier list to fav *) - -val exp_fav_add : fav -> Exp.t -> unit -(** [exp_fav_add fav exp] extends [fav] with the free variables of [exp] *) - -val exp_fav : Exp.t -> fav - -val exp_fav_list : Exp.t -> Ident.t list - -val ident_in_exp : Ident.t -> Exp.t -> bool - -val strexp_fav_add : fav -> strexp -> unit - -val atom_fav_add : fav -> atom -> unit - -val atom_fav : atom -> fav - -val hpred_fav_add : fav -> hpred -> unit - -val hpred_fav : hpred -> fav - -val hpara_shallow_av : hpara -> fav -(** Variables in hpara, excluding bound vars in the body *) - -val hpara_dll_shallow_av : hpara_dll -> fav +val hpara_dll_shallow_free_vars : hpara_dll -> Ident.t Sequence.t (** Variables in hpara_dll, excluding bound vars in the body *) (** {2 Substitution} *) -type exp_subst [@@deriving compare] +type exp_subst = private (Ident.t * Exp.t) list [@@deriving compare] type subst = [`Exp of exp_subst | `Typ of Typ.type_subst_t] [@@deriving compare] @@ -557,9 +498,9 @@ val sub_map : (Ident.t -> Ident.t) -> (Exp.t -> Exp.t) -> exp_subst -> exp_subst val extend_sub : exp_subst -> Ident.t -> Exp.t -> exp_subst option (** Extend substitution and return [None] if not possible. *) -val sub_fav_add : fav -> exp_subst -> unit -(** Free auxilary variables in the domain and range of the - substitution. *) +val exp_subst_free_vars : exp_subst -> Ident.t Sequence.t + +val exp_subst_gen_free_vars : exp_subst -> (unit, Ident.t) Sequence.Generator.t (** substitution functions WARNING: these functions do not ensure that the results are normalized. *) diff --git a/infer/src/backend/Attribute.ml b/infer/src/backend/Attribute.ml index 2f9fbcc89..8f96dac49 100644 --- a/infer/src/backend/Attribute.ml +++ b/infer/src/backend/Attribute.ml @@ -324,12 +324,12 @@ let deallocate_stack_vars tenv (p: 'a Prop.t) pvars = in let p'' = let res = ref p' in - let p'_fav = Prop.prop_fav p' in + let p'_fav = Prop.free_vars p' |> Ident.set_of_sequence in let do_var (v, freshv) = (* static locals are not stack-allocated *) if not (Pvar.is_static_local v) then (* the address of a de-allocated stack var in in the post *) - if Sil.fav_mem p'_fav freshv then ( + if Ident.Set.mem freshv p'_fav then ( stack_vars_address_in_post := v :: !stack_vars_address_in_post ; let pred = Sil.Apred (Adangling DAaddr_stack_var, [Exp.Var freshv]) in res := add_or_replace tenv !res pred ) diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml index 5d1a18602..30a722ffd 100644 --- a/infer/src/backend/BuiltinDefn.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -195,7 +195,9 @@ let create_type tenv n_lexp typ prop = let sigma_fp = prop.Prop.sigma_fp in let prop' = Prop.set prop ~sigma:(hpred :: sigma) in let prop'' = - let has_normal_variables = Sil.fav_exists (Sil.exp_fav n_lexp) Ident.is_normal in + let has_normal_variables = + Exp.free_vars n_lexp |> Sequence.exists ~f:Ident.is_normal + in if is_undefined_opt tenv prop n_lexp || has_normal_variables then prop' else Prop.set prop' ~sigma_fp:(hpred :: sigma_fp) in diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index ec6d1b65f..390b7a131 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -40,12 +40,6 @@ let sigma_rewrite tenv p r : Prop.normal Prop.t option = Some (Prop.normalize tenv p_new) -let sigma_fav_list sigma = Sil.fav_to_list (Prop.sigma_fav sigma) - -let sigma_fav_in_pvars = Sil.fav_imperative_to_functional Prop.sigma_fav_in_pvars_add - -let sigma_fav_in_pvars_list sigma = Sil.fav_to_list (sigma_fav_in_pvars sigma) - (******************** Start of SLL abstraction rules *****************) let create_fresh_primeds_ls para = let id_base = Ident.create_fresh Ident.kprimed in @@ -76,24 +70,30 @@ let create_condition_ls ids_private id_base p_leftover (inst: Sil.exp_subst) = let insts_of_private_ids = Sil.sub_range inst_private in (insts_of_private_ids, insts_of_public_ids, inst_of_base) in - let fav_insts_of_public_ids = List.concat_map ~f:Sil.exp_fav_list insts_of_public_ids in - let fav_insts_of_private_ids = List.concat_map ~f:Sil.exp_fav_list insts_of_private_ids in - let fav_p_leftover, _ = - let sigma = p_leftover.Prop.sigma in - (sigma_fav_list sigma, sigma_fav_in_pvars_list sigma) - in (* let fav_inst_of_base = Sil.exp_fav_list inst_of_base in L.out "@[.... application of condition ....@\n@."; L.out "@[<4> private ids : %a@\n@." pp_exp_list insts_of_private_ids; L.out "@[<4> public ids : %a@\n@." pp_exp_list insts_of_public_ids; *) - (* (not (IList.intersect compare fav_inst_of_base fav_in_pvars)) && *) Exp.program_vars inst_of_base |> Sequence.is_empty && List.for_all ~f:(fun e -> Exp.program_vars e |> Sequence.is_empty) insts_of_private_ids - && not (List.exists ~f:Ident.is_normal fav_insts_of_private_ids) - && not (IList.intersect Ident.compare fav_insts_of_private_ids fav_p_leftover) - && not (IList.intersect Ident.compare fav_insts_of_private_ids fav_insts_of_public_ids) + && + let fav_insts_of_private_ids = + Sequence.of_list insts_of_private_ids |> Sequence.concat_map ~f:Exp.free_vars + |> Sequence.memoize + in + not (Sequence.exists fav_insts_of_private_ids ~f:Ident.is_normal) + && + let fav_insts_of_private_ids = Ident.set_of_sequence fav_insts_of_private_ids in + let intersects_fav_insts_of_private_ids s = + Sequence.exists s ~f:(fun id -> Ident.Set.mem id fav_insts_of_private_ids) + in + (* [fav_insts_of_private_ids] does not intersect the free vars in [p_leftover.sigma] *) + Prop.sigma_free_vars p_leftover.Prop.sigma |> Fn.non intersects_fav_insts_of_private_ids + && (* [fav_insts_of_private_ids] does not intersect the free vars in [insts_of_public_ids] *) + List.for_all insts_of_public_ids ~f:(fun e -> + Exp.free_vars e |> Fn.non intersects_fav_insts_of_private_ids ) let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para: Sil.hpara) = @@ -860,15 +860,15 @@ let abstract_pure_part tenv p ~(from_abstract_footprint: bool) = let do_pure pure = let pi_filtered = let sigma = p.Prop.sigma in - let fav_sigma = Prop.sigma_fav sigma in - let fav_nonpure = Prop.prop_fav_nonpure p in + let fav_sigma = Prop.sigma_free_vars sigma |> Ident.set_of_sequence in + let fav_nonpure = Prop.non_pure_free_vars p |> Ident.set_of_sequence in (* vars in current and footprint sigma *) let filter atom = - let fav' = Sil.atom_fav atom in - Sil.fav_for_all fav' (fun id -> - if Ident.is_primed id then Sil.fav_mem fav_sigma id - else if Ident.is_footprint id then Sil.fav_mem fav_nonpure id - else true ) + Sil.atom_free_vars atom + |> Sequence.for_all ~f:(fun id -> + if Ident.is_primed id then Ident.Set.mem id fav_sigma + else if Ident.is_footprint id then Ident.Set.mem id fav_nonpure + else true ) in List.filter ~f:filter pure in @@ -908,27 +908,20 @@ let abstract_pure_part tenv p ~(from_abstract_footprint: bool) = let abstract_gc tenv p = let pi = p.Prop.pi in let p_without_pi = Prop.normalize tenv (Prop.set p ~pi:[]) in - let fav_p_without_pi = Prop.prop_fav p_without_pi in + let fav_p_without_pi = Prop.free_vars p_without_pi |> Ident.set_of_sequence in (* let weak_filter atom = let fav_atom = atom_fav atom in IList.intersect compare fav_p_without_pi fav_atom in *) + let check fav_seq = + Sequence.is_empty fav_seq + || (* non-empty intersection with [fav_p_without_pi] *) + Sequence.exists fav_seq ~f:(fun id -> Ident.Set.mem id fav_p_without_pi) + in let strong_filter = function | Sil.Aeq (e1, e2) | Sil.Aneq (e1, e2) -> - let fav_e1 = Sil.exp_fav e1 in - let fav_e2 = Sil.exp_fav e2 in - let intersect_e1 _ = - IList.intersect Ident.compare (Sil.fav_to_list fav_e1) (Sil.fav_to_list fav_p_without_pi) - in - let intersect_e2 _ = - IList.intersect Ident.compare (Sil.fav_to_list fav_e2) (Sil.fav_to_list fav_p_without_pi) - in - let no_fav_e1 = Sil.fav_is_empty fav_e1 in - let no_fav_e2 = Sil.fav_is_empty fav_e2 in - (no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ()) + check (Exp.free_vars e1) && check (Exp.free_vars e2) | (Sil.Apred _ | Anpred _) as a -> - let fav_a = Sil.atom_fav a in - Sil.fav_is_empty fav_a - || IList.intersect Ident.compare (Sil.fav_to_list fav_a) (Sil.fav_to_list fav_p_without_pi) + check (Sil.atom_free_vars a) in let new_pi = List.filter ~f:strong_filter pi in let prop = Prop.normalize tenv (Prop.set p ~pi:new_pi) in @@ -950,11 +943,10 @@ end) (** find the id's in sigma reachable from the given roots *) let sigma_reachable root_fav sigma = - let fav_to_set fav = Ident.idlist_to_idset (Sil.fav_to_list fav) in - let reach_set = ref (fav_to_set root_fav) in + let reach_set = ref root_fav in let edges = ref [] in let do_hpred hpred = - let hp_fav_set = fav_to_set (Sil.hpred_fav hpred) in + let hp_fav_set = Sil.hpred_free_vars hpred |> Ident.set_of_sequence in let add_entry e = edges := (e, hp_fav_set) :: !edges in List.iter ~f:add_entry (Sil.hpred_entries hpred) in @@ -1012,9 +1004,6 @@ let check_observer_is_unsubscribed_deallocation tenv prop e = let check_junk ?original_prop pname tenv prop = - let fav_sub_sigmafp = Sil.fav_new () in - Sil.sub_fav_add fav_sub_sigmafp prop.Prop.sub ; - Prop.sigma_fav_add fav_sub_sigmafp prop.Prop.sigma_fp ; let leaks_reported = ref [] in let remove_junk_once fp_part fav_root sigma = let id_considered_reachable = @@ -1025,7 +1014,7 @@ let check_junk ?original_prop pname tenv prop = let should_remove_hpred entries = let predicate = function | Exp.Var id -> - (Ident.is_primed id || Ident.is_footprint id) && not (Sil.fav_mem fav_root id) + (Ident.is_primed id || Ident.is_footprint id) && not (Ident.Set.mem id fav_root) && not (id_considered_reachable id) | _ -> false @@ -1169,8 +1158,14 @@ let check_junk ?original_prop pname tenv prop = if Int.equal (List.length sigma') (List.length sigma) then sigma' else remove_junk fp_part fav_root sigma' in - let sigma_new = remove_junk false fav_sub_sigmafp prop.Prop.sigma in - let sigma_fp_new = remove_junk true (Sil.fav_new ()) prop.Prop.sigma_fp in + let sigma_new = + let fav_sub = Sil.exp_subst_free_vars prop.Prop.sub |> Ident.set_of_sequence in + let fav_sub_sigmafp = + Prop.sigma_free_vars prop.Prop.sigma_fp |> Ident.set_of_sequence ~init:fav_sub + in + remove_junk false fav_sub_sigmafp prop.Prop.sigma + in + let sigma_fp_new = remove_junk true Ident.Set.empty prop.Prop.sigma_fp in if Prop.equal_sigma prop.Prop.sigma sigma_new && Prop.equal_sigma prop.Prop.sigma_fp sigma_fp_new then prop else Prop.normalize tenv (Prop.set prop ~sigma:sigma_new ~sigma_fp:sigma_fp_new) diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index d3b542623..9cfa27204 100644 --- a/infer/src/backend/absarray.ml +++ b/infer/src/backend/absarray.ml @@ -586,7 +586,7 @@ let check_after_array_abstraction tenv prop = if !Config.footprint then let path = StrexpMatch.path_from_exp_offsets root offs in index_is_pointed_to tenv prop path ind - else not (Sil.fav_exists (Sil.exp_fav ind) Ident.is_primed) + else not (Exp.free_vars ind |> Sequence.exists ~f:Ident.is_primed) in let rec check_se root offs typ = function | Sil.Eexp _ -> @@ -631,21 +631,19 @@ let remove_redundant_elements tenv prop = Prop.d_prop prop ; L.d_ln () ; let occurs_at_most_once : Ident.t -> bool = - (* the variable occurs at most once in the footprint or current part *) - let fav_curr = Sil.fav_new () in - let fav_foot = Sil.fav_new () in - Sil.fav_duplicates := true ; - Sil.sub_fav_add fav_curr prop.Prop.sub ; - Prop.pi_fav_add fav_curr prop.Prop.pi ; - Prop.sigma_fav_add fav_curr prop.Prop.sigma ; - Prop.pi_fav_add fav_foot prop.Prop.pi_fp ; - Prop.sigma_fav_add fav_foot prop.Prop.sigma_fp ; - let favl_curr = Sil.fav_to_list fav_curr in - let favl_foot = Sil.fav_to_list fav_foot in - Sil.fav_duplicates := false ; - let num_occur l id = List.length (List.filter ~f:(fun id' -> Ident.equal id id') l) in - let at_most_once v = num_occur favl_curr v <= 1 && num_occur favl_foot v <= 1 in - at_most_once + let fav_curr = + let ( @@@ ) = Sequence.append in + Sil.exp_subst_free_vars prop.Prop.sub @@@ Prop.pi_free_vars prop.Prop.pi + @@@ Prop.sigma_free_vars prop.Prop.sigma + in + let fav_foot = + Sequence.append (Prop.pi_free_vars prop.Prop.pi_fp) (Prop.sigma_free_vars prop.Prop.sigma_fp) + in + let at_most_once seq id = + Sequence.filter seq ~f:(Ident.equal id) |> Sequence.length_is_bounded_by ~max:1 + in + let at_most_once_in_curr_or_foot v = at_most_once fav_curr v && at_most_once fav_foot v in + at_most_once_in_curr_or_foot in let modified = ref false in let filter_redundant_e_se fp_part (e, se) = diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index c16d99473..f58451d05 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -44,7 +44,7 @@ let equal_sigma sigma1 sigma2 = let sigma_get_start_lexps_sort sigma = let exp_compare_neg e1 e2 = -Exp.compare e1 e2 in - let filter e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in + let filter e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in let lexps = Sil.hpred_list_get_lexps filter sigma in List.sort ~cmp:exp_compare_neg lexps @@ -576,7 +576,7 @@ module Rename : sig val lookup_list_todo : side -> Exp.t list -> Exp.t list - val to_subst_proj : side -> Sil.fav -> Sil.exp_subst + val to_subst_proj : side -> unit Ident.HashQueue.t -> Sil.exp_subst val to_subst_emb : side -> Sil.exp_subst (* @@ -596,7 +596,7 @@ end = struct let f = function | Exp.Var id, e, _ | e, Exp.Var id, _ -> Ident.is_footprint id - && Sil.fav_for_all (Sil.exp_fav e) (fun id -> not (Ident.is_primed id)) + && Exp.free_vars e |> Sequence.for_all ~f:(fun id -> not (Ident.is_primed id)) | _ -> false in @@ -684,7 +684,9 @@ end = struct let to_subst_proj (side: side) vars = let renaming_restricted = - List.filter ~f:(function _, _, Exp.Var i -> Sil.fav_mem vars i | _ -> assert false) !tbl + List.filter + ~f:(function _, _, Exp.Var i -> Ident.HashQueue.mem vars i | _ -> assert false) + !tbl in let sub_list_side = List.map @@ -780,13 +782,9 @@ end = struct L.d_ln () ) ; Some (a_res, a_op) in - let exp_contains_only_normal_ids e = - let fav = Sil.exp_fav e in - Sil.fav_for_all fav Ident.is_normal - in + let exp_contains_only_normal_ids e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in let atom_contains_only_normal_ids a = - let fav = Sil.atom_fav a in - Sil.fav_for_all fav Ident.is_normal + Sil.atom_free_vars a |> Sequence.for_all ~f:Ident.is_normal in let normal_ids_only = atom_contains_only_normal_ids atom_in in if normal_ids_only then Some (atom_in, atom_in) @@ -840,15 +838,14 @@ end = struct | Some res -> res | None -> - let fav1 = Sil.exp_fav e1 in - let fav2 = Sil.exp_fav e2 in - let no_ren1 = not (Sil.fav_exists fav1 can_rename) in - let no_ren2 = not (Sil.fav_exists fav2 can_rename) in let some_primed () = - Sil.fav_exists fav1 Ident.is_primed || Sil.fav_exists fav2 Ident.is_primed + Exp.free_vars e1 |> Sequence.exists ~f:Ident.is_primed + || Exp.free_vars e2 |> Sequence.exists ~f:Ident.is_primed in let e = - if no_ren1 && no_ren2 then + if not (Exp.free_vars e1 |> Sequence.exists ~f:can_rename) + && not (Exp.free_vars e2 |> Sequence.exists ~f:can_rename) + then if Exp.equal e1 e2 then e1 else ( L.d_strln "failure reason 13" ; raise Sil.JoinFail ) else match default_op with @@ -1432,7 +1429,7 @@ let same_pred (hpred1: Sil.hpred) (hpred2: Sil.hpred) : bool = let sigma_renaming_check (lhs: side) (sigma: Prop.sigma) (sigma_new: Prop.sigma) = (* apply the lhs / rhs of the renaming to sigma, * and check that the renaming of primed vars is injective *) - let fav_sigma = Prop.sigma_fav sigma_new in + let fav_sigma = Prop.sigma_free_vars sigma_new |> Ident.hashqueue_of_sequence in let sub = Rename.to_subst_proj lhs fav_sigma in let sigma' = Prop.sigma_sub (`Exp sub) sigma_new in equal_sigma sigma sigma' @@ -1840,8 +1837,8 @@ let pi_partial_meet tenv (p: Prop.normal Prop.t) (ep1: 'a Prop.t) (ep2: 'b Prop. let dom1 = Ident.idlist_to_idset (Sil.sub_domain sub1) in let dom2 = Ident.idlist_to_idset (Sil.sub_domain sub2) in let handle_atom sub dom atom = - let fav_list = Sil.fav_to_list (Sil.atom_fav atom) in - if List.for_all ~f:(fun id -> Ident.Set.mem id dom) fav_list then Sil.atom_sub (`Exp sub) atom + if Sil.atom_free_vars atom |> Sequence.for_all ~f:(fun id -> Ident.Set.mem id dom) then + Sil.atom_sub (`Exp sub) atom else ( L.d_str "handle_atom failed on " ; Sil.d_atom atom ; L.d_ln () ; raise Sil.JoinFail ) in let f1 p' atom = Prop.prop_atom_and tenv p' (handle_atom sub1 dom1 atom) in @@ -1870,7 +1867,7 @@ let eprop_partial_meet tenv (ep1: 'a Prop.t) (ep2: 'b Prop.t) : 'c Prop.t = let sub1 = ep1.Prop.sub in let sub2 = ep2.Prop.sub in let range1 = Sil.sub_range sub1 in - let f e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in + let f e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in Sil.equal_exp_subst sub1 sub2 && List.for_all ~f range1 in if not (sub_check ()) then ( L.d_strln "sub_check() failed" ; raise Sil.JoinFail ) @@ -1920,7 +1917,7 @@ let eprop_partial_join' tenv mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed let sub2 = ep2.Prop.sub in let sub_common, sub1_only, sub2_only = Sil.sub_symmetric_difference sub1 sub2 in let sub_common_normal, sub_common_other = - let f e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in + let f e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in Sil.sub_range_partition f sub_common in let eqs1, eqs2 = @@ -1970,12 +1967,14 @@ let footprint_partial_join' tenv (p1: Prop.normal Prop.t) (p2: Prop.normal Prop. let efp = eprop_partial_join' tenv JoinState.Pre fp1 fp2 in let pi_fp = let pi_fp0 = Prop.get_pure efp in - let f a = Sil.fav_for_all (Sil.atom_fav a) Ident.is_footprint in + let f a = Sil.atom_free_vars a |> Sequence.for_all ~f:Ident.is_footprint in List.filter ~f pi_fp0 in let sigma_fp = let sigma_fp0 = efp.Prop.sigma in - let f a = Sil.fav_exists (Sil.hpred_fav a) (fun a -> not (Ident.is_footprint a)) in + let f a = + Sil.hpred_free_vars a |> Sequence.exists ~f:(fun a -> not (Ident.is_footprint a)) + in if List.exists ~f sigma_fp0 then ( L.d_strln "failure reason 66" ; raise Sil.JoinFail ) ; sigma_fp0 in diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 6b0c3703b..696a96ed2 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -365,15 +365,13 @@ let do_after_node node = Printer.node_finish_session node (** Return the list of normal ids occurring in the instructions *) let instrs_get_normal_vars instrs = - let fav = Sil.fav_new () in - let do_instr instr = - let do_e e = Sil.exp_fav_add fav e in - let exps = Sil.instr_get_exps instr in - List.iter ~f:do_e exps + let do_instr res instr = + Sil.instr_get_exps instr + |> List.fold_left ~init:res ~f:(fun res e -> + Exp.free_vars e |> Sequence.filter ~f:Ident.is_normal + |> Ident.hashqueue_of_sequence ~init:res ) in - List.iter ~f:do_instr instrs ; - Sil.fav_filter_ident fav Ident.is_normal ; - Sil.fav_to_list fav + List.fold_left ~init:(Ident.HashQueue.create ()) ~f:do_instr instrs |> Ident.HashQueue.keys (** Perform symbolic execution for a node starting from an initial prop *) @@ -571,13 +569,13 @@ let compute_visited vset = let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list = let pname = Procdesc.get_proc_name pdesc in let sub = - let fav = Sil.fav_new () in - Paths.PathSet.iter (fun prop _ -> Prop.prop_fav_add fav prop) pathset ; - let sub_list = - List.map - ~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.knormal))) - (Sil.fav_to_list fav) + let fav = + Paths.PathSet.fold + (fun prop _ res -> Prop.free_vars prop |> Ident.hashqueue_of_sequence ~init:res) + pathset (Ident.HashQueue.create ()) + |> Ident.HashQueue.keys in + let sub_list = List.map ~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.knormal))) fav in Sil.exp_subst_of_list sub_list in let pre_post_visited_list = @@ -736,7 +734,7 @@ let initial_prop_from_emp tenv curr_f = initial_prop tenv curr_f Prop.prop_emp t (** Construct an initial prop from an existing pre with formals *) let initial_prop_from_pre tenv curr_f pre = if !Config.footprint then - let vars = Sil.fav_to_list (Prop.prop_fav pre) in + let vars = Prop.free_vars pre |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in let sub_list = List.map ~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.kfootprint))) vars in diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index c507885e6..03f8ea3a9 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -152,7 +152,7 @@ and isel_match isel1 sub vars isel2 = None | (idx1, se1') :: isel1', (idx2, se2') :: isel2' -> let idx2 = Sil.exp_sub (`Exp sub) idx2 in - let sanity_check = not (List.exists ~f:(fun id -> Sil.ident_in_exp id idx2) vars) in + let sanity_check = not (List.exists ~f:(fun id -> Exp.ident_mem idx2 id) vars) in if not sanity_check then ( let pe = Pp.text in L.internal_error "@[.... Sanity Check Failure while Matching Index-Strexps ....@\n" ; @@ -202,9 +202,7 @@ let rec instantiate_to_emp p condition (sub: Sil.exp_subst) vars = function None | Sil.Hlseg (_, _, e1, e2, _) -> ( - let fully_instantiated = - not (List.exists ~f:(fun id -> Sil.ident_in_exp id e1) vars) - in + let fully_instantiated = not (List.exists ~f:(fun id -> Exp.ident_mem e1 id) vars) in if not fully_instantiated then None else let e1' = Sil.exp_sub (`Exp sub) e1 in @@ -215,8 +213,7 @@ let rec instantiate_to_emp p condition (sub: Sil.exp_subst) vars = function instantiate_to_emp p condition sub_new vars_leftover hpats ) | Sil.Hdllseg (_, _, iF, oB, oF, iB, _) -> let fully_instantiated = - not - (List.exists ~f:(fun id -> Sil.ident_in_exp id iF || Sil.ident_in_exp id oB) vars) + not (List.exists ~f:(fun id -> Exp.ident_mem iF id || Exp.ident_mem oB id) vars) in if not fully_instantiated then None else @@ -338,7 +335,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats = let filter = gen_filter_lseg k2 para2 e_start2 e_end2 es_shared2 in let do_emp_lseg _ = let fully_instantiated_start2 = - not (List.exists ~f:(fun id -> Sil.ident_in_exp id e_start2) vars) + not (List.exists ~f:(fun id -> Exp.ident_mem e_start2 id) vars) in if not fully_instantiated_start2 then None else @@ -407,7 +404,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats = let filter = gen_filter_dllseg k2 para2 iF2 oB2 oF2 iB2 es_shared2 in let do_emp_dllseg _ = let fully_instantiated_iFoB2 = - not (List.exists ~f:(fun id -> Sil.ident_in_exp id iF2 || Sil.ident_in_exp id oB2) vars) + not (List.exists ~f:(fun id -> Exp.ident_mem iF2 id || Exp.ident_mem oB2 id) vars) in if not fully_instantiated_iFoB2 then None else @@ -425,9 +422,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats = prop_match_with_impl_sub tenv p condition sub_new vars_leftover hpat_next hpats_rest in let do_para_dllseg _ = - let fully_instantiated_iF2 = - not (List.exists ~f:(fun id -> Sil.ident_in_exp id iF2) vars) - in + let fully_instantiated_iF2 = not (List.exists ~f:(fun id -> Exp.ident_mem iF2 id) vars) in if not fully_instantiated_iF2 then None else let iF2' = Sil.exp_sub (`Exp sub) iF2 in diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index 08425e98b..865fec692 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -632,7 +632,8 @@ end = struct (!el1, !el2) - (** It's the caller's resposibility to ensure that Prop.prop_rename_primed_footprint_vars was called on the prop *) + (** It's the caller's responsibility to ensure that [Prop.prop_rename_primed_footprint_vars] was + called on the prop *) let add_renamed_prop (p: Prop.normal Prop.t) (path: Path.t) (ps: t) : t = let path_new = try diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 371b9696a..06163f2bf 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -28,6 +28,9 @@ type normal (** kind for exposed props *) type exposed +(** kind for sorted props *) +type sorted + type pi = Sil.atom list [@@deriving compare] type sigma = Sil.hpred list [@@deriving compare] @@ -56,6 +59,8 @@ module Core : sig val unsafe_cast_to_normal : exposed t -> normal t (** Cast an exposed prop to a normalized one by just changing the type *) + + val unsafe_cast_to_sorted : exposed t -> sorted t end = struct (** A proposition. The following invariants are mantained. [sub] is of the form id1 = e1 ... idn = en where: the id's are distinct and do not @@ -84,12 +89,18 @@ end = struct let unsafe_cast_to_normal (p: exposed t) : normal t = (p :> normal t) + + let unsafe_cast_to_sorted (p: exposed t) : sorted t = (p :> sorted t) end include Core (** {2 Basic Functions for Propositions} *) +let expose (p: normal t) : exposed t = Obj.magic p + +let expose_sorted (p: sorted t) : exposed t = Obj.magic p + (** {1 Functions for Comparison} *) (** Comparison between propositions. Lexicographical order. *) @@ -357,44 +368,45 @@ let d_proplist_with_typ (pl: 'a t list) = L.add_print_action (PTprop_list_with_t (** {1 Functions for computing free non-program variables} *) -let pi_fav_add fav pi = List.iter ~f:(Sil.atom_fav_add fav) pi +let pi_gen_free_vars pi = ISequence.gen_sequence_list pi ~f:Sil.atom_gen_free_vars -let pi_fav = Sil.fav_imperative_to_functional pi_fav_add +let pi_free_vars pi = Sequence.Generator.run (pi_gen_free_vars pi) -let sigma_fav_add fav sigma = List.iter ~f:(Sil.hpred_fav_add fav) sigma +let sigma_gen_free_vars sigma = ISequence.gen_sequence_list sigma ~f:Sil.hpred_gen_free_vars -let sigma_fav = Sil.fav_imperative_to_functional sigma_fav_add +let sigma_free_vars sigma = Sequence.Generator.run (sigma_gen_free_vars sigma) -let prop_footprint_fav_add fav prop = sigma_fav_add fav prop.sigma_fp ; pi_fav_add fav prop.pi_fp +(** Find free variables in the footprint part of the prop *) +let footprint_gen_free_vars {sigma_fp; pi_fp} = + Sequence.Generator.(sigma_gen_free_vars sigma_fp >>= fun () -> pi_gen_free_vars pi_fp) -(** Find fav of the footprint part of the prop *) -let prop_footprint_fav prop = Sil.fav_imperative_to_functional prop_footprint_fav_add prop -let prop_fav_add fav prop = - sigma_fav_add fav prop.sigma ; - sigma_fav_add fav prop.sigma_fp ; - Sil.sub_fav_add fav prop.sub ; - pi_fav_add fav prop.pi ; - pi_fav_add fav prop.pi_fp +let footprint_free_vars prop = Sequence.Generator.run (footprint_gen_free_vars prop) +let gen_free_vars {sigma; sigma_fp; sub; pi; pi_fp} = + let open Sequence.Generator in + sigma_gen_free_vars sigma + >>= fun () -> + sigma_gen_free_vars sigma_fp + >>= fun () -> + Sil.exp_subst_gen_free_vars sub + >>= fun () -> pi_gen_free_vars pi >>= fun () -> pi_gen_free_vars pi_fp -let prop_fav p = Sil.fav_imperative_to_functional prop_fav_add p -(** free vars of the prop, excluding the pure part *) -let prop_fav_nonpure_add fav prop = sigma_fav_add fav prop.sigma ; sigma_fav_add fav prop.sigma_fp +let free_vars prop = Sequence.Generator.run (gen_free_vars prop) -(** free vars, except pi and sub, of current and footprint parts *) -let prop_fav_nonpure = Sil.fav_imperative_to_functional prop_fav_nonpure_add +let exposed_gen_free_vars prop = gen_free_vars (unsafe_cast_to_normal prop) -let hpred_fav_in_pvars_add fav (hpred: Sil.hpred) = - match hpred with - | Hpointsto (Lvar _, sexp, _) -> - Sil.strexp_fav_add fav sexp - | Hpointsto _ | Hlseg _ | Hdllseg _ -> - () +let sorted_gen_free_vars prop = exposed_gen_free_vars (expose_sorted prop) + +let sorted_free_vars prop = Sequence.Generator.run (sorted_gen_free_vars prop) + +(** free vars of the prop, excluding the pure part *) +let non_pure_gen_free_vars {sigma; sigma_fp} = + Sequence.Generator.(sigma_gen_free_vars sigma >>= fun () -> sigma_gen_free_vars sigma_fp) -let sigma_fav_in_pvars_add fav sigma = List.iter ~f:(hpred_fav_in_pvars_add fav) sigma +let non_pure_free_vars prop = Sequence.Generator.run (non_pure_gen_free_vars prop) (** {2 Functions for Subsitition} *) @@ -1629,17 +1641,18 @@ module Normalize = struct let footprint_normalize tenv prop = let nsigma = sigma_normalize tenv Sil.sub_empty prop.sigma_fp in let npi = pi_normalize tenv Sil.sub_empty nsigma prop.pi_fp in - let fp_vars = - let fav = pi_fav npi in - sigma_fav_add fav nsigma ; fav + let ids_primed = + let fav = + pi_free_vars npi |> Sequence.filter ~f:Ident.is_primed |> Ident.hashqueue_of_sequence + in + sigma_free_vars nsigma |> Sequence.filter ~f:Ident.is_primed + |> Ident.hashqueue_of_sequence ~init:fav |> Ident.HashQueue.keys in - Sil.fav_filter_ident fp_vars Ident.is_primed ; (* only keep primed vars *) let npi', nsigma' = - if Sil.fav_is_empty fp_vars then (npi, nsigma) + if List.is_empty ids_primed then (npi, nsigma) else (* replace primed vars by fresh footprint vars *) - let ids_primed = Sil.fav_to_list fp_vars in let ids_footprint = List.map ~f:(fun id -> (id, Ident.create_fresh Ident.kfootprint)) ids_primed in @@ -1655,7 +1668,7 @@ module Normalize = struct (** This function assumes that if (x,Exp.Var(y)) in sub, then compare x y = 1 *) let sub_normalize sub = - let f (id, e) = not (Ident.is_primed id) && not (Sil.ident_in_exp id e) in + let f (id, e) = not (Ident.is_primed id) && not (Exp.ident_mem e id) in let sub' = Sil.sub_filter_pair ~f sub in if Sil.equal_exp_subst sub sub' then sub else sub' @@ -1667,7 +1680,7 @@ module Normalize = struct else let p' = match a' with - | Aeq (Var i, e) when Sil.ident_in_exp i e -> + | Aeq (Var i, e) when Exp.ident_mem e i -> p | Aeq (Var i, e) -> let sub_list = [(i, e)] in @@ -1698,7 +1711,7 @@ module Normalize = struct else let p'' = match a' with - | Aeq (Exp.Var i, e) when not (Sil.ident_in_exp i e) -> + | Aeq (Exp.Var i, e) when not (Exp.ident_mem e i) -> let mysub = Sil.subst_of_list [(i, e)] in let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in let pi_fp' = a' :: pi_normalize tenv mysub sigma_fp' p'.pi_fp in @@ -1854,7 +1867,7 @@ end let sigma_get_start_lexps_sort sigma = let exp_compare_neg e1 e2 = -Exp.compare e1 e2 in - let filter e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in + let filter e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in let lexps = Sil.hpred_list_get_lexps filter sigma in List.sort ~cmp:exp_compare_neg lexps @@ -1908,17 +1921,15 @@ let sigma_dfs_sort tenv sigma = final () ; sigma' -let prop_dfs_sort tenv p = +let dfs_sort tenv p : sorted t = let sigma = p.sigma in let sigma' = sigma_dfs_sort tenv sigma in let sigma_fp = p.sigma_fp in let sigma_fp' = sigma_dfs_sort tenv sigma_fp in let p' = set p ~sigma:sigma' ~sigma_fp:sigma_fp' in (* L.out "@[<2>P SORTED:@\n%a@\n@." pp_prop p'; *) - p' - + unsafe_cast_to_sorted p' -let prop_fav_add_dfs tenv fav prop = prop_fav_add fav (prop_dfs_sort tenv prop) let rec strexp_get_array_indices acc (se: Sil.strexp) = match se with @@ -1946,7 +1957,14 @@ let sigma_get_array_indices sigma = List.rev indices -let compute_reindexing fav_add get_id_offset list = +let compute_reindexing_from_indices list = + let get_id_offset (e: Exp.t) = + match e with + | BinOp (PlusA, Var id, Const Cint offset) -> + if Ident.is_primed id then Some (id, offset) else None + | _ -> + None + in let rec select list_passed list_seen = function | [] -> list_passed @@ -1957,10 +1975,9 @@ let compute_reindexing fav_add get_id_offset list = | None -> list_passed | Some (id, _) -> - let fav = Sil.fav_new () in - List.iter ~f:(fav_add fav) list_seen ; - List.iter ~f:(fav_add fav) list_passed ; - if Sil.fav_exists fav (Ident.equal id) then list_passed else x :: list_passed + let find_id_in_list l = List.exists l ~f:(fun e -> Exp.ident_mem e id) in + if find_id_in_list list_seen || find_id_in_list list_passed then list_passed + else x :: list_passed in let list_seen_new = x :: list_seen in select list_passed_new list_seen_new list_rest @@ -1977,18 +1994,6 @@ let compute_reindexing fav_add get_id_offset list = Sil.exp_subst_of_list reindexing -let compute_reindexing_from_indices indices = - let get_id_offset (e: Exp.t) = - match e with - | BinOp (PlusA, Var id, Const Cint offset) -> - if Ident.is_primed id then Some (id, offset) else None - | _ -> - None - in - let fav_add = Sil.exp_fav_add in - compute_reindexing fav_add get_id_offset indices - - let apply_reindexing tenv (exp_subst: Sil.exp_subst) prop = let subst = `Exp exp_subst in let nsigma = Normalize.sigma_normalize tenv subst prop.sigma in @@ -1997,7 +2002,7 @@ let apply_reindexing tenv (exp_subst: Sil.exp_subst) prop = let dom_subst = List.map ~f:fst (Sil.sub_to_list exp_subst) in let in_dom_subst id = List.exists ~f:(Ident.equal id) dom_subst in let sub' = Sil.sub_filter (fun id -> not (in_dom_subst id)) prop.sub in - let contains_substituted_id e = Sil.fav_exists (Sil.exp_fav e) in_dom_subst in + let contains_substituted_id e = Exp.free_vars e |> Sequence.exists ~f:in_dom_subst in let sub_eqs, sub_keep = Sil.sub_range_partition contains_substituted_id sub' in let eqs = Sil.sub_to_list sub_eqs in let atoms = @@ -2034,9 +2039,8 @@ let prop_rename_array_indices tenv prop = apply_reindexing tenv subst prop -let compute_renaming fav = - let ids = Sil.fav_to_list fav in - let ids_primed, ids_nonprimed = List.partition_tf ~f:Ident.is_primed ids in +let compute_renaming free_vars = + let ids_primed, ids_nonprimed = List.partition_tf ~f:Ident.is_primed free_vars in let ids_footprint = List.filter ~f:Ident.is_footprint ids_nonprimed in let id_base_primed = Ident.create Ident.kprimed 0 in let id_base_footprint = Ident.create Ident.kfootprint 0 in @@ -2149,7 +2153,9 @@ and hpred_captured_ren ren (hpred: Sil.hpred) : Sil.hpred = and hpara_ren (para: Sil.hpara) : Sil.hpara = - let av = Sil.hpara_shallow_av para in + let av = + Sil.hpara_shallow_free_vars para |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys + in let ren = compute_renaming av in let root = ident_captured_ren ren para.root in let next = ident_captured_ren ren para.next in @@ -2160,7 +2166,9 @@ and hpara_ren (para: Sil.hpara) : Sil.hpara = and hpara_dll_ren (para: Sil.hpara_dll) : Sil.hpara_dll = - let av = Sil.hpara_dll_shallow_av para in + let av = + Sil.hpara_dll_shallow_free_vars para |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys + in let ren = compute_renaming av in let iF = ident_captured_ren ren para.cell in let oF = ident_captured_ren ren para.flink in @@ -2182,10 +2190,8 @@ let prop_rename_primed_footprint_vars tenv (p: normal t) : normal t = let p = prop_rename_array_indices tenv p in let bound_vars = let filter id = Ident.is_footprint id || Ident.is_primed id in - let p_dfs = prop_dfs_sort tenv p in - let fvars_in_p = prop_fav p_dfs in - Sil.fav_filter_ident fvars_in_p filter ; - fvars_in_p + dfs_sort tenv p |> sorted_free_vars |> Sequence.filter ~f:filter |> Ident.hashqueue_of_sequence + |> Ident.HashQueue.keys in let ren = compute_renaming bound_vars in let sub' = sub_captured_ren ren p.sub in @@ -2206,8 +2212,6 @@ let prop_rename_primed_footprint_vars tenv (p: normal t) : normal t = unsafe_cast_to_normal p' -let expose (p: normal t) : exposed t = Obj.magic p - (** Apply subsitution to prop. *) let prop_sub subst (prop: 'a t) : exposed t = let pi = pi_sub subst (prop.pi @ pi_of_subst prop.sub) in @@ -2222,11 +2226,10 @@ let prop_ren_sub tenv (ren_sub: Sil.exp_subst) (prop: normal t) : normal t = Normalize.normalize tenv (prop_sub (`Exp ren_sub) prop) -(** Existentially quantify the [fav] in [prop]. - [fav] should not contain any primed variables. *) -let exist_quantify tenv fav (prop: normal t) : normal t = - let ids = Sil.fav_to_list fav in - if List.exists ~f:Ident.is_primed ids then assert false ; +(** Existentially quantify the [ids] in [prop]. [ids] should not contain any primed variables. If + [ids_queue] is passed then the function uses it instead of [ids] for membership tests. *) +let exist_quantify tenv ?ids_queue ids (prop: normal t) : normal t = + assert (not (List.exists ~f:Ident.is_primed ids)) ; (* sanity check *) if List.is_empty ids then prop else @@ -2234,8 +2237,15 @@ let exist_quantify tenv fav (prop: normal t) : normal t = let ren_sub = Sil.exp_subst_of_list (List.map ~f:gen_fresh_id_sub ids) in let prop' = (* throw away x=E if x becomes x_ *) - let mem_idlist i = List.exists ~f:(fun id -> Ident.equal i id) in - let sub = Sil.sub_filter (fun i -> not (mem_idlist i ids)) prop.sub in + let filter = + match ids_queue with + | Some q -> + (* this is more efficient than a linear scan of [ids] *) + fun id -> not (Ident.HashQueue.mem q id) + | None -> + fun id -> not (List.mem ~equal:Ident.equal ids id) + in + let sub = Sil.sub_filter filter prop.sub in if Sil.equal_exp_subst sub prop.sub then prop else unsafe_cast_to_normal (set prop ~sub) in (* @@ -2257,9 +2267,20 @@ let prop_expmap (fe: Exp.t -> Exp.t) prop = set prop ~pi ~sigma ~pi_fp ~sigma_fp -(** convert identifiers in fav to kind [k] *) -let vars_make_unprimed tenv fav prop = - let ids = Sil.fav_to_list fav in +(** convert the normal vars to primed vars *) +let prop_normal_vars_to_primed_vars tenv p = + let ids_queue = + free_vars p |> Sequence.filter ~f:Ident.is_normal |> Ident.hashqueue_of_sequence + in + exist_quantify tenv ~ids_queue (Ident.HashQueue.keys ids_queue) p + + +(** convert the primed vars to normal vars. *) +let prop_primed_vars_to_normal_vars tenv (prop: normal t) : normal t = + let ids = + free_vars prop |> Sequence.filter ~f:Ident.is_primed |> Ident.hashqueue_of_sequence + |> Ident.HashQueue.keys + in let ren_sub = Sil.exp_subst_of_list (List.map ~f:(fun i -> (i, Exp.Var (Ident.create_fresh Ident.knormal))) ids) @@ -2267,20 +2288,6 @@ let vars_make_unprimed tenv fav prop = prop_ren_sub tenv ren_sub prop -(** convert the normal vars to primed vars. *) -let prop_normal_vars_to_primed_vars tenv p = - let fav = prop_fav p in - Sil.fav_filter_ident fav Ident.is_normal ; - exist_quantify tenv fav p - - -(** convert the primed vars to normal vars. *) -let prop_primed_vars_to_normal_vars tenv (p: normal t) : normal t = - let fav = prop_fav p in - Sil.fav_filter_ident fav Ident.is_primed ; - vars_make_unprimed tenv fav p - - let from_pi pi = set prop_emp ~pi let from_sigma sigma = set prop_emp ~sigma @@ -2412,7 +2419,7 @@ let prop_iter_make_id_primed tenv id iter = (List.rev pairs_unpid, List.rev pairs_pid) | (eq :: eqs_cur: pi) -> match eq with - | Aeq (Var id1, e1) when Sil.ident_in_exp id1 e1 -> + | Aeq (Var id1, e1) when Exp.ident_mem e1 id1 -> L.internal_error "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n" ; L.internal_error "Broken Assumption: id notin e for all (id,e) in sub@\n" ; L.internal_error "(id,e) : (%a,%a)@\n" Ident.pp id1 Exp.pp e1 ; @@ -2457,28 +2464,32 @@ let prop_iter_make_id_primed tenv id iter = ; pit_new= sigma_sub sub_use iter.pit_new } -let prop_iter_footprint_fav_add fav iter = - sigma_fav_add fav iter.pit_sigma_fp ; - pi_fav_add fav iter.pit_pi_fp - - (** Find fav of the footprint part of the iterator *) -let prop_iter_footprint_fav iter = - Sil.fav_imperative_to_functional prop_iter_footprint_fav_add iter +let prop_iter_footprint_gen_free_vars {pit_sigma_fp; pit_pi_fp} = + Sequence.Generator.(sigma_gen_free_vars pit_sigma_fp >>= fun () -> pi_gen_free_vars pit_pi_fp) -let prop_iter_fav_add fav iter = - Sil.sub_fav_add fav iter.pit_sub ; - pi_fav_add fav iter.pit_pi ; - pi_fav_add fav (List.map ~f:snd iter.pit_newpi) ; - sigma_fav_add fav iter.pit_old ; - sigma_fav_add fav iter.pit_new ; - Sil.hpred_fav_add fav iter.pit_curr ; - prop_iter_footprint_fav_add fav iter +let prop_iter_footprint_free_vars iter = + Sequence.Generator.run (prop_iter_footprint_gen_free_vars iter) (** Find fav of the iterator *) -let prop_iter_fav iter = Sil.fav_imperative_to_functional prop_iter_fav_add iter +let prop_iter_gen_free_vars ({pit_sub; pit_pi; pit_newpi; pit_old; pit_new; pit_curr} as iter) = + let open Sequence.Generator in + Sil.exp_subst_gen_free_vars pit_sub + >>= fun () -> + pi_gen_free_vars pit_pi + >>= fun () -> + pi_gen_free_vars (List.map ~f:snd pit_newpi) + >>= fun () -> + sigma_gen_free_vars pit_old + >>= fun () -> + sigma_gen_free_vars pit_new + >>= fun () -> + Sil.hpred_gen_free_vars pit_curr >>= fun () -> prop_iter_footprint_gen_free_vars iter + + +let prop_iter_free_vars iter = Sequence.Generator.run (prop_iter_gen_free_vars iter) (** Extract the sigma part of the footprint *) let prop_iter_get_footprint_sigma iter = iter.pit_sigma_fp diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 25123b750..1d10dccfb 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -20,6 +20,9 @@ type normal (** kind for exposed props *) type exposed +(** kind for sorted props *) +type sorted + (** Proposition. *) type pi = Sil.atom list @@ -93,33 +96,21 @@ val pp_proplist_with_typ : Pp.env -> Format.formatter -> normal t list -> unit val d_proplist_with_typ : 'a t list -> unit -val pi_fav : atom list -> fav -(** Compute free non-program variables of pi *) - -val pi_fav_add : fav -> atom list -> unit - -val sigma_fav_add : fav -> hpred list -> unit -(** Compute free non-program variables of sigma *) +val pi_free_vars : pi -> Ident.t Sequence.t -val sigma_fav : hpred list -> fav +val sigma_free_vars : sigma -> Ident.t Sequence.t -val sigma_fav_in_pvars_add : fav -> hpred list -> unit -(** returns free non-program variables that are used to express - the contents of stack variables *) +val free_vars : normal t -> Ident.t Sequence.t -val prop_fav_add : fav -> 'a t -> unit -(** Compute free non-program variables of prop *) +val gen_free_vars : normal t -> (unit, Ident.t) Sequence.Generator.t -val prop_fav_add_dfs : Tenv.t -> fav -> 'a t -> unit -(** Compute free non-program variables of prop, visited in depth first order *) +val footprint_free_vars : normal t -> Ident.t Sequence.t -val prop_fav : normal t -> fav +val sorted_gen_free_vars : sorted t -> (unit, Ident.t) Sequence.Generator.t -val prop_fav_nonpure : normal t -> fav -(** free vars, except pi and sub, of current and footprint parts *) +val non_pure_free_vars : normal t -> Ident.t Sequence.t -val prop_footprint_fav : 'a t -> fav -(** Find fav of the footprint part of the prop *) +val dfs_sort : Tenv.t -> normal t -> sorted t val pi_sub : subst -> atom list -> atom list (** Apply substitution for pi *) @@ -266,7 +257,8 @@ val prop_expand : Tenv.t -> normal t -> normal t list (** {2 Functions for existentially quantifying and unquantifying variables} *) -val exist_quantify : Tenv.t -> fav -> normal t -> normal t +val exist_quantify : + Tenv.t -> ?ids_queue:unit Ident.HashQueue.t -> Ident.t list -> normal t -> normal t (** Existentially quantify the [ids] in [prop]. *) val prop_normal_vars_to_primed_vars : Tenv.t -> normal t -> normal t @@ -317,10 +309,10 @@ val prop_iter_update_current : 'a prop_iter -> hpred -> 'a prop_iter val prop_iter_prev_then_insert : 'a prop_iter -> hpred -> 'a prop_iter (** Insert before the current element of the iterator. *) -val prop_iter_footprint_fav : 'a prop_iter -> fav +val prop_iter_footprint_free_vars : 'a prop_iter -> Ident.t Sequence.t (** Find fav of the footprint part of the iterator *) -val prop_iter_fav : 'a prop_iter -> fav +val prop_iter_free_vars : 'a prop_iter -> Ident.t Sequence.t (** Find fav of the iterator *) val prop_iter_get_footprint_sigma : 'a prop_iter -> hpred list diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 0b8c87775..03c0a8021 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1127,7 +1127,7 @@ end = struct let implication_rhs = ref (Prop.expose Prop.prop_emp) - let fav_in_array_len = ref (Sil.fav_new ()) + let fav_in_array_len = ref Ident.Set.empty (* free variables in array len position *) let bounds_checks = ref [] @@ -1149,15 +1149,13 @@ end = struct (** free vars in array len position in current strexp part of prop *) let prop_fav_len prop = - let fav = Sil.fav_new () in - let do_hpred = function + let do_hpred fav = function | Sil.Hpointsto (_, Sil.Earray ((Exp.Var _ as len), _, _), _) -> - Sil.exp_fav_add fav len + Exp.free_vars len |> Ident.set_of_sequence ~init:fav | _ -> - () + fav in - List.iter ~f:do_hpred prop.Prop.sigma ; - fav + List.fold_left ~init:Ident.Set.empty ~f:do_hpred prop.Prop.sigma let reset lhs rhs = @@ -1191,8 +1189,8 @@ end = struct (** atom considered array bounds check if it contains vars present in array length position in the pre *) let atom_is_array_bounds_check atom = - let fav_a = Sil.atom_fav atom in - Prop.atom_is_inequality atom && Sil.fav_exists fav_a (fun a -> Sil.fav_mem !fav_in_array_len a) + Prop.atom_is_inequality atom + && Sil.atom_free_vars atom |> Sequence.exists ~f:(fun id -> Ident.Set.mem id !fav_in_array_len) let get_bounds_checks () = !bounds_checks @@ -1368,10 +1366,8 @@ let exp_imply tenv calc_missing (subs: subst2) e1_in e2_in : subst2 = | e1, Exp.Var v2 -> let occurs_check v e = (* check whether [v] occurs in normalized [e] *) - if Sil.fav_mem (Sil.exp_fav e) v - && Sil.fav_mem - (Sil.exp_fav (Prop.exp_normalize_prop ~destructive:true tenv Prop.prop_emp e)) - v + if Exp.ident_mem e v + && Exp.ident_mem (Prop.exp_normalize_prop ~destructive:true tenv Prop.prop_emp e) v then raise (IMPL_EXC ("occurs check", subs, EXC_FALSE_EXPS (e1, e2))) in if Ident.is_primed v2 then @@ -1723,7 +1719,7 @@ let hpred_has_primed_lhs sub hpred = | Exp.BinOp (Binop.PlusPI, e1, _) -> find_primed e1 | _ -> - Sil.fav_exists (Sil.exp_fav e) Ident.is_primed + Exp.free_vars e |> Sequence.exists ~f:Ident.is_primed in let exp_has_primed e = find_primed (Sil.exp_sub sub e) in match hpred with @@ -2565,7 +2561,9 @@ let check_array_bounds tenv (sub1, sub2) prop = let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 = try ProverState.reset prop1 prop2 ; - let filter (id, e) = Ident.is_normal id && Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in + let filter (id, e) = + Ident.is_normal id && Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal + in let sub1_base = Sil.sub_filter_pair ~f:filter prop1.Prop.sub in let pi1, pi2 = (Prop.get_pure prop1, Prop.get_pure prop2) in let sigma1, sigma2 = (prop1.Prop.sigma, prop2.Prop.sigma) in diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index e754e854d..b8e19fc7d 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -379,11 +379,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp handle_case [] [] array_cont -let exp_has_only_footprint_ids e = - let fav = Sil.exp_fav e in - Sil.fav_filter_ident fav (fun id -> not (Ident.is_footprint id)) ; - Sil.fav_is_empty fav - +let exp_has_only_footprint_ids e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_footprint let laundry_offset_for_footprint max_stamp offs_in = let rec laundry offs_seen eqs offs = @@ -543,12 +539,7 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp = check_offset se offset -let fav_max_stamp fav = - let max_stamp = ref 0 in - let f id = max_stamp := max !max_stamp (Ident.get_stamp id) in - List.iter ~f (Sil.fav_to_list fav) ; - max_stamp - +let id_max_stamp curr_max id = max curr_max (Ident.get_stamp id) (** [prop_iter_extend_ptsto iter lexp] extends the current psto predicate in [iter] with enough fields to follow the path in @@ -560,12 +551,11 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = Sil.d_exp lexp ; L.d_ln () ) ; let offset = Sil.exp_get_offsets lexp in - let max_stamp = fav_max_stamp (Prop.prop_iter_fav iter) in - let max_stamp_val = !max_stamp in + let max_stamp = Prop.prop_iter_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp in let extend_footprint_pred = function | Sil.Hpointsto (e, se, te) -> let atoms_se_te_list = - strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp_val) se te + strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp) se te offset inst in List.map @@ -575,8 +565,8 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = match hpara.Sil.body with | (Sil.Hpointsto (e', se', te')) :: body_rest -> let atoms_se_te_list = - strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp_val) se' - te' offset inst + strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp) se' te' + offset inst in let atoms_body_list = List.map @@ -624,7 +614,8 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = in let iter_list = let atoms_se_te_list = - strexp_extend_values pname tenv orig_prop false extend_kind max_stamp se te offset inst + strexp_extend_values pname tenv orig_prop false extend_kind (ref max_stamp) se te offset + inst in List.map ~f:(atoms_se_te_to_iter e) atoms_se_te_list in @@ -702,9 +693,9 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = that [root(lexp): typ] is the current hpred of the iterator. typ is the type of the root of lexp. *) let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst = - let max_stamp = fav_max_stamp (Prop.prop_footprint_fav prop) in + let max_stamp = Prop.footprint_free_vars prop |> Sequence.fold ~init:0 ~f:id_max_stamp in let ptsto, ptsto_foot, atoms = - mk_ptsto_exp_footprint pname tenv prop (lexp, typ) max_stamp inst + mk_ptsto_exp_footprint pname tenv prop (lexp, typ) (ref max_stamp) inst in L.d_strln "++++ Adding footprint frame" ; Prop.d_prop (Prop.prop_hpred_star Prop.prop_emp ptsto) ; @@ -1068,9 +1059,11 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst = L.d_str "typ:" ; Typ.d_full typ ; L.d_ln () ) ; - let max_stamp = fav_max_stamp (Prop.prop_iter_footprint_fav iter) in + let max_stamp = + Prop.prop_iter_footprint_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp + in let ptsto, ptsto_foot, atoms = - mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst + mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) (ref max_stamp) inst in L.d_strln "++++ Adding footprint frame" ; Prop.d_prop (Prop.prop_hpred_star Prop.prop_emp ptsto) ; @@ -1147,10 +1140,10 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = check_field_splitting () ; match Prop.prop_iter_current tenv iter with | Sil.Hpointsto (e, se, te), offset -> - let max_stamp = fav_max_stamp (Prop.prop_iter_fav iter) in + let max_stamp = Prop.prop_iter_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp in let atoms_se_te_list = - strexp_extend_values pname tenv orig_prop false Ident.kprimed max_stamp se te offset - inst + strexp_extend_values pname tenv orig_prop false Ident.kprimed (ref max_stamp) se te + offset inst in let handle_case (atoms', se', te') = let iter' = diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 16fc4b7a7..c31423df5 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -40,11 +40,14 @@ module Jprop = struct let to_prop = function Prop (_, p) -> p | Joined (_, p, _, _) -> p - let rec fav_add_dfs tenv fav = function - | Prop (_, p) -> - Prop.prop_fav_add_dfs tenv fav p - | Joined (_, p, jp1, jp2) -> - Prop.prop_fav_add_dfs tenv fav p ; fav_add_dfs tenv fav jp1 ; fav_add_dfs tenv fav jp2 + let rec sorted_gen_free_vars tenv = + let open Sequence.Generator in + function + | Prop (_, p) -> + Prop.dfs_sort tenv p |> Prop.sorted_gen_free_vars + | Joined (_, p, jp1, jp2) -> + Prop.dfs_sort tenv p |> Prop.sorted_gen_free_vars + >>= fun () -> sorted_gen_free_vars tenv jp1 >>= fun () -> sorted_gen_free_vars tenv jp2 let rec normalize tenv = function @@ -94,13 +97,17 @@ module Jprop = struct L.add_print_action (L.PTjprop_list, Obj.repr (shallow, jplist)) - let rec fav_add fav = function - | Prop (_, p) -> - Prop.prop_fav_add fav p - | Joined (_, p, jp1, jp2) -> - Prop.prop_fav_add fav p ; fav_add fav jp1 ; fav_add fav jp2 + let rec gen_free_vars = + let open Sequence.Generator in + function + | Prop (_, p) -> + Prop.gen_free_vars p + | Joined (_, p, jp1, jp2) -> + Prop.gen_free_vars p >>= fun () -> gen_free_vars jp1 >>= fun () -> gen_free_vars jp2 + let free_vars jp = Sequence.Generator.run (gen_free_vars jp) + let rec jprop_sub sub = function | Prop (n, p) -> Prop (n, Prop.prop_sub sub p) @@ -190,12 +197,15 @@ end = struct let tospecs specs = specs - let spec_fav tenv (spec: Prop.normal spec) : Sil.fav = - let fav = Sil.fav_new () in - Jprop.fav_add_dfs tenv fav spec.pre ; - List.iter ~f:(fun (p, _) -> Prop.prop_fav_add_dfs tenv fav p) spec.posts ; - fav + let gen_free_vars tenv (spec: Prop.normal spec) = + let open Sequence.Generator in + Jprop.sorted_gen_free_vars tenv spec.pre + >>= fun () -> + ISequence.gen_sequence_list spec.posts ~f:(fun (p, _) -> + Prop.dfs_sort tenv p |> Prop.sorted_gen_free_vars ) + + let free_vars tenv spec = Sequence.Generator.run (gen_free_vars tenv spec) let spec_sub tenv sub spec = { pre= Jprop.normalize tenv (Jprop.jprop_sub sub spec.pre) @@ -206,8 +216,7 @@ end = struct (** Convert spec into normal form w.r.t. variable renaming *) let normalize tenv (spec: Prop.normal spec) : Prop.normal spec = - let fav = spec_fav tenv spec in - let idlist = Sil.fav_to_list fav in + let idlist = free_vars tenv spec |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in let count = ref 0 in let sub = Sil.subst_of_list diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index a83ae8cf9..9c45539f1 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -31,8 +31,7 @@ module Jprop : sig val d_list : bool -> Prop.normal t list -> unit (** dump a joined prop list, the boolean indicates whether to print toplevel props only *) - val fav_add : Sil.fav -> 'a t -> unit - (** Add fav to a jprop *) + val free_vars : Prop.normal t -> Ident.t Sequence.t val filter : ('a t -> 'b option) -> 'a t list -> 'b list (** [jprop_filter filter joinedprops] applies [filter] to the elements diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index 8ba2a82a4..4115c8f4a 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -250,8 +250,7 @@ let get_prop_tenv_pdesc () = !gs.last_prop_tenv_pdesc (** extract the footprint of the prop, and turn it into a normalized precondition using spec variables *) let extract_pre p tenv pdesc abstract_fun = let sub = - let fav = Prop.prop_fav p in - let idlist = Sil.fav_to_list fav in + let idlist = Prop.free_vars p |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in let count = ref 0 in Sil.subst_of_list (List.map diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index f44256e5f..ee9dc2e24 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1346,7 +1346,7 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path [ Abs.remove_redundant_array_elements current_pname tenv (Abs.abstract current_pname tenv prop_) ] | Sil.Remove_temps (temps, _) -> - ret_old_path [Prop.exist_quantify tenv (Sil.fav_from_list temps) prop_] + ret_old_path [Prop.exist_quantify tenv temps prop_] | Sil.Declare_locals (ptl, _) -> let sigma_locals = let add_None (x, typ) = @@ -1742,9 +1742,10 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let prop_primed_to_normal p = (* Rename primed vars with fresh normal vars, and return them *) - let fav = Prop.prop_fav p in - Sil.fav_filter_ident fav Ident.is_primed ; - let ids_primed = Sil.fav_to_list fav in + let ids_primed = + Prop.free_vars p |> Sequence.filter ~f:Ident.is_primed |> Ident.hashqueue_of_sequence + |> Ident.HashQueue.keys + in let ids_primed_normal = List.map ~f:(fun id -> (id, Ident.create_fresh Ident.knormal)) ids_primed in @@ -1752,18 +1753,16 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t), Sil.subst_of_list (List.map ~f:(fun (id1, id2) -> (id1, Exp.Var id2)) ids_primed_normal) in let p' = Prop.normalize tenv (Prop.prop_sub ren_sub p) in - let fav_normal = Sil.fav_from_list (List.map ~f:snd ids_primed_normal) in + let fav_normal = List.map ~f:snd ids_primed_normal in (p', fav_normal) in let prop_normal_to_primed fav_normal p = (* rename given normal vars to fresh primed *) - if List.is_empty (Sil.fav_to_list fav_normal) then p else Prop.exist_quantify tenv fav_normal p + if List.is_empty fav_normal then p else Prop.exist_quantify tenv fav_normal p in try let pre_process_prop p = - let p', fav = - if Sil.instr_is_auxiliary instr then (p, Sil.fav_new ()) else prop_primed_to_normal p - in + let p', fav = if Sil.instr_is_auxiliary instr then (p, []) else prop_primed_to_normal p in let p'' = let map_res_action e ra = (* update the vpath in resource attributes *) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 5b449b204..59f751df0 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -110,10 +110,12 @@ let spec_rename_vars pname spec = | Specs.Jprop.Joined (n, p, jp1, jp2) -> Specs.Jprop.Joined (n, prop_add_callee_suffix p, jp1, jp2) in - let fav = Sil.fav_new () in - Specs.Jprop.fav_add fav spec.Specs.pre ; - List.iter ~f:(fun (p, _) -> Prop.prop_fav_add fav p) spec.Specs.posts ; - let ids = Sil.fav_to_list fav in + let fav = + let fav = Specs.Jprop.free_vars spec.Specs.pre |> Ident.hashqueue_of_sequence in + List.fold_left spec.Specs.posts ~init:fav ~f:(fun fav (p, _) -> + Prop.free_vars p |> Ident.hashqueue_of_sequence ~init:fav ) + in + let ids = Ident.HashQueue.keys fav in let ids' = List.map ~f:(fun i -> (i, Ident.create_fresh Ident.kprimed)) ids in let ren_sub = Sil.subst_of_list (List.map ~f:(fun (i, i') -> (i, Exp.Var i')) ids') in let pre' = Specs.Jprop.jprop_sub ren_sub spec.Specs.pre in @@ -154,9 +156,7 @@ let spec_find_rename trace_call summary : (int * Prop.exposed Specs.spec) list * let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_fld missing_fld frame_typ missing_typ = let hpred_has_only_footprint_vars hpred = - let fav = Sil.fav_new () in - Sil.hpred_fav_add fav hpred ; - Sil.fav_for_all fav Ident.is_footprint + Sil.hpred_free_vars hpred |> Sequence.for_all ~f:Ident.is_footprint in let sub = Sil.sub_join sub1 sub2 in let sub1_inverse = @@ -168,28 +168,29 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_ Sil.exp_subst_of_list_duplicates sub1_inverse_list in let fav_actual_pre = - let fav_sub2 = - (* vars which represent expansions of fields *) - let fav = Sil.fav_new () in - List.iter ~f:(Sil.exp_fav_add fav) (Sil.sub_range sub2) ; - let filter id = Int.equal (Ident.get_stamp id) (-1) in - Sil.fav_filter_ident fav filter ; fav - in - let fav_pre = Prop.prop_fav actual_pre in - Sil.ident_list_fav_add (Sil.fav_to_list fav_sub2) fav_pre ; - fav_pre + let fav_pre = Prop.free_vars actual_pre |> Ident.hashqueue_of_sequence in + let filter id = Int.equal (Ident.get_stamp id) (-1) in + (* vars which represent expansions of fields *) + Sil.sub_range sub2 + |> List.fold_left ~init:fav_pre ~f:(fun res e -> + Exp.free_vars e |> Sequence.filter ~f:filter |> Ident.hashqueue_of_sequence ~init:res ) in - let fav_missing = Prop.sigma_fav (Prop.sigma_sub (`Exp sub) missing_sigma) in - Prop.pi_fav_add fav_missing (Prop.pi_sub (`Exp sub) missing_pi) ; let fav_missing_primed = - let filter id = Ident.is_primed id && not (Sil.fav_mem fav_actual_pre id) in - Sil.fav_copy_filter_ident fav_missing filter + let filter id = Ident.is_primed id && not (Ident.HashQueue.mem fav_actual_pre id) in + let fav = + Prop.sigma_sub (`Exp sub) missing_sigma |> Prop.sigma_free_vars |> Sequence.filter ~f:filter + |> Ident.hashqueue_of_sequence + in + Prop.pi_sub (`Exp sub) missing_pi |> Prop.pi_free_vars |> Sequence.filter ~f:filter + |> Ident.hashqueue_of_sequence ~init:fav |> Ident.HashQueue.keys + in + let fav_missing_fld = + Prop.sigma_sub (`Exp sub) missing_fld |> Prop.sigma_free_vars |> Ident.hashqueue_of_sequence in - let fav_missing_fld = Prop.sigma_fav (Prop.sigma_sub (`Exp sub) missing_fld) in let map_var_to_pre_var_or_fresh id = match Sil.exp_sub (`Exp sub1_inverse) (Exp.Var id) with | Exp.Var id' -> - if Sil.fav_mem fav_actual_pre id' || Ident.is_path id' + if Ident.HashQueue.mem fav_actual_pre id' || Ident.is_path id' (* a path id represents a position in the pre *) then Exp.Var id' else Exp.Var (Ident.create_fresh Ident.kprimed) @@ -197,16 +198,11 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_ assert false in let sub_list = Sil.sub_to_list sub in - let fav_sub_list = - let fav_sub = Sil.fav_new () in - List.iter ~f:(fun (_, e) -> Sil.exp_fav_add fav_sub e) sub_list ; - Sil.fav_to_list fav_sub - in let sub1 = let f id = - if Sil.fav_mem fav_actual_pre id then (id, Exp.Var id) + if Ident.HashQueue.mem fav_actual_pre id then (id, Exp.Var id) else if Ident.is_normal id then (id, map_var_to_pre_var_or_fresh id) - else if Sil.fav_mem fav_missing_fld id then (id, Exp.Var id) + else if Ident.HashQueue.mem fav_missing_fld id then (id, Exp.Var id) else if Ident.is_footprint id then (id, Exp.Var id) else let dom1 = Sil.sub_domain sub1 in @@ -214,7 +210,7 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_ let dom2 = Sil.sub_domain sub2 in let rng2 = Sil.sub_range sub2 in let vars_actual_pre = - List.map ~f:(fun id -> Exp.Var id) (Sil.fav_to_list fav_actual_pre) + List.map ~f:(fun id -> Exp.Var id) (Ident.HashQueue.keys fav_actual_pre) in L.d_str "fav_actual_pre: " ; Sil.d_exp_list vars_actual_pre ; @@ -236,11 +232,16 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_ L.d_ln () ; assert false in + let fav_sub_list = + List.fold_left sub_list ~init:(Ident.HashQueue.create ()) ~f:(fun fav (_, e) -> + Exp.free_vars e |> Ident.hashqueue_of_sequence ~init:fav ) + |> Ident.HashQueue.keys + in Sil.subst_of_list (List.map ~f fav_sub_list) in let sub2_list = let f id = (id, Exp.Var (Ident.create_fresh Ident.kfootprint)) in - List.map ~f (Sil.fav_to_list fav_missing_primed) + List.map ~f fav_missing_primed in let sub_list' = List.map ~f:(fun (id, e) -> (id, Sil.exp_sub sub1 e)) sub_list in let sub' = Sil.subst_of_list (sub2_list @ sub_list') in @@ -683,8 +684,7 @@ let prop_footprint_add_pi_sigma_starfld_sigma tenv (prop: 'a Prop.t) pi_new sigm | [] -> current_pi | a :: new_pi' -> - let fav = Prop.pi_fav [a] in - if Sil.fav_exists fav (fun id -> not (Ident.is_footprint id)) then ( + if Sil.atom_free_vars a |> Sequence.exists ~f:(fun id -> not (Ident.is_footprint id)) then ( L.d_warning "dropping atom with non-footprint variable" ; L.d_ln () ; Sil.d_atom a ; @@ -1187,18 +1187,17 @@ let remove_constant_string_class tenv prop = and remove pointsto's whose lhs is a constant string *) let quantify_path_idents_remove_constant_strings tenv (prop: Prop.normal Prop.t) : Prop.normal Prop.t = - let fav = Prop.prop_fav prop in - Sil.fav_filter_ident fav Ident.is_path ; - remove_constant_string_class tenv (Prop.exist_quantify tenv fav prop) + let ids_queue = + Prop.free_vars prop |> Sequence.filter ~f:Ident.is_path |> Ident.hashqueue_of_sequence + in + let ids_list = Ident.HashQueue.keys ids_queue in + remove_constant_string_class tenv (Prop.exist_quantify tenv ~ids_queue ids_list prop) (** Strengthen the footprint by adding pure facts from the current part *) let prop_pure_to_footprint tenv (p: 'a Prop.t) : Prop.normal Prop.t = let is_footprint_atom_not_attribute a = - not (Attribute.is_pred a) - && - let a_fav = Sil.atom_fav a in - Sil.fav_for_all a_fav Ident.is_footprint + not (Attribute.is_pred a) && Sil.atom_free_vars a |> Sequence.for_all ~f:Ident.is_footprint in let pure = Prop.get_pure p in let new_footprint_atoms = List.filter ~f:is_footprint_atom_not_attribute pure in diff --git a/infer/src/base/ISequence.ml b/infer/src/base/ISequence.ml new file mode 100644 index 000000000..59ee91ffe --- /dev/null +++ b/infer/src/base/ISequence.ml @@ -0,0 +1,14 @@ +(* + * Copyright (c) 2018 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd + +let rec gen_sequence_list ~f = + let open Sequence.Generator in + function [] -> return () | x :: tl -> f x >>= fun () -> gen_sequence_list ~f tl diff --git a/infer/src/base/ISequence.mli b/infer/src/base/ISequence.mli new file mode 100644 index 000000000..85fac26fb --- /dev/null +++ b/infer/src/base/ISequence.mli @@ -0,0 +1,15 @@ +(* + * Copyright (c) 2018 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd + +(** Utility functions for sequences *) + +val gen_sequence_list : + f:('a -> (unit, 'b) Sequence.Generator.t) -> 'a list -> (unit, 'b) Sequence.Generator.t diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml index 5f5d0dd5b..3aa4d1c0c 100644 --- a/infer/src/istd/IList.ml +++ b/infer/src/istd/IList.ml @@ -65,20 +65,6 @@ let rec merge_sorted_nodup compare res xs1 xs2 = else merge_sorted_nodup compare (x2 :: res) xs1 xs2' -let intersect compare l1 l2 = - let l1_sorted = List.sort compare l1 in - let l2_sorted = List.sort compare l2 in - let rec f l1 l2 = - match (l1, l2) with - | [], _ | _, [] -> - false - | x1 :: l1', x2 :: l2' -> - let x_comparison = compare x1 x2 in - if x_comparison = 0 then true else if x_comparison < 0 then f l1' l2 else f l1 l2' - in - f l1_sorted l2_sorted - - let inter compare xs ys = let rev_sort xs = List.sort (fun x y -> compare y x) xs in let rev_xs = rev_sort xs in diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli index 0f421d564..3871292a9 100644 --- a/infer/src/istd/IList.mli +++ b/infer/src/istd/IList.mli @@ -19,10 +19,6 @@ val remove_irrelevant_duplicates : ('a -> 'a -> int) -> ('a -> bool) -> 'a list val merge_sorted_nodup : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list -> 'a list (** The function works on sorted lists without duplicates *) -val intersect : ('a -> 'a -> int) -> 'a list -> 'a list -> bool -(** Returns whether there is an intersection in the elements of the two lists. - The compare function is required to sort the lists. *) - val inter : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list (** [inter cmp xs ys] are the elements in both [xs] and [ys], sorted according to [cmp]. *)