[pulse] conjoin caller arith sooner to get more canonical values thro…

…ughout post application

Summary: This could help with arrays too, like the previous diff.

Reviewed By: dulmarod

Differential Revision: D50087871

fbshipit-source-id: 0b87888d4c3260684e3561b5c49fb9ac9ab98cf8

infer/src/pulse/PulseInterproc.ml

@@ -729,18 +729,17 @@ let apply_post path callee_proc_name call_location callee_summary call_state =
     {call_state with subst; rev_subst}
   in
   let r =
+    call_state
+    |> conjoin_callee_arith `Post (AbductiveDomain.Summary.get_path_condition callee_summary)
     (* subst was suitable for pre but post may know more equalities, take them into account now *)
-    normalize_subst_for_post call_state
-    |> apply_unknown_effects callee_summary
-    |> apply_post_from_callee_pre path callee_proc_name call_location callee_summary
+    >>| normalize_subst_for_post
+    >>| apply_unknown_effects callee_summary
+    >>= apply_post_from_callee_pre path callee_proc_name call_location callee_summary
     >>= apply_post_from_callee_post path callee_proc_name call_location callee_summary
     >>| add_attributes `Post path callee_proc_name call_location
           (AbductiveDomain.Summary.get_post callee_summary).attrs
     >>| record_skipped_calls callee_proc_name call_location callee_summary
     >>| record_need_closure_specialization callee_summary
-    >>= conjoin_callee_arith `Post (AbductiveDomain.Summary.get_path_condition callee_summary)
-    (* normalize subst again now that we know more arithmetic facts *)
-    >>| normalize_subst_for_post
     >>| read_return_value path callee_proc_name call_location callee_summary
   in
   PerfEvent.(log (fun logger -> log_end_event logger ())) ;

infer/tests/codetoanalyze/java/pulse/issues.exp

@@ -119,9 +119,9 @@ codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.Nu
 codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.call_incr_deref2_bad():void, 12, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.call_incr_deref3_bad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,when calling `void NullPointerExceptions.incr_deref3(NullPointerExceptions$A,NullPointerExceptions$A,NullPointerExceptions$A)` here,parameter `a1` of void NullPointerExceptions.incr_deref3(NullPointerExceptions$A,NullPointerExceptions$A,NullPointerExceptions$A),invalid access occurs here]
 codetoanalyze/java/pulse/NullPointerExceptionsMoreTests.java, codetoanalyze.java.infer.NullPointerExceptionsMoreTests.testNullStringDereferencedBad():int, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
-codetoanalyze/java/pulse/NullSafeExample.java, OtherClass.buggyMethodBad():java.lang.String, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `new` (modelled),in call to `OtherClass.<init>()`,is assigned to the null pointer,assigned,return from call to `OtherClass.<init>()`,in call to `OtherClass OtherClass.canReturnNull()`,parameter `this` of OtherClass OtherClass.canReturnNull(),returned,return from call to `OtherClass OtherClass.canReturnNull()`,assigned,invalid access occurs here]
-codetoanalyze/java/pulse/NullSafeExample.java, NullsafeExampleLocal.testingNullsafeLocalMode():void, 3, NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS, no_bucket, ERROR, [allocated by call to `new` (modelled),in call to `OtherClass.<init>()`,is assigned to the null pointer,assigned,return from call to `OtherClass.<init>()`,in call to `OtherClass OtherClass.canReturnNull()`,parameter `this` of OtherClass OtherClass.canReturnNull(),returned,return from call to `OtherClass OtherClass.canReturnNull()`,assigned,assigned,invalid access occurs here]
-codetoanalyze/java/pulse/NullSafeExample.java, NullsafeExampleStrict.testingNullsafeStrictMode():void, 3, NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS, no_bucket, ERROR, [allocated by call to `new` (modelled),in call to `OtherClass.<init>()`,is assigned to the null pointer,assigned,return from call to `OtherClass.<init>()`,in call to `OtherClass OtherClass.canReturnNull()`,parameter `this` of OtherClass OtherClass.canReturnNull(),returned,return from call to `OtherClass OtherClass.canReturnNull()`,assigned,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/NullSafeExample.java, OtherClass.buggyMethodBad():java.lang.String, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `OtherClass.<init>()`,is assigned to the null pointer,assigned,return from call to `OtherClass.<init>()`,in call to `OtherClass OtherClass.canReturnNull()`,parameter `this` of OtherClass OtherClass.canReturnNull(),returned,return from call to `OtherClass OtherClass.canReturnNull()`,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/NullSafeExample.java, NullsafeExampleLocal.testingNullsafeLocalMode():void, 3, NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS, no_bucket, ERROR, [in call to `OtherClass.<init>()`,is assigned to the null pointer,assigned,return from call to `OtherClass.<init>()`,in call to `OtherClass OtherClass.canReturnNull()`,parameter `this` of OtherClass OtherClass.canReturnNull(),returned,return from call to `OtherClass OtherClass.canReturnNull()`,assigned,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/NullSafeExample.java, NullsafeExampleStrict.testingNullsafeStrictMode():void, 3, NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS, no_bucket, ERROR, [in call to `OtherClass.<init>()`,is assigned to the null pointer,assigned,return from call to `OtherClass.<init>()`,in call to `OtherClass OtherClass.canReturnNull()`,parameter `this` of OtherClass OtherClass.canReturnNull(),returned,return from call to `OtherClass OtherClass.canReturnNull()`,assigned,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.testCheckNotNullArgLatent(java.lang.Object):void, 3, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.checkStateConditionSatBad():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.checkArgumentSatBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]

infer/tests/codetoanalyze/objcpp/pulse/issues.exp

@@ -7,7 +7,7 @@ codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatent, 7, NI
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatentBad, 1, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [when calling `testCallMethodReturnsnonPODLatent` here,parameter `b` of testCallMethodReturnsnonPODLatent,taking "then" branch,is assigned to the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [is assigned to the null pointer,assigned,when calling `SomeObject.ptr` here,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testTraceBad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to 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, [global variable `SomeObject.sharedInstance.shared` accessed here,in call to `SomeObject.sharedInstance`,is assigned to the null pointer,assigned,returned,return from call to `SomeObject.sharedInstance`,when calling `SomeObject.returnsnonPOD` here,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 assigned to the null pointer,assigned,returned,return from call to `SomeObject.sharedInstance`,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallNullptrBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, unrelated_invalidation, 3, NIL_INSERTION_INTO_COLLECTION_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,assigned,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `obj` of unrelated_invalidation,in call to `SomeObject.anotherObject`,parameter `self` of SomeObject.anotherObject,a message sent to nil returns nil,return from call to `SomeObject.anotherObject`,assigned,in call to `AnotherObject.unknown_function`,parameter `self` of AnotherObject.unknown_function,a message sent to nil returns nil,return from call to `AnotherObject.unknown_function`,in call to `value insertion into collection literal` (modelled),invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, nilMessagingSharedPtrRefBad, 1, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [in call to `Builder.getResult`,is assigned to the null pointer,returned,return from call to `Builder.getResult`,when calling `Result.shared_ptr_of_int_ref` here,invalid access occurs here]