[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

@@ -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

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

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]

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) {}
+  }
 }

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]