From 319e3ed271e81618bdd809823c2dbb9e065e2794 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Fri, 3 Feb 2017 11:16:25 -0800 Subject: [PATCH] [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 | 8 +++- infer/src/eradicate/typeOrigin.ml | 9 +++- infer/src/eradicate/typeState.ml | 37 ++++++++++------ .../java/eradicate/FieldNotInitialized.java | 42 +++++++++++++++++++ .../java/eradicate/ReturnNotNullable.java | 10 +++++ .../codetoanalyze/java/eradicate/issues.exp | 2 + 6 files changed, 91 insertions(+), 17 deletions(-) diff --git a/infer/src/eradicate/typeAnnotation.ml b/infer/src/eradicate/typeAnnotation.ml index d8bbf715c..e35101305 100644 --- a/infer/src/eradicate/typeAnnotation.ml +++ b/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 diff --git a/infer/src/eradicate/typeOrigin.ml b/infer/src/eradicate/typeOrigin.ml index 5a03c32fe..f8e0bbb4b 100644 --- a/infer/src/eradicate/typeOrigin.ml +++ b/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 diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml index 69530adf0..24dd62f4a 100644 --- a/infer/src/eradicate/typeState.ml +++ b/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) diff --git a/infer/tests/codetoanalyze/java/eradicate/FieldNotInitialized.java b/infer/tests/codetoanalyze/java/eradicate/FieldNotInitialized.java index 69758c6dd..232ca40c7 100644 --- a/infer/tests/codetoanalyze/java/eradicate/FieldNotInitialized.java +++ b/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(); + } + } + } diff --git a/infer/tests/codetoanalyze/java/eradicate/ReturnNotNullable.java b/infer/tests/codetoanalyze/java/eradicate/ReturnNotNullable.java index 5830cb448..0401d4ad8 100644 --- a/infer/tests/codetoanalyze/java/eradicate/ReturnNotNullable.java +++ b/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 + } + } } diff --git a/infer/tests/codetoanalyze/java/eradicate/issues.exp b/infer/tests/codetoanalyze/java/eradicate/issues.exp index 4000f4552..9fb31f6a7 100644 --- a/infer/tests/codetoanalyze/java/eradicate/issues.exp +++ b/infer/tests/codetoanalyze/java/eradicate/issues.exp @@ -1,4 +1,5 @@ codetoanalyze/java/eradicate/ActivityFieldNotInitialized.java, ActivityFieldNotInitialized$BadActivityWithOnCreate.(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.(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.(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.(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.(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.]