diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 90b731d5e..2e3de29b4 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1030,11 +1030,11 @@ let cycle_has_weak_or_unretained_or_assign_field cycle = let check_observer_is_unsubscribed_deallocation prop e = let pvar_opt = match Prop.get_resource_attribute prop e with - | Some (true, Aresource ({ ra_vpath = Some (DecompiledExp.Dpvar pvar) })) -> Some pvar + | Some (Apred (Aresource ({ ra_vpath = Some (Dpvar pvar) }), _)) -> Some pvar | _ -> None in let loc = State.get_loc () in match Prop.get_observer_attribute prop e with - | Some (true, Aobserver) -> + | Some (Apred (Aobserver, _)) -> (match pvar_opt with | Some pvar when Config.nsnotification_center_checker_backend -> L.d_strln (" ERROR: Object " ^ (Pvar.to_string pvar) ^ @@ -1100,12 +1100,12 @@ let check_junk ?original_prop pname tenv prop = let do_entry e = check_observer_is_unsubscribed_deallocation prop e; match Prop.get_resource_attribute prop e with - | Some (true, (Aresource ({ ra_kind = Racquire }) as a)) -> + | Some (Apred (Aresource ({ ra_kind = Racquire }) as a, _)) -> L.d_str "ATTRIBUTE: "; Sil.d_attribute a; L.d_ln (); res := Some a | _ -> (match Prop.get_undef_attribute prop e with - | Some (true, (Aundef _ as a)) -> + | Some (Apred (Aundef _ as a, _)) -> res := Some a | _ -> ()) in IList.iter do_entry entries; diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 58080593e..b381d0317 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -56,7 +56,7 @@ let is_special_field class_names field_name_opt field = let hpred_is_open_resource prop = function | Sil.Hpointsto(e, _, _) -> (match Prop.get_resource_attribute prop e with - | Some (true, Aresource { ra_kind = Racquire; ra_res = res }) -> Some res + | Some (Apred (Aresource { ra_kind = Racquire; ra_res = res }, _)) -> Some res | _ -> None) | _ -> None @@ -848,7 +848,7 @@ let create_dereference_desc | Some (DExp.Dpvar pvar) | Some (DExp.Dpvaraddr pvar) -> (match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with - | Some (true, Aobjc_null (v,fs)) -> + | Some (Apred (Aobjc_null (v,fs), _)) -> let e = IList.fold_left (fun e f -> Sil.Lfield (e, f, Typ.Tvoid)) (Sil.Lvar v) fs in Localise.parameter_field_not_null_checked_desc desc e | _ -> diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index 2a4b4387a..accd6c9d6 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -399,7 +399,7 @@ let deref_str_array_bound size_opt index_opt = let deref_str_uninitialized alloc_att_opt = let tags = Tags.create () in let creation_str = match alloc_att_opt with - | Some (true, Sil.Aresource ({ ra_kind = Racquire } as ra)) -> + | Some (Sil.Apred (Aresource ({ ra_kind = Racquire } as ra), _)) -> "after allocation " ^ by_call_to_ra tags ra | _ -> "after declaration" in { tags = tags; diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli index 6afa0f827..8a41d9d28 100644 --- a/infer/src/backend/localise.mli +++ b/infer/src/backend/localise.mli @@ -162,7 +162,7 @@ val deref_str_dangling : Sil.dangling_kind option -> deref_str val deref_str_array_bound : IntLit.t option -> IntLit.t option -> deref_str (** dereference strings for an uninitialized access whose lhs has the given attribute *) -val deref_str_uninitialized : (bool * Sil.attribute) option -> deref_str +val deref_str_uninitialized : Sil.atom option -> deref_str (** dereference strings for nonterminal nil arguments in c/objc variadic methods *) val deref_str_nil_argument_in_variadic_method : Procname.t -> int -> int -> deref_str diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 417b647bf..ce3442894 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -312,21 +312,18 @@ let execute___cast builtin_args let set_resource_attribute prop path n_lexp loc ra_res = let prop' = match Prop.get_resource_attribute prop n_lexp with - | Some (true, Aresource ra) -> - Prop.add_or_replace_exp_attribute - prop - true - (Sil.Aresource { ra with Sil.ra_res = ra_res }) - n_lexp + | Some (Apred (Aresource ra, _)) -> + Prop.add_or_replace_exp_attribute prop (Apred (Aresource { ra with ra_res }, n_lexp)) | _ -> - ( 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 - Prop.add_or_replace_exp_attribute prop true (Aresource ra) n_lexp) in + let pname = Sil.mem_alloc_pname Sil.Mnew in + let ra = + { Sil. + ra_kind = Racquire; + ra_res = ra_res; + ra_pname = pname; + ra_loc = loc; + ra_vpath = None } in + Prop.add_or_replace_exp_attribute prop (Apred (Aresource ra, n_lexp)) in [(prop', path)] (** Set the attibute of the value as file *) @@ -548,7 +545,7 @@ let execute___set_autorelease_attribute let prop = return_result lexp prop_ ret_ids in if Config.objc_memory_model_on then let n_lexp, prop = check_arith_norm_exp pname lexp prop in - let prop' = Prop.add_or_replace_exp_attribute prop true Aautorelease n_lexp in + let prop' = Prop.add_or_replace_exp_attribute prop (Apred (Aautorelease, n_lexp)) in [(prop', path)] else execute___no_op prop path | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -559,7 +556,7 @@ let execute___release_autorelease_pool : Builtin.ret_typ = if Config.objc_memory_model_on then let autoreleased_objects = Prop.get_atoms_with_attribute Sil.Aautorelease prop_ in - let prop_without_attribute = Prop.remove_attribute prop_ true Aautorelease in + let prop_without_attribute = Prop.remove_attribute prop_ Aautorelease in let call_release res exp = match res with | (prop', path'):: _ -> @@ -585,12 +582,12 @@ let execute___release_autorelease_pool let set_attr pdesc prop path exp attr = let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp pname exp prop in - [(Prop.add_or_replace_exp_attribute prop true attr n_lexp, path)] + [(Prop.add_or_replace_exp_attribute prop (Apred (attr, n_lexp)), path)] let delete_attr pdesc prop path exp attr = let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp pname exp prop in - [(Prop.remove_attribute_from_exp prop true attr n_lexp, path)] + [(Prop.remove_attribute_from_exp prop (Apred (attr, n_lexp)), path)] (** Set attibute att *) @@ -698,11 +695,7 @@ let _execute_free mk loc acc iter = (* mark value as freed *) let p_res = Prop.add_or_replace_exp_attribute_check_changed - Tabulation.check_attr_dealloc_mismatch - prop - true - (Aresource ra) - lexp in + Tabulation.check_attr_dealloc_mismatch prop (Apred (Aresource ra, lexp)) in p_res :: acc | (Sil.Hpointsto _, _ :: _) -> assert false (* alignment error *) | _ -> assert false (* should not happen *) @@ -803,7 +796,7 @@ let execute_alloc mk can_return_null Sil.ra_loc = loc; Sil.ra_vpath = None } in (* mark value as allocated *) - Prop.add_or_replace_exp_attribute prop' true (Aresource ra) exp_new in + Prop.add_or_replace_exp_attribute prop' (Apred (Aresource ra, exp_new)) 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/prop.ml b/infer/src/backend/prop.ml index 2fbb0487a..386f942b3 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1790,9 +1790,9 @@ let prop_reset_inst inst_map prop = (** {2 Attributes} *) (** Return the exp and attribute marked in the atom if any, and return None otherwise *) -let atom_get_exp_attribute = function - | Sil.Apred (a, e) -> Some (true, a, e) - | Sil.Anpred (a, e) -> Some (false, a, e) +let atom_get_exp_attribute atom = + match atom with + | Sil.Apred _ | Anpred _ -> Some atom | _ -> None (** Check whether an atom is used to mark an attribute *) @@ -1804,8 +1804,7 @@ let get_exp_attributes prop exp = let nexp = exp_normalize_prop prop exp in let atom_get_attr attributes atom = match atom with - | Sil.Apred (att, e) when Sil.exp_equal e nexp -> (true, att) :: attributes - | Sil.Anpred (att, e) when Sil.exp_equal e nexp -> (false, att) :: attributes + | Sil.Apred (_, e) | Anpred (_, e) when Sil.exp_equal e nexp -> atom :: attributes | _ -> attributes in IList.fold_left atom_get_attr [] prop.pi @@ -1816,11 +1815,13 @@ let attributes_in_same_category attr1 attr2 = let get_attribute prop exp category = let atts = get_exp_attributes prop exp in - try Some (IList.find - (fun (_, att) -> - Sil.attribute_category_equal - (Sil.attribute_to_category att) category) - atts) + try + Some + (IList.find (function + | Sil.Apred (att, _) | Anpred (att, _) -> + Sil.attribute_category_equal (Sil.attribute_to_category att) category + | _ -> false + ) atts) with Not_found -> None let get_undef_attribute prop exp = @@ -1849,7 +1850,10 @@ let get_retval_attribute prop exp = let has_dangling_uninit_attribute prop exp = let la = get_exp_attributes prop exp in - IList.exists (fun (pol, a) -> pol && Sil.attribute_equal a (Adangling DAuninit)) la + IList.exists (function + | Sil.Apred (a, _) -> Sil.attribute_equal a (Adangling DAuninit) + | _ -> false + ) la (** Get all the attributes of the prop *) let get_all_attributes prop = @@ -1866,77 +1870,76 @@ let set_exp_attribute ?(footprint = false) ?(polarity = true) prop attr exp = (if polarity then Sil.Apred (attr, exp) else Sil.Anpred (attr, exp)) (** Replace an attribute associated to the expression *) -let add_or_replace_exp_attribute_check_changed check_attribute_change prop pol0 att0 exp = - let nexp = exp_normalize_prop prop exp in - let atom_map a = match a with - | Sil.Apred (att, e) | Anpred (att, e) -> - if Sil.exp_equal nexp e && attributes_in_same_category att att0 then - begin +let add_or_replace_exp_attribute_check_changed check_attribute_change prop atom0 = + match atom0 with + | Sil.Apred (att0, exp0) | Anpred (att0, exp0) -> + let nexp = exp_normalize_prop prop exp0 in + let atom = Sil.atom_replace_exp [(exp0, nexp)] atom0 in + let atom_map = function + | Sil.Apred (att, exp) | Anpred (att, exp) + when Sil.exp_equal nexp exp && attributes_in_same_category att att0 -> check_attribute_change att att0; - if pol0 then Sil.Apred (att0, e) else Sil.Anpred (att0, e) - end - else a - | _ -> a in - let pi = get_pi prop in - let pi' = IList.map_changed atom_map pi in - if pi == pi' - then set_exp_attribute prop ~polarity:pol0 att0 nexp - else replace_pi pi' prop - -let add_or_replace_exp_attribute prop pol att exp = + atom + | a -> + a in + let pi = get_pi prop in + let pi' = IList.map_changed atom_map pi in + if pi == pi' + then prop_atom_and prop atom + else replace_pi pi' prop + | _ -> + prop + +let add_or_replace_exp_attribute prop atom = (* 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 pol att exp + add_or_replace_exp_attribute_check_changed check_attr_changed prop atom (** mark Sil.Var's or Sil.Lvar's as undefined *) let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos = let att_undef = Sil.Aundef (callee_pname, ret_annots, loc, path_pos) in let mark_var_as_undefined exp prop = match exp with - | Sil.Var _ | Sil.Lvar _ -> add_or_replace_exp_attribute prop true att_undef exp + | Sil.Var _ | Lvar _ -> add_or_replace_exp_attribute prop (Apred (att_undef, exp)) | _ -> prop in IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark -let remove_attribute_by_filter ~f prop = - let atom_remove atom pi = match atom with - | Sil.Apred (att_old, exp) -> - if f true att_old exp then - pi - else atom:: pi - | Sil.Anpred (att_old, exp) -> - if f false att_old exp then - pi - else atom:: pi - | _ -> atom:: pi in - let pi' = IList.fold_right atom_remove (get_pi prop) [] in - replace_pi pi' prop +let filter_atoms ~f prop = + replace_pi (IList.filter f (get_pi prop)) prop (** Remove an attribute from all the atoms in the heap *) -let remove_attribute prop pol0 att0 = - let f pol att _ = bool_equal pol0 pol && Sil.attribute_equal att0 att in - remove_attribute_by_filter ~f prop +let remove_attribute prop att0 = + let f = function + | Sil.Apred (att, _) | Anpred (att, _) -> not (Sil.attribute_equal att0 att) + | _ -> true in + filter_atoms ~f prop let remove_resource_attribute ra_kind ra_res = - let f pol att_old _ = match att_old with - | Sil.Aresource res_action when pol -> - Sil.res_act_kind_compare res_action.Sil.ra_kind ra_kind == 0 - && Sil.resource_compare res_action.Sil.ra_res ra_res == 0 - | _ -> false in - remove_attribute_by_filter ~f - -let remove_attribute_from_exp prop pol att exp = - let nexp = exp_normalize_prop prop exp in - let f pol_old att_old e = - bool_equal pol pol_old && Sil.attribute_equal att_old att && Sil.exp_equal nexp e in - remove_attribute_by_filter ~f prop + let f = function + | Sil.Apred (Aresource res_action, _) -> + Sil.res_act_kind_compare res_action.ra_kind ra_kind <> 0 + || Sil.resource_compare res_action.ra_res ra_res <> 0 + | _ -> true in + filter_atoms ~f + +let remove_attribute_from_exp prop atom = + match atom with + | Sil.Apred (_, exp) | Anpred (_, exp) -> + let nexp = exp_normalize_prop prop exp in + let natom = Sil.atom_replace_exp [(exp,nexp)] atom in + let f a = not (Sil.atom_equal natom a) in + filter_atoms ~f prop + | _ -> + replace_pi (get_pi prop) prop (* Replace an attribute OBJC_NULL($n1) with OBJC_NULL(var) when var = $n1, and also sets $n1 = 0 *) let replace_objc_null prop lhs_exp rhs_exp = match get_objc_null_attribute prop rhs_exp, rhs_exp with - | Some (pol, att), Sil.Var _ -> - let prop = remove_attribute_from_exp prop pol att rhs_exp in + | Some atom, Sil.Var _ -> + let prop = remove_attribute_from_exp prop atom in let prop = conjoin_eq rhs_exp Sil.exp_zero prop in - add_or_replace_exp_attribute prop true att lhs_exp + let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in + add_or_replace_exp_attribute prop natom | _ -> prop let rec nullify_exp_with_objc_null prop exp = @@ -1948,8 +1951,8 @@ let rec nullify_exp_with_objc_null prop exp = nullify_exp_with_objc_null prop exp | Sil.Var _ -> (match get_objc_null_attribute prop exp with - | Some (pol, att) -> - let prop' = remove_attribute_from_exp prop pol att exp in + | Some atom -> + let prop' = remove_attribute_from_exp prop atom in conjoin_eq exp Sil.exp_zero prop' | _ -> prop) | _ -> prop @@ -1992,7 +1995,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 | _ -> - res := add_or_replace_exp_attribute !res true (Adiv0 proc_node_session) e; + res := add_or_replace_exp_attribute !res (Apred (Adiv0 proc_node_session, e)); false in let rec walk = function | Sil.Var _ -> () @@ -2050,7 +2053,7 @@ 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; - res := add_or_replace_exp_attribute !res true (Adangling DAaddr_stack_var) (Var freshv) + res := add_or_replace_exp_attribute !res (Apred (Adangling DAaddr_stack_var, Var freshv)) end in IList.iter do_var !fresh_address_vars; !res in @@ -2850,7 +2853,7 @@ let find_equal_formal_path e prop = | Some (v, rev_fs) -> Some (v, IList.rev rev_fs) | None -> match get_objc_null_attribute prop e with - | Some (true, Aobjc_null (v,fs)) -> Some (v,fs) + | Some (Apred (Aobjc_null (v,fs), _)) -> Some (v,fs) | _ -> None (** translate an if-then-else expression *) diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 6fd65102f..b58065cf4 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -285,37 +285,37 @@ val atom_is_attribute : atom -> bool val attribute_map_resource : normal t -> (Sil.exp -> Sil.res_action -> Sil.res_action) -> normal t (** Return the exp and attribute marked in the atom if any, and return None otherwise *) -val atom_get_exp_attribute : atom -> (bool * Sil.attribute * Sil.exp) option +val atom_get_exp_attribute : atom -> atom option (** Get the attributes associated to the expression, if any *) -val get_exp_attributes : 'a t -> exp -> (bool * attribute) list +val get_exp_attributes : 'a t -> exp -> atom list (** Get the undef attribute associated to the expression, if any *) -val get_undef_attribute : 'a t -> exp -> (bool * attribute) option +val get_undef_attribute : 'a t -> exp -> atom option (** Get the resource attribute associated to the expression, if any *) -val get_resource_attribute : 'a t -> exp -> (bool * attribute) option +val get_resource_attribute : 'a t -> exp -> atom option (** Get the taint attribute associated to the expression, if any *) -val get_taint_attribute : 'a t -> exp -> (bool * attribute) option +val get_taint_attribute : 'a t -> exp -> atom option (** Get the autorelease attribute associated to the expression, if any *) -val get_autorelease_attribute : 'a t -> exp -> (bool * attribute) option +val get_autorelease_attribute : 'a t -> exp -> atom option (** Get the div0 attribute associated to the expression, if any *) -val get_div0_attribute : 'a t -> exp -> (bool * attribute) option +val get_div0_attribute : 'a t -> exp -> atom option (** Get the observer attribute associated to the expression, if any *) -val get_observer_attribute : 'a t -> exp -> (bool * attribute) option +val get_observer_attribute : 'a t -> exp -> atom option (** Get the objc null attribute associated to the expression, if any *) -val get_objc_null_attribute : 'a t -> exp -> (bool * attribute) option +val get_objc_null_attribute : 'a t -> exp -> atom option (** Get the retval null attribute associated to the expression, if any *) -val get_retval_attribute : 'a t -> exp -> (bool * attribute) option +val get_retval_attribute : 'a t -> exp -> atom option (** Get all the attributes of the prop *) -val get_all_attributes : 'a t -> (bool * attribute * exp) list +val get_all_attributes : 'a t -> atom list val has_dangling_uninit_attribute : 'a t -> exp -> bool @@ -323,18 +323,18 @@ val has_dangling_uninit_attribute : 'a t -> exp -> bool val set_exp_attribute : ?footprint: bool -> ?polarity: bool -> normal t -> attribute -> exp -> normal t -val add_or_replace_exp_attribute_check_changed : (Sil.attribute -> Sil.attribute -> unit) -> - normal t -> bool -> attribute -> exp -> normal t +val add_or_replace_exp_attribute_check_changed : + (Sil.attribute -> Sil.attribute -> unit) -> normal t -> atom -> normal t (** Replace an attribute associated to the expression *) -val add_or_replace_exp_attribute : normal t -> bool -> attribute -> exp -> normal t +val add_or_replace_exp_attribute : normal t -> atom -> normal t (** mark Sil.Var's or Sil.Lvar's as undefined *) val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Typ.item_annotation -> Location.t -> Sil.path_pos -> normal t (** Remove an attribute from all the atoms in the heap *) -val remove_attribute : 'a t -> bool -> Sil.attribute -> normal t +val remove_attribute : 'a t -> Sil.attribute -> normal t val remove_resource_attribute : Sil.res_act_kind -> Sil.resource -> 'a t -> normal t @@ -345,7 +345,7 @@ val replace_objc_null : normal t -> exp -> exp -> normal t val nullify_exp_with_objc_null : normal t -> exp -> normal t (** Remove an attribute from an exp in the heap *) -val remove_attribute_from_exp : 'a t -> bool -> Sil.attribute -> exp -> normal t +val remove_attribute_from_exp : 'a t -> atom -> 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 diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 63f819f81..491c65717 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -744,7 +744,7 @@ let add_guarded_by_constraints prop lexp pdesc = (* or the prop says we already have the lock *) IList.exists (function - | (true, Sil.Alocked) -> true + | Sil.Apred (Alocked, _) -> true | _ -> false) (Prop.get_exp_attributes prop guarded_by_exp) in let should_warn pdesc = @@ -1200,8 +1200,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = end else let is_nullable_attr = function - | (true, Sil.Aretval (pname, ret_attr)) - | (true, Sil.Aundef (pname, ret_attr, _, _)) + | Sil.Apred ((Aretval (pname, ret_attr) | Aundef (pname, ret_attr, _, _)), _) when Annotations.ia_is_nullable ret_attr -> nullable_obj_str := Some (Procname.to_string pname); true @@ -1273,17 +1272,17 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = else raise (Exceptions.Null_dereference (err_desc, __POS__)) end; match attribute_opt with - | Some (true, Adangling dk) -> + | Some (Apred (Adangling dk, _)) -> let deref_str = Localise.deref_str_dangling (Some dk) in let err_desc = Errdesc.explain_dereference deref_str prop (State.get_loc ()) in raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__)) - | Some (true, Aundef (s, _, undef_loc, _)) -> + | Some (Apred (Aundef (s, _, undef_loc, _), _)) -> if Config.angelic_execution then () else let deref_str = Localise.deref_str_undef (s, undef_loc) in let err_desc = Errdesc.explain_dereference deref_str prop loc in raise (Exceptions.Skip_pointer_dereference (err_desc, __POS__)) - | Some (true, Aresource ({ ra_kind = Rrelease } as ra)) -> + | Some (Apred (Aresource ({ ra_kind = Rrelease } as ra), _)) -> let deref_str = Localise.deref_str_freed ra in let err_desc = Errdesc.explain_dereference ~use_buckets: true deref_str prop loc in raise (Exceptions.Use_after_free (err_desc, __POS__)) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index b3c7a7b1e..27c85fb55 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -476,11 +476,11 @@ let check_already_dereferenced pname cond prop = raising an exception in that case *) let check_deallocate_static_memory prop_after = let check_deallocated_attribute = function - | true, Sil.Aresource ({ ra_kind = Rrelease } as ra), Sil.Lvar pv + | Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), Lvar pv) when Pvar.is_local pv || Pvar.is_global pv -> let freed_desc = Errdesc.explain_deallocate_stack_var pv ra in raise (Exceptions.Deallocate_stack_variable freed_desc) - | true, Sil.Aresource ({ ra_kind = Rrelease } as ra), Sil.Const (Cstr s) -> + | Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), Const (Cstr s)) -> let freed_desc = Errdesc.explain_deallocate_constant_string s ra in raise (Exceptions.Deallocate_static_memory freed_desc) | _ -> () in @@ -738,7 +738,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r | [ret_id] -> ( match Prop.find_equal_formal_path receiver prop with | Some (v,fs) -> - Prop.add_or_replace_exp_attribute prop true (Aobjc_null (v,fs)) (Var ret_id) + Prop.add_or_replace_exp_attribute prop (Apred (Aobjc_null (v,fs), Var ret_id)) | None -> Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop ) @@ -843,7 +843,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_ | Typ.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop | _ -> prop in let add_tainted_post ret_exp callee_pname prop = - Prop.add_or_replace_exp_attribute prop true (Ataint callee_pname) ret_exp in + Prop.add_or_replace_exp_attribute prop (Apred (Ataint callee_pname, ret_exp)) in if Config.angelic_execution && not (is_rec_call callee_pname) then (* introduce a fresh program variable to allow abduction on the return value *) @@ -872,7 +872,7 @@ let add_taint prop lhs_id rhs_exp pname tenv = if Taint.has_taint_annotation fieldname struct_typ then let taint_info = { Sil.taint_source = pname; taint_kind = Tk_unknown; } in - Prop.add_or_replace_exp_attribute prop true (Ataint taint_info) (Var lhs_id) + Prop.add_or_replace_exp_attribute prop (Apred (Ataint taint_info, Var lhs_id)) else prop in match rhs_exp with @@ -903,7 +903,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ let prop' = Prop.prop_iter_to_prop iter' in let prop'' = if lookup_uninitialized then - Prop.add_or_replace_exp_attribute prop' true (Adangling DAuninit) (Var id) + Prop.add_or_replace_exp_attribute prop' (Apred (Adangling DAuninit, Var id)) else prop' in let prop''' = if Config.taint_analysis @@ -932,15 +932,16 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ [Prop.conjoin_eq (Sil.Var id) value prop] | None -> let exp_get_undef_attr exp = - let fold_undef_pname callee_opt (pol, attr) = - if Option.is_none callee_opt && pol && Sil.attr_is_undef attr then Some attr - else callee_opt in + let fold_undef_pname callee_opt atom = + match callee_opt, atom with + | None, Sil.Apred (Aundef _, _) -> Some atom + | _ -> callee_opt in IList.fold_left fold_undef_pname None (Prop.get_exp_attributes prop exp) in let prop' = if Config.angelic_execution then (* when we try to deref an undefined value, add it to the footprint *) match exp_get_undef_attr n_rhs_exp' with - | Some (Sil.Aundef (callee_pname, ret_annots, callee_loc, _)) -> + | Some (Apred (Aundef (callee_pname, ret_annots, callee_loc, _), _)) -> let has_nullable_annot = Annotations.ia_is_nullable ret_annots in add_constraints_on_retval pdesc prop n_rhs_exp' ~has_nullable_annot typ callee_pname callee_loc @@ -1362,7 +1363,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call and check_untainted exp taint_kind caller_pname callee_pname prop = match Prop.get_taint_attribute prop exp with - | Some (true, Ataint taint_info) -> + | Some (Apred (Ataint taint_info, _)) -> let err_desc = Errdesc.explain_tainted_value_reaching_sensitive_function prop @@ -1374,7 +1375,7 @@ and check_untainted exp taint_kind caller_pname callee_pname prop = Exceptions.Tainted_value_reaching_sensitive_function (err_desc, __POS__) in Reporting.log_warning caller_pname exn; - Prop.add_or_replace_exp_attribute prop true (Auntaint taint_info) exp + Prop.add_or_replace_exp_attribute prop (Apred (Auntaint taint_info, exp)) | _ -> if !Config.footprint then let taint_info = { Sil.taint_source = callee_pname; taint_kind; } in @@ -1388,10 +1389,9 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots args; proc_name= callee_pname; loc; instr; } = let remove_file_attribute prop = let do_exp p (e, _) = - let do_attribute q = function - | (pol, (Sil.Aresource res_action as res)) - when res_action.Sil.ra_res = Sil.Rfile -> - Prop.remove_attribute q pol res + let do_attribute q atom = + match atom with + | Sil.Apred ((Aresource {ra_res = Rfile} as res), _) -> Prop.remove_attribute q res | _ -> q in IList.fold_left do_attribute p (Prop.get_exp_attributes p e) in let filtered_args = diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 179a12f13..5e2efcdae 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -318,11 +318,11 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = else if Sil.exp_equal e_sub Sil.exp_minus_one then Some (Deref_minusone, desc true (Localise.deref_str_dangling None)) else match Prop.get_resource_attribute actual_pre e_sub with - | Some (true, Aresource ({ ra_kind = Rrelease } as ra)) -> + | Some (Apred (Aresource ({ ra_kind = Rrelease } as ra), _)) -> Some (Deref_freed ra, desc true (Localise.deref_str_freed ra)) | _ -> (match Prop.get_undef_attribute actual_pre e_sub with - | Some (true, Aundef (s, _, loc, pos)) -> + | Some (Apred (Aundef (s, _, loc, pos), _)) -> Some (Deref_undef (s, loc, pos), desc false (Localise.deref_str_undef (s, loc))) | _ -> None) in let check_hpred = function @@ -360,8 +360,9 @@ let post_process_sigma (sigma: Sil.hpred list) loc : Sil.hpred list = (** check for interprocedural path errors in the post *) let check_path_errors_in_post caller_pname post post_path = - let check_attr (pol, att, e) = match att with - | Sil.Adiv0 path_pos when pol -> + let check_attr atom = + match atom with + | Sil.Apred (Adiv0 path_pos, e) -> if Prover.check_zero e then let desc = Errdesc.explain_divide_by_zero e (State.get_node ()) (State.get_loc ()) in let new_path, path_pos_opt = @@ -382,7 +383,7 @@ let check_path_errors_in_post caller_pname post post_path = let post_process_post caller_pname callee_pname loc actual_pre ((post: Prop.exposed Prop.t), post_path) = let actual_pre_has_freed_attribute e = match Prop.get_resource_attribute actual_pre e with - | Some (true, Aresource ({ ra_kind = Rrelease })) -> true + | Some (Apred (Aresource ({ ra_kind = Rrelease }), _)) -> true | _ -> false in let atom_update_alloc_attribute = function | Sil.Apred (Aresource ra, e) @@ -604,9 +605,8 @@ let prop_copy_footprint_pure p1 p2 = (* if [atom] represents an attribute [att], add the attribure to [prop] *) match Prop.atom_get_exp_attribute atom with | None -> prop - | Some (pol, att, exp) -> - Prop.add_or_replace_exp_attribute_check_changed - check_attr_dealloc_mismatch prop pol att exp in + | Some atom -> + Prop.add_or_replace_exp_attribute_check_changed check_attr_dealloc_mismatch prop atom in IList.fold_left replace_attr (Prop.normalize res_noattr) pi2_attr (** check if an expression is an exception *) @@ -837,7 +837,7 @@ let check_taint_on_variadic_function callee_pname caller_pname actual_params cal IList.iter(fun (e,_) -> L.d_str (" " ^ (Sil.exp_to_string e) ^ " "); match Prop.get_taint_attribute calling_prop e with - | Some (true, Ataint taint_info) -> + | Some (Apred (Ataint taint_info, _)) -> report_taint_error e taint_info callee_pname caller_pname calling_prop | _ -> ()) actual_params'; L.d_strln" ]" @@ -883,11 +883,10 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts = "if (get() != null) get().something()" pattern *) let last_call_ret_non_null = IList.exists - (fun (pol, attr, exp) -> - match attr with - | Sil.Aretval (pname, _) when pol && Procname.equal callee_pname pname -> - Prover.check_disequal prop exp Sil.exp_zero - | _ -> false) + (function + | Sil.Apred (Aretval (pname, _), exp) when Procname.equal callee_pname pname -> + Prover.check_disequal prop exp Sil.exp_zero + | _ -> false) (Prop.get_all_attributes prop) in if last_call_ret_non_null then let returns_null prop = @@ -905,9 +904,8 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts = let taint_retval (prop, path) = let prop_normal = Prop.normalize prop in let prop' = - Prop.add_or_replace_exp_attribute prop_normal true - (Ataint { taint_source = callee_pname; taint_kind; }) - (Var ret_id) + Prop.add_or_replace_exp_attribute prop_normal + (Apred (Ataint { taint_source = callee_pname; taint_kind; }, Var ret_id)) |> Prop.expose in (prop', path) in IList.map taint_retval posts @@ -937,11 +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.atom_get_exp_attribute atom with - | Some (_, Ataint _, e) -> + let collect_taint_untaint_exprs acc_map atom = + match Prop.atom_get_exp_attribute atom with + | Some (Apred (Ataint _, e)) -> let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in Sil.ExpMap.add e (atom :: taint_atoms, untaint_atoms) acc_map - | Some (_, Auntaint _, e) -> + | Some (Apred (Auntaint _, e)) -> let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in Sil.ExpMap.add e (taint_atoms, atom :: untaint_atoms) acc_map | _ -> acc_map in @@ -957,7 +956,7 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_ let report_taint_errors e (taint_atoms, _untaint_atoms) = let report_one_error taint_atom = let taint_info = match Prop.atom_get_exp_attribute taint_atom with - | Some (_, Ataint taint_info, _) -> taint_info + | Some (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 diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index 1763181a0..eb0e55148 100644 --- a/infer/src/backend/taint.ml +++ b/infer/src/backend/taint.ml @@ -379,6 +379,6 @@ let add_tainting_attribute att pvar_param prop = when Pvar.equal pvar pvar_param -> L.d_strln ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^ (Pvar.to_string pvar)); - Prop.add_or_replace_exp_attribute prop_acc true att rhs + Prop.add_or_replace_exp_attribute prop_acc (Apred (att, rhs)) | _ -> prop_acc) prop (Prop.get_sigma prop)