[pulse] model some early exit functions

Summary:
Copied on the ownership checker logic: return the initial value of the
domain as return. This can probably be improved.

Reviewed By: mbouaziz

Differential Revision: D12888102

fbshipit-source-id: 9e2dac7fc

infer/src/checkers/Pulse.ml

@@ -89,18 +89,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         read_all actuals astate
 
 
-  let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc astate =
+  let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) flags call_loc astate =
     let model =
       match call with
       | Indirect _ ->
           (* function pointer, etc.: skip for now *)
           None
       | Direct callee_pname ->
-          PulseModels.dispatch callee_pname
+          PulseModels.dispatch callee_pname flags
     in
     match model with
     | None ->
-        exec_call ret call actuals _flags call_loc astate >>| PulseDomain.havoc_var (fst ret)
+        exec_call ret call actuals flags call_loc astate >>| PulseDomain.havoc_var (fst ret)
     | Some model ->
         model call_loc ~ret ~actuals astate
 

infer/src/checkers/PulseModels.ml

@@ -17,6 +17,10 @@ type exec_fun =
 
 type model = exec_fun
 
+module Misc = struct
+  let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok PulseDomain.initial
+end
+
 module C = struct
   let free : model =
    fun location ~ret:_ ~actuals astate ->
@@ -119,7 +123,10 @@ let builtins_dispatcher =
     [ (BuiltinDecl.__delete, Cplusplus.delete)
     ; (BuiltinDecl.__placement_new, Cplusplus.placement_new)
     ; (BuiltinDecl.__variable_initialization, C.variable_initialization)
-    ; (BuiltinDecl.free, C.free) ]
+    ; (BuiltinDecl.abort, Misc.early_exit)
+    ; (BuiltinDecl.exit, Misc.early_exit)
+    ; (BuiltinDecl.free, C.free)
+    ; (BuiltinDecl.objc_cpp_throw, Misc.early_exit) ]
   in
   let builtins_map =
     Hashtbl.create
@@ -137,9 +144,13 @@ let builtins_dispatcher =
   fun proc_name -> Hashtbl.find builtins_map proc_name
 
 
-let dispatch proc_name =
+let dispatch proc_name flags =
   match builtins_dispatcher proc_name with
+  | Some _ as result ->
+      result
+  | None -> (
+    match ProcNameDispatcher.dispatch () proc_name with
     | Some _ as result ->
         result
     | None ->
-      ProcNameDispatcher.dispatch () proc_name
+        if flags.CallFlags.cf_noreturn then Some Misc.early_exit else None )

infer/src/checkers/PulseModels.mli

@@ -15,4 +15,4 @@ type exec_fun =
 
 type model = exec_fun
 
-val dispatch : Typ.Procname.t -> model option
+val dispatch : Typ.Procname.t -> CallFlags.t -> model option

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

@@ -2,9 +2,6 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AF
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70, column 7 here,accessed `*(ptr)` here]
 codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 26, column 5 here,accessed `*(result)` here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_delete_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 111, column 5 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_delete_throw_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 129, column 5 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, FP_gated_exit_abort_ok, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 120, column 5 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 82, column 5 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 18, column 3 here,accessed `s` here]

infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp

@@ -105,7 +105,7 @@ void use_in_loop_bad() {
   }
 }
 
-Simple* FP_gated_delete_abort_ok(bool b) {
+Simple* gated_delete_abort_ok(bool b) {
   auto s = new Simple{1};
   if (b) {
     delete s;
@@ -114,7 +114,7 @@ Simple* FP_gated_delete_abort_ok(bool b) {
   return s;
 }
 
-Simple* FP_gated_exit_abort_ok(bool b) {
+Simple* gated_exit_abort_ok(bool b) {
   auto s = new Simple{1};
   if (b) {
     delete s;
@@ -123,7 +123,7 @@ Simple* FP_gated_exit_abort_ok(bool b) {
   return s;
 }
 
-Simple* FP_gated_delete_throw_ok(bool b) {
+Simple* gated_delete_throw_ok(bool b) {
   auto s = new Simple{1};
   if (b) {
     delete s;