[litho] Add sematics of assume null

Summary:
This diff adds semantics of assume null, heuristics.  When `assume(x == null)`, it removes the
methods called on the builder `*x` from the abstract state.

```
x -> {p}
p -> {method1 called}

assume(x == null)

x -> {p}
```

This heuristics is unsound: Even though `x` (a pointer to builder object) points-to an builder
object, which cannot imply that the object `p` does not exist in the concrete semantics.  The
unsoundness may appear when there is an alias (see the FP test added).

Reviewed By: ezgicicek

Differential Revision: D21502923

fbshipit-source-id: 2e392bd89

infer/src/checkers/LithoDomain.ml

@@ -401,6 +401,17 @@ module Mem = struct
     {x with created= Created.add lhs (Created.lookup rhs created) created}
 
 
+  let assume_null path ({created; method_called} as x) =
+    match CreatedLocations.is_singleton_or_more (Created.lookup path created) with
+    | Singleton loc ->
+        let method_called =
+          MethodCalled.remove {created_location= loc; is_build_called= false} method_called
+        in
+        {x with method_called}
+    | Empty | More ->
+        x
+
+
   let call_create lhs typ_name location ({created} as x) =
     let created_location =
       CreatedLocation.ByCreateMethod {location; typ_name; latest_callsite= location}
@@ -521,6 +532,8 @@ let map_no_return_called f x = {x with no_return_called= f x.no_return_called}
 
 let assign ~lhs ~rhs = map_no_return_called (Mem.assign ~lhs ~rhs)
 
+let assume_null x = map_no_return_called (Mem.assume_null x)
+
 let call_create lhs typ_name location = map_no_return_called (Mem.call_create lhs typ_name location)
 
 let call_builder ~ret ~receiver callee =

infer/src/checkers/LithoDomain.mli

@@ -53,6 +53,9 @@ val init : Tenv.t -> Procname.t -> (Pvar.t * Typ.t) list -> LocalAccessPath.t ->
 
 val assign : lhs:LocalAccessPath.t -> rhs:LocalAccessPath.t -> t -> t
 
+val assume_null : LocalAccessPath.t -> t -> t
+(** Semantics of null assume statement, i.e., [assume(x==null)] *)
+
 val call_create : LocalAccessPath.t -> Typ.name -> Location.t -> t -> t
 (** Semantics of builder creation method *)
 

infer/src/checkers/RequiredProps.ml

@@ -206,6 +206,13 @@ module TransferFunctions = struct
           ~caller:astate ~callee:callee_summary )
 
 
+  let assume_null caller_pname x astate =
+    let access_path =
+      Domain.LocalAccessPath.make (HilExp.AccessExpression.to_access_path x) caller_pname
+    in
+    Domain.assume_null access_path astate
+
+
   let exec_instr astate {interproc= {proc_desc; tenv}; get_proc_summary_and_formals} _
       (instr : HilInstr.t) : Domain.t =
     let caller_pname = Procdesc.get_proc_name proc_desc in
@@ -270,6 +277,18 @@ module TransferFunctions = struct
               astate
         in
         if HilExp.AccessExpression.is_return_var lhs_ae then Domain.call_return astate else astate
+    | Assume (BinaryOperator (Eq, AccessExpression x, null), _, _, _)
+      when HilExp.is_null_literal null ->
+        assume_null caller_pname x astate
+    | Assume (BinaryOperator (Eq, null, AccessExpression x), _, _, _)
+      when HilExp.is_null_literal null ->
+        assume_null caller_pname x astate
+    | Assume (UnaryOperator (LNot, BinaryOperator (Ne, AccessExpression x, null), _), _, _, _)
+      when HilExp.is_null_literal null ->
+        assume_null caller_pname x astate
+    | Assume (UnaryOperator (LNot, BinaryOperator (Ne, null, AccessExpression x), _), _, _, _)
+      when HilExp.is_null_literal null ->
+        assume_null caller_pname x astate
     | _ ->
         astate
 

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

@@ -521,4 +521,36 @@ public class RequiredProps {
     builder1.prop1(new Object()).prop3(new Object()).build();
     builder2.prop3(new Object()).build();
   }
+
+  public void nullableBuilderOk(boolean b) {
+    MyComponent.Builder builderOk =
+        mMyComponent.create().prop1(new Object()).prop2(new Object()).prop3(new Object());
+    MyComponent.Builder builder = null;
+    if (b) {
+      builder = mMyComponent.create().prop1(new Object()).prop2(new Object());
+    }
+    (builder == null ? builderOk : builder.prop3(new Object())).build();
+  }
+
+  public void nullableBuilderBad(boolean b) {
+    MyComponent.Builder builderOk =
+        mMyComponent.create().prop1(new Object()).prop2(new Object()).prop3(new Object());
+    MyComponent.Builder builder = null;
+    if (b) {
+      builder = mMyComponent.create().prop2(new Object());
+    }
+    (builder == null ? builderOk : builder.prop3(new Object())).build();
+  }
+
+  public void nullableBuilderAliasOk_FP(boolean b) {
+    MyComponent.Builder builder =
+        mMyComponent.create().prop1(new Object()).prop2(new Object()).prop3(new Object());
+    MyComponent.Builder alias = builder;
+    if (b) {
+      builder = null;
+    }
+    if (builder == null) {
+      alias.build();
+    }
+  }
 }

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

@@ -26,6 +26,9 @@ codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.l
 codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.missingProp1InBothBranchesBeforeBuildBad(boolean):com.facebook.litho.Component, 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(...)]
 codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.missingProp2InOneBranchBeforeBuildBad(boolean):com.facebook.litho.Component, 4, 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(...),calls prop1(...)]
 codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.missingProp3InOneBranchBeforeBuildBad(boolean):com.facebook.litho.Component, 3, 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.nullableBuilderAliasOk_FP(boolean):void, 2, 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.nullableBuilderAliasOk_FP(boolean):void, 2, 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.nullableBuilderBad(boolean):void, 5, 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.setProp3InCalleeButForgetProp1Bad():com.facebook.litho.Component, 1, 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.setRequiredOnBothBranchesMissingProp3Bad(boolean):com.facebook.litho.Component, 1, 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.setRequiredOnOneBothBranchesWithCreateOk_FP(boolean):com.facebook.litho.Component, 1, 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(...)]