[infer][backend] refactoring code for getting reachable hpred's/pure atoms from a prop

Summary: factored this functionality into prop.ml and eliminated some duplicate functionality in sil.ml/propgraph.ml

infer/src/backend/prop.ml

@@ -1517,6 +1517,50 @@ let prop_sigma_star (p : 'a t) (sigma : Sil.hpred list) : exposed t =
   let sigma' = sigma @ p.sigma in
   { p with sigma = sigma' }
 
+(** get the set of expressions on the righthand side of [hpred] *)
+let hpred_get_targets = function
+  | Sil.Hpointsto (_, rhs, _) ->
+      let rec collect_exps exps = function
+        | Sil.Eexp (Sil.Const (Sil.Cexn e), _) -> Sil.ExpSet.add e exps
+        | Sil.Eexp (e, _) -> Sil.ExpSet.add e exps
+        | Sil.Estruct (flds, _) ->
+            list_fold_left (fun exps (_, strexp) -> collect_exps exps strexp) exps flds
+        | Sil.Earray (_, elems, _) ->
+            list_fold_left (fun exps (index, strexp) -> collect_exps exps strexp) exps elems in
+      collect_exps Sil.ExpSet.empty rhs
+  | Sil.Hlseg (_, _, _, e, el) ->
+      list_fold_left (fun exps e -> Sil.ExpSet.add e exps) Sil.ExpSet.empty (e :: el)
+  | Sil.Hdllseg (_, _, _, oB, oF, iB, el) ->
+      (* only one direction supported for now *)
+      list_fold_left (fun exps e -> Sil.ExpSet.add e exps) Sil.ExpSet.empty (oB :: oF :: iB :: el)
+
+(** return the set of hpred's and exp's in [sigma] that are reachable from an expression in
+    [exps] *)
+let compute_reachable_hpreds sigma exps =
+  let rec compute_reachable_hpreds_rec sigma (reach, exps) =
+    let add_hpred_if_reachable (reach, exps) = function
+      | Sil.Hpointsto (lhs, _, _) as hpred when Sil.ExpSet.mem lhs exps->
+          let reach' = Sil.HpredSet.add hpred reach in
+          let reach_exps = hpred_get_targets hpred in
+          (reach', Sil.ExpSet.union exps reach_exps)
+      | _ -> reach, exps in
+    let reach', exps' = list_fold_left add_hpred_if_reachable (reach, exps) sigma in
+    if (Sil.HpredSet.cardinal reach) = (Sil.HpredSet.cardinal reach') then (reach, exps)
+    else compute_reachable_hpreds_rec sigma (reach', exps') in
+  compute_reachable_hpreds_rec sigma (Sil.HpredSet.empty, exps)
+
+(** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *)
+let compute_reachable_atoms pi exps =
+  let rec exp_contains = function
+    | exp when Sil.ExpSet.mem exp exps -> true
+    | Sil.UnOp (_, e, _) | Sil.Cast (_, e) | Sil.Lfield (e, _, _) -> exp_contains e
+    | Sil.BinOp (_, e0, e1) | Sil.Lindex (e0, e1) -> exp_contains e0 || exp_contains e1
+    | _ -> false in
+  list_filter
+    (function
+      | Sil.Aeq (lhs, rhs) | Sil.Aneq (lhs, rhs) -> exp_contains lhs || exp_contains rhs)
+    pi
+
 (** Eliminates all empty lsegs from sigma, and collect equalities
     The empty lsegs include
     (a) "lseg_pe para 0 e elist",

infer/src/backend/prop.mli

@@ -459,6 +459,16 @@ val prop_iter_gc_fields : unit prop_iter -> unit prop_iter
 
 val find_equal_formal_path : exp -> 'a t -> Sil.exp option
 
+(** get the set of expressions on the righthand side of [hpred] *)
+val hpred_get_targets : Sil.hpred -> Sil.ExpSet.t
+
+(** return the set of hpred's and exp's in [sigma] that are reachable from an expression in
+    [exps] *)
+val compute_reachable_hpreds : hpred list -> Sil.ExpSet.t -> Sil.HpredSet.t * Sil.ExpSet.t
+
+(** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *)
+val compute_reachable_atoms : Sil.atom list -> Sil.ExpSet.t -> Sil.atom list
+
 (** {2 Internal modules} *)
 
 module Metrics : sig

infer/src/backend/propgraph.ml

@@ -52,9 +52,7 @@ let edge_get_source = function
 
 (** Return the successor nodes of the edge *)
 let edge_get_succs = function
-  | Ehpred (Sil.Hpointsto(_, se, _)) -> Sil.strexp_get_target_exps se
-  | Ehpred (Sil.Hlseg(_, _, _, e, el)) -> e:: el
-  | Ehpred (Sil.Hdllseg(_, _, _, oB, oF, iB, elist)) -> oB:: oF:: iB:: elist (* only one direction supported for now *)
+  | Ehpred hpred -> Sil.ExpSet.elements (Prop.hpred_get_targets hpred)
   | Eatom (Sil.Aeq (_, e2)) -> [e2]
   | Eatom (Sil.Aneq (_, e2)) -> [e2]
   | Esub_entry (s, e) -> [e]

infer/src/backend/sil.mli

@@ -1359,9 +1359,6 @@ val hpara_instantiate : hpara -> exp -> exp -> exp list -> Ident.t list * hpred
     for some fresh [_zs'].*)
 val hpara_dll_instantiate : hpara_dll -> exp -> exp -> exp -> exp list -> Ident.t list * hpred list
 
-(** Return the list of expressions that could be understood as outgoing arrows from the strexp *)
-val strexp_get_target_exps : strexp -> exp list
-
 (** Iterate over all the subtypes in the type (including the type itself) *)
 val typ_iter_types : (typ -> unit) -> typ -> unit
 (** Iterate over all the types (and subtypes) in the expression *)