[pulse] Adapting --pulse-model-return-nonnull for Java

Summary:
The `--pulse-model-return-nonnull` config option currently works for C++. Now we
will be using it also for Java. Changing type from string list to regexp to
make it more general.

Reviewed By: ezgicicek

Differential Revision: D26367888

fbshipit-source-id: 9a06b9b32

infer/man/man1/infer-analyze.txt

@@ -271,8 +271,9 @@ OPTIONS
        --pulse-model-release-pattern string
            Regex of methods that should be modelled as release in Pulse
 
-       --pulse-model-return-nonnull +string
-           Methods that should be modelled as returning non-null in Pulse
+       --pulse-model-return-nonnull string
+           Regex of methods that should be modelled as returning non-null in
+           Pulse
 
        --pulse-model-skip-pattern string
            Regex of methods that should be modelled as "skip" in Pulse

infer/man/man1/infer-full.txt

@@ -955,9 +955,9 @@ OPTIONS
            Regex of methods that should be modelled as release in Pulse       
     See also infer-analyze(1).
 
-       --pulse-model-return-nonnull +string
-           Methods that should be modelled as returning non-null in Pulse       
-    See also infer-analyze(1).
+       --pulse-model-return-nonnull string
+           Regex of methods that should be modelled as returning non-null in
+           Pulse           See also infer-analyze(1).
 
        --pulse-model-skip-pattern string
            Regex of methods that should be modelled as "skip" in Pulse       
@@ -1820,7 +1820,7 @@ INTERNAL OPTIONS
            Cancel the effect of --pulse-model-release-pattern.
 
        --pulse-model-return-nonnull-reset
-           Set --pulse-model-return-nonnull to the empty list.
+           Cancel the effect of --pulse-model-return-nonnull.
 
        --pulse-model-skip-pattern-reset
            Cancel the effect of --pulse-model-skip-pattern.

infer/man/man1/infer.txt

@@ -955,9 +955,9 @@ OPTIONS
            Regex of methods that should be modelled as release in Pulse       
     See also infer-analyze(1).
 
-       --pulse-model-return-nonnull +string
-           Methods that should be modelled as returning non-null in Pulse       
-    See also infer-analyze(1).
+       --pulse-model-return-nonnull string
+           Regex of methods that should be modelled as returning non-null in
+           Pulse           See also infer-analyze(1).
 
        --pulse-model-skip-pattern string
            Regex of methods that should be modelled as "skip" in Pulse       

infer/src/base/Config.ml

@@ -1905,9 +1905,9 @@ and pulse_model_release_pattern =
 
 
 and pulse_model_return_nonnull =
-  CLOpt.mk_string_list ~long:"pulse-model-return-nonnull"
+  CLOpt.mk_string_opt ~long:"pulse-model-return-nonnull"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
-    "Methods that should be modelled as returning non-null in Pulse"
+    "Regex of methods that should be modelled as returning non-null in Pulse"
 
 
 and pulse_model_skip_pattern =
@@ -3137,7 +3137,7 @@ and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_patt
 
 and pulse_model_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_pattern
 
-and pulse_model_return_nonnull = RevList.to_list !pulse_model_return_nonnull
+and pulse_model_return_nonnull = Option.map ~f:Str.regexp !pulse_model_return_nonnull
 
 and pulse_model_skip_pattern = Option.map ~f:Str.regexp !pulse_model_skip_pattern
 

infer/src/base/Config.mli

@@ -481,7 +481,7 @@ val pulse_model_alloc_pattern : Str.regexp option
 
 val pulse_model_release_pattern : Str.regexp option
 
-val pulse_model_return_nonnull : string list
+val pulse_model_return_nonnull : Str.regexp option
 
 val pulse_model_skip_pattern : Str.regexp option
 

infer/src/pulse/PulseModels.ml

@@ -1075,11 +1075,6 @@ module ProcNameDispatcher = struct
     let abort_matchers =
       get_cpp_matchers ~model:(fun _ -> Misc.early_exit) Config.pulse_model_abort
     in
-    let return_nonnull_matchers =
-      get_cpp_matchers
-        ~model:(fun m -> Misc.return_positive ~desc:m)
-        Config.pulse_model_return_nonnull
-    in
     let match_regexp_opt r_opt (_tenv, proc_name) _ =
       Option.exists r_opt ~f:(fun r ->
           let s = Procname.to_string proc_name in
@@ -1087,7 +1082,7 @@ module ProcNameDispatcher = struct
     in
     let map_context_tenv f (x, _) = f x in
     make_dispatcher
-      ( transfer_ownership_matchers @ abort_matchers @ return_nonnull_matchers
+      ( transfer_ownership_matchers @ abort_matchers
       @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
         ; +match_builtin BuiltinDecl.malloc <>$ capt_exp $--> C.malloc
         ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete
@@ -1382,6 +1377,9 @@ module ProcNameDispatcher = struct
           <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
         ; +match_builtin BuiltinDecl.__objc_alloc_no_fail <>$ capt_exp $--> ObjC.alloc_not_null
         ; -"NSObject" &:: "init" <>$ capt_arg_payload $--> Misc.id_first_arg
+        ; +match_regexp_opt Config.pulse_model_return_nonnull
+          &::.*--> Misc.return_positive
+                     ~desc:"modelled as returning not null due to configuration option"
         ; +match_regexp_opt Config.pulse_model_skip_pattern
           &::.*++> Misc.skip "modelled as skip due to configuration option" ] )
 end

infer/tests/codetoanalyze/cpp/pulse/.inferconfig

@@ -1,5 +1,5 @@
 {
   "pulse-model-abort": ["ns1::ns2::fun_abort"],
-  "pulse-model-return-nonnull": ["Handle::get"],
+  "pulse-model-return-nonnull": "Handle::get",
   "pulse-model-skip-pattern": "skip_model::SkipAll::.*\\|.*SkipSome<.*>::skip_me"
 }