From 9f81b7c8800bbb8dcd852d8c49a93a5393fd4179 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 27 Apr 2020 04:14:42 -0700 Subject: [PATCH] [inferbo] Add models of infer annotations Reviewed By: jvillard Differential Revision: D21226982 fbshipit-source-id: 4b63b19b8 --- infer/src/absint/PatternMatch.ml | 4 ++ infer/src/absint/PatternMatch.mli | 3 ++ .../src/bufferoverrun/bufferOverrunModels.ml | 30 +++++++++++-- .../java/performance/InferAnnotationTest.java | 45 +++++++++++++++++++ .../codetoanalyze/java/performance/issues.exp | 5 +++ 5 files changed, 84 insertions(+), 3 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/performance/InferAnnotationTest.java diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index 4b6045108..155fa7cfc 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -101,6 +101,10 @@ let implements_google class_name = implements ("com.google." ^ class_name) let implements_android class_name = implements ("android." ^ class_name) +let implements_infer_annotation class_name = + implements ("com.facebook.infer.annotation." ^ class_name) + + let implements_jackson class_name = implements ("com.fasterxml.jackson." ^ class_name) let implements_org_json class_name = implements ("org.json." ^ class_name) diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli index b33c604df..d918970e5 100644 --- a/infer/src/absint/PatternMatch.mli +++ b/infer/src/absint/PatternMatch.mli @@ -91,6 +91,9 @@ val implements_google : string -> Tenv.t -> string -> bool val implements_android : string -> Tenv.t -> string -> bool (** Check whether class implements a class of Android *) +val implements_infer_annotation : string -> Tenv.t -> string -> bool +(** Check whether class implements a class of Infer annotation *) + val implements_xmob_utils : string -> Tenv.t -> string -> bool (** Check whether class implements a class of xmod.utils *) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 6f5b49191..9580d1386 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -915,6 +915,12 @@ module Collection = struct key is found in the map *) let put coll_id = {exec= change_size_by_incr_or_not coll_id; check= no_check} + let put_with_elem coll_id elem_exp = + let put_model = put coll_id in + let exec env ~ret mem = put_model.exec env ~ret mem |> set_elem_exec env coll_id elem_exp in + {put_model with exec} + + (* The return value is set by [set_itv_updated_by_addition] in order to be sure that it can be used as a control variable value in the cost checker. *) let size coll_exp = @@ -1304,6 +1310,15 @@ module Object = struct {exec; check= no_check} end +module InferAnnotation = struct + let assert_get index_exp coll_exp = + match coll_exp with + | Exp.Var coll_id -> + Collection.get_at_index coll_id index_exp + | _ -> + no_model +end + module Call = struct let dispatch : (Tenv.t, model, unit) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in @@ -1520,8 +1535,8 @@ module Call = struct ; +PatternMatch.implements_map &:: "entrySet" <>$ capt_exp $!--> Collection.iterator ; +PatternMatch.implements_map &:: "keySet" <>$ capt_exp $!--> Collection.iterator ; +PatternMatch.implements_map &:: "values" <>$ capt_exp $!--> Collection.iterator - ; +PatternMatch.implements_map &:: "put" <>$ capt_var_exn $+ any_arg $+ any_arg - $--> Collection.put + ; +PatternMatch.implements_map &:: "put" <>$ capt_var_exn $+ any_arg $+ capt_exp + $--> Collection.put_with_elem ; +PatternMatch.implements_org_json "JSONArray" &:: "put" <>$ capt_var_exn $+...$--> Collection.put ; +PatternMatch.implements_map &:: "putAll" <>$ capt_var_exn $+ capt_exp @@ -1569,5 +1584,14 @@ module Call = struct $--> eval_binop ~f:(Itv.min_sem ~use_minmax_bound:true) ; +PatternMatch.implements_lang "Enum" &:: "name" &::.*--> JavaString.inferbo_constant_string ; +PatternMatch.implements_lang "Class" - &:: "getCanonicalName" &::.*--> JavaString.inferbo_constant_string ] + &:: "getCanonicalName" &::.*--> JavaString.inferbo_constant_string + ; +PatternMatch.implements_infer_annotation "Assertions" + &:: "assertNotNull" <>$ capt_exp $+...$--> id + ; +PatternMatch.implements_infer_annotation "Assertions" + &:: "assumeNotNull" <>$ capt_exp $+...$--> id + ; +PatternMatch.implements_infer_annotation "Assertions" + &:: "nullsafeFIXME" <>$ capt_exp $+...$--> id + ; +PatternMatch.implements_infer_annotation "Assertions" + &:: "assertGet" <>$ capt_exp $+ capt_exp $--> InferAnnotation.assert_get + ; +PatternMatch.implements_infer_annotation "Assertions" &::.*--> no_model ] end diff --git a/infer/tests/codetoanalyze/java/performance/InferAnnotationTest.java b/infer/tests/codetoanalyze/java/performance/InferAnnotationTest.java new file mode 100644 index 000000000..4d8ca4105 --- /dev/null +++ b/infer/tests/codetoanalyze/java/performance/InferAnnotationTest.java @@ -0,0 +1,45 @@ +/* + * 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 com.facebook.infer.annotation.Assertions; +import java.util.ArrayList; +import java.util.HashMap; + +public class InferAnnotationTest { + + public void assert_not_null_linear(Integer x) { + for (int i = 0; i < Assertions.assertNotNull(x); i++) {} + } + + public void assert_not_null_explanation_linear(Integer x) { + for (int i = 0; i < Assertions.assertNotNull(x, "explanation"); i++) {} + } + + public void assume_not_null_linear(Integer x) { + for (int i = 0; i < Assertions.assumeNotNull(x); i++) {} + } + + public void assume_not_null_explanation_linear(Integer x) { + for (int i = 0; i < Assertions.assumeNotNull(x, "explanation"); i++) {} + } + + public void nullsafe_fixme_linear(Integer x) { + for (int i = 0; i < Assertions.nullsafeFIXME(x, "explanation"); i++) {} + } + + public void assert_get_list_constant() { + ArrayList a = new ArrayList<>(); + a.add(5); + for (int i = 0; i < Assertions.assertGet(0, a); i++) {} + } + + public void assert_get_map_constant() { + HashMap m = new HashMap(); + m.put(0, 5); + for (int i = 0; i < Assertions.assertGet(0, m); i++) {} + } +} diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index d98d7d2f9..be6e64685 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -118,6 +118,11 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 545, O(1), degree = 0] codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 15] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ test.a, O(test.a), degree = 1,{test.a},Loop at line 16] +codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.assert_not_null_explanation_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 19,{x},Loop at line 19] +codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.assert_not_null_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 15,{x},Loop at line 15] +codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.assume_not_null_explanation_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 27,{x},Loop at line 27] +codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.assume_not_null_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 23,{x},Loop at line 23] +codetoanalyze/java/performance/InferAnnotationTest.java, InferAnnotationTest.nullsafe_fixme_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x + 7 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 31,{x},Loop at line 31] codetoanalyze/java/performance/InheritanceTest.java, InheritanceTest$Impl1.foo(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 34] codetoanalyze/java/performance/InheritanceTest.java, InheritanceTest$UniqueImpl.foo(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 15] codetoanalyze/java/performance/InheritanceTest.java, InheritanceTest$UniqueImpl4.top_cost(InheritanceTest$MyInterface3):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 58]