eliminate need to use attr_check_changed when adding or replacing attributes

Reviewed By: cristianoc

Differential Revision: D2691127

fb-gh-sync-id: bb57503

infer/src/backend/prop.ml

@@ -1828,7 +1828,7 @@ let set_exp_attribute prop exp att =
   conjoin_neq exp exp_att prop
 
 (** Replace an attribute associated to the expression *)
-let add_or_replace_exp_attribute check_attribute_change prop exp att =
+let add_or_replace_exp_attribute_check_changed check_attribute_change prop exp att =
   let nexp = exp_normalize_prop prop exp in
   let found = ref false in
   let atom_map a = match a with
@@ -1838,7 +1838,6 @@ let add_or_replace_exp_attribute check_attribute_change prop exp att =
           begin
             found := true;
             check_attribute_change att_old att;
-
             let e1, e2 = exp_reorder e (Sil.Const (Sil.Cattribute att)) in
             Sil.Aneq (e1, e2)
           end
@@ -1848,13 +1847,17 @@ let add_or_replace_exp_attribute check_attribute_change prop exp att =
   if !found then replace_pi pi' prop
   else set_exp_attribute prop nexp att
 
+let add_or_replace_exp_attribute prop exp att =
+  (* wrapper for the most common case: do nothing *)
+  let check_attr_changed = (fun _ _ -> ()) in
+  add_or_replace_exp_attribute_check_changed check_attr_changed prop exp att
+
 (** mark Sil.Var's or Sil.Lvar's as undefined *)
 let mark_vars_as_undefined prop vars_to_mark callee_pname loc path_pos =
   let att_undef = Sil.Aundef (callee_pname, loc, path_pos) in
   let mark_var_as_undefined exp prop =
-    let do_nothing _ _ = () in
     match exp with
-    | Sil.Var _ | Sil.Lvar _ -> add_or_replace_exp_attribute do_nothing prop exp att_undef
+    | Sil.Var _ | Sil.Lvar _ -> add_or_replace_exp_attribute prop exp att_undef
     | _ -> prop in
   IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark
 
@@ -1888,7 +1891,7 @@ let replace_objc_null prop lhs_exp rhs_exp =
   | Some att, Sil.Var var ->
       let prop = remove_attribute_from_exp att prop rhs_exp in
       let prop = conjoin_eq rhs_exp Sil.exp_zero prop in
-      add_or_replace_exp_attribute (fun a1 a2 -> ()) prop lhs_exp att
+      add_or_replace_exp_attribute prop lhs_exp att
   | _ -> prop
 
 (** Get all the attributes of the prop *)
@@ -1919,12 +1922,6 @@ let attribute_map_resource prop f =
   let pi' = IList.map atom_map pi in
   replace_pi pi' prop
 
-(** if [atom] represents an attribute [att], add the attribure to [prop] *)
-let replace_atom_attribute check_attribute_change prop atom =
-  match atom_get_exp_attribute atom with
-  | None -> prop
-  | Some (exp, att) -> add_or_replace_exp_attribute check_attribute_change prop exp att
-
 (** type for arithmetic problems *)
 type arith_problem =
   | Div0 of Sil.exp (* division by zero *)
@@ -1939,8 +1936,7 @@ let find_arithmetic_problem proc_node_session prop exp =
     match exp_normalize_prop prop e with
     | Sil.Const c when iszero_int_float c -> true
     | _ ->
-        let check_attr_change att_old att_new = () in
+        res := add_or_replace_exp_attribute !res e (Sil.Adiv0 proc_node_session);
-        res := add_or_replace_exp_attribute check_attr_change !res e (Sil.Adiv0 proc_node_session);
         false in
   let rec walk = function
     | Sil.Var _ -> ()
@@ -1989,8 +1985,8 @@ let deallocate_stack_vars p pvars =
       if Sil.fav_mem p'_fav freshv then (* the address of a de-allocated stack var in in the post *)
         begin
           stack_vars_address_in_post := v :: !stack_vars_address_in_post;
-          let check_attribute_change att_old att_new = () in
+          res :=
-          res := add_or_replace_exp_attribute check_attribute_change !res (Sil.Var freshv) (Sil.Adangling Sil.DAaddr_stack_var)
+            add_or_replace_exp_attribute !res (Sil.Var freshv) (Sil.Adangling Sil.DAaddr_stack_var)
         end in
     IList.iter do_var !fresh_address_vars;
     !res in

infer/src/backend/prop.mli

@@ -296,8 +296,11 @@ val has_dangling_uninit_attribute : 'a t -> exp -> bool
 
 val set_exp_attribute : normal t -> exp -> attribute -> normal t
 
+val add_or_replace_exp_attribute_check_changed : (Sil.attribute -> Sil.attribute -> unit) ->
+  normal t -> exp -> attribute -> normal t
+
 (** Replace an attribute associated to the expression *)
-val add_or_replace_exp_attribute : (Sil.attribute -> Sil.attribute -> unit) -> normal t -> exp -> attribute -> normal t
+val add_or_replace_exp_attribute : normal t -> exp -> attribute -> normal t
 
 (** mark Sil.Var's or Sil.Lvar's as undefined *)
 val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Location.t ->
@@ -315,9 +318,6 @@ val remove_attribute_from_exp : Sil.attribute -> 'a t -> exp -> normal t
 (** Retireve all the atoms in the heap that contain a specific attribute *)
 val get_atoms_with_attribute : Sil.attribute -> 'a t -> Sil.exp list
 
-(** if [atom] represents an attribute [att], add the attribure to [prop] *)
-val replace_atom_attribute : (Sil.attribute -> Sil.attribute -> unit) -> normal t -> atom -> normal t
-
 (** Return the sub part of [prop]. *)
 val get_sub : 'a t -> subst
 

infer/src/backend/symExec.ml

@@ -277,8 +277,7 @@ let execute_letderef pdesc tenv id rhs_exp acc_in iter =
         let prop'' =
           if lookup_uninitialized
           then
-            let check_attr_change att_old att_new = () in
+            Prop.add_or_replace_exp_attribute prop' (Sil.Var id) (Sil.Adangling Sil.DAuninit)
-            Prop.add_or_replace_exp_attribute check_attr_change prop' (Sil.Var id) (Sil.Adangling Sil.DAuninit)
           else prop' in
         prop'' :: acc in
       begin
@@ -793,8 +792,7 @@ let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc
     | [ret_id] ->
         (match Prop.find_equal_formal_path receiver prop with
          | Some info ->
-             Prop.add_or_replace_exp_attribute (fun a1 a2 -> ()) prop (Sil.Var ret_id)
+             Prop.add_or_replace_exp_attribute prop (Sil.Var ret_id) (Sil.Aobjc_null info)
-               (Sil.Aobjc_null info)
          | None -> Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop)
     | _ -> prop in
   if is_receiver_null then  (* objective-c instance method with a null receiver just return objc_null(res) *)
@@ -1745,13 +1743,14 @@ module ModelBuiltins = struct
   let set_resource_attribute prop path n_lexp loc ra_res =
     let prop' = match Prop.get_resource_attribute prop n_lexp with
       | Some (Sil.Aresource (_ as ra)) ->
-          let check_attr_change att_old att_new = () in
+          Prop.add_or_replace_exp_attribute
-          Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp (Sil.Aresource { ra with Sil.ra_res = ra_res })
+            prop
+            n_lexp
+            (Sil.Aresource { ra with Sil.ra_res = ra_res })
       | _ ->
           ( let pname = Sil.mem_alloc_pname Sil.Mnew in
             let ra = { Sil.ra_kind = Sil.Racquire; Sil.ra_res = ra_res; Sil.ra_pname = pname; Sil.ra_loc = loc; Sil.ra_vpath = None } in
-            let check_attr_change att_old att_new = () in
+            Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Aresource ra)) in
-            Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp (Sil.Aresource ra)) in
     [(prop', path)]
 
   (** Set the attibute of the value as file *)
@@ -1803,11 +1802,7 @@ module ModelBuiltins = struct
         let pname = Cfg.Procdesc.get_proc_name pdesc in
         let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         let prop' = match Prop.get_taint_attribute prop n_lexp with
-          | _ ->
+          | _ -> Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Ataint pname) in
-              let check_attr_change att_old att_new = () in
-              let p'= Prop.add_or_replace_exp_attribute check_attr_change
-                  prop n_lexp (Sil.Ataint pname) in
-              p' in
         [(prop', path)]
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
@@ -1820,9 +1815,7 @@ module ModelBuiltins = struct
         let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
         let prop' = match Prop.get_taint_attribute prop n_lexp with
           | _ ->
-              let check_attr_change att_old att_new = () in
+              Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Auntaint) in
-              let p'= Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp (Sil.Auntaint) in
-              p' in
         [(prop', path)]
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
@@ -1991,8 +1984,7 @@ module ModelBuiltins = struct
         let prop = return_result lexp _prop ret_ids in
         if !Config.objc_memory_model_on then
           let n_lexp, prop = exp_norm_check_arith pname prop lexp in
-          let check_attr_change att_old att_new = () in
+          let prop' = Prop.add_or_replace_exp_attribute prop n_lexp Sil.Aautorelease in
-          let prop' = Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp Sil.Aautorelease in
           [(prop', path)]
         else execute___no_op prop path
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
@@ -2056,8 +2048,13 @@ module ModelBuiltins = struct
         let prop = Prop.prop_iter_remove_curr_then_to_prop iter in
         let pname = Sil.mem_dealloc_pname mk in
         let ra = { Sil.ra_kind = Sil.Rrelease; Sil.ra_res = Sil.Rmemory mk; Sil.ra_pname = pname; Sil.ra_loc = loc; Sil.ra_vpath = None } in
+        (* mark value as freed *)
         let p_res =
-          Prop.add_or_replace_exp_attribute Tabulation.check_attr_dealloc_mismatch prop lexp (Sil.Aresource ra) in (* mark value as freed *)
+          Prop.add_or_replace_exp_attribute_check_changed
+            Tabulation.check_attr_dealloc_mismatch
+            prop
+            lexp
+            (Sil.Aresource ra) in
         p_res :: acc
     | (Sil.Hpointsto _, o :: os) -> assert false (* alignment error *)
     | _ -> assert false (* should not happen *)
@@ -2142,8 +2139,8 @@ module ModelBuiltins = struct
       let pname = Sil.mem_alloc_pname mk in
       let prop' = Prop.normalize (Prop.prop_sigma_star prop [ptsto_new]) in
       let ra = { Sil.ra_kind = Sil.Racquire; Sil.ra_res = Sil.Rmemory mk; Sil.ra_pname = pname; Sil.ra_loc = loc; Sil.ra_vpath = None } in
-      let check_attr_change att_old att_new = () in
+      (* mark value as allocated *)
-      Prop.add_or_replace_exp_attribute check_attr_change prop' exp_new (Sil.Aresource ra) in (* mark value as allocated *)
+      Prop.add_or_replace_exp_attribute prop' exp_new (Sil.Aresource ra) in
     let prop_alloc = Prop.conjoin_eq (Sil.Var ret_id) exp_new prop_plus_ptsto in
     if can_return_null then
       let prop_null = Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop in

infer/src/backend/tabulation.ml

@@ -541,7 +541,11 @@ let prop_copy_footprint_pure p1 p2 =
   let pi2_attr, pi2_noattr = IList.partition Prop.atom_is_attribute 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 *)
-    Prop.replace_atom_attribute check_attr_dealloc_mismatch prop atom in
+    (** if [atom] represents an attribute [att], add the attribure to [prop] *)
+    match Prop.atom_get_exp_attribute atom with
+    | None -> prop
+    | Some (exp, att) ->
+        Prop.add_or_replace_exp_attribute_check_changed check_attr_dealloc_mismatch prop exp att in
   IList.fold_left replace_attr (Prop.normalize res_noattr) pi2_attr
 
 (** check if an expression is an exception *)