From 724fbc4ad6becfdb109e70a5e8727d7f663abe4e Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 28 Jun 2021 01:26:40 -0700 Subject: [PATCH] [pulse] Revise semantics of TextUtils.is_empty Summary: There are two changes: 1/ Fix incorrect merge of two cases (empty and not-empty) ``` let<*> astate_equal_zero = ... in let<*> astate_not_zero = ... in [Ok (ContinueProgram astate_equal_zero); Ok (ContinueProgram astate_not_zero)] ``` This was an incorrect merge, because if there is an error in the former case `astate_equal_zero`, it doesn't even evaluate the latter case `astate_not_zero`. 2/ Cover all cases precisely. There are actually three cases to cover: * `TextUtils.is_empty(null) = true` * `TextUtils.is_empty("") = true` * `TextUtils.is_empty("abc") = false` However, in the previous model, it missed the second case. Reviewed By: jvillard Differential Revision: D29393579 fbshipit-source-id: e59d9a60d --- infer/src/pulse/PulseModels.ml | 39 +++++++++++++------ .../java/pulse/TextUtilsExample.java | 2 +- .../tests/codetoanalyze/java/pulse/issues.exp | 1 + .../codetoanalyze/java/pulse/issues.exp-isl | 1 + 4 files changed, 30 insertions(+), 13 deletions(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 502f6ff41..e5e5b8f0f 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -614,6 +614,8 @@ module JavaObject = struct PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate end +let string_length_access = HilExp.Access.FieldAccess PulseOperations.ModeledField.string_length + module StdBasicString = struct let internal_string = Fieldname.make @@ -623,8 +625,6 @@ module StdBasicString = struct let internal_string_access = HilExp.Access.FieldAccess internal_string - let string_length_access = HilExp.Access.FieldAccess PulseOperations.ModeledField.string_length - let to_internal_string path location bstring astate = PulseOperations.eval_access path Read location bstring internal_string_access astate @@ -1476,19 +1476,34 @@ module JavaPreconditions = struct end module Android = struct - let text_utils_is_empty ~desc (address, hist) : model = - fun {location; ret= ret_id, _} astate -> + let text_utils_is_empty ~desc ((addr, hist) as addr_hist) : model = + fun {path; 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 + let astate_null = + let<*> astate = PulseArithmetic.prune_eq_zero addr astate in + let<+> astate = PulseArithmetic.and_eq_int ret_val IntLit.one astate in + PulseOperations.write_id ret_id (ret_val, event :: hist) astate + in + let astate_not_null = + let<*> astate = PulseArithmetic.prune_positive addr astate in + let<*> astate, (len_addr, hist) = + PulseOperations.eval_access path Read location addr_hist string_length_access astate + in + let astate = PulseOperations.write_id ret_id (ret_val, event :: hist) astate in + let astate_empty = + let<*> astate = PulseArithmetic.prune_eq_zero len_addr astate in + let<+> astate = PulseArithmetic.and_eq_int ret_val IntLit.one astate in + astate + in + let astate_not_empty = + let<*> astate = PulseArithmetic.prune_positive len_addr astate in + let<+> astate = PulseArithmetic.and_eq_int ret_val IntLit.zero astate in + astate + in + List.rev_append astate_empty astate_not_empty in - [Ok (ContinueProgram astate_equal_zero); Ok (ContinueProgram astate_not_zero)] + List.rev_append astate_null astate_not_null end module StringSet = Caml.Set.Make (String) diff --git a/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java b/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java index 66f23b3f7..e397cd879 100644 --- a/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java +++ b/infer/tests/codetoanalyze/java/pulse/TextUtilsExample.java @@ -23,7 +23,7 @@ public class TextUtilsExample { } } - public void FN_testTextUtilsIsEmptyEmptyStrBad() { + public void testTextUtilsIsEmptyEmptyStrBad() { if (TextUtils.isEmpty("")) { Object o = null; o.toString(); diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 9d228f269..6f3863322 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -67,4 +67,5 @@ codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.Supp codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.shouldReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.FP_testTextUtilsIsEmptyOk(java.lang.String):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] +codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyEmptyStrBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyNullBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp-isl b/infer/tests/codetoanalyze/java/pulse/issues.exp-isl index d700464d2..7b07dcf6f 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp-isl +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp-isl @@ -67,4 +67,5 @@ codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.Supp codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.shouldReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.FP_testTextUtilsIsEmptyOk(java.lang.String):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] +codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyEmptyStrBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/TextUtilsExample.java, TextUtilsExample.testTextUtilsIsEmptyNullBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]