From 401109b4eb9d54ef8831ee953a3436ec3e2bb72e Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Tue, 8 Sep 2015 15:21:53 -0200 Subject: [PATCH] [Eradicate] Allow assigning null to fields marked @InjectView to support ButterKnife. --- infer/src/backend/abs.ml | 2 +- infer/src/backend/errdesc.ml | 16 ++++++------- infer/src/backend/procname.ml | 24 +++++++++---------- infer/src/backend/prop.ml | 6 ++--- infer/src/checkers/annotations.ml | 3 +++ infer/src/checkers/annotations.mli | 1 + infer/src/checkers/eradicateChecks.ml | 8 +++++-- infer/src/checkers/typeErr.ml | 8 +++---- .../java/eradicate/FieldNotNullable.java | 20 +++++++++++++++- 9 files changed, 57 insertions(+), 31 deletions(-) diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index b269cc981..cd4f54437 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1373,7 +1373,7 @@ let check_junk ?original_prop pname tenv prop = If it does, and [Config.allowleak] is true, remove the junk, otherwise raise a Leak exception. *) let abstract_junk ?original_prop pname tenv prop = Absarray.array_abstraction_performed := false; - check_junk ~original_prop: original_prop pname tenv prop + check_junk ~original_prop pname tenv prop (** Remove redundant elements in an array, and check for junk afterwards *) let remove_redundant_array_elements pname tenv prop = diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index b9a2c57aa..9b6fdd194 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -765,11 +765,11 @@ let create_dereference_desc if outermost_dereference is true, stop at the outermost dereference (skipping e.g. outermost field access) *) let _explain_access - ?use_buckets: (use_buckets = false) - ?outermost_array: (outermost_array = false) - ?outermost_dereference: (outermost_dereference = false) - ?is_nullable: (is_nullable = false) - ?is_premature_nil: (is_premature_nil = false) + ?(use_buckets = false) + ?(outermost_array = false) + ?(outermost_dereference = false) + ?(is_nullable = false) + ?(is_premature_nil = false) deref_str prop loc = let rec find_outermost_dereference node e = match e with | Sil.Const c -> @@ -830,9 +830,9 @@ let _explain_access (** Produce a description of which expression is dereferenced in the current instruction, if any. The subexpression to focus on is obtained by removing field and index accesses. *) let explain_dereference - ?use_buckets: (use_buckets = false) - ?is_nullable: (is_nullable = false) - ?is_premature_nil: (is_premature_nil = false) + ?(use_buckets = false) + ?(is_nullable = false) + ?(is_premature_nil = false) deref_str prop loc = _explain_access ~use_buckets ~outermost_array: false ~outermost_dereference: true ~is_nullable ~is_premature_nil diff --git a/infer/src/backend/procname.ml b/infer/src/backend/procname.ml index cb77462e5..8f7717bf4 100644 --- a/infer/src/backend/procname.ml +++ b/infer/src/backend/procname.ml @@ -1,12 +1,12 @@ (* -* Copyright (c) 2009 - 2013 Monoidics ltd. -* Copyright (c) 2013 - present Facebook, Inc. -* All rights reserved. -* -* This source code is licensed under the BSD style license found in the -* LICENSE file in the root directory of this source tree. An additional grant -* of patent rights can be found in the PATENTS file in the same directory. -*) + * Copyright (c) 2009 - 2013 Monoidics ltd. + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) (** Module for Procedure Names *) @@ -257,7 +257,7 @@ let java_is_static = function | _ -> assert false (** Prints a string of a java procname with the given level of verbosity *) -let java_to_string ?withclass: (wc = false) j verbosity = +let java_to_string ?(withclass = false) j verbosity = match verbosity with | VERBOSE | NON_VERBOSE -> (* if verbose, then package.class.method(params): rtype, @@ -276,7 +276,7 @@ let java_to_string ?withclass: (wc = false) j verbosity = else return_type ^ separator ^ output | SIMPLE -> (* methodname(...) or without ... if there are no parameters *) let cls_prefix = - if wc then + if withclass then java_type_to_string j.classname verbosity ^ "." else "" in let params = @@ -406,9 +406,9 @@ let to_string p = | OBJC_BLOCK name -> name (** Convenient representation of a procname for external tools (e.g. eclipse plugin) *) -let to_simplified_string ?withclass: (wc = false) p = +let to_simplified_string ?(withclass = false) p = match p with - | JAVA j -> (java_to_string ~withclass: wc j SIMPLE) + | JAVA j -> (java_to_string ~withclass j SIMPLE) | C_FUNCTION (c1, c2) | STATIC (c1, c2) -> to_readable_string (c1, c2) false ^ "()" | C_METHOD osig -> c_method_to_string osig SIMPLE diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 49de9629c..d2de57100 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1662,7 +1662,7 @@ let rec prop_atom_and ?(footprint = false) (p : normal t) (a : Sil.atom) : norma (sub_normalize sub', pi_normalize sub' nsigma' p.pi, nsigma') in let (eqs_zero, nsigma'') = sigma_remove_emptylseg nsigma' in let p' = { p with sub = nsub'; pi = npi'; sigma = nsigma''} in - list_fold_left (prop_atom_and ~footprint: footprint) p' eqs_zero + list_fold_left (prop_atom_and ~footprint) p' eqs_zero | Sil.Aeq (e1, e2) when (Sil.exp_compare e1 e2 = 0) -> p | Sil.Aneq (e1, e2) -> @@ -1697,11 +1697,11 @@ let rec prop_atom_and ?(footprint = false) (p : normal t) (a : Sil.atom) : norma (** Conjoin [exp1]=[exp2] with a symbolic heap [prop]. *) let conjoin_eq ?(footprint = false) exp1 exp2 prop = - prop_atom_and ~footprint: footprint prop (Sil.Aeq(exp1, exp2)) + prop_atom_and ~footprint prop (Sil.Aeq(exp1, exp2)) (** Conjoin [exp1!=exp2] with a symbolic heap [prop]. *) let conjoin_neq ?(footprint = false) exp1 exp2 prop = - prop_atom_and ~footprint: footprint prop (Sil.Aneq (exp1, exp2)) + prop_atom_and ~footprint prop (Sil.Aneq (exp1, exp2)) (** Return the spatial part *) let get_sigma (p: 'a t) : Sil.hpred list = p.sigma diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index d15156c2b..73f034565 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -127,6 +127,9 @@ let ia_is_inject ia = (ia_ends_with ia) [inject; inject_view; bind] +let ia_is_inject_view ia = + ia_ends_with ia inject_view + let ia_is_mutable ia = ia_ends_with ia mutable_ diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index 78611aaa4..5f89b41e6 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -59,6 +59,7 @@ val ia_get_strict : Sil.item_annotation -> Sil.annotation option val ia_is_initializer : Sil.item_annotation -> bool val ia_is_inject : Sil.item_annotation -> bool +val ia_is_inject_view : Sil.item_annotation -> bool val ia_is_mutable : Sil.item_annotation -> bool val ia_is_nullable : Sil.item_annotation -> bool val ia_is_nonnull : Sil.item_annotation -> bool diff --git a/infer/src/checkers/eradicateChecks.ml b/infer/src/checkers/eradicateChecks.ml index bec28b30d..16c5b4037 100644 --- a/infer/src/checkers/eradicateChecks.ml +++ b/infer/src/checkers/eradicateChecks.ml @@ -195,10 +195,14 @@ let check_field_assignment typecheck_expr node instr_ref curr_pname typestate exp_rhs (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) loc in let should_report_nullable = + let field_is_inject_view () = match t_ia_opt with + | Some (_, ia) -> Annotations.ia_is_inject_view ia + | _ -> false in TypeAnnotation.get_value Annotations.Nullable ta_lhs = false && TypeAnnotation.get_value Annotations.Nullable ta_rhs = true && PatternMatch.type_is_class t_lhs && - not (Ident.java_fieldname_is_outer_instance fname) in + not (Ident.java_fieldname_is_outer_instance fname) && + not (field_is_inject_view ()) in let should_report_absent = activate_optional_present && TypeAnnotation.get_value Annotations.Present ta_lhs = true && @@ -207,7 +211,7 @@ let check_field_assignment let should_report_mutable = let field_is_mutable () = match t_ia_opt with | Some (_, ia) -> Annotations.ia_is_mutable ia - | _ -> true in + | _ -> false in activate_field_not_mutable && not (Procname.is_constructor curr_pname) && not (Procname.is_class_initializer curr_pname) && diff --git a/infer/src/checkers/typeErr.ml b/infer/src/checkers/typeErr.ml index 4435b8666..1c34d7a6b 100644 --- a/infer/src/checkers/typeErr.ml +++ b/infer/src/checkers/typeErr.ml @@ -509,11 +509,11 @@ let report_error_now (Cfg.Node.get_proc_desc node) kind_s loc - ~advice: advice - ~field_name: field_name - ~origin_loc: origin_loc + ~advice + ~field_name + ~origin_loc ~exception_kind: (fun k d -> Exceptions.Eradicate (k, d)) - ~always_report: always_report + ~always_report description diff --git a/infer/tests/codetoanalyze/java/eradicate/FieldNotNullable.java b/infer/tests/codetoanalyze/java/eradicate/FieldNotNullable.java index 0648b2e9b..d25b7a91d 100644 --- a/infer/tests/codetoanalyze/java/eradicate/FieldNotNullable.java +++ b/infer/tests/codetoanalyze/java/eradicate/FieldNotNullable.java @@ -28,8 +28,10 @@ abstract class A { } } -public class FieldNotNullable extends A { +// for butterknife +@interface InjectView {} +public class FieldNotNullable extends A { @Nullable String x; String y; @@ -362,4 +364,20 @@ class NestedFieldAccess { } } + // support assignments of null to @InjectView fields, generated by butterknife + class SupportButterKnife { + @InjectView String s; + + SupportButterKnife() { + } + + void dereferencingIsOK() { + int n = s.length(); + } + + void assignNullIsOK() { + s = null; + } + } + }