From b64ed0bbf2f7f0e8b0881c9149580437dad23874 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 24 Mar 2020 09:09:33 -0700 Subject: [PATCH] [impurity] Consider functions with empty pulse summary as impure Summary: As exemplified by added tests, pulse computes an empty summary (with 0 disjuncts) whenever it discovers a contradiction which might be caused by: - discovering aliasing in memory - widening limited number of times in loops and concluding that loop exit conditions are never taken However, AFAIU, it is not possible to have a function with 0 disjunct apart from such anomalities. Even a function which does nothing like `void foo(){}` has 1 disjuncts: ``` Pulse: 1 pre/post(s) #0: PRE: { roots={ }; mem ={ }; attrs={ };} POST: { roots={ }; mem ={ }; attrs={ };} SKIPPED_CALLS: { } ``` The aim of this diff is to consider functions with 0 disjuncts as **impure** because most often such cases are impure, rather than actually pure. Reviewed By: skcho Differential Revision: D20619504 fbshipit-source-id: 3a8502c90 --- infer/src/checkers/impurity.ml | 37 ++++++++++--------- .../codetoanalyze/cpp/impurity/array_test.cpp | 11 +++++- .../codetoanalyze/cpp/impurity/issues.exp | 1 + .../java/impurity/PurityModeled.java | 13 +++++-- .../codetoanalyze/java/impurity/issues.exp | 3 ++ 5 files changed, 43 insertions(+), 22 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 8842d714e..b686d2a50 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -155,15 +155,31 @@ let extract_impurity tenv pdesc pre_post : ImpurityDomain.t = {modified_globals; modified_params; skipped_calls} -let report_errors summary proc_name pname_loc modified_opt = +let checker {exe_env; Callbacks.summary} : Summary.t = + let proc_name = Summary.get_proc_name summary in + 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 modified_opt with + ( match summary.payloads.pulse with | None -> Reporting.log_error summary ~loc:pname_loc ~ltr:[impure_fun_ltr] IssueType.impure_function impure_fun_desc - | Some (ImpurityDomain.{modified_globals; modified_params; skipped_calls} as astate) -> - if Purity.should_report proc_name && not (ImpurityDomain.is_pure astate) then + | Some [] -> + let impure_fun_desc = + F.asprintf "Impure function %a with empty 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 pre_posts -> + let (ImpurityDomain.{modified_globals; modified_params; skipped_calls} as impurity_astate) = + List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc pre_post -> + let modified = extract_impurity tenv pdesc pre_post in + ImpurityDomain.join acc modified ) + in + if Purity.should_report proc_name && not (ImpurityDomain.is_pure impurity_astate) then let modified_ltr param_source set acc = ImpurityDomain.ModifiedVarSet.fold (ImpurityDomain.add_to_errlog ~nesting:1 param_source) @@ -185,16 +201,3 @@ let report_errors summary proc_name pname_loc modified_opt = in Reporting.log_error summary ~loc:pname_loc ~ltr IssueType.impure_function impure_fun_desc ) ; summary - - -let checker {exe_env; Callbacks.summary} : Summary.t = - let proc_name = Summary.get_proc_name summary in - 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 - summary.payloads.pulse - |> Option.map ~f:(fun pre_posts -> - List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc pre_post -> - let modified = extract_impurity tenv pdesc pre_post in - ImpurityDomain.join acc modified ) ) - |> report_errors summary proc_name pname_loc diff --git a/infer/tests/codetoanalyze/cpp/impurity/array_test.cpp b/infer/tests/codetoanalyze/cpp/impurity/array_test.cpp index 798442fab..e6fbb0fc9 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/array_test.cpp +++ b/infer/tests/codetoanalyze/cpp/impurity/array_test.cpp @@ -22,9 +22,16 @@ void call_array_mod_impure(int a[10]) { array_mod_impure(a, b, 9); } -void call_array_mod_with_fresh_pure() { +void call_array_mod_with_fresh_pure_FP() { int a[10]; - array_mod_impure(a, a, 0); + array_mod_impure(a, a, 0); // aliasing of arguments, pulse returns empty + // summary which causes the function to be + // considered impure +} +void call_array_mod_with_both_fresh_pure() { + int a[10]; + int b[10]; + array_mod_impure(a, b, 0); } // modifies array diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index 89838c79a..e9cb389de 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -4,6 +4,7 @@ codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter `a` modified here] codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter `b` modified here,parameter `a` modified here] codetoanalyze/cpp/impurity/array_test.cpp, call_array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_array_mod_impure,when calling `array_mod_impure` here,parameter `a` modified here] +codetoanalyze/cpp/impurity/array_test.cpp, call_array_mod_with_fresh_pure_FP, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_array_mod_with_fresh_pure_FP with empty pulse summary] codetoanalyze/cpp/impurity/array_test.cpp, modify_direct_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_direct_impure,parameter `array` modified here] codetoanalyze/cpp/impurity/array_test.cpp, modify_ptr_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_ptr_impure,parameter `array` modified here] codetoanalyze/cpp/impurity/global_test.cpp, call_modify_global, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_modify_global,when calling `modify_global_array_impure` here,global variable `a` modified here,when calling `modify_global_primitive_impure` here,global variable `x` modified here] diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index 1142b30bf..62dbf2a1a 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -87,12 +87,19 @@ class PurityModeled { // Pulse can only widen a fixed number of times, hence it thinks // that the exit of the loop never reaches and results in empty // post. - void timing_call_in_loop_impure_FN() { + void timing_call_in_loop_impure() { for (int i = 0; i < 10; i++) { System.nanoTime(); } } + // Pulse can only widen a fixed number of times, hence it thinks + // that the exit of the loop never reaches and results in empty + // post which is considered to be impure. + void constant_loop_pure_FP() { + for (int i = 0; i < 10; i++) {} + } + // Since n is symbolic, pruning doesn't result in infeasible path, // but we assume that the parameter [n] must be 3 due to constant(4) // "widening" in pulse. @@ -105,8 +112,8 @@ class PurityModeled { // Due to getting the wrong summary for the callee (a=3), Pulse ends // up thinking that the parameter [a] must be 3 in the loop. Hence, as // a result of pruning, exit node becomes infeasible and we get - // empty summary. - void call_timing_symb_impure_FN(int a) { + // empty summary which is considered to be impure. + void call_timing_symb_impure(int a) { for (int i = 0; i < a; i++) { timing_call_in_loop_symb_impure(a); } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 3065b1569..97ac83ec0 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -16,8 +16,10 @@ codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(j codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_via_call_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here] codetoanalyze/java/impurity/Localities.java, Localities.newHashCode_impure():int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.newHashCode_impure(),call to skipped function int Object.hashCode() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.append_impure(java.lang.StringBuilder):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.append_impure(StringBuilder),parameter `strBuilder` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_impure(int) with empty pulse summary] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_unrelated_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_unrelated_impure(int,int),when calling `void PurityModeled.timing_call_in_loop_symb_impure(int)` here,call to skipped function long System.nanoTime() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_write_impure(),when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.constant_loop_pure_FP():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.constant_loop_pure_FP() with empty pulse summary] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_add_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_add_impure(ArrayList),parameter `list` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_addall_impure(java.util.ArrayList,java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_addall_impure(ArrayList,ArrayList),parameter `list1` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_set_impure(ArrayList),parameter `list` was potentially invalidated by `std::vector::assign()` here] @@ -26,6 +28,7 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loo codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.process_queue_impure(java.util.ArrayList,java.util.Queue):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.process_queue_impure(ArrayList,Queue),parameter `queue` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.replace_impure(java.lang.String):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.replace_impure(String),parameter `s` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_impure() with empty pulse summary] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_symb_impure(int),call to skipped function long System.nanoTime() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),call to skipped function void PrintStream.write(byte[],int,int) occurs here] 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]