[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

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

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

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

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
+  let dont_propagate =
-  then [], [] (* don't propagate exceptions to exit node *)
+    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

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();
+    }
+  }
 }