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

@@ -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

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 =
+  let is_pred atom =
-    atom_get a <> None
+    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
+    let do_atom a = if is_pred a then res := a :: !res in
-      | Some attr -> res := attr :: !res
-      | None -> () in
     IList.iter do_atom prop.pi;
     IList.rev !res
 

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
+  val is_pred : atom -> bool
-
-  (** Return the exp and attribute marked in the atom if any, and return None otherwise *)
-  val atom_get : atom -> atom option
 
   (** Add an attribute associated to the argument expressions *)
   val add : ?footprint: bool -> ?polarity: bool -> normal t -> PredSymb.t -> Exp.t list -> normal t

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
+    if Prop.Attribute.is_pred atom then
-    | None -> prop
+      Prop.Attribute.add_or_replace_check_changed check_attr_dealloc_mismatch prop atom
-    | Some atom ->
+    else
-        Prop.Attribute.add_or_replace_check_changed check_attr_dealloc_mismatch prop atom in
+      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 =
+  let collect_taint_untaint_exprs acc_map (atom: Sil.atom) =
-    match Prop.Attribute.atom_get atom with
+    match atom with
-    | Some (Apred (Ataint _, [e])) ->
+    | 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 report_one_error (taint_atom: Sil.atom) =
-      let taint_info = match Prop.Attribute.atom_get taint_atom with
+      let taint_info = match taint_atom with
-        | Some (Apred (Ataint taint_info, _)) -> taint_info
+        | 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