From 6ffe204252c83e46bbb7293e25e0f2fb40fc136d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 8 Aug 2016 09:46:54 -0700 Subject: [PATCH] Make Aobjc_null attribute a binary predicate Summary: Change the Aobjc_null attribute from a family of unary predicates, one for each Pvar.t * Ident.fieldname list, to a single binary predicate. This diff should not change behavior except for printing of Aobjc_null attributes. Also, operations such as free variables, etc. should now behave correctly with respect to variables occurring in the arguments of Aobjc_null. Reviewed By: cristianoc Differential Revision: D3669392 fbshipit-source-id: fe4434a --- infer/src/IR/Sil.re | 20 ++++++-------------- infer/src/IR/Sil.rei | 2 +- infer/src/backend/errdesc.ml | 5 ++--- infer/src/backend/prop.ml | 8 ++++---- infer/src/backend/prop.mli | 2 +- infer/src/backend/symExec.ml | 4 ++-- 6 files changed, 16 insertions(+), 25 deletions(-) diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index cafec9ee7..d30baa035 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -106,7 +106,7 @@ type attribute = /** value appeared in second argument of division at given path position */ | Adiv0 of path_pos /** attributed exp is null due to a call to a method with given path as null receiver */ - | Aobjc_null of Pvar.t (list Ident.fieldname) + | Aobjc_null /** value was returned from a call to the given procedure, plus the annots of the return value */ | Aretval of Procname.t Typ.item_annotation /** denotes an object registered as an observers to a notification center */ @@ -481,7 +481,7 @@ let attribute_to_category att => | Aunlocked => AClock | Aautorelease => ACautorelease | Adiv0 _ => ACdiv0 - | Aobjc_null _ => ACobjc_null + | Aobjc_null => ACobjc_null | Aretval _ => ACretval | Aundef _ => ACundef | Aobserver @@ -528,15 +528,9 @@ let attribute_compare (att1: attribute) (att2: attribute) :int => | (Adiv0 pp1, Adiv0 pp2) => path_pos_compare pp1 pp2 | (Adiv0 _, _) => (-1) | (_, Adiv0 _) => 1 - | (Aobjc_null v1 fs1, Aobjc_null v2 fs2) => - let n = Pvar.compare v1 v2; - if (n != 0) { - n - } else { - IList.compare Ident.fieldname_compare fs1 fs2 - } - | (Aobjc_null _, _) => (-1) - | (_, Aobjc_null _) => 1 + | (Aobjc_null, Aobjc_null) => 0 + | (Aobjc_null, _) => (-1) + | (_, Aobjc_null) => 1 | (Aretval pn1 annots1, Aretval pn2 annots2) => let n = Procname.compare pn1 pn2; if (n != 0) { @@ -1056,9 +1050,7 @@ let attribute_to_string pe => | Alocked => "LOCKED" | Aunlocked => "UNLOCKED" | Adiv0 (_, _) => "DIV0" - | Aobjc_null v fs => - "OBJC_NULL[" ^ - String.concat "." [Pvar.to_string v, ...IList.map Ident.fieldname_to_string fs] ^ "]" + | Aobjc_null => "OBJC_NULL" | Aretval pn _ => "RET" ^ Binop.str pe Lt ^ Procname.to_string pn ^ Binop.str pe Gt | Aobserver => "OBSERVER" | Aunsubscribed_observer => "UNSUBSCRIBED_OBSERVER"; diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index 668e645a9..65edd633e 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -94,7 +94,7 @@ type attribute = /** value appeared in second argument of division at given path position */ | Adiv0 of path_pos /** attributed exp is null due to a call to a method with given path as null receiver */ - | Aobjc_null of Pvar.t (list Ident.fieldname) + | Aobjc_null /** value was returned from a call to the given procedure, plus the annots of the return value */ | Aretval of Procname.t Typ.item_annotation /** denotes an object registered as an observers to a notification center */ diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index b381d0317..b7a3e23dd 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -848,9 +848,8 @@ let create_dereference_desc | Some (DExp.Dpvar pvar) | Some (DExp.Dpvaraddr pvar) -> (match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with - | 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 + | Some (Apred (Aobjc_null, [_; vfs])) -> + Localise.parameter_field_not_null_checked_desc desc vfs | _ -> desc) | Some (DExp.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ )) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index ff5703748..2abc19de0 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -2821,7 +2821,7 @@ let find_equal_formal_path e prop = | Sil.Hpointsto (Sil.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal(_, _) ), _) when Sil.exp_equal exp2 e && (Pvar.is_local pvar1 || Pvar.is_seed pvar1) -> - Some (pvar1, []) + Some (Sil.Lvar pvar1) | Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) -> IList.fold_right (fun (field, strexp) res -> match res with @@ -2830,15 +2830,15 @@ let find_equal_formal_path e prop = match strexp with | Sil.Eexp (exp2, _) when Sil.exp_equal exp2 e -> (match find_in_sigma exp1 seen_hpreds with - | Some (v, rev_fs) -> Some (v, field :: rev_fs) + | Some vfs -> Some (Sil.Lfield (vfs, field, Typ.Tvoid)) | None -> None) | _ -> None) fields None | _ -> None) (get_sigma prop) None in match find_in_sigma e [] with - | Some (v, rev_fs) -> Some (v, IList.rev rev_fs) + | Some vfs -> Some vfs | None -> match get_objc_null_attribute prop e with - | Some (Apred (Aobjc_null (v,fs), _)) -> Some (v,fs) + | Some (Apred (Aobjc_null, [_; vfs])) -> Some vfs | _ -> None (** translate an if-then-else expression *) diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index c5a728433..85ba383d4 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -497,7 +497,7 @@ val prop_iter_make_id_primed : Ident.t -> 'a prop_iter -> 'a prop_iter (** Collect garbage fields. *) val prop_iter_gc_fields : unit prop_iter -> unit prop_iter -val find_equal_formal_path : exp -> 'a t -> (Pvar.t * Ident.fieldname list) option +val find_equal_formal_path : exp -> 'a t -> exp option (** return the set of subexpressions of [strexp] *) val strexp_get_exps : Sil.strexp -> Sil.ExpSet.t diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 55964d033..9812f99ca 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -737,8 +737,8 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r match ret_ids with | [ret_id] -> ( match Prop.find_equal_formal_path receiver prop with - | Some (v,fs) -> - Prop.add_or_replace_attribute prop (Apred (Aobjc_null (v,fs), [Sil.Var ret_id])) + | Some vfs -> + Prop.add_or_replace_attribute prop (Apred (Aobjc_null, [Sil.Var ret_id; vfs])) | None -> Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop )