From 60496f2ae4178adb8ddf967bf4bdc5153573dd1b Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 9 Aug 2016 03:37:26 -0700 Subject: [PATCH] Minor cleanup of Prop.Attributes interface Summary: The atom_get operation is essentially redundant now. Reviewed By: cristianoc Differential Revision: D3683836 fbshipit-source-id: 741cc1a --- infer/src/backend/dom.ml | 2 +- infer/src/backend/prop.ml | 16 +++++----------- infer/src/backend/prop.mli | 5 +---- infer/src/backend/tabulation.ml | 26 +++++++++++++------------- 4 files changed, 20 insertions(+), 29 deletions(-) diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 64f4bfc9e..b66a5295d 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -1642,7 +1642,7 @@ let pi_partial_join mode | None -> None | Some (a_res, a_op) -> if mode = JoinState.Pre then join_atom_check_pre p_op a_op; - if Prop.Attribute.atom_is a then join_atom_check_attribute p_op a_op; + if Prop.Attribute.is_pred a then join_atom_check_attribute p_op a_op; if not (Prover.check_atom p_op a_op) then None else begin match Prop.atom_exp_le_const a_op with diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 2656c35d4..c7e926eeb 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1776,15 +1776,11 @@ let prop_reset_inst inst_map prop = (** {2 Attributes} *) module Attribute = struct - (** Return the exp and attribute marked in the atom if any, and return None otherwise *) - let atom_get atom = - match atom with - | Sil.Apred _ | Anpred _ -> Some atom - | _ -> None - (** Check whether an atom is used to mark an attribute *) - let atom_is a = - atom_get a <> None + let is_pred atom = + match atom with + | Sil.Apred _ | Anpred _ -> true + | _ -> false (** Add an attribute associated to the argument expressions *) let add ?(footprint = false) ?(polarity = true) prop attr args = @@ -1826,9 +1822,7 @@ module Attribute = struct (** Get all the attributes of the prop *) let get_all prop = let res = ref [] in - let do_atom a = match atom_get a with - | Some attr -> res := attr :: !res - | None -> () in + let do_atom a = if is_pred a then res := a :: !res in IList.iter do_atom prop.pi; IList.rev !res diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 15ad94049..632b8e61a 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -283,10 +283,7 @@ val conjoin_neq : ?footprint: bool -> Exp.t -> Exp.t -> normal t -> normal t module Attribute : sig (** Check whether an atom is used to mark an attribute *) - val atom_is : atom -> bool - - (** Return the exp and attribute marked in the atom if any, and return None otherwise *) - val atom_get : atom -> atom option + val is_pred : atom -> bool (** Add an attribute associated to the argument expressions *) val add : ?footprint: bool -> ?polarity: bool -> normal t -> PredSymb.t -> Exp.t list -> normal t diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 4abd34bc4..cf8fcfb53 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -599,14 +599,14 @@ let prop_copy_footprint_pure p1 p2 = Prop.replace_sigma_footprint (Prop.get_sigma_footprint p1) (Prop.replace_pi_footprint (Prop.get_pi_footprint p1) p2) in let pi2 = Prop.get_pi p2' in - let pi2_attr, pi2_noattr = IList.partition Prop.Attribute.atom_is pi2 in + let pi2_attr, pi2_noattr = IList.partition Prop.Attribute.is_pred pi2 in let res_noattr = Prop.replace_pi (Prop.get_pure p1 @ pi2_noattr) p2' in let replace_attr prop atom = (* call replace_atom_attribute which deals with existing attibutes *) (* if [atom] represents an attribute [att], add the attribure to [prop] *) - match Prop.Attribute.atom_get atom with - | None -> prop - | Some atom -> - Prop.Attribute.add_or_replace_check_changed check_attr_dealloc_mismatch prop atom in + if Prop.Attribute.is_pred atom then + Prop.Attribute.add_or_replace_check_changed check_attr_dealloc_mismatch prop atom + else + prop in IList.fold_left replace_attr (Prop.normalize res_noattr) pi2_attr (** check if an expression is an exception *) @@ -935,12 +935,12 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_ let combined_pi = calling_pi @ missing_pi_sub in (* build a map from exp -> [taint attrs, untaint attrs], keeping only exprs with both kinds of attrs (we will flag errors on those exprs) *) - let collect_taint_untaint_exprs acc_map atom = - match Prop.Attribute.atom_get atom with - | Some (Apred (Ataint _, [e])) -> + let collect_taint_untaint_exprs acc_map (atom: Sil.atom) = + match atom with + | Apred (Ataint _, [e]) -> let taint_atoms, untaint_atoms = try Exp.Map.find e acc_map with Not_found -> ([], []) in Exp.Map.add e (atom :: taint_atoms, untaint_atoms) acc_map - | Some (Apred (Auntaint _, [e])) -> + | Apred (Auntaint _, [e]) -> let taint_atoms, untaint_atoms = try Exp.Map.find e acc_map with Not_found -> ([], []) in Exp.Map.add e (taint_atoms, atom :: untaint_atoms) acc_map | _ -> acc_map in @@ -954,9 +954,9 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_ "kind" (e.g. security, privacy) of the taint and untaint match, but for now we don't look at the untaint atoms *) let report_taint_errors e (taint_atoms, _untaint_atoms) = - let report_one_error taint_atom = - let taint_info = match Prop.Attribute.atom_get taint_atom with - | Some (Apred (Ataint taint_info, _)) -> taint_info + let report_one_error (taint_atom: Sil.atom) = + let taint_info = match taint_atom with + | Apred (Ataint taint_info, _) -> taint_info | _ -> failwith "Expected to get taint attr on atom" in report_taint_error e taint_info callee_pname caller_pname calling_prop in IList.iter report_one_error taint_atoms in @@ -1109,7 +1109,7 @@ let quantify_path_idents_remove_constant_strings (prop: Prop.normal Prop.t) : Pr (** Strengthen the footprint by adding pure facts from the current part *) let prop_pure_to_footprint (p: 'a Prop.t) : Prop.normal Prop.t = let is_footprint_atom_not_attribute a = - not (Prop.Attribute.atom_is a) + not (Prop.Attribute.is_pred a) && let a_fav = Sil.atom_fav a in Sil.fav_for_all a_fav Ident.is_footprint in