From 3f8ee7df493f951bf34fe43096cae091310ebd26 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Mon, 23 Jan 2017 09:33:48 -0800 Subject: [PATCH] [Eradicate] Fix issue in Eradicate's check for field initialization Summary: Eradicate currently considers a field initialized if it's simply accessed (not written to), or initialized with another initialized field. This fixes the issue. Reviewed By: jvillard Differential Revision: D4449541 fbshipit-source-id: 06265a8 --- infer/src/eradicate/eradicateChecks.ml | 12 ++++- .../java/eradicate/FieldNotInitialized.java | 52 +++++++++++++++++++ .../codetoanalyze/java/eradicate/issues.exp | 4 ++ 3 files changed, 67 insertions(+), 1 deletion(-) diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml index 95b8db5a6..82fd1bd1d 100644 --- a/infer/src/eradicate/eradicateChecks.ml +++ b/infer/src/eradicate/eradicateChecks.ml @@ -259,10 +259,20 @@ let check_constructor_initialization tenv list in let may_be_assigned_in_final_typestate = + let origin_is_initialized = function + | TypeOrigin.Undef -> + false + | TypeOrigin.Field (f, _) -> + (* field initialized with another field needing initialization *) + let circular = + IList.exists (fun (f', _, _) -> Ident.equal_fieldname f f') fields in + not circular + | _ -> + true in final_type_annotation_with false (Lazy.force final_initializer_typestates) - (fun ta -> TypeAnnotation.get_origin ta <> TypeOrigin.Undef) in + (fun ta -> origin_is_initialized (TypeAnnotation.get_origin ta)) in let may_be_nullable_in_final_typestate () = final_type_annotation_with diff --git a/infer/tests/codetoanalyze/java/eradicate/FieldNotInitialized.java b/infer/tests/codetoanalyze/java/eradicate/FieldNotInitialized.java index 3d1cf21b3..69758c6dd 100644 --- a/infer/tests/codetoanalyze/java/eradicate/FieldNotInitialized.java +++ b/infer/tests/codetoanalyze/java/eradicate/FieldNotInitialized.java @@ -44,4 +44,56 @@ public class FieldNotInitialized { f = null; // OK the framework could write null into the field g = null; // OK the framework could write null into the field } + + + class OnlyRead { + Object o; + + OnlyRead() { + Object x = o; // not initialized + } + } + + class WriteItself { + Object o; + + WriteItself() { + o = o; // not initialized + } + } + + class Swap { + Object o1; + Object o2; + + Swap() { + o1 = o2; // not initialized + o2 = new Object(); + } + } + + class SwapOK { + Object o1; + Object o2; + + SwapOK() { + o1 = new Object(); + o2 = o1; + } + } + + + class OnlyReadIndirect { + Object o1; + Object o2; + + private void indirect() { + Object x = o1; // not initialized + o2 = new Object(); + } + + OnlyReadIndirect() { + indirect(); + } + } } diff --git a/infer/tests/codetoanalyze/java/eradicate/issues.exp b/infer/tests/codetoanalyze/java/eradicate/issues.exp index d67f770d6..4000f4552 100644 --- a/infer/tests/codetoanalyze/java/eradicate/issues.exp +++ b/infer/tests/codetoanalyze/java/eradicate/issues.exp @@ -1,4 +1,8 @@ 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$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`] +codetoanalyze/java/eradicate/FieldNotInitialized.java, FieldNotInitialized$WriteItself.(FieldNotInitialized), 0, ERADICATE_FIELD_NOT_INITIALIZED, [Field `FieldNotInitialized$WriteItself.o` is not initialized in the constructor and is not declared `@Nullable`] codetoanalyze/java/eradicate/FieldNotInitialized.java, FieldNotInitialized.(), 0, ERADICATE_FIELD_NOT_INITIALIZED, [Field `FieldNotInitialized.a` is not initialized in the constructor and is not declared `@Nullable`] codetoanalyze/java/eradicate/FieldNotNullable.java, FieldNotNullable.(Integer), -25, ERADICATE_FIELD_NOT_NULLABLE, [origin,Field `FieldNotNullable.static_s` can be null but is not declared `@Nullable`. (Origin: null constant at line 39)] codetoanalyze/java/eradicate/FieldNotNullable.java, FieldNotNullable.(String), -2, ERADICATE_FIELD_NOT_NULLABLE, [origin,Field `FieldNotNullable.static_s` can be null but is not declared `@Nullable`. (Origin: null constant at line 39)]