diff --git a/infer/annotations/com/facebook/infer/annotation/FalseOnNull.java b/infer/annotations/com/facebook/infer/annotation/FalseOnNull.java new file mode 100644 index 000000000..668788c81 --- /dev/null +++ b/infer/annotations/com/facebook/infer/annotation/FalseOnNull.java @@ -0,0 +1,22 @@ +/* +* Copyright (c) 2015 - 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. +*/ + +package com.facebook.infer.annotation; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * Annotation for a boolean function returning false when the argument is null. + */ +@Retention(RetentionPolicy.CLASS) +@Target({ElementType.METHOD}) +public @interface FalseOnNull {} diff --git a/infer/annotations/com/facebook/infer/annotation/TrueOnNull.java b/infer/annotations/com/facebook/infer/annotation/TrueOnNull.java new file mode 100644 index 000000000..5ed7e0ddf --- /dev/null +++ b/infer/annotations/com/facebook/infer/annotation/TrueOnNull.java @@ -0,0 +1,22 @@ +/* +* Copyright (c) 2015 - 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. +*/ + +package com.facebook.infer.annotation; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * Annotation for a boolean function returning true when the argument is null. + */ +@Retention(RetentionPolicy.CLASS) +@Target({ElementType.METHOD}) +public @interface TrueOnNull {} diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index 73f034565..99be090a1 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -99,6 +99,7 @@ let initializer_ = "Initializer" let inject = "Inject" let inject_view = "InjectView" let bind = "Bind" +let false_on_null = "FalseOnNull" let mutable_ = "Mutable" let nullable = "Nullable" let nonnull = "Nonnull" @@ -106,6 +107,7 @@ let camel_nonnull = "NonNull" let notnull = "NotNull" let present = "Present" let strict = "com.facebook.infer.annotation.Strict" +let true_on_null = "TrueOnNull" let verify_annotation = "com.facebook.infer.annotation.Verify" let ia_is_nullable ia = @@ -119,6 +121,12 @@ let ia_is_nonnull ia = (ia_ends_with ia) [nonnull; notnull; camel_nonnull] +let ia_is_false_on_null ia = + ia_ends_with ia false_on_null + +let ia_is_true_on_null ia = + ia_ends_with ia true_on_null + let ia_is_initializer ia = ia_ends_with ia initializer_ diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index 5f89b41e6..b071158d4 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -57,13 +57,15 @@ val ia_has_annotation_with : Sil.item_annotation -> (Sil.annotation -> bool) -> val ia_get_strict : Sil.item_annotation -> Sil.annotation option +val ia_is_false_on_null : Sil.item_annotation -> bool 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 +val ia_is_nullable : Sil.item_annotation -> bool val ia_is_present : Sil.item_annotation -> bool +val ia_is_true_on_null : Sil.item_annotation -> bool val ia_is_verify : Sil.item_annotation -> bool val ia_iter : (Sil.annotation -> unit) -> Sil.item_annotation -> unit diff --git a/infer/src/checkers/eradicateChecks.ml b/infer/src/checkers/eradicateChecks.ml index 16c5b4037..3156ea98b 100644 --- a/infer/src/checkers/eradicateChecks.ml +++ b/infer/src/checkers/eradicateChecks.ml @@ -115,6 +115,8 @@ let check_array_access type from_call = | From_condition (** Direct condition *) | From_instanceof (** x instanceof C *) + | From_is_false_on_null (** returns false on null *) + | From_is_true_on_null (** returns true on null *) | From_optional_isPresent (** x.isPresent *) | From_containsKey (** x.containsKey *) diff --git a/infer/src/checkers/modelTables.ml b/infer/src/checkers/modelTables.ml index 279e13799..112f851ce 100644 --- a/infer/src/checkers/modelTables.ml +++ b/infer/src/checkers/modelTables.ml @@ -1,11 +1,11 @@ (* -* 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) 2015 - 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. + *) (* * This file is a big bunch of tables; they read better with really long lines. @@ -89,6 +89,13 @@ let optional_isPresent_list : ((_ * bool list) * _) list = (o, []), "com.google.common.base.Optional.isPresent():boolean"; ] +(** Models for boolean functions that return true on null. *) +let true_on_null_list : ((_ * bool list) * _) list = + [ + n1, "android.text.TextUtils.isEmpty(java.lang.CharSequence):boolean"; + ] + + (** Models for Map.containsKey *) let containsKey_list = [ @@ -226,6 +233,7 @@ let check_not_null_table, check_not_null_parameter_table = mk_table check_not_null_list, mk_table check_not_null_parameter_list let check_state_table = mk_table check_state_list let check_argument_table = mk_table check_argument_list +let containsKey_table = mk_table containsKey_list let optional_get_table = mk_table optional_get_list let optional_isPresent_table = mk_table optional_isPresent_list -let containsKey_table = mk_table containsKey_list +let true_on_null_table = mk_table true_on_null_list diff --git a/infer/src/checkers/modelTables.mli b/infer/src/checkers/modelTables.mli index 87d4dce61..731feede0 100644 --- a/infer/src/checkers/modelTables.mli +++ b/infer/src/checkers/modelTables.mli @@ -1,6 +1,11 @@ (* -* Copyright (c) 2013 - Facebook. All rights reserved. -*) + * Copyright (c) 2015 - 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. + *) type model_table_t = (string, bool * bool list) Hashtbl.t @@ -11,6 +16,7 @@ val check_not_null_table : model_table_t val check_not_null_parameter_table : (string, int) Hashtbl.t val check_state_table : model_table_t val check_argument_table : model_table_t +val containsKey_table : model_table_t val optional_get_table : model_table_t val optional_isPresent_table : model_table_t -val containsKey_table : model_table_t +val true_on_null_table : model_table_t diff --git a/infer/src/checkers/models.ml b/infer/src/checkers/models.ml index 3a6e3754b..1b3b26c54 100644 --- a/infer/src/checkers/models.ml +++ b/infer/src/checkers/models.ml @@ -217,6 +217,11 @@ let is_optional_get proc_name = let is_optional_isPresent proc_name = table_has_procedure optional_isPresent_table proc_name +(** Check if the procedure returns true on null. *) +let is_true_on_null proc_name = + table_has_procedure true_on_null_table proc_name + + (** Check if the procedure is Map.containsKey(). *) let is_containsKey proc_name = table_has_procedure containsKey_table proc_name diff --git a/infer/src/checkers/typeAnnotation.mli b/infer/src/checkers/typeAnnotation.mli index 560904871..f42bd8f3c 100644 --- a/infer/src/checkers/typeAnnotation.mli +++ b/infer/src/checkers/typeAnnotation.mli @@ -22,5 +22,6 @@ val get_origin : t -> TypeOrigin.t val get_value : Annotations.annotation -> t -> bool val join : t -> t -> t option val origin_is_fun_library : t -> bool +val set_value : Annotations.annotation -> bool -> t -> t val to_string : t -> string val with_origin : t -> TypeOrigin.t -> t diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml index a187d7cef..a2c6a6d76 100644 --- a/infer/src/checkers/typeCheck.ml +++ b/infer/src/checkers/typeCheck.ml @@ -44,12 +44,40 @@ module ComplexExpressions = struct let procname_optional_isPresent = Models.is_optional_isPresent let procname_instanceof = Procname.equal SymExec.ModelBuiltins.__instanceof + + let procname_is_false_on_null get_proc_desc pn = + match get_proc_desc pn with + | Some pdesc -> + let proc_attributes = Specs.pdesc_resolve_attributes pdesc in + let annotated_signature = + Models.get_modelled_annotated_signature proc_attributes in + let ret_ann, _ = annotated_signature.Annotations.ret in + Annotations.ia_is_false_on_null ret_ann + | None -> + false + + let procname_is_true_on_null get_proc_desc pn = + let annotated_true_on_null () = + match get_proc_desc pn with + | Some pdesc -> + let proc_attributes = Specs.pdesc_resolve_attributes pdesc in + let annotated_signature = + Models.get_modelled_annotated_signature proc_attributes in + let ret_ann, _ = annotated_signature.Annotations.ret in + Annotations.ia_is_true_on_null ret_ann + | None -> + false in + Models.is_true_on_null pn || + annotated_true_on_null () + let procname_containsKey = Models.is_containsKey (** Recognize *all* the procedures treated specially in conditionals *) - let procname_used_in_condition pn = + let procname_used_in_condition get_proc_desc pn = procname_optional_isPresent pn || procname_instanceof pn || + procname_is_false_on_null get_proc_desc pn || + procname_is_true_on_null get_proc_desc pn || procname_containsKey pn || SymExec.function_is_builtin pn @@ -283,7 +311,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc let handle_function_call call_node id = match Errdesc.find_normal_variable_funcall call_node id with | Some (Sil.Const (Sil.Cfun pn), _, _, _) - when not (ComplexExpressions.procname_used_in_condition pn) -> + when not (ComplexExpressions.procname_used_in_condition get_proc_desc pn) -> begin match ComplexExpressions.exp_to_string node' exp with | None -> default @@ -780,6 +808,14 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc let from_optional_isPresent e : Sil.exp option = from_call ComplexExpressions.procname_optional_isPresent e in + (* check if the expression is coming from a procedure returning false on null *) + let from_is_false_on_null e : Sil.exp option = + from_call (ComplexExpressions.procname_is_false_on_null get_proc_desc) e in + + (* check if the expression is coming from a procedure returning true on null *) + let from_is_true_on_null e : Sil.exp option = + from_call (ComplexExpressions.procname_is_true_on_null get_proc_desc) e in + (* check if the expression is coming from Map.containsKey *) let from_containsKey e : Sil.exp option = from_call ComplexExpressions.procname_containsKey e in @@ -812,23 +848,53 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc typestate, e, EradicateChecks.From_condition end in + let set_flag e' ann b typestate2 = (* add constraint on e' for annotation ann *) + let handle_pvar typestate' pvar = + match TypeState.lookup_pvar pvar typestate' with + | Some (t, ta1, locs) -> + if TypeAnnotation.get_value ann ta1 <> b then + let ta2 = TypeAnnotation.set_value ann b ta1 in + TypeState.add_pvar pvar (t, ta2, locs) typestate' + else typestate' + | None -> typestate' in + match e' with + | Sil.Lvar pvar -> + pvar_apply loc handle_pvar typestate2 pvar + | _ -> typestate2 in match c with | Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e) | Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i -> typecheck_expr_for_errors typestate e loc; - let e', typestate' = convert_complex_exp_to_pvar node' false e typestate loc in + let typestate1, e1, from_call = match from_is_true_on_null e with + | Some e1 -> + typestate, e1, EradicateChecks.From_is_true_on_null + | None -> + typestate, e, EradicateChecks.From_condition in + let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in let (typ, ta, _) = - typecheck_expr_simple typestate' e' Sil.Tvoid TypeOrigin.ONone loc in + typecheck_expr_simple typestate2 e' Sil.Tvoid TypeOrigin.ONone loc in + if checks.eradicate then EradicateChecks.check_zero find_canonical_duplicate get_proc_desc curr_pname node' e' typ ta true_branch EradicateChecks.From_condition idenv linereader loc instr_ref; - typestate' + begin + match from_call with + | EradicateChecks.From_is_true_on_null -> + (* if f returns true on null, then false branch implies != null *) + if TypeAnnotation.get_value Annotations.Nullable ta + then set_flag e' Annotations.Nullable false typestate2 + else typestate2 + | _ -> + typestate2 + end + | Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e) | Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i -> + typecheck_expr_for_errors typestate e loc; let typestate1, e1, from_call = match from_instanceof e with | Some e1 -> (* (e1 instanceof C) implies (e1 != null) *) typestate, e1, EradicateChecks.From_instanceof @@ -839,33 +905,23 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc typestate, e1, EradicateChecks.From_optional_isPresent | None -> begin - match from_containsKey e with - | Some e1 when ComplexExpressions.functions_idempotent () -> - handle_containsKey e - | _ -> - typestate, e, EradicateChecks.From_condition + match from_is_false_on_null e with + | Some e1 -> + typestate, e1, EradicateChecks.From_is_false_on_null + | None -> + begin + match from_containsKey e with + | Some e1 when ComplexExpressions.functions_idempotent () -> + handle_containsKey e + | _ -> + typestate, e, EradicateChecks.From_condition + end end end in - typecheck_expr_for_errors typestate1 e1 loc; let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in let (typ, ta, _) = typecheck_expr_simple typestate2 e' Sil.Tvoid TypeOrigin.ONone loc in - let set_flag e' ann b = (* add constraint on e' for annotation ann *) - let handle_pvar typestate' pvar = - match TypeState.lookup_pvar pvar typestate' with - | Some (t, ta1, locs) -> - if TypeAnnotation.get_value ann ta1 <> b then - let origin = TypeAnnotation.get_origin ta1 in - let ta2 = TypeAnnotation.const ann b origin in - TypeState.add_pvar pvar (t, ta2, locs) typestate' - else typestate' - | None -> typestate' in - match e' with - | Sil.Lvar pvar -> - pvar_apply loc handle_pvar typestate2 pvar - | _ -> typestate2 in - if checks.eradicate then EradicateChecks.check_nonzero find_canonical_duplicate get_proc_desc curr_pname node e' typ ta true_branch from_call idenv linereader loc instr_ref; @@ -873,13 +929,16 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc match from_call with | EradicateChecks.From_optional_isPresent -> if TypeAnnotation.get_value Annotations.Present ta = false - then set_flag e' Annotations.Present true + then set_flag e' Annotations.Present true typestate2 else typestate2 + | EradicateChecks.From_is_true_on_null -> + typestate2 | EradicateChecks.From_condition + | EradicateChecks.From_containsKey | EradicateChecks.From_instanceof - | EradicateChecks.From_containsKey -> + | EradicateChecks.From_is_false_on_null -> if TypeAnnotation.get_value Annotations.Nullable ta then - set_flag e' Annotations.Nullable false + set_flag e' Annotations.Nullable false typestate2 else typestate2 end diff --git a/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java b/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java index 9d533953a..6a544623d 100644 --- a/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java +++ b/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java @@ -9,11 +9,14 @@ package codetoanalyze.java.eradicate; +import android.text.TextUtils; import com.google.common.base.Preconditions; import java.lang.System; import javax.annotation.Nullable; import com.facebook.infer.annotation.Assertions; +import com.facebook.infer.annotation.FalseOnNull; +import com.facebook.infer.annotation.TrueOnNull; public class NullMethodCall { @@ -239,5 +242,55 @@ public class NullMethodCall { int n = s.length(); } + + static class MyTextUtils { + + @TrueOnNull + static boolean isEmpty(@Nullable java.lang.CharSequence s) { + return s == null || s.equals(""); + } + + @FalseOnNull + static boolean isNotEmpty(@Nullable java.lang.CharSequence s) { + return s != null && s.length() > 0; + } + } + + class TestTextUtilsIsEmpty { + void textUtilsNotIsEmpty(@Nullable CharSequence s) { + if (!TextUtils.isEmpty(s)) { + s.toString(); // OK + } + } + + void textUtilsIsEmpty(@Nullable CharSequence s) { + if (TextUtils.isEmpty(s)) { + s.toString(); // BAD + } + } + + void myTextUtilsNotIsEmpty(@Nullable CharSequence s) { + if (!MyTextUtils.isEmpty(s)) { + s.toString(); // OK + } + } + + void myTextUtilsIsEmpty(@Nullable CharSequence s) { + if (MyTextUtils.isEmpty(s)) { + s.toString(); // BAD + } + } + void myTextUtilsIsNotEmpty(@Nullable CharSequence s) { + if (MyTextUtils.isNotEmpty(s)) { + s.toString(); // OK + } + } + + void myTextUtilsNotIsNotEmpty(@Nullable CharSequence s) { + if (!MyTextUtils.isNotEmpty(s)) { + s.toString(); // BAD + } + } + } } diff --git a/infer/tests/endtoend/java/eradicate/NullMethodCallTest.java b/infer/tests/endtoend/java/eradicate/NullMethodCallTest.java index 9d6787823..9c9e70f93 100644 --- a/infer/tests/endtoend/java/eradicate/NullMethodCallTest.java +++ b/infer/tests/endtoend/java/eradicate/NullMethodCallTest.java @@ -46,6 +46,9 @@ public class NullMethodCallTest { "testFieldAssignmentIfThenElse", "testExceptionPerInstruction", "testSystemGetPropertyReturn", + "textUtilsIsEmpty", + "myTextUtilsIsEmpty", + "myTextUtilsNotIsNotEmpty", }; assertThat( "Results should contain " + NULL_METHOD_CALL,