[Eradicate] Change Eradicate's join to forget values not present on both paths

Reviewed By: jeremydubreil

Differential Revision: D4501036

fbshipit-source-id: 29fcb11

infer/src/eradicate/typeAnnotation.ml

@@ -63,7 +63,8 @@ let to_string ta =
   nullable_s ^ present_s
 
 let join ta1 ta2 =
-  let choose_left = match get_nullable ta1, get_nullable ta2 with
+  let nul1, nul2 = get_nullable ta1, get_nullable ta2 in
+  let choose_left = match nul1, nul2 with
     | false, true ->
         false
     | _ ->
@@ -71,7 +72,10 @@ let join ta1 ta2 =
   let ta_chosen, ta_other =
     if choose_left then ta1, ta2 else ta2, ta1 in
   let present = get_present ta1 && get_present ta2 in
-  let origin = TypeOrigin.join ta_chosen.origin ta_other.origin in
+  let origin =
+    if Bool.equal nul1 nul2
+    then TypeOrigin.join ta_chosen.origin ta_other.origin
+    else ta_chosen.origin in
   let ta' =
     set_present present
       { ta_chosen with

infer/src/eradicate/typeOrigin.ml

@@ -84,5 +84,10 @@ let get_description tenv origin =
 
 let join o1 o2 = match o1, o2 with (* left priority *)
   | Undef, _
-  | _, Undef -> Undef
-  | _ -> o1
+  | _, Undef ->
+      Undef
+  | Field _, (Const _ | Formal _ | Proc _ | New) ->
+      (* low priority to Field, to support field initialization patterns *)
+      o2
+  | _ ->
+      o1

infer/src/eradicate/typeState.ml

@@ -87,9 +87,13 @@ let range_add_locs (typ, ta, locs1) locs2 =
   let locs' = locs_join locs1 locs2 in
   (typ, ta, locs')
 
-(** Join m2 to m1 if there are no inconsistencies, otherwise return m1. *)
+(** Only keep variables if they are present on both sides of the join. *)
+let only_keep_intersection = true
+
+(** Join two maps.
+    If only_keep_intersection is true, keep only variables present on both sides. *)
 let map_join m1 m2 =
-  let tjoined = ref m1 in
+  let tjoined = ref (if only_keep_intersection then M.empty else m1) in
   let range_join (typ1, ta1, locs1) (typ2, ta2, locs2) =
     match TypeAnnotation.join ta1 ta2 with
     | None -> None
@@ -101,10 +105,11 @@ let map_join m1 m2 =
     try
       let range1 = M.find exp2 m1 in
       (match range_join range1 range2 with
-       | None -> ()
+       | None ->
+           if only_keep_intersection then tjoined := M.add exp2 range1 !tjoined
        | Some range' -> tjoined := M.add exp2 range' !tjoined)
     with Not_found ->
-      tjoined := M.add exp2 range2 !tjoined in
+      if not only_keep_intersection then tjoined := M.add exp2 range2 !tjoined in
   let missing_rhs exp1 range1 = (* handle elements missing in the rhs *)
     try
       ignore (M.find exp1 m2)
@@ -113,7 +118,7 @@ let map_join m1 m2 =
       let range1' =
         let ta1' = TypeAnnotation.with_origin ta1 TypeOrigin.Undef in
         (t1, ta1', locs1) in
-      tjoined := M.add exp1 range1' !tjoined in
+      if not only_keep_intersection then tjoined := M.add exp1 range1' !tjoined in
   if phys_equal m1 m2 then m1
   else (
     M.iter extend_lhs m2;
@@ -122,14 +127,20 @@ let map_join m1 m2 =
   )
 
 let join ext t1 t2 =
-  if Config.eradicate_debug
-  then L.stderr "@.@.**********join@.-------@.%a@.------@.%a@.********@.@."
-      (pp ext) t1
-      (pp ext) t2;
-  {
-    map = map_join t1.map t2.map;
-    extension = ext.join t1.extension t2.extension;
-  }
+  let tjoin =
+    {
+      map = map_join t1.map t2.map;
+      extension = ext.join t1.extension t2.extension;
+    } in
+  if Config.write_html then
+    begin
+      let s = F.asprintf "State 1:@.%a@.State 2:@.%a@.After Join:@.%a@."
+          (pp ext) t1
+          (pp ext) t2
+          (pp ext) tjoin in
+      L.d_strln s;
+    end;
+  tjoin
 
 let lookup_id id typestate =
   try Some (M.find (Exp.Var id) typestate.map)

infer/tests/codetoanalyze/java/eradicate/FieldNotInitialized.java

@@ -96,4 +96,46 @@ public class FieldNotInitialized {
       indirect();
     }
   }
+
+  class ConditionalFieldInit {
+    Object o1;
+    @Nullable Object o2 = null;
+    public ConditionalFieldInit() {
+        if (o2 != null) {
+            o1 = new Object(); // Not always initialized
+        }
+    }
+  }
+
+  class InitIfNull {
+    Object o;
+
+    public InitIfNull() {
+      if (o == null)
+        o = new Object();
+    }
+  }
+
+  class InitIfNull2 {
+    Object o;
+
+    public InitIfNull2(Object x) {
+      if (o == null)
+        o = x;
+    }
+  }
+
+  class InitIfNull3 {
+    Object o;
+
+    Object getNotNull() {
+      return new Object();
+    }
+
+    public InitIfNull3() {
+      if (o == null)
+        o = getNotNull();
+    }
+  }
+
 }

infer/tests/codetoanalyze/java/eradicate/ReturnNotNullable.java

@@ -136,4 +136,14 @@ public class ReturnNotNullable {
     definitelyDoesNotReturnNull().toString();
   }
 
+  static class ConditionalAssignment {
+    @Nullable Object f1;
+    static Object test(boolean b) {
+        ConditionalAssignment x = new ConditionalAssignment();
+        if (b) {
+            x.f1 = new Object();
+        }
+        return x.f1; // can be null
+    }
+  }
 }

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

@@ -1,4 +1,5 @@
 codetoanalyze/java/eradicate/ActivityFieldNotInitialized.java, ActivityFieldNotInitialized$BadActivityWithOnCreate.<init>(ActivityFieldNotInitialized), 0, ERADICATE_FIELD_NOT_INITIALIZED, [Field `ActivityFieldNotInitialized$BadActivityWithOnCreate.field` is not initialized in the constructor and is not declared `@Nullable`]
+codetoanalyze/java/eradicate/FieldNotInitialized.java, FieldNotInitialized$ConditionalFieldInit.<init>(FieldNotInitialized), 0, ERADICATE_FIELD_NOT_INITIALIZED, [Field `FieldNotInitialized$ConditionalFieldInit.o1` is not initialized in the constructor and is not declared `@Nullable`]
 codetoanalyze/java/eradicate/FieldNotInitialized.java, FieldNotInitialized$OnlyRead.<init>(FieldNotInitialized), 0, ERADICATE_FIELD_NOT_INITIALIZED, [Field `FieldNotInitialized$OnlyRead.o` is not initialized in the constructor and is not declared `@Nullable`]
 codetoanalyze/java/eradicate/FieldNotInitialized.java, FieldNotInitialized$OnlyReadIndirect.<init>(FieldNotInitialized), 0, ERADICATE_FIELD_NOT_INITIALIZED, [Field `FieldNotInitialized$OnlyReadIndirect.o1` is not initialized in the constructor and is not declared `@Nullable`]
 codetoanalyze/java/eradicate/FieldNotInitialized.java, FieldNotInitialized$Swap.<init>(FieldNotInitialized), 0, ERADICATE_FIELD_NOT_INITIALIZED, [Field `FieldNotInitialized$Swap.o1` is not initialized in the constructor and is not declared `@Nullable`]
@@ -41,6 +42,7 @@ codetoanalyze/java/eradicate/ParameterNotNullable.java, String ParameterNotNulla
 codetoanalyze/java/eradicate/ParameterNotNullable.java, URL ParameterNotNullable.testClassGetResourceArgument(Class), 1, ERADICATE_PARAMETER_NOT_NULLABLE, [origin,`getResource(...)` needs a non-null value in parameter 1 but argument `null` can be null. (Origin: null constant at line 76)]
 codetoanalyze/java/eradicate/ParameterNotNullable.java, void ParameterNotNullable.callNull(), 2, ERADICATE_PARAMETER_NOT_NULLABLE, [origin,`test(...)` needs a non-null value in parameter 1 but argument `s` can be null. (Origin: null constant at line 38)]
 codetoanalyze/java/eradicate/ParameterNotNullable.java, void ParameterNotNullable.callNullable(String), 1, ERADICATE_PARAMETER_NOT_NULLABLE, [`test(...)` needs a non-null value in parameter 1 but argument `s` can be null. (Origin: method parameter s)]
+codetoanalyze/java/eradicate/ReturnNotNullable.java, Object ReturnNotNullable$ConditionalAssignment.test(boolean), 0, ERADICATE_RETURN_NOT_NULLABLE, [origin,Method `test(...)` may return null but it is not annotated with `@Nullable`. (Origin: field ReturnNotNullable$ConditionalAssignment.f1 at line 146)]
 codetoanalyze/java/eradicate/ReturnNotNullable.java, Object ReturnNotNullable.tryWithResourcesReturnNullable(String), 0, ERADICATE_RETURN_NOT_NULLABLE, [origin,Method `tryWithResourcesReturnNullable(...)` may return null but it is not annotated with `@Nullable`. (Origin: call to returnNullOK() at line 91)]
 codetoanalyze/java/eradicate/ReturnNotNullable.java, String ReturnNotNullable.redundantEq(), 0, ERADICATE_RETURN_OVER_ANNOTATED, [Method `redundantEq()` is annotated with `@Nullable` but never returns null.]
 codetoanalyze/java/eradicate/ReturnNotNullable.java, String ReturnNotNullable.redundantEq(), 2, ERADICATE_CONDITION_REDUNDANT_NONNULL, [The condition s is always false according to the existing annotations.]