From f719294d41b6925ed39bff7b1ca7892a42964b8a Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Fri, 5 Mar 2021 03:32:56 -0800 Subject: [PATCH] [pulse] Model for TextUtils.isEmpty() Summary: Providing model for the android function TextUtils.isEmpty(). For now, this always returns false assuming that the given value is not null. Reviewed By: jvillard Differential Revision: D26779619 fbshipit-source-id: 3d8e26813 --- infer/src/pulse/PulseModels.ml | 19 +++++++++ .../java/pulse/TextUtilsExample.java | 40 +++++++++++++++++++ .../tests/codetoanalyze/java/pulse/issues.exp | 4 ++ 3 files changed, 63 insertions(+) create mode 100644 infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index c62a3b7bb..ffbf362f4 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -1078,6 +1078,22 @@ module JavaPreconditions = struct PulseArithmetic.prune_positive address astate |> ok_continue end +module Android = struct + let text_utils_is_empty ~desc (address, hist) : model = + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let ret_val = AbstractValue.mk_fresh () in + let astate = PulseOperations.write_id ret_id (ret_val, event :: hist) astate in + let astate_equal_zero = + PulseArithmetic.and_eq_int ret_val IntLit.zero astate + |> PulseArithmetic.prune_positive address + in + let astate_not_zero = + PulseArithmetic.and_eq_int ret_val IntLit.one astate |> PulseArithmetic.prune_eq_zero address + in + [Ok (ContinueProgram astate_equal_zero); Ok (ContinueProgram astate_not_zero)] +end + module StringSet = Caml.Set.Make (String) module ProcNameDispatcher = struct @@ -1411,6 +1427,9 @@ module ProcNameDispatcher = struct &:: "nextElement" <>$ capt_arg_payload $!--> fun x -> StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) ) + ; +map_context_tenv (PatternMatch.Java.implements_android "text.TextUtils") + &:: "isEmpty" <>$ capt_arg_payload + $--> Android.text_utils_is_empty ~desc:"TextUtils.isEmpty" ; -"dispatch_sync" &++> ObjC.dispatch_sync ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_create_or_copy &--> C.malloc_no_param diff --git a/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java b/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java new file mode 100644 index 000000000..e397cd879 --- /dev/null +++ b/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java @@ -0,0 +1,40 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +import android.text.TextUtils; + +public class TextUtilsExample { + + public void FP_testTextUtilsIsEmptyOk(String s) { + if (TextUtils.isEmpty(s)) { + Object o = null; + o.toString(); + } + } + + public void testTextUtilsIsEmptyBad() { + String s = "#@%^&%"; + if (!TextUtils.isEmpty(s)) { + Object o = null; + o.toString(); + } + } + + public void testTextUtilsIsEmptyEmptyStrBad() { + if (TextUtils.isEmpty("")) { + Object o = null; + o.toString(); + } + } + + public void testTextUtilsIsEmptyNullBad() { + String s = null; + if (TextUtils.isEmpty(s)) { + Object o = null; + o.toString(); + } + } +} diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 6120fba98..ef4d4d1e4 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -60,3 +60,7 @@ codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.Supp codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.(), 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.FP_shouldNotReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.shouldReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.FP_testTextUtilsIsEmptyOk(java.lang.String):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyEmptyStrBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyNullBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]