diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 554be4d71..01e38fc80 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -139,23 +139,27 @@ let is_modeled_pure tenv pname = (** Given Pulse summary, extract impurity info, i.e. parameters and global variables that are modified by the function and skipped functions. *) let extract_impurity tenv pdesc (exec_state : PulseExecutionState.t) : ImpurityDomain.t = - match exec_state with - | ExitProgram astate | ContinueProgram astate -> - (* TODO: consider impure even though the program only exits with pre=post *) - let pre_heap = (PulseAbductiveDomain.get_pre astate).BaseDomain.heap in - let post = PulseAbductiveDomain.get_post astate in - let post_stack = post.BaseDomain.stack in - let pname = Procdesc.get_proc_name pdesc in - let modified_params = - Procdesc.get_formals pdesc |> get_modified_params pname post_stack pre_heap post - in - let modified_globals = get_modified_globals pre_heap post post_stack in - let skipped_calls = - PulseAbductiveDomain.get_skipped_calls astate - |> PulseAbductiveDomain.SkippedCalls.filter (fun proc_name _ -> - Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) ) - in - {modified_globals; modified_params; skipped_calls} + let astate, exited = + match exec_state with + | ExitProgram astate -> + (astate, true) + | ContinueProgram astate -> + (astate, false) + in + let pre_heap = (PulseAbductiveDomain.get_pre astate).BaseDomain.heap in + let post = PulseAbductiveDomain.get_post astate in + let post_stack = post.BaseDomain.stack in + let pname = Procdesc.get_proc_name pdesc in + let modified_params = + Procdesc.get_formals pdesc |> get_modified_params pname post_stack pre_heap post + in + let modified_globals = get_modified_globals pre_heap post post_stack in + let skipped_calls = + PulseAbductiveDomain.get_skipped_calls astate + |> PulseAbductiveDomain.SkippedCalls.filter (fun proc_name _ -> + Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) ) + in + {modified_globals; modified_params; skipped_calls; exited} let checker {exe_env; Callbacks.summary} : Summary.t = diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index 4811f8c87..3efd41c21 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -20,34 +20,39 @@ module ModifiedVar = struct end module ModifiedVarSet = AbstractDomain.FiniteSet (ModifiedVar) +module Exited = AbstractDomain.BooleanOr type t = { modified_params: ModifiedVarSet.t ; modified_globals: ModifiedVarSet.t - ; skipped_calls: SkippedCalls.t } + ; skipped_calls: SkippedCalls.t + ; exited: Exited.t } -let is_pure {modified_globals; modified_params; skipped_calls} = +let is_pure {modified_globals; modified_params; skipped_calls; exited} = ModifiedVarSet.is_empty modified_globals && ModifiedVarSet.is_empty modified_params && SkippedCalls.is_empty skipped_calls + && Exited.is_bottom exited let pure = { modified_params= ModifiedVarSet.empty ; modified_globals= ModifiedVarSet.empty - ; skipped_calls= SkippedCalls.empty } + ; skipped_calls= SkippedCalls.empty + ; exited= Exited.bottom } let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else - let {modified_globals= mg1; modified_params= mp1; skipped_calls= uk1} = astate1 in - let {modified_globals= mg2; modified_params= mp2; skipped_calls= uk2} = astate2 in + let {modified_globals= mg1; modified_params= mp1; skipped_calls= uk1; exited= e1} = astate1 in + let {modified_globals= mg2; modified_params= mp2; skipped_calls= uk2; exited= e2} = astate2 in PhysEqual.optim2 ~res: { modified_globals= ModifiedVarSet.join mg1 mg2 ; modified_params= ModifiedVarSet.join mp1 mp2 - ; skipped_calls= SkippedCalls.union (fun _pname t1 _ -> Some t1) uk1 uk2 } + ; skipped_calls= SkippedCalls.union (fun _pname t1 _ -> Some t1) uk1 uk2 + ; exited= Exited.join e1 e2 } astate1 astate2 diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 65884a58e..11ee46e55 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -19,10 +19,13 @@ module ModifiedVarSet : sig include AbstractDomain.FiniteSetS with type elt = ModifiedVar.t end +module Exited = AbstractDomain.BooleanOr + type t = { modified_params: ModifiedVarSet.t ; modified_globals: ModifiedVarSet.t - ; skipped_calls: PulseAbductiveDomain.SkippedCalls.t } + ; skipped_calls: PulseAbductiveDomain.SkippedCalls.t + ; exited: Exited.t } val pure : t diff --git a/infer/tests/codetoanalyze/cpp/impurity/exit_test.cpp b/infer/tests/codetoanalyze/cpp/impurity/exit_test.cpp index 278777729..be9634935 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/exit_test.cpp +++ b/infer/tests/codetoanalyze/cpp/impurity/exit_test.cpp @@ -8,13 +8,13 @@ int x; -void exit_positive_impure_FN(int a[10], int b) { +void exit_positive_impure(int a[10], int b) { if (b > 0) { exit(0); } } -void unreachable_impure_FN(int a[10], int b) { - exit_positive_impure_FN(a, 10); - x = 9; +void unreachable_impure(int a[10]) { + exit_positive_impure(a, 10); + x = 9; // unreachable } diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index e295cf8a5..6375675f4 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -7,6 +7,8 @@ codetoanalyze/cpp/impurity/array_test.cpp, call_array_mod_impure, 0, IMPURE_FUNC 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/exit_test.cpp, exit_positive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function exit_positive_impure] +codetoanalyze/cpp/impurity/exit_test.cpp, unreachable_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function unreachable_impure] 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] codetoanalyze/cpp/impurity/global_test.cpp, local_static_var_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function local_static_var_impure,global variable `local_static_var_impure.arr` modified here] codetoanalyze/cpp/impurity/global_test.cpp, modify_global_array_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_array_impure,global variable `a` modified here] diff --git a/infer/tests/codetoanalyze/java/impurity/Test.java b/infer/tests/codetoanalyze/java/impurity/Test.java index d558c1f1d..575173b24 100644 --- a/infer/tests/codetoanalyze/java/impurity/Test.java +++ b/infer/tests/codetoanalyze/java/impurity/Test.java @@ -89,13 +89,10 @@ class Test { return System.nanoTime(); } - // In pulse, we get Exited summary where pre=post - // TODO: change impurity to track exit as impure - void exit_impure_FN() { + void exit_impure() { System.exit(1); } - // In pulse, we get Exited summary where pre=post void modify_exit_impure(int[] a) { a[0] = 0; System.exit(1); diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index b199f6e27..894365845 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -34,6 +34,7 @@ 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()] 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.modify_exit_impure(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.modify_exit_impure(int[]),parameter `a` modified here]