[IR] `Sequence`-like interface to walk over program variables in expressions

Summary:
The goal is to allocate less and generally be more efficient than handling
lists with uniqueness constraints.

Reviewed By: mbouaziz, jberdine

Differential Revision: D7098904

fbshipit-source-id: 7111f07

infer/src/IR/Exp.ml

@@ -290,3 +290,27 @@ let is_objc_block_closure = function
       Typ.Procname.is_objc_block name
   | _ ->
       false
+
+
+let rec gen_program_vars =
+  let open Sequence.Generator in
+  function
+    | Lvar name ->
+        yield name
+    | Const _ | Var _ | Sizeof {dynamic_length= None} ->
+        return ()
+    | Cast (_, e) | Exn e | Lfield (e, _, _) | Sizeof {dynamic_length= Some e} | UnOp (_, e, _) ->
+        gen_program_vars e
+    | 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
+
+
+let program_vars e = Sequence.Generator.run (gen_program_vars e)

infer/src/IR/Exp.mli

@@ -119,6 +119,9 @@ val lt : t -> t -> t
 val get_vars : t -> Ident.t list * Pvar.t list
 (** Extract the ids and pvars from an expression *)
 
+val program_vars : t -> Pvar.t Sequence.t
+(** all the program variables appearing in the expression *)
+
 val fold_captured : f:('a -> Pvar.t -> 'a) -> t -> 'a -> 'a
 (** Extract the program variables captured by this expression *)
 

infer/src/IR/Sil.ml

@@ -1013,32 +1013,6 @@ let hpred_list_get_lexps (filter: Exp.t -> bool) (hlist: hpred list) : Exp.t lis
 
 let hpred_entries hpred = hpred_get_lexp [] hpred
 
-(** {2 Functions for computing program variables} *)
-let rec exp_fpv e =
-  match (e : Exp.t) with
-  | Var _ ->
-      []
-  | Exn e ->
-      exp_fpv e
-  | Closure {captured_vars} ->
-      List.map ~f:(fun (_, pvar, _) -> pvar) captured_vars
-  | Const _ ->
-      []
-  | Cast (_, e) | UnOp (_, e, _) ->
-      exp_fpv e
-  | BinOp (_, e1, e2) ->
-      exp_fpv e1 @ exp_fpv e2
-  | Lvar name ->
-      [name]
-  | Lfield (e, _, _) ->
-      exp_fpv e
-  | Lindex (e1, e2) ->
-      exp_fpv e1 @ exp_fpv e2
-  (* TODO: Sizeof length expressions may contain variables, do not ignore them. *)
-  | Sizeof _ ->
-      []
-
-
 (** {2 Functions for computing free non-program variables} *)
 
 (** Type of free variables. These include primed, normal and footprint variables.

infer/src/IR/Sil.mli

@@ -407,10 +407,6 @@ val hpred_entries : hpred -> Exp.t list
 
 (** {2 Function for computing lexps in sigma} *)
 
-val exp_fpv : Exp.t -> Pvar.t list
-
-(** {2 Functions for computing free non-program variables} *)
-
 (** Type of free variables. These include primed, normal and footprint variables.
     We remember the order in which variables are added. *)
 type fav

infer/src/backend/abs.ml

@@ -82,8 +82,6 @@ let create_condition_ls ids_private id_base p_leftover (inst: Sil.exp_subst) =
     let sigma = p_leftover.Prop.sigma in
     (sigma_fav_list sigma, sigma_fav_in_pvars_list sigma)
   in
-  let fpv_inst_of_base = Sil.exp_fpv inst_of_base in
-  let fpv_insts_of_private_ids = List.concat_map ~f:Sil.exp_fpv insts_of_private_ids in
   (*
   let fav_inst_of_base = Sil.exp_fav_list inst_of_base in
   L.out "@[.... application of condition ....@\n@.";
@@ -91,7 +89,8 @@ let create_condition_ls ids_private id_base p_leftover (inst: Sil.exp_subst) =
   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)) && *)
-  List.is_empty fpv_inst_of_base && List.is_empty fpv_insts_of_private_ids
+  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)