From d97e1c8fdb32c4437773c1396ee8ee0022b5fd93 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 26 Mar 2020 09:46:35 -0700 Subject: [PATCH] [pulse][impurity] Add model for System.exit() Summary: - Model `System.exit()` as early_exit and add a test - Tweak message of methods that are impure due to having no pulse summary (and add a test) Reviewed By: skcho Differential Revision: D20668979 fbshipit-source-id: 6b5589aae --- infer/src/checkers/impurity.ml | 8 ++++++-- infer/src/pulse/PulseModels.ml | 1 + infer/tests/codetoanalyze/cpp/impurity/issues.exp | 2 +- infer/tests/codetoanalyze/java/impurity/Test.java | 10 ++++++++++ infer/tests/codetoanalyze/java/impurity/issues.exp | 2 ++ 5 files changed, 20 insertions(+), 3 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index b686d2a50..5429457bf 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -160,10 +160,12 @@ let checker {exe_env; Callbacks.summary} : Summary.t = let pdesc = Summary.get_proc_desc summary in let pname_loc = Procdesc.get_loc pdesc in let tenv = Exe_env.get_tenv exe_env proc_name in - let impure_fun_desc = F.asprintf "Impure function %a" Procname.pp proc_name in - let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in ( match summary.payloads.pulse with | None -> + let impure_fun_desc = + F.asprintf "Impure function %a with no pulse summary" Procname.pp proc_name + in + let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in Reporting.log_error summary ~loc:pname_loc ~ltr:[impure_fun_ltr] IssueType.impure_function impure_fun_desc | Some [] -> @@ -194,6 +196,8 @@ let checker {exe_env; Callbacks.summary} : Summary.t = trace acc ) skipped_calls [] in + let impure_fun_desc = F.asprintf "Impure function %a" Procname.pp proc_name in + let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in let ltr = impure_fun_ltr :: modified_ltr Formal modified_params diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 5f13cc455..4d328794d 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -413,6 +413,7 @@ module ProcNameDispatcher = struct ; +match_builtin BuiltinDecl.__cast <>$ capt_arg_payload $+...$--> Misc.id_first_arg ; +match_builtin BuiltinDecl.abort <>--> Misc.early_exit ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit + ; +PatternMatch.implements_lang "System" &:: "exit" <>--> Misc.early_exit ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size ; (* consider that all fbstrings are small strings to avoid false positives due to manual ref-counting *) diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index e9cb389de..e295cf8a5 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -14,7 +14,7 @@ codetoanalyze/cpp/impurity/global_test.cpp, modify_global_inside_lamda_impure::l codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global variable `x` modified here] codetoanalyze/cpp/impurity/invalid_test.cpp, Simple::operator=, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Simple::operator=,parameter `this` modified here] codetoanalyze/cpp/impurity/invalid_test.cpp, delete_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function delete_param_impure,parameter `s` was invalidated by `delete` here] -codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double_free_global_impure] +codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double_free_global_impure with no pulse summary] codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_impure` here,global variable `global_pointer` accessed here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_impure` here,global variable `global_pointer` accessed here,invalid access occurs here] codetoanalyze/cpp/impurity/invalid_test.cpp, free_global_pointer_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_global_pointer_impure,global variable `global_pointer` was invalidated by call to `free()` here] codetoanalyze/cpp/impurity/invalid_test.cpp, free_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_param_impure,parameter `x` was invalidated by call to `free()` here] diff --git a/infer/tests/codetoanalyze/java/impurity/Test.java b/infer/tests/codetoanalyze/java/impurity/Test.java index 04cae09c0..06ec71e03 100644 --- a/infer/tests/codetoanalyze/java/impurity/Test.java +++ b/infer/tests/codetoanalyze/java/impurity/Test.java @@ -88,4 +88,14 @@ class Test { static long systemNanoTime_impure() { return System.nanoTime(); } + + // In pulse, we get 0 disjuncts as a summary, hence consider this as impure + void exit_impure() { + System.exit(1); + } + + // We get no pulse summary, hence consider this as impure + void while_true_impure() { + while (true) {} + } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 97ac83ec0..c280d251f 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -34,9 +34,11 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():voi codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` modified here] codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` modified here] codetoanalyze/java/impurity/Test.java, Test.call_impure_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.call_impure_impure(int),when calling `void Test.set_impure(int,int)` here,parameter `this` modified here] +codetoanalyze/java/impurity/Test.java, Test.exit_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.exit_impure() with empty pulse summary] codetoanalyze/java/impurity/Test.java, Test.global_array_set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.global_array_set_impure(int,int),global variable `Test` modified here] codetoanalyze/java/impurity/Test.java, Test.local_field_write_impure(Test):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.local_field_write_impure(Test),parameter `x` modified here] codetoanalyze/java/impurity/Test.java, Test.parameter_field_write_impure(Test,boolean):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.parameter_field_write_impure(Test,boolean),parameter `test` modified here] codetoanalyze/java/impurity/Test.java, Test.set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.set_impure(int,int),parameter `this` modified here] codetoanalyze/java/impurity/Test.java, Test.swap_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.swap_impure(int[],int,int),parameter `array` modified here] codetoanalyze/java/impurity/Test.java, Test.systemNanoTime_impure():long, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function long Test.systemNanoTime_impure(),call to skipped function long System.nanoTime() occurs here] +codetoanalyze/java/impurity/Test.java, Test.while_true_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.while_true_impure() with no pulse summary]