diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 5f6857ab7..04535584f 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -48,13 +48,12 @@ let add_invalid_and_modified ~check_empty attrs acc = (** Given Pulse summary, extract impurity info, i.e. parameters and global variables that are - modified by the function. - - TODO: keep track of impure library calls *) -let extract_impurity pdesc pre_post : ImpurityDomain.t = + modified by the function and skipped functions. *) +let extract_impurity tenv pdesc pre_post : ImpurityDomain.t = let pre_heap = (AbductiveDomain.extract_pre pre_post).BaseDomain.heap in - let post_heap = (AbductiveDomain.extract_post pre_post).BaseDomain.heap in - let post_stack = (AbductiveDomain.extract_post pre_post).BaseDomain.stack in + let post = AbductiveDomain.extract_post pre_post in + let post_heap = post.BaseDomain.heap in + let post_stack = post.BaseDomain.stack in let add_to_modified var addr acc = let rec aux acc ~addr_to_explore ~visited : ImpurityDomain.trace list = match addr_to_explore with @@ -116,39 +115,61 @@ let extract_impurity pdesc pre_post : ImpurityDomain.t = (fun var (addr, _) acc -> if Var.is_global var then add_to_modified var addr acc else acc) post_stack ImpurityDomain.ModifiedVarSet.empty in - {modified_globals; modified_params} + let is_modeled_pure pname = + match PurityModels.ProcName.dispatch tenv pname with + | Some callee_summary -> + PurityDomain.is_pure callee_summary + | None -> + false + in + let skipped_calls_map = + post.BaseDomain.skipped_calls_map + |> BaseDomain.SkippedCallsMap.filter (fun proc_name _ -> + Purity.should_report proc_name && not (is_modeled_pure proc_name) ) + in + {modified_globals; modified_params; skipped_calls_map} -let report_errors summary modified_opt = - let pdesc = Summary.get_proc_desc summary in - let proc_name = Procdesc.get_proc_name pdesc in - let pname_loc = Procdesc.get_loc pdesc in +let report_errors summary proc_name pname_loc modified_opt = 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 | None -> Reporting.log_error summary ~loc:pname_loc ~ltr:[impure_fun_ltr] IssueType.impure_function impure_fun_desc - | Some (ImpurityDomain.{modified_globals; modified_params} as astate) -> + | Some (ImpurityDomain.{modified_globals; modified_params; skipped_calls_map} as astate) -> if Purity.should_report proc_name && not (ImpurityDomain.is_pure astate) then let modified_ltr param_source set acc = ImpurityDomain.ModifiedVarSet.fold (ImpurityDomain.add_to_errlog ~nesting:1 param_source) set acc in + let skipped_functions = + PulseBaseDomain.SkippedCallsMap.fold + (fun proc_name trace acc -> + PulseTrace.add_to_errlog ~nesting:1 + ~pp_immediate:(fun fmt -> + F.fprintf fmt "call to skipped function %a occurs here" Procname.pp proc_name ) + trace acc ) + skipped_calls_map [] + in let ltr = impure_fun_ltr - :: modified_ltr Formal modified_params (modified_ltr Global modified_globals []) + :: modified_ltr Formal modified_params + (modified_ltr Global modified_globals skipped_functions) in Reporting.log_error summary ~loc:pname_loc ~ltr IssueType.impure_function impure_fun_desc ) ; summary -let checker {Callbacks.summary} : Summary.t = +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 : PulseSummary.t) -> + |> Option.map ~f:(fun pre_posts -> List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc pre_post -> - let modified = extract_impurity pdesc pre_post in + let modified = extract_impurity tenv pdesc pre_post in ImpurityDomain.join acc modified ) ) - |> report_errors summary + |> report_errors summary proc_name pname_loc diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index d058fc5d6..3da3cfaa7 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -21,22 +21,34 @@ end module ModifiedVarSet = AbstractDomain.FiniteSet (ModifiedVar) -type t = {modified_params: ModifiedVarSet.t; modified_globals: ModifiedVarSet.t} +type t = + { modified_params: ModifiedVarSet.t + ; modified_globals: ModifiedVarSet.t + ; skipped_calls_map: PulseBaseDomain.SkippedCallsMap.t } -let is_pure {modified_globals; modified_params} = - ModifiedVarSet.is_empty modified_globals && ModifiedVarSet.is_empty modified_params +let is_pure {modified_globals; modified_params; skipped_calls_map} = + ModifiedVarSet.is_empty modified_globals + && ModifiedVarSet.is_empty modified_params + && PulseBaseDomain.SkippedCallsMap.is_empty skipped_calls_map -let pure = {modified_params= ModifiedVarSet.empty; modified_globals= ModifiedVarSet.empty} +let pure = + { modified_params= ModifiedVarSet.empty + ; modified_globals= ModifiedVarSet.empty + ; skipped_calls_map= PulseBaseDomain.SkippedCallsMap.empty } + let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else - let {modified_globals= mg1; modified_params= mp1} = astate1 in - let {modified_globals= mg2; modified_params= mp2} = astate2 in + let {modified_globals= mg1; modified_params= mp1; skipped_calls_map= uk1} = astate1 in + let {modified_globals= mg2; modified_params= mp2; skipped_calls_map= uk2} = astate2 in PhysEqual.optim2 ~res: - {modified_globals= ModifiedVarSet.join mg1 mg2; modified_params= ModifiedVarSet.join mp1 mp2} + { modified_globals= ModifiedVarSet.join mg1 mg2 + ; modified_params= ModifiedVarSet.join mp1 mp2 + ; skipped_calls_map= + PulseBaseDomain.SkippedCallsMap.union (fun _pname t1 _ -> Some t1) uk1 uk2 } astate1 astate2 diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 1cc918ee6..629876dde 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -18,7 +18,10 @@ module ModifiedVarSet : sig include AbstractDomain.FiniteSetS with type elt = ModifiedVar.t end -type t = {modified_params: ModifiedVarSet.t; modified_globals: ModifiedVarSet.t} +type t = + { modified_params: ModifiedVarSet.t + ; modified_globals: ModifiedVarSet.t + ; skipped_calls_map: PulseBaseDomain.SkippedCallsMap.t } val pure : t diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index 453d898ea..3c3ee6693 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -23,10 +23,11 @@ codetoanalyze/cpp/impurity/invalid_test.cpp, swap_impure, 0, IMPURE_FUNCTION, no codetoanalyze/cpp/impurity/param_test.cpp, create_cycle_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function create_cycle_impure,parameter `x` of create_cycle_impure,parameter `x` modified here] codetoanalyze/cpp/impurity/param_test.cpp, invalidate_local_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function invalidate_local_impure,parameter `pp` of invalidate_local_impure,parameter `pp` modified here] codetoanalyze/cpp/impurity/param_test.cpp, modify_mut_ref_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_mut_ref_impure,parameter `x` of modify_mut_ref_impure,parameter `x` modified here] -codetoanalyze/cpp/impurity/unmodeled.cpp, output_stream_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function output_stream_impure,global variable `std::cout` accessed here,global variable `std::cout` modified here] +codetoanalyze/cpp/impurity/unmodeled.cpp, output_stream_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function output_stream_impure,global variable `std::cout` accessed here,global variable `std::cout` modified here,call to skipped function std::basic_ostream>::operator<< occurs here,call to skipped function std::operator<<_> occurs here] +codetoanalyze/cpp/impurity/unmodeled.cpp, random_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function random_impure,call to skipped function rand occurs here] codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter `vec` of assign_impure,parameter `vec` modified here] codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter `vec` of clear_impure,parameter `vec` modified here] -codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter `vec` of insert_impure,parameter `vec` modified here] +codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter `vec` of insert_impure,parameter `vec` modified here,call to skipped function std::vector>::begin occurs here] codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter `vec` of push_back_impure,parameter `vec` modified here] -codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec_other` of push_back_in_loop_impure,assigned,parameter `vec_other` modified here,parameter `vec` of push_back_in_loop_impure,parameter `vec` modified here] -codetoanalyze/cpp/impurity/vector.cpp, set_zero_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function set_zero_impure,parameter `numbers` of set_zero_impure,assigned,parameter `numbers` modified here] +codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec_other` of push_back_in_loop_impure,assigned,parameter `vec_other` modified here,parameter `vec` of push_back_in_loop_impure,parameter `vec` modified here,call to skipped function std::vector>::begin occurs here,call to skipped function std::vector>::end occurs here] +codetoanalyze/cpp/impurity/vector.cpp, set_zero_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function set_zero_impure,parameter `numbers` of set_zero_impure,assigned,parameter `numbers` modified here,call to skipped function std::vector>::begin occurs here,call to skipped function std::vector>::end occurs here] diff --git a/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp b/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp index c5004422b..6908c09bb 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp +++ b/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp @@ -8,4 +8,4 @@ void output_stream_impure() { std::cout << "Hello, world!" << std::endl; } -int random_impure_FN() { std::rand(); } +int random_impure() { std::rand(); } diff --git a/infer/tests/codetoanalyze/java/impurity/Localities.java b/infer/tests/codetoanalyze/java/impurity/Localities.java index 5d62a57c4..0714902d1 100644 --- a/infer/tests/codetoanalyze/java/impurity/Localities.java +++ b/infer/tests/codetoanalyze/java/impurity/Localities.java @@ -101,7 +101,7 @@ class Localities { } // @loc: T - private int newHashCode_impure_FN() { + private int newHashCode_impure() { return new Object().hashCode(); } diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index 0530f7921..cc1f9b45a 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -6,10 +6,17 @@ */ class PurityModeled { - double math_random_impure_FN() { + double math_random_impure() { return Math.random(); } + double math_random_infeasible_pure(int x) { + if (x > 1 && x < 2) { + return Math.random(); // this path will never be taken + } + return 0; + } + void arraycopy_pure_FP(int[] src) { int[] dst = {5, 10, 20, 30, 40, 50}; // copies an array from the specified source array @@ -19,4 +26,23 @@ class PurityModeled { public void array_length_loop_pure(Integer[] array) { for (int i = 0; i < array.length; i++) {} } + + void write_impure() { + byte[] temp = new byte[4]; + System.out.write(temp, 0, 4); + } + + void call_write_impure() { + write_impure(); + } + + int math_random_in_loop_impure(int x) { + int p = 0; + for (int i = 0; i < x; i++) { + p += Math.random(); + call_write_impure(); + } + + return p; + } } diff --git a/infer/tests/codetoanalyze/java/impurity/Test.java b/infer/tests/codetoanalyze/java/impurity/Test.java index c032b987c..04cae09c0 100644 --- a/infer/tests/codetoanalyze/java/impurity/Test.java +++ b/infer/tests/codetoanalyze/java/impurity/Test.java @@ -85,7 +85,7 @@ class Test { } // All unmodeled calls should be considered impure - static long systemNanoTime_impure_FN() { + static long systemNanoTime_impure() { return System.nanoTime(); } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 05391388c..f59fa7d29 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -13,7 +13,12 @@ codetoanalyze/java/impurity/Localities.java, Localities.incrementAll_impure(java codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.makeAllZero_impure(ArrayList),parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here,parameter `list` of void Localities.makeAllZero_impure(ArrayList),assigned,passed as argument to `Iterator.next` (modelled),return from call to `Iterator.next` (modelled),assigned,assigned,parameter `list` modified here] codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_first_el_impure(ArrayList),parameter `list` of void Localities.modify_first_el_impure(ArrayList),passed as argument to `Collection.get()` (modelled),return from call to `Collection.get()` (modelled),assigned,assigned,parameter `list` modified here] 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),parameter `list` of void Localities.modify_via_call_impure(ArrayList),passed as argument to `Localities$Foo Localities.get_first_pure(ArrayList)`,return from call to `Localities$Foo Localities.get_first_pure(ArrayList)`,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` of void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` 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.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` of void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` modified here,call to skipped function void System.arraycopy(Object,int,Object,int,int) 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(),global variable `java.lang.System` accessed here,when calling `void PurityModeled.write_impure()` here,global variable `java.lang.System` accessed here,global variable `lang.System` modified here,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.math_random_impure():double, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double PurityModeled.math_random_impure(),call to skipped function double Math.random() occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loop_impure(int):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int PurityModeled.math_random_in_loop_impure(int),global variable `java.lang.System` accessed here,when calling `void PurityModeled.call_write_impure()` here,global variable `java.lang.System` accessed here,when calling `void PurityModeled.write_impure()` here,global variable `java.lang.System` accessed here,global variable `lang.System` modified here,when calling `void PurityModeled.call_write_impure()` here,when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here,call to skipped function double Math.random() occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),global variable `java.lang.System` accessed here,global variable `lang.System` modified here,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` accessed here,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` of void Test.alias_impure(int[],int,int),assigned,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),parameter `this` of void Test.call_impure_impure(int),when calling `void Test.set_impure(int,int)` here,parameter `this` of void Test.set_impure(int,int),parameter `this` modified here] @@ -22,3 +27,4 @@ codetoanalyze/java/impurity/Test.java, Test.local_field_write_impure(Test):void, 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` of 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` of 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` of void Test.swap_impure(int[],int,int),parameter `array` modified here,parameter `array` of 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]