[litho] Make analysis null return aware

Summary:
This diff avoids that null-retuned path's abstract value ruins that of non-null-returned path.
What this diff does is: when joining two abstract states, one is null-return-path and the other is
non-null-return-path (`return obj;`), it keeps the method calls of `obj` from the
non-null-return-path.

While this design is unsound, I think it should work in practice.

Reviewed By: ezgicicek

Differential Revision: D19348313

fbshipit-source-id: cf5d0f3ff

infer/src/checkers/LithoDomain.ml

@@ -220,6 +220,22 @@ module MethodCalled = struct
 
   include AbstractDomain.Map (Key) (MethodCalls)
 
+  let join_ignore_null_ret =
+    let override created_locations ~from ~to_ =
+      let f k from_v to_v =
+        if CreatedLocations.mem k.Key.created_location created_locations then from_v else to_v
+      in
+      merge f from to_
+    in
+    fun ~ret_x ~ret_y ~x ~y ->
+      let res = join x y in
+      let is_null_x = CreatedLocations.is_empty ret_x in
+      let is_null_y = CreatedLocations.is_empty ret_y in
+      if is_null_x && not is_null_y then override ret_y ~from:y ~to_:res
+      else if is_null_y && not is_null_x then override ret_x ~from:x ~to_:res
+      else res
+
+
   let add_one created_location v x =
     let f = function
       | None ->
@@ -340,6 +356,14 @@ module Mem = struct
     ; method_called= MethodCalled.join x.method_called y.method_called }
 
 
+  let join_ignore_null_ret ret_path x y =
+    { created= Created.join x.created y.created
+    ; method_called=
+        (let ret_x = Created.lookup ret_path x.created in
+         let ret_y = Created.lookup ret_path y.created in
+         MethodCalled.join_ignore_null_ret ~ret_x ~ret_y ~x:x.method_called ~y:y.method_called ) }
+
+
   let widen ~prev ~next ~num_iters =
     { created= Created.widen ~prev:prev.created ~next:next.created ~num_iters
     ; method_called= MethodCalled.widen ~prev:prev.method_called ~next:next.method_called ~num_iters
@@ -463,7 +487,7 @@ module Mem = struct
     update_latest_callsite callsite ~prev:caller ~next
 end
 
-type t = {no_return_called: Mem.t; return_called: Mem.t}
+type t = {ret_path: LocalAccessPath.t; no_return_called: Mem.t; return_called: Mem.t}
 
 let pp fmt {no_return_called; return_called} =
   F.fprintf fmt "@[<v 0>@[NoReturnCalled:@;%a@]@,@[ReturnCalled:@;%a@]@]" Mem.pp no_return_called
@@ -478,17 +502,19 @@ let leq ~lhs ~rhs =
 
 
 let join x y =
-  { no_return_called= Mem.join x.no_return_called y.no_return_called
-  ; return_called= Mem.join x.return_called y.return_called }
+  { ret_path= x.ret_path
+  ; no_return_called= Mem.join x.no_return_called y.no_return_called
+  ; return_called= Mem.join_ignore_null_ret x.ret_path x.return_called y.return_called }
 
 
 let widen ~prev ~next ~num_iters =
-  { no_return_called= Mem.widen ~prev:prev.no_return_called ~next:next.no_return_called ~num_iters
+  { ret_path= prev.ret_path
+  ; no_return_called= Mem.widen ~prev:prev.no_return_called ~next:next.no_return_called ~num_iters
   ; return_called= Mem.widen ~prev:prev.return_called ~next:next.return_called ~num_iters }
 
 
-let init tenv pname formals =
-  {no_return_called= Mem.init tenv pname formals; return_called= Mem.empty}
+let init tenv pname formals ret_path =
+  {ret_path; no_return_called= Mem.init tenv pname formals; return_called= Mem.empty}
 
 
 let map_no_return_called f x = {x with no_return_called= f x.no_return_called}
@@ -503,8 +529,8 @@ let call_builder ~ret ~receiver callee =
 
 let call_build_method ~ret ~receiver = map_no_return_called (Mem.call_build_method ~ret ~receiver)
 
-let call_return {no_return_called; return_called} =
-  {no_return_called= Mem.empty; return_called= Mem.join no_return_called return_called}
+let call_return {ret_path; no_return_called; return_called} =
+  {ret_path; no_return_called= Mem.empty; return_called= Mem.join no_return_called return_called}
 
 
 let subst ~callsite ~formals ~actuals ~ret_id_typ ~caller_pname ~callee_pname ~caller ~callee =

infer/src/checkers/LithoDomain.mli

@@ -13,6 +13,8 @@ module LocalAccessPath : sig
 
   val make : AccessPath.t -> Procname.t -> t
 
+  val make_from_pvar : Pvar.t -> Typ.t -> Procname.t -> t
+
   val make_from_access_expression : HilExp.AccessExpression.t -> Procname.t -> t
 end
 
@@ -47,7 +49,7 @@ val subst :
 (** type for saving in summary payload *)
 type summary = Mem.t
 
-val init : Tenv.t -> Procname.t -> (Pvar.t * Typ.t) list -> t
+val init : Tenv.t -> Procname.t -> (Pvar.t * Typ.t) list -> LocalAccessPath.t -> t
 
 val assign : lhs:LocalAccessPath.t -> rhs:LocalAccessPath.t -> t -> t
 

infer/src/checkers/RequiredProps.ml

@@ -298,7 +298,12 @@ let checker {Callbacks.summary; exe_env} =
   let proc_name = Summary.get_proc_name summary in
   let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
   let proc_data = ProcData.make summary tenv (init_extras summary) in
-  let initial = Domain.init tenv proc_name (Procdesc.get_pvar_formals proc_desc) in
+  let ret_path =
+    let ret_var = Procdesc.get_ret_var proc_desc in
+    let ret_typ = Procdesc.get_ret_type proc_desc in
+    Domain.LocalAccessPath.make_from_pvar ret_var ret_typ proc_name
+  in
+  let initial = Domain.init tenv proc_name (Procdesc.get_pvar_formals proc_desc) ret_path in
   match Analyzer.compute_post proc_data ~initial with
   | Some post ->
       let is_void_func = Procdesc.get_ret_type proc_desc |> Typ.is_void in

infer/tests/codetoanalyze/java/litho-required-props/RequiredProps.java

@@ -460,11 +460,26 @@ public class RequiredProps {
     return builder;
   }
 
-  public Component callCreateJoinOk_FP(boolean b) {
+  public Component callCreateJoinOk(boolean b) {
 
     return createJoin(b).prop1(new Object()).build();
   }
 
+  public MyComponent.Builder returnNullWithProp3(boolean b, MyComponent.Builder builder) {
+    if (b) {
+      builder.prop3(new Object());
+      return null;
+    }
+    return builder;
+  }
+
+  public void callReturnNullWithProp3_FP(boolean b) {
+    MyComponent.Builder builder = mMyComponent.create();
+    if (returnNullWithProp3(b, builder) == null) {
+      builder.prop1(new Object()).build();
+    }
+  }
+
   private static Component setProp3AndBuild(MyComponent.Builder builder) {
     return setProp3(builder).build();
   }

infer/tests/codetoanalyze/java/litho-required-props/issues.exp

@@ -13,9 +13,8 @@ codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.l
 codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.buildWithout1Bad():com.facebook.litho.Component, 0, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop2(...),calls prop3(...)]
 codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.buildWithout3Bad():com.facebook.litho.Component, 0, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop3** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop1(...),calls prop2(...)]
 codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.callBuildSuffixWithoutRequiredBad():com.facebook.litho.Component, 0, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop2(...),calls prop3(...)]
-codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.callCreateJoinBad(boolean):com.facebook.litho.Component, -12, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop3** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...)]
-codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.callCreateJoinBad(boolean):com.facebook.litho.Component, -12, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...)]
-codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.callCreateJoinOk_FP(boolean):com.facebook.litho.Component, -29, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop3** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop1(...)]
+codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.callCreateJoinBad(boolean):com.facebook.litho.Component, -12, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop3(...)]
+codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.callReturnNullWithProp3_FP(boolean):void, 0, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop3** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop1(...)]
 codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.castImpossibleOk_FP(java.lang.Object):void, 0, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component com.facebook.litho.MyLithoComponent, but is not set before the call to build(),calls com.facebook.litho.MyLithoComponent.create(...)]
 codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.castImpossibleOk_FP(java.lang.Object):void, 0, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop2** is required for component com.facebook.litho.MyLithoComponent, but is not set before the call to build(),calls com.facebook.litho.MyLithoComponent.create(...)]
 codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.castMissingOneBad(java.lang.Object):void, -4, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component com.facebook.litho.MyLithoComponent, but is not set before the call to build(),calls com.facebook.litho.MyLithoComponent.create(...),calls prop2(...)]