pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse][nullptr][objc] A separate issue type for nil insertion into collections

Browse Source 
Reviewed By: jvillard

Differential Revision: D28221909

fbshipit-source-id: 49750ceb3
master
Daiva Naudziuniene 4 years ago committed by Facebook GitHub Bot
parent 53b2ec61de
commit cc8b6fb8c1
13 changed files with 58 additions and 23 deletions
Show Stats Download Patch File Download Diff File

1
infer/man/man1/infer-full.txt
Unescape View File

@ -541,6 +541,7 @@ OPTIONS
MULTIPLE_WEAKSELF (enabled by default),
MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default),
Missing_fld (enabled by default),
NIL_INSERTION_INTO_COLLECTION (disabled by default),
NIL_MESSAGING_TO_NON_POD (disabled by default),
NULLPTR_DEREFERENCE (enabled by default),
NULL_DEREFERENCE (enabled by default),

1
infer/man/man1/infer-report.txt
Unescape View File

@ -218,6 +218,7 @@ OPTIONS
MULTIPLE_WEAKSELF (enabled by default),
MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default),
Missing_fld (enabled by default),
NIL_INSERTION_INTO_COLLECTION (disabled by default),
NIL_MESSAGING_TO_NON_POD (disabled by default),
NULLPTR_DEREFERENCE (enabled by default),
NULL_DEREFERENCE (enabled by default),

1
infer/man/man1/infer.txt
Unescape View File

@ -541,6 +541,7 @@ OPTIONS
MULTIPLE_WEAKSELF (enabled by default),
MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default),
Missing_fld (enabled by default),
NIL_INSERTION_INTO_COLLECTION (disabled by default),
NIL_MESSAGING_TO_NON_POD (disabled by default),
NULLPTR_DEREFERENCE (enabled by default),
NULL_DEREFERENCE (enabled by default),

17
infer/src/base/IssueType.ml
Unescape View File

@ -789,6 +789,18 @@ let mutable_local_variable_in_component_file =
[%blob "../../documentation/issues/MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE.md"]
let nil_insertion_into_collection =
register ~enabled:false ~id:"NIL_INSERTION_INTO_COLLECTION" Error Pulse
~user_documentation:"Inserting nil into a collection is an error in Objective-C."
let nil_messaging_to_non_pod =
register ~enabled:false ~id:"NIL_MESSAGING_TO_NON_POD" Error Pulse
~user_documentation:
"Calling a method that returns a C++ non-POD object on the nil object is undefined behavior \
in Objective-C++."
let null_dereference =
register ~id:"NULL_DEREFERENCE" Error Biabduction
~user_documentation:"See [NULLPTR_DEREFERENCE](#nullptr_dereference)."
@ -799,11 +811,6 @@ let nullptr_dereference =
~user_documentation:[%blob "../../documentation/issues/NULLPTR_DEREFERENCE.md"]
let nil_messaging_to_non_pod =
register ~enabled:false ~id:"NIL_MESSAGING_TO_NON_POD" Error Pulse
~user_documentation:"See [NULLPTR_DEREFERENCE](#nullptr_dereference)."
let optional_empty_access =
register ~id:"OPTIONAL_EMPTY_ACCESS" Error Pulse
~user_documentation:[%blob "../../documentation/issues/OPTIONAL_EMPTY_ACCESS.md"]

2
infer/src/base/IssueType.mli
Unescape View File

@ -278,6 +278,8 @@ val mutable_local_variable_in_component_file : t
val nil_messaging_to_non_pod : t
val nil_insertion_into_collection : t
val null_dereference : t
val nullptr_dereference : t

4
infer/src/pulse/PulseAbductiveDomain.ml
Unescape View File

@ -245,10 +245,10 @@ module AddressAttributes = struct
if phys_equal new_pre astate.pre then astate else {astate with pre= new_pre}
let check_valid access_trace addr astate =
let check_valid ?must_be_valid_reason access_trace addr astate =
let+ () = BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs in
(* if [address] is in [pre] and it should be valid then that fact goes in the precondition *)
abduce_attribute addr (MustBeValid (access_trace, None)) astate
abduce_attribute addr (MustBeValid (access_trace, must_be_valid_reason)) astate
let check_initialized access_trace addr astate =

7
infer/src/pulse/PulseAbductiveDomain.mli
Unescape View File

@ -115,7 +115,12 @@ module AddressAttributes : sig
val add_attrs : AbstractValue.t -> Attributes.t -> t -> t
val check_valid : Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t * Trace.t) result
val check_valid :
?must_be_valid_reason:Invalidation.must_be_valid_reason
-> Trace.t
-> AbstractValue.t
-> t
-> (t, Invalidation.t * Trace.t) result
val check_initialized : Trace.t -> AbstractValue.t -> t -> (t, unit) result

7
infer/src/pulse/PulseInvalidation.ml
Unescape View File

@ -52,11 +52,14 @@ type t =
| JavaIterator of java_iterator_function
[@@deriving compare, equal]
type must_be_valid_reason = SelfOfNonPODReturnMethod [@@deriving compare, equal]
type must_be_valid_reason = SelfOfNonPODReturnMethod | InsertionIntoCollection
[@@deriving compare, equal]
let pp_must_be_valid_reason f = function
| None ->
F.fprintf f "None"
| Some InsertionIntoCollection ->
F.fprintf f "InsertionIntoCollection"
| Some SelfOfNonPODReturnMethod ->
F.fprintf f "SelfOfNonPODReturnMethod"
@ -69,6 +72,8 @@ let issue_type_of_cause invalidation must_be_valid_reason =
match must_be_valid_reason with
| None ->
IssueType.nullptr_dereference
| Some InsertionIntoCollection ->
IssueType.nil_insertion_into_collection
| Some SelfOfNonPODReturnMethod ->
IssueType.nil_messaging_to_non_pod )
| ConstantDereference _ ->

3
infer/src/pulse/PulseInvalidation.mli
Unescape View File

@ -40,7 +40,8 @@ val pp : F.formatter -> t -> unit
val describe : F.formatter -> t -> unit
type must_be_valid_reason = SelfOfNonPODReturnMethod [@@deriving compare, equal]
type must_be_valid_reason = SelfOfNonPODReturnMethod | InsertionIntoCollection
[@@deriving compare, equal]
val pp_must_be_valid_reason : F.formatter -> must_be_valid_reason option -> unit

10
infer/src/pulse/PulseModels.ml
Unescape View File

@ -263,10 +263,16 @@ module ObjC = struct
fun {location} astate ->
let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
let<*> astate, _ =
PulseOperations.eval_access Read location (value, event :: value_hist) Dereference astate
PulseOperations.eval_access ~must_be_valid_reason:Invalidation.InsertionIntoCollection Read
location
(value, event :: value_hist)
Dereference astate
in
let<+> astate, _ =
PulseOperations.eval_access Read location (key, event :: key_hist) Dereference astate
PulseOperations.eval_access ~must_be_valid_reason:Invalidation.InsertionIntoCollection Read
location
(key, event :: key_hist)
Dereference astate
in
astate
end

10
infer/src/pulse/PulseOperations.ml
Unescape View File

@ -49,10 +49,10 @@ end
include Import
let check_addr_access access_mode location (address, history) astate =
let check_addr_access ?must_be_valid_reason access_mode location (address, history) astate =
let access_trace = Trace.Immediate {location; history} in
let* astate =
AddressAttributes.check_valid access_trace address astate
AddressAttributes.check_valid ?must_be_valid_reason access_trace address astate
|> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
ReportableError
{ diagnostic=
@ -61,7 +61,7 @@ let check_addr_access access_mode location (address, history) astate =
; invalidation
; invalidation_trace
; access_trace
; must_be_valid_reason= None }
; must_be_valid_reason }
; astate } )
in
match access_mode with
@ -173,8 +173,8 @@ end
let eval_var location hist var astate = Stack.eval location hist var astate
let eval_access mode location addr_hist access astate =
let+ astate = check_addr_access mode location addr_hist astate in
let eval_access ?must_be_valid_reason mode location addr_hist access astate =
let+ astate = check_addr_access ?must_be_valid_reason mode location addr_hist astate in
Memory.eval_edge addr_hist access astate

10
infer/src/pulse/PulseOperations.mli
Unescape View File

@ -67,7 +67,12 @@ include module type of Import
type t = AbductiveDomain.t
val check_addr_access :
access_mode -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t
?must_be_valid_reason:Invalidation.must_be_valid_reason
-> access_mode
-> Location.t
-> AbstractValue.t * ValueHistory.t
-> t
-> t AccessResult.t
(** Check that the [address] is not known to be invalid *)
module Closures : sig
@ -101,7 +106,8 @@ val eval_deref_isl :
Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t list
val eval_access :
access_mode
?must_be_valid_reason:Invalidation.must_be_valid_reason
-> access_mode
-> Location.t
-> AbstractValue.t * ValueHistory.t
-> BaseMemory.Access.t

8
infer/tests/codetoanalyze/objcpp/pulse/issues.exp
Unescape View File

@ -1,13 +1,13 @@
codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm, A.create_no_release_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `ABFDataCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilInDictBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, addObjectKeyNilInDictBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,assigned,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, addObjectKeyNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, dereferenceNilBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,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`,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, testNilMessagingForModelNilNilOK_FP, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
codetoanalyze/objcpp/pulse/NPEBasic.mm, testNilMessagingForModelNotNilDictBad, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from call to `NSMutableDictionary.setObject:forKey:` (modelled),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,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from 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,passed as argument to `NSMutableDictionary.setObject:forKey:` (modelled),return from 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, [source of the null value part of the trace starts here,when calling `SomeObject.returnsNil` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `SomeObject.returnsNil`,return from call to `SomeObject.returnsNil`,passed as argument to `SomeObject.get`,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, testTraceBad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,passed as argument to `SomeObject.getXPtr`,return from call to `SomeObject.getXPtr`,assigned,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,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]

Write Preview
Loading…
Cancel
Save