From d670bdd61a23b1da61ecc971df7c5dffd9b77d31 Mon Sep 17 00:00:00 2001
From: Cristiano Calcagno <cristianoc@fb.com>
Date: Fri, 16 Dec 2016 02:19:24 -0800
Subject: [PATCH] [eradicate] Add support for methods that don't return
 (System.exit)

Reviewed By: jeremydubreil

Differential Revision: D4335991

fbshipit-source-id: 9b2af48
---
 infer/src/eradicate/modelTables.ml                |  8 ++++++++
 infer/src/eradicate/modelTables.mli               |  1 +
 infer/src/eradicate/models.ml                     |  6 +++++-
 infer/src/eradicate/typeCheck.ml                  | 13 +++++++++++--
 .../java/eradicate/NullMethodCall.java            | 15 +++++++++++++++
 5 files changed, 40 insertions(+), 3 deletions(-)

diff --git a/infer/src/eradicate/modelTables.ml b/infer/src/eradicate/modelTables.ml
index 1d041e6de..f247778c4 100644
--- a/infer/src/eradicate/modelTables.ml
+++ b/infer/src/eradicate/modelTables.ml
@@ -228,6 +228,13 @@ let annotated_list_present =
     (n, [o]), "com.google.common.base.Optional.of(java.lang.Object):com.google.common.base.Optional";
   ]
 
+(** Models for methods that do not return *)
+let noreturn_list =
+  [
+    (o, [o]), "java.lang.System.exit(int):void";
+  ]
+
+
 type model_table_t = (string, bool * bool list) Hashtbl.t
 
 let mk_table list =
@@ -248,4 +255,5 @@ let containsKey_table = mk_table containsKey_list
 let mapPut_table = mk_table mapPut_list
 let optional_get_table = mk_table optional_get_list
 let optional_isPresent_table = mk_table optional_isPresent_list
+let noreturn_table = mk_table noreturn_list
 let true_on_null_table = mk_table true_on_null_list
diff --git a/infer/src/eradicate/modelTables.mli b/infer/src/eradicate/modelTables.mli
index c16707efc..2dfbdd372 100644
--- a/infer/src/eradicate/modelTables.mli
+++ b/infer/src/eradicate/modelTables.mli
@@ -25,4 +25,5 @@ val containsKey_table : model_table_t
 val mapPut_table : model_table_t
 val optional_get_table : model_table_t
 val optional_isPresent_table : model_table_t
+val noreturn_table : model_table_t
 val true_on_null_table : model_table_t
diff --git a/infer/src/eradicate/models.ml b/infer/src/eradicate/models.ml
index ff990ae21..ebc3d9677 100644
--- a/infer/src/eradicate/models.ml
+++ b/infer/src/eradicate/models.ml
@@ -139,7 +139,7 @@ let get_modelled_annotated_signature proc_attributes =
     else ann_sig in
   let lookup_models_strict ann_sig =
     if use_models
-       && Hashtbl.mem annotated_table_strict proc_id
+    && Hashtbl.mem annotated_table_strict proc_id
     then
       Annotations.annotated_signature_mark_return_strict ann_sig
     else
@@ -179,6 +179,10 @@ let is_check_state proc_name =
 let is_check_argument proc_name =
   table_has_procedure check_argument_table proc_name
 
+(** Check if the procedure does not return. *)
+let is_noreturn proc_name =
+  table_has_procedure noreturn_table proc_name
+
 (** Check if the procedure is Optional.get(). *)
 let is_optional_get proc_name =
   table_has_procedure optional_get_table proc_name
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index db05056e4..f3ac4a541 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -1066,7 +1066,12 @@ let typecheck_node
   let instr_ref_gen = TypeErr.InstrRef.create_generator node in
 
   let typestates_exn = ref [] in
+  let noreturn = ref false in
+
   let handle_exceptions typestate instr = match instr with
+    | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), _, _, _)
+      when Models.is_noreturn callee_pname ->
+        noreturn := true
     | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), _, _, _) ->
         let callee_attributes_opt =
           Specs.proc_resolve_attributes callee_pname in
@@ -1101,6 +1106,10 @@ let typecheck_node
   TypeErr.node_reset_forall canonical_node;
 
   let typestate_succ = IList.fold_left (do_instruction ext) typestate instrs in
-  if Procdesc.Node.get_kind node = Procdesc.Node.exn_sink_kind
-  then [], [] (* don't propagate exceptions to exit node *)
+  let dont_propagate =
+    Procdesc.Node.get_kind node = Procdesc.Node.exn_sink_kind (* don't propagate exceptions *)
+    ||
+    !noreturn in
+  if dont_propagate
+  then [], [] (* don't propagate to exit node *)
   else [typestate_succ], !typestates_exn
diff --git a/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java b/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java
index 391c7c500..c2ba3ae3e 100644
--- a/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java
+++ b/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java
@@ -292,4 +292,19 @@ public class NullMethodCall {
       }
     }
   }
+
+  class SystemExitDoesNotReturn {
+    native boolean whoknows();
+
+    void testOK() {
+      String s = null;
+      if (whoknows()) {
+        s = "a";
+      }
+      else {
+        System.exit(1);
+      }
+      int n = s.length();
+    }
+  }
 }