From 63b1d1ac1cdab26570fd8132c6a4bb101904ab8f Mon Sep 17 00:00:00 2001 From: Dulma Rodriguez Date: Fri, 3 Jul 2015 10:23:30 -0100 Subject: [PATCH] Revert "[clang] Removing the case of flagging npes in initialisers. This causes many FPs." Summary: This reverts commit 306f5b71c24042c89f71848898402cbc9269c543. Turns out that developers think that this bugs should be fixed. So leaving it in for now until I gather more information. --- infer/src/backend/prover.ml | 6 ++++-- infer/src/backend/symExec.ml | 24 +++++++++++++++++++--- infer/tests/endtoend/objc/NPESelfTest.java | 4 ++-- 3 files changed, 27 insertions(+), 7 deletions(-) diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 8d81c9e89..d3c17b709 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -821,8 +821,9 @@ let check_inconsistency_base prop = Sil.pvar_is_seed pv | _ -> false in list_exists do_hpred sigma in - let inconsistent_self () = (* "self" cannot be null in ObjC *) + let inconsistent_self () = (* "self" cannot be null in ObjC, outside of initializers *) let procdesc = Cfg.Node.get_proc_desc (State.get_node ()) in + let procname = Cfg.Procdesc.get_proc_name procdesc in let procedure_attr = Cfg.Procdesc.get_attributes procdesc in let do_hpred = function | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) -> @@ -830,7 +831,8 @@ let check_inconsistency_base prop = Sil.exp_equal e Sil.exp_zero && Sil.pvar_is_seed pv && Sil.pvar_get_name pv = Mangled.from_string "self" && - procedure_attr.Sil.is_objc_instance_method + procedure_attr.Sil.is_objc_instance_method && + not (Procname.is_constructor procname) | _ -> false in list_exists do_hpred sigma in let inconsistent_atom = function diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 900650dbc..e486b6587 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -784,6 +784,13 @@ let handle_special_cases_call tenv cfg pname actual_params = else pname, actual_params let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc callee_pname loc path = + let receiver_self receiver prop = + list_exists (fun hpred -> + match hpred with + | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) -> + Sil.exp_equal e receiver && Sil.pvar_is_seed pv && + Sil.pvar_get_name pv = Mangled.from_string "self" + | _ -> false) (Prop.get_sigma prop) in let path_description = "Message "^(Procname.to_simplified_string callee_pname)^" with receiver nil returns nil." in let receiver = (match actual_pars with | (e, _):: _ -> e @@ -793,6 +800,10 @@ let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc match actual_pars with | (e, _):: _ when Sil.exp_equal e Sil.exp_zero || Option.is_some (Prop.get_objc_null_attribute pre e) -> true | _ -> false in + let prop_null = + match ret_ids with + | [ret_id] -> Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero pre + | _ -> pre in let add_objc_null_attribute_or_nullify_result prop = match ret_ids with | [ret_id] -> @@ -815,16 +826,22 @@ let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc | _ -> false in if !Config.footprint && not is_undef then let res_null = (* returns: (objc_null(res) /\ receiver=0) or an empty list of results *) - let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in + let is_receiver_self = receiver_self receiver pre in + let pre_with_attr_or_null = + if is_receiver_self then prop_null + else add_objc_null_attribute_or_nullify_result pre in let propset = prune_ne tenv false receiver Sil.exp_zero pre_with_attr_or_null in if Propset.is_empty propset then [] else let prop = list_hd (Propset.to_proplist propset) in - let path = Paths.Path.add_description path path_description in + let path = + if is_receiver_self then path + else Paths.Path.add_description path path_description in [(prop, path)] in res_null @ res else res (* Not known if receiver = 0 and not footprint. Standard tabulation *) + let normalize_params pdesc prop actual_params = let norm_arg (p, args) (e, t) = let e', p' = exp_norm_check_arith pdesc p e in @@ -832,6 +849,7 @@ let normalize_params pdesc prop actual_params = let prop, args = list_fold_left norm_arg (prop, []) actual_params in (prop, list_rev args) + (** Execute [instr] with a symbolic heap [prop].*) let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path : (Prop.normal Prop.t * Paths.Path.t) list = @@ -1146,7 +1164,7 @@ and call_unknown_or_scan is_scan cfg pdesc tenv pre path let do_exp p (e, t) = let do_attribute q = function | Sil.Aresource res_action as res - when res_action.Sil.ra_res = Sil.Rfile -> + when res_action.Sil.ra_res = Sil.Rfile -> Prop.remove_attribute res q | _ -> q in list_fold_left do_attribute p (Prop.get_exp_attributes p e) in diff --git a/infer/tests/endtoend/objc/NPESelfTest.java b/infer/tests/endtoend/objc/NPESelfTest.java index 369526cbd..79d9ca169 100644 --- a/infer/tests/endtoend/objc/NPESelfTest.java +++ b/infer/tests/endtoend/objc/NPESelfTest.java @@ -60,8 +60,8 @@ public class NPESelfTest { throws InterruptedException, IOException, InferException { InferResults inferResults = InferRunner.runInferObjC(inferCmdNPD); assertThat( - "NPE should not be found", inferResults, - doesNotContain( + "NPE should be found", inferResults, + contains( NULL_DEREFERENCE, NPE_FILE, "init"));