[impurity] Consider exited functions as impure

Summary: Consider functions that simply exit as impure by extending the impurity domain with `AbstractDomain.BooleanOr` that signifies whether the program exited.

Reviewed By: skcho

Differential Revision: D20941628

fbshipit-source-id: 19bc90e66

infer/src/checkers/impurity.ml

@@ -139,9 +139,13 @@ 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 =
+  let astate, exited =
     match exec_state with
-  | ExitProgram astate | ContinueProgram astate ->
-      (* TODO: consider impure even though the program only exits with pre=post *)
+    | 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
@@ -155,7 +159,7 @@ let extract_impurity tenv pdesc (exec_state : PulseExecutionState.t) : ImpurityD
     |> 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}
+  {modified_globals; modified_params; skipped_calls; exited}
 
 
 let checker {exe_env; Callbacks.summary} : Summary.t =

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
 
 

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
 

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
 }

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]

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);

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]