diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index c13b5245a..bc7dea518 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -326,15 +326,6 @@ module AddressAttributes = struct map_post_attrs astate ~f:(BaseAddressAttributes.add_unreachable_at addr location) - let replace_must_be_valid_reason path reason addr astate = - match BaseAddressAttributes.get_must_be_valid addr (astate.pre :> base_domain).attrs with - | Some (_timestamp, trace, _reason) -> - remove_must_be_valid_attr addr astate - |> abduce_attribute addr (MustBeValid (path.PathContext.timestamp, trace, Some reason)) - | None -> - astate - - let is_end_of_collection addr astate = BaseAddressAttributes.is_end_of_collection addr (astate.post :> base_domain).attrs diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 93bb803ff..973b19041 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -131,9 +131,6 @@ module AddressAttributes : sig val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t - val replace_must_be_valid_reason : - PathContext.t -> Invalidation.must_be_valid_reason -> AbstractValue.t -> t -> t - val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index e4657244f..492ff0ff6 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -288,10 +288,8 @@ let call tenv path ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary. PulseObjectiveCSummary.mk_objc_method_nil_summary tenv procdesc (ExecutionDomain.mk_initial tenv procdesc) |> Option.value_map ~default:[] ~f:(fun nil_summary -> - let<*> nil_astate = nil_summary in call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals procdesc - ([ContinueProgram nil_astate] :> ExecutionDomain.t list) - astate ) + [nil_summary] astate ) in result_unknown @ result_unknown_nil in diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index e8a68f871..47925b56b 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -36,46 +36,79 @@ let init_fields_zero tenv path location ~zero addr typ astate = init_fields_zero_helper addr typ astate +(** Constructs summary [{self = 0} {return = self}] when [proc_desc] returns a POD type. This allows + us to connect invalidation with invalid access in the trace *) let mk_objc_method_nil_summary_aux tenv proc_desc astate = - (* Constructs summary {self = 0} {return = self}. - This allows us to connect invalidation with invalid access in the trace *) let path = PathContext.initial in let location = Procdesc.get_loc proc_desc in let self = mk_objc_self_pvar proc_desc in - let* astate, (self_value, self_history) = - PulseOperations.eval_deref path location (Lvar self) astate + (* HACK: we are operating on an "empty" initial state and do not expect to create any alarms + (nothing is Invalid in the initial state) or unsatisfiability (we won't create arithmetic + contradictions) *) + let assert_ok = function Ok x -> x | Error _ -> assert false in + let astate, (self_value, self_history) = + PulseOperations.eval_deref path location (Lvar self) astate |> assert_ok in - let* astate = PulseArithmetic.prune_eq_zero self_value astate in + let astate = PulseArithmetic.prune_eq_zero self_value astate |> assert_ok in let event = ValueHistory.NilMessaging location in let updated_self_value_hist = (self_value, event :: self_history) in match List.last (Procdesc.get_formals proc_desc) with | Some (last_formal, {desc= Tptr (typ, _)}) when Mangled.is_return_param last_formal -> let ret_param_var = Procdesc.get_ret_param_var proc_desc in - let* astate, ret_param_var_addr_hist = - PulseOperations.eval_deref path location (Lvar ret_param_var) astate + let astate, ret_param_var_addr_hist = + PulseOperations.eval_deref path location (Lvar ret_param_var) astate |> assert_ok in init_fields_zero tenv path location ~zero:updated_self_value_hist ret_param_var_addr_hist typ astate + |> assert_ok | _ -> let ret_var = Procdesc.get_ret_var proc_desc in - let* astate, ret_var_addr_hist = - PulseOperations.eval path Write location (Lvar ret_var) astate + let astate, ret_var_addr_hist = + PulseOperations.eval path Write location (Lvar ret_var) astate |> assert_ok in PulseOperations.write_deref path location ~ref:ret_var_addr_hist ~obj:updated_self_value_hist astate + |> assert_ok + + +let mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate = + (* same HACK as above *) + let assert_ok = function Ok x -> x | Error _ -> assert false in + let path = PathContext.initial in + let location = Procdesc.get_loc proc_desc in + let self = mk_objc_self_pvar proc_desc in + let astate, (self_value, _self_history) = + PulseOperations.eval_deref path location (Lvar self) astate |> assert_ok + in + let trace = Trace.Immediate {location; history= []} in + let astate = PulseArithmetic.prune_eq_zero self_value astate |> assert_ok in + match AbductiveDomain.summary_of_post tenv proc_desc location astate with + | Unsat | Sat (Error _) -> + assert false + | Sat (Ok astate) -> + ExecutionDomain.LatentInvalidAccess + { astate + ; address= self_value + ; must_be_valid= + (trace, Some (SelfOfNonPODReturnMethod (Procdesc.get_ret_type_from_signature proc_desc))) + ; calling_context= [] } let mk_objc_method_nil_summary tenv proc_desc initial = let proc_name = Procdesc.get_proc_name proc_desc in match (initial, proc_name) with - | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} - when Procdesc.is_ret_type_pod proc_desc -> - (* In ObjC, when a method is called on nil, there is no NPE, - the method is actually not called and the return value is 0/false/nil. - We create a nil summary to avoid reporting NPE in this case. - However, there is an exception in the case where the return type is non-POD. - In that case it's UB and we want to report an error. *) - Some (mk_objc_method_nil_summary_aux tenv proc_desc astate) + | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} -> + if Procdesc.is_ret_type_pod proc_desc then + (* In ObjC, when a method is called on nil, there is no NPE, + the method is actually not called and the return value is 0/false/nil. + We create a nil summary to avoid reporting NPE in this case. + However, there is an exception in the case where the return type is non-POD. + In that case it's UB and we want to report an error. *) + let astate = mk_objc_method_nil_summary_aux tenv proc_desc astate in + Some (ContinueProgram astate) + else + let summary = mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate in + Some summary | ContinueProgram _, _ | ExitProgram _, _ | AbortProgram _, _ @@ -90,8 +123,7 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} let self = mk_objc_self_pvar proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in match (astate, proc_name) with - | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} - when Procdesc.is_ret_type_pod proc_desc -> + | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} -> let result = let* astate, value = PulseOperations.eval_deref PathContext.initial location (Lvar self) astate @@ -111,44 +143,16 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} let append_objc_actual_self_positive procdesc self_actual astate = let procname = Procdesc.get_proc_name procdesc in match procname with - | Procname.ObjC_Cpp {kind= ObjCInstanceMethod} when Procdesc.is_ret_type_pod procdesc -> + | Procname.ObjC_Cpp {kind= ObjCInstanceMethod} -> Option.value_map self_actual ~default:(Ok astate) ~f:(fun ((self, _), _) -> PulseArithmetic.prune_positive self astate ) | _ -> Ok astate -let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_log} astate = - let path = PathContext.initial in - let location = Procdesc.get_loc proc_desc in - let self = mk_objc_self_pvar proc_desc in - let proc_name = Procdesc.get_proc_name proc_desc in - match (astate, proc_name) with - | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} - when not (Procdesc.is_ret_type_pod proc_desc) -> - let result = - (* add reason for must be valid to be because the return type is non pod *) - let+ astate, value = PulseOperations.eval_deref path location (Lvar self) astate in - AddressAttributes.replace_must_be_valid_reason path - (SelfOfNonPODReturnMethod (Procdesc.get_ret_type_from_signature proc_desc)) - (fst value) astate - in - PulseReport.report_result tenv proc_desc err_log location result - | ContinueProgram _, _ - | ExitProgram _, _ - | AbortProgram _, _ - | LatentAbortProgram _, _ - | LatentInvalidAccess _, _ - | ISLLatentMemoryError _, _ -> - [astate] - - -let update_objc_method_posts ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) - ~initial_astate ~posts = +let update_objc_method_posts {InterproceduralAnalysis.tenv; proc_desc} ~initial_astate ~posts = match mk_objc_method_nil_summary tenv proc_desc initial_astate with | None -> - List.concat_map ~f:(update_must_be_valid_reason analysis_data) posts - | Some result -> - let location = Procdesc.get_loc proc_desc in - let nil_summary = PulseReport.report_result tenv proc_desc err_log location result in - nil_summary @ posts + posts + | Some nil_summary -> + nil_summary :: posts diff --git a/infer/src/pulse/PulseObjectiveCSummary.mli b/infer/src/pulse/PulseObjectiveCSummary.mli index 2e2b289c3..3dd55787a 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.mli +++ b/infer/src/pulse/PulseObjectiveCSummary.mli @@ -29,4 +29,4 @@ val append_objc_self_positive : for other kinds of methods *) val mk_objc_method_nil_summary : - Tenv.t -> Procdesc.t -> ExecutionDomain.t -> AbductiveDomain.t AccessResult.t option + Tenv.t -> Procdesc.t -> ExecutionDomain.t -> ExecutionDomain.t option diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index a007e05e9..cc0b7b21a 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp @@ -23,14 +23,14 @@ codetoanalyze/objcpp/pulse/NPEBasic.mm, replaceObjectsAtIndexesWithNilObjectsInA codetoanalyze/objcpp/pulse/NPEBasic.mm, replaceObjectsAtNilIndexesWithObjectsInArrayBad, 1, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `replaceObjectsAtIndexesWithObjectsInArray` here,parameter `indexset` of replaceObjectsAtIndexesWithObjectsInArray,in call to `NSMutableArray.replaceObjectsAtIndexes:withObjects:` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, setByAddingObjectBad, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `setByAddingObject` here,parameter `object` of setByAddingObject,in call to `NSSet.setByAddingObject` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, setWithObjectBad, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `setWithObject` here,parameter `object` of setWithObject,in call to `NSSet.setWithObject` (modelled),invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [is the null pointer,assigned,when calling `SomeObject.ptr` here,parameter `self` of SomeObject.ptr,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatent, 7, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatentBad, 1, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `testCallMethodReturnsnonPODLatent`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `SomeObject.ptr`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.ptr` here,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatent, 7, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [*** LATENT ***,calling context starts here,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatentBad, 1, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `testCallMethodReturnsnonPODLatent`,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, testNilMessagingForModelNilNilOK_FP, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,in call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, testNilMessagingForModelNotNilDictBad, 1, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,in call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [in call to `SomeObject.returnsNil`,is the null pointer,returned,return from call to `SomeObject.returnsNil`,in call to `SomeObject.get`,parameter `self` of SomeObject.get,a message sent to nil returns nil,return from call to `SomeObject.get`,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,in call to `SomeObject.returnsNil`,is the null pointer,returned,return from call to `SomeObject.returnsNil`,in call to `SomeObject.get`,parameter `self` of SomeObject.get,a message sent to nil returns nil,return from call to `SomeObject.get`,assigned,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here] codetoanalyze/objcpp/pulse/NPEBasic.mm, testTraceBad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,in call to `SomeObject.getXPtr`,parameter `self` of SomeObject.getXPtr,a message sent to nil returns nil,return from call to `SomeObject.getXPtr`,assigned,invalid access occurs here] -codetoanalyze/objcpp/pulse/NPEBasic.mm, unknown_call_twice_FP, 4, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [in call to `SomeObject.sharedInstance`,is the null pointer,assigned,returned,return from call to `SomeObject.sharedInstance`,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here] +codetoanalyze/objcpp/pulse/NPEBasic.mm, unknown_call_twice_FP, 4, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,in call to `SomeObject.sharedInstance`,is the null pointer,assigned,returned,return from call to `SomeObject.sharedInstance`,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here] codetoanalyze/objcpp/pulse/use_after_delete.mm, PulseTest.deref_deleted_in_objc_method_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here] codetoanalyze/objcpp/pulse/use_after_delete.mm, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]