From 60000be43b9eeb056069c5ae96c211a05056a5a8 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 24 Jul 2015 11:03:43 -0600 Subject: [PATCH] [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 | 44 ++++++++++++++++++++++++++++++++++ infer/src/backend/prop.mli | 10 ++++++++ infer/src/backend/propgraph.ml | 4 +--- infer/src/backend/sil.mli | 3 --- 4 files changed, 55 insertions(+), 6 deletions(-) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 518ccf3d6..ee293adae 100644 --- a/infer/src/backend/prop.ml +++ b/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", diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 5abb7b270..cd36c2ac0 100644 --- a/infer/src/backend/prop.mli +++ b/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 diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml index f7c599737..a1b833ef8 100644 --- a/infer/src/backend/propgraph.ml +++ b/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] diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index e7663da82..937a384f8 100644 --- a/infer/src/backend/sil.mli +++ b/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 *)