[impurity] Consider functions with no pulse summary as impure

Summary: If we have no pulse summary (most likely caused by pulse finding a legit issue with the code), let's consider the function as impure.

Reviewed By: jvillard

Differential Revision: D17906016

fbshipit-source-id: 671d3e0ba

infer/src/checkers/impurity.ml

@@ -113,34 +113,36 @@ let extract_impurity pdesc pre_post : ImpurityDomain.t =
   {modified_globals; modified_params}
 
 
-let report_errors summary (ImpurityDomain.{modified_globals; modified_params} as astate) =
+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
-  if Purity.should_report pdesc && not (ImpurityDomain.is_pure astate) then
-    let impure_fun_desc = F.asprintf "Impure function %a" Typ.Procname.pp proc_name in
-    let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in
-    let modified_ltr ~str set acc =
-      ImpurityDomain.ModifiedVarSet.fold (ImpurityDomain.add_to_errlog ~nesting:1 ~str) set acc
-    in
-    let ltr =
-      impure_fun_ltr
-      :: modified_ltr ~str:"parameter" modified_params
-           (modified_ltr ~str:"global var" modified_globals [])
-    in
-    Reporting.log_error summary ~loc:pname_loc ~ltr IssueType.impure_function impure_fun_desc
+  let impure_fun_desc = F.asprintf "Impure function %a" Typ.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) ->
+      if Purity.should_report pdesc && not (ImpurityDomain.is_pure astate) then
+        let modified_ltr ~str set acc =
+          ImpurityDomain.ModifiedVarSet.fold (ImpurityDomain.add_to_errlog ~nesting:1 ~str) set acc
+        in
+        let ltr =
+          impure_fun_ltr
+          :: modified_ltr ~str:"parameter" modified_params
+               (modified_ltr ~str:"global var" modified_globals [])
+        in
+        Reporting.log_error summary ~loc:pname_loc ~ltr IssueType.impure_function impure_fun_desc
+  ) ;
+  summary
 
 
 let checker ({Callbacks.summary} as callback) : Summary.t =
   let pulse_summary = Pulse.checker callback in
-  match pulse_summary.payloads.pulse with
-  | Some pre_posts ->
-      let modified =
-        List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc pre_post ->
-            let modified = extract_impurity (Summary.get_proc_desc summary) pre_post in
-            ImpurityDomain.join acc modified )
-      in
-      report_errors summary modified ; summary
-  | None ->
-      debug "@\n\n[WARNING] Couldn't find any Pulse summary to extract impurity information." ;
-      summary
+  pulse_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 (Summary.get_proc_desc summary) pre_post in
+             ImpurityDomain.join acc modified ) )
+  |> report_errors summary

infer/tests/codetoanalyze/cpp/impurity/invalid_test.cpp

@@ -9,8 +9,8 @@
 int* global_pointer;
 
 void free_global_pointer_impure() { free(global_pointer); }
-// If Pulse raises an error, it stops the world and has no summary.
-void double_free_global_impure_FN() {
+// If Pulse raises an error, consider the function as impure.
+void double_free_global_impure() {
   free_global_pointer_impure();
   free_global_pointer_impure();
 }

infer/tests/codetoanalyze/cpp/impurity/issues.exp

@@ -12,7 +12,8 @@ codetoanalyze/cpp/impurity/global_test.cpp, modify_global_array_impure, 0, IMPUR
 codetoanalyze/cpp/impurity/global_test.cpp, modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(), 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(),global var 'x' is modified at line 33, column 22]
 codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global var 'x' is modified at line 10, column 41]
 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_FN, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_impure` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_impure` here,invalid access occurs 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, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_impure` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_impure` 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 var '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]
 codetoanalyze/cpp/impurity/invalid_test.cpp, reassign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function reassign_impure,parameter 's' is modified at line 34, column 3]