diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index d62632022..3859a1a1d 100644 --- a/infer/src/backend/prop.ml +++ b/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 check_attr_change !res e (Sil.Adiv0 proc_node_session); + res := add_or_replace_exp_attribute !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 := add_or_replace_exp_attribute check_attribute_change !res (Sil.Var freshv) (Sil.Adangling Sil.DAaddr_stack_var) + res := + 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 diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 30b22ec4d..b81b144a0 100644 --- a/infer/src/backend/prop.mli +++ b/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 diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index de48a3c51..866865bb2 100644 --- a/infer/src/backend/symExec.ml +++ b/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 check_attr_change prop' (Sil.Var id) (Sil.Adangling Sil.DAuninit) + Prop.add_or_replace_exp_attribute 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) - (Sil.Aobjc_null info) + Prop.add_or_replace_exp_attribute prop (Sil.Var ret_id) (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 check_attr_change prop n_lexp (Sil.Aresource { ra with Sil.ra_res = ra_res }) + Prop.add_or_replace_exp_attribute + 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 check_attr_change prop n_lexp (Sil.Aresource ra)) in + Prop.add_or_replace_exp_attribute 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 - | _ -> - 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.add_or_replace_exp_attribute prop n_lexp (Sil.Ataint pname) 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 - let p'= Prop.add_or_replace_exp_attribute check_attr_change prop n_lexp (Sil.Auntaint) in - p' in + Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Auntaint) 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 check_attr_change prop n_lexp Sil.Aautorelease in + let prop' = Prop.add_or_replace_exp_attribute 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 - Prop.add_or_replace_exp_attribute check_attr_change prop' exp_new (Sil.Aresource ra) in (* mark value as allocated *) + (* 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 diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 2006710fd..be0c9a161 100644 --- a/infer/src/backend/tabulation.ml +++ b/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 *)