From 8fa098474e18b299a14ecbec8ca50def3e10fdc0 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 26 Nov 2019 08:04:04 -0800 Subject: [PATCH] [cost] Fix the model of substring Summary: This diff fixes the model of substring. Problem: The cost model of the substring function was to return `size of string - start index` as a cost. However, sometimes this was a negative number, because of state abstractions on paths, array elements, call contexts, etc, which caused an exception inadvertently. This diff changes the model to return just `size of string`, when it cannot say `size of string` is bigger than `start index`. Reviewed By: ezgicicek Differential Revision: D18707954 fbshipit-source-id: 63f27e461 --- infer/src/checkers/costModels.ml | 5 ++++- infer/tests/codetoanalyze/java/performance/StringTest.java | 5 +++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/infer/src/checkers/costModels.ml b/infer/src/checkers/costModels.ml index ffb26b4c1..1e13ce0a2 100644 --- a/infer/src/checkers/costModels.ml +++ b/infer/src/checkers/costModels.ml @@ -49,8 +49,11 @@ end module JavaString = struct let substring_aux ~begin_idx ~end_v {integer_type_widths; location} inferbo_mem = let begin_v = BufferOverrunSemantics.eval integer_type_widths begin_idx inferbo_mem in + let begin_itv = BufferOverrunDomain.Val.get_itv begin_v in + let end_itv = BufferOverrunDomain.Val.get_itv end_v in let itv = - Itv.minus (BufferOverrunDomain.Val.get_itv end_v) (BufferOverrunDomain.Val.get_itv begin_v) + if Boolean.is_true (Itv.le_sem begin_itv end_itv) then Itv.minus end_itv begin_itv + else end_itv in CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.substring" location diff --git a/infer/tests/codetoanalyze/java/performance/StringTest.java b/infer/tests/codetoanalyze/java/performance/StringTest.java index e41d5c660..c6654fd9e 100644 --- a/infer/tests/codetoanalyze/java/performance/StringTest.java +++ b/infer/tests/codetoanalyze/java/performance/StringTest.java @@ -29,4 +29,9 @@ class StringTest { int index = indexof_linear(mId); return mId.substring(0, index); } + + private String startsWith_constant() { + String s = ""; + return s.startsWith(",") ? s.substring(1) : s; + } }