[pulse] add option to skip functions/classes

Summary:
This can be useful to make pulse forget about tricky parts of the code.

Treat "skipped" procedures as unknown so heuristics for mutating the
return value and parameters passed by reference are applied.

Reviewed By: ezgicicek

Differential Revision: D23729410

fbshipit-source-id: d7a4924a8

infer/man/man1/infer-analyze.txt

@@ -261,6 +261,9 @@ OPTIONS
        --pulse-model-return-nonnull +string
            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
+
        --pulse-model-transfer-ownership +string
            Methods that should be modelled as transfering memory ownership in
            Pulse. Accepted formats are method or namespace::method

infer/man/man1/infer-full.txt

@@ -920,6 +920,10 @@ OPTIONS
            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       
+    See also infer-analyze(1).
+
        --pulse-model-transfer-ownership +string
            Methods that should be modelled as transfering memory ownership in
            Pulse. Accepted formats are method or namespace::method       
@@ -1724,6 +1728,9 @@ INTERNAL OPTIONS
        --pulse-model-return-nonnull-reset
            Set --pulse-model-return-nonnull to the empty list.
 
+       --pulse-model-skip-pattern-reset
+           Cancel the effect of --pulse-model-skip-pattern.
+
        --pulse-model-transfer-ownership-reset
            Set --pulse-model-transfer-ownership to the empty list.
 

infer/man/man1/infer.txt

@@ -920,6 +920,10 @@ OPTIONS
            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       
+    See also infer-analyze(1).
+
        --pulse-model-transfer-ownership +string
            Methods that should be modelled as transfering memory ownership in
            Pulse. Accepted formats are method or namespace::method       

infer/src/absint/ProcnameDispatcher.ml

@@ -852,6 +852,8 @@ module Call = struct
 
   let ( &::.*--> ) name_matcher f = name_matcher <...>! () &::.*! () $! () $+...$--> f
 
+  let ( &::.*++> ) name_matcher f = name_matcher <...>! () &::.*! () $! () $++$--> f
+
   let ( $!--> ) args_matcher f =
     args_matcher $* exact_args_or_retry wrong_args_internal_error $*--> f
 end

infer/src/absint/ProcnameDispatcher.mli

@@ -139,7 +139,6 @@ module type NameCommon = sig
        ('context, 'f_in, 'f_out, 'arg_payload) name_matcher
     -> 'f_in
     -> ('context, 'f_out, 'arg_payload) matcher
-
   (** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates),
       accepts ALL function arguments, binds the function *)
 end
@@ -324,6 +323,13 @@ module Call : sig
   (** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates),
       accepts ALL function arguments, binds the function *)
 
+  val ( &::.*++> ) :
+       ('context, 'f_in, 'arg_payload FuncArg.t list -> 'f_out, 'arg_payload) name_matcher
+    -> 'f_in
+    -> ('context, 'f_out, 'arg_payload) matcher
+  (** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates),
+      captures ALL function arguments as a list, binds the function *)
+
   val ( $!--> ) :
        ('context, 'f_in, 'f_proc_out, 'f_out, 'arg_payload) args_matcher
     -> 'f_in

infer/src/base/Config.ml

@@ -1874,6 +1874,12 @@ and pulse_model_return_nonnull =
     "Methods that should be modelled as returning non-null in Pulse"
 
 
+and pulse_model_skip_pattern =
+  CLOpt.mk_string_opt ~long:"pulse-model-skip-pattern"
+    ~in_help:InferCommand.[(Analyze, manual_generic)]
+    "Regex of methods that should be modelled as \"skip\" in Pulse"
+
+
 and pulse_model_transfer_ownership =
   CLOpt.mk_string_list ~long:"pulse-model-transfer-ownership"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
@@ -3002,6 +3008,8 @@ and pulse_model_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_
 
 and pulse_model_return_nonnull = !pulse_model_return_nonnull
 
+and pulse_model_skip_pattern = Option.map ~f:Str.regexp !pulse_model_skip_pattern
+
 and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership =
   let models =
     let re = Str.regexp "::" in

infer/src/base/Config.mli

@@ -463,6 +463,8 @@ val pulse_model_release_pattern : Str.regexp option
 
 val pulse_model_return_nonnull : string list
 
+val pulse_model_skip_pattern : Str.regexp option
+
 val pulse_model_transfer_ownership_namespace : (string * string) list
 
 val pulse_model_transfer_ownership : string list

infer/src/pulse/PulseModels.ml

@@ -74,7 +74,28 @@ module Misc = struct
     PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue
 
 
-  let skip : model = fun _ ~callee_procname:_ _ ~ret:_ astate -> PulseOperations.ok_continue astate
+  (** Pretend the function call is a call to an "unknown" function, i.e. a function for which we
+      don't have the implementation. This triggers a bunch of heuristics, e.g. to havoc arguments we
+      suspect are passed by reference. *)
+  let unknown_call skip_reason args : model =
+   fun _ ~callee_procname location ~ret astate ->
+    let actuals =
+      List.map args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= actual; typ} ->
+          (actual, typ) )
+    in
+    let formals_opt =
+      AnalysisCallbacks.proc_resolve_attributes callee_procname
+      |> Option.map ~f:ProcAttributes.get_pvar_formals
+    in
+    Ok
+      [ ExecutionDomain.ContinueProgram
+          (PulseOperations.unknown_call location (Model skip_reason) ~ret ~actuals ~formals_opt
+             astate) ]
+
+
+  (** don't actually do nothing, apply the heuristics for unknown calls (this may or may not be a
+      good idea) *)
+  let skip = unknown_call
 
   let nondet ~fn_name : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
@@ -819,7 +840,7 @@ end
 module StringSet = Caml.Set.Make (String)
 
 module ProcNameDispatcher = struct
-  let dispatch : (Tenv.t, model, arg_payload) ProcnameDispatcher.Call.dispatcher =
+  let dispatch : (Tenv.t * Procname.t, model, arg_payload) ProcnameDispatcher.Call.dispatcher =
     let open ProcnameDispatcher.Call in
     let match_builtin builtin _ s = String.equal s (Procname.get_method builtin) in
     let pushback_modeled =
@@ -859,6 +880,13 @@ module ProcNameDispatcher = struct
         ~model:(fun m -> Misc.return_positive ~desc:m)
         Config.pulse_model_return_nonnull
     in
+    let match_regexp_opt r_opt (_tenv, proc_name) _ =
+      Option.value_map ~default:false r_opt ~f:(fun r ->
+          let s = Procname.to_string proc_name in
+          let r = Str.string_match r s 0 in
+          r )
+    in
+    let map_context_tenv f (x, _) = f x in
     make_dispatcher
       ( transfer_ownership_matchers @ abort_matchers @ return_nonnull_matchers
       @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
@@ -872,13 +900,16 @@ module ProcNameDispatcher = struct
         ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit
         ; +match_builtin BuiltinDecl.__infer_initializer_list
           <>$ capt_arg_payload $+...$--> Misc.id_first_arg
-        ; +PatternMatch.Java.implements_lang "System" &:: "exit" <>--> Misc.early_exit
+        ; +map_context_tenv (PatternMatch.Java.implements_lang "System")
+          &:: "exit" <>--> Misc.early_exit
         ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size
         ; (* consider that all fbstrings are small strings to avoid false positives due to manual
              ref-counting *)
           -"folly" &:: "fbstring_core" &:: "category" &--> Misc.return_int Int64.zero
-        ; -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip
-        ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip
+        ; -"folly" &:: "DelayedDestruction" &:: "destroy"
+          &++> Misc.skip "folly::DelayedDestruction::destroy is modelled as skip"
+        ; -"folly" &:: "SocketAddress" &:: "~SocketAddress"
+          &++> Misc.skip "folly::SocketAddress's destructor is modelled as skip"
         ; -"folly" &:: "Optional" &:: "Optional" <>$ capt_arg_payload
           $+ any_arg_of_typ (-"folly" &:: "None")
           $--> FollyOptional.assign_none ~desc:"folly::Optional::Optional(=None)"
@@ -906,11 +937,11 @@ module ProcNameDispatcher = struct
         ; -"std" &:: "function" &:: "operator()" $ capt_arg $++$--> StdFunction.operator_call
         ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg
           $--> StdFunction.assign ~desc:"std::function::operator="
-        ; +PatternMatch.Java.implements_lang "Object"
+        ; +map_context_tenv (PatternMatch.Java.implements_lang "Object")
           &:: "clone" $ capt_arg_payload $--> JavaObject.clone
-        ; ( +PatternMatch.Java.implements_lang "System"
+        ;  +map_context_tenv (PatternMatch.Java.implements_lang "System")
           &:: "arraycopy" $ capt_arg_payload $+ any_arg $+ capt_arg_payload
-          $+...$--> fun src dest -> Misc.shallow_copy_model "System.arraycopy" dest src )
+          $+...$--> (fun src dest -> Misc.shallow_copy_model "System.arraycopy" dest src )
         ; -"std" &:: "atomic" &:: "atomic" <>$ capt_arg_payload $+ capt_arg_payload
           $--> StdAtomicInteger.constructor
         ; -"std" &:: "__atomic_base" &:: "fetch_add" <>$ capt_arg_payload $+ capt_arg_payload
@@ -1002,79 +1033,81 @@ module ProcNameDispatcher = struct
         ; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_arg_payload
           $--> StdVector.invalidate_references ShrinkToFit
         ; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back
-        ; +PatternMatch.Java.implements_collection
+        ; +map_context_tenv PatternMatch.Java.implements_collection
           &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $--> JavaCollection.add
-        ; +PatternMatch.Java.implements_list
+        ; +map_context_tenv PatternMatch.Java.implements_list
           &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload
           $--> JavaCollection.add_at
-        ; +PatternMatch.Java.implements_collection
+        ; +map_context_tenv PatternMatch.Java.implements_collection
           &:: "remove" <>$ capt_arg_payload $+ any_arg $--> JavaCollection.remove
-        ; +PatternMatch.Java.implements_list
+        ; +map_context_tenv PatternMatch.Java.implements_list
           &:: "remove" <>$ capt_arg_payload $+ capt_arg_payload $+ any_arg
           $--> JavaCollection.remove_at
-        ; +PatternMatch.Java.implements_collection
+        ; +map_context_tenv PatternMatch.Java.implements_collection
           &::+ (fun _ str -> StringSet.mem str pushback_modeled)
           <>$ capt_arg_payload $+...$--> StdVector.push_back
-        ; +PatternMatch.Java.implements_queue
+        ; +map_context_tenv PatternMatch.Java.implements_queue
           &::+ (fun _ str -> StringSet.mem str pushback_modeled)
           <>$ capt_arg_payload $+...$--> StdVector.push_back
-        ; +PatternMatch.Java.implements_lang "StringBuilder"
+        ; +map_context_tenv( PatternMatch.Java.implements_lang "StringBuilder")
           &::+ (fun _ str -> StringSet.mem str pushback_modeled)
           <>$ capt_arg_payload $+...$--> StdVector.push_back
-        ; +PatternMatch.Java.implements_lang "StringBuilder"
+        ; +map_context_tenv( PatternMatch.Java.implements_lang "StringBuilder")
           &:: "setLength" <>$ capt_arg_payload
           $+...$--> StdVector.invalidate_references ShrinkToFit
-        ; +PatternMatch.Java.implements_lang "String"
+        ; +map_context_tenv (PatternMatch.Java.implements_lang "String")
           &::+ (fun _ str -> StringSet.mem str pushback_modeled)
           <>$ capt_arg_payload $+...$--> StdVector.push_back
-        ; +PatternMatch.Java.implements_iterator
+        ; +map_context_tenv PatternMatch.Java.implements_iterator
           &:: "remove" <>$ capt_arg_payload
           $+...$--> JavaIterator.remove ~desc:"remove"
-        ; +PatternMatch.Java.implements_map &:: "put" <>$ capt_arg_payload
-          $+...$--> StdVector.push_back
-        ; +PatternMatch.Java.implements_map &:: "putAll" <>$ capt_arg_payload
-          $+...$--> StdVector.push_back
+        ; +map_context_tenv PatternMatch.Java.implements_map
+          &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back
+        ; +map_context_tenv PatternMatch.Java.implements_map
+          &:: "putAll" <>$ capt_arg_payload $+...$--> StdVector.push_back
         ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve
-        ; +PatternMatch.Java.implements_collection
+        ; +map_context_tenv PatternMatch.Java.implements_collection
           &:: "get" <>$ capt_arg_payload $+ capt_arg_payload
           $--> StdVector.at ~desc:"Collection.get()"
-        ; +PatternMatch.Java.implements_list
+        ; +map_context_tenv PatternMatch.Java.implements_list
           &:: "set" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload
           $--> JavaCollection.set
-        ; +PatternMatch.Java.implements_iterator
+        ; +map_context_tenv PatternMatch.Java.implements_iterator
           &:: "hasNext"
           &--> Misc.nondet ~fn_name:"Iterator.hasNext()"
-        ; +PatternMatch.Java.implements_enumeration
+        ; +map_context_tenv PatternMatch.Java.implements_enumeration
           &:: "hasMoreElements"
           &--> Misc.nondet ~fn_name:"Enumeration.hasMoreElements()"
-        ; +PatternMatch.Java.implements_lang "Object"
+        ; +map_context_tenv( PatternMatch.Java.implements_lang "Object")
           &:: "equals"
           &--> Misc.nondet ~fn_name:"Object.equals"
-        ; +PatternMatch.Java.implements_lang "Iterable"
+        ; +map_context_tenv (PatternMatch.Java.implements_lang "Iterable")
           &:: "iterator" <>$ capt_arg_payload
           $+...$--> JavaIterator.constructor ~desc:"Iterable.iterator"
-        ; +PatternMatch.Java.implements_iterator
+        ; +map_context_tenv PatternMatch.Java.implements_iterator
           &:: "next" <>$ capt_arg_payload
           $!--> JavaIterator.next ~desc:"Iterator.next()"
-        ; ( +PatternMatch.Java.implements_enumeration
+        ; ( +map_context_tenv PatternMatch.Java.implements_enumeration
           &:: "nextElement" <>$ capt_arg_payload
           $!--> fun x ->
           StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) )
-        ; +PatternMatch.ObjectiveC.is_core_graphics_create_or_copy &++> C.malloc
-        ; +PatternMatch.ObjectiveC.is_core_foundation_create_or_copy &++> C.malloc
+        ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_create_or_copy &++> C.malloc
+        ; +map_context_tenv PatternMatch.ObjectiveC.is_core_foundation_create_or_copy &++> C.malloc
         ; +match_builtin BuiltinDecl.malloc_no_fail <>$ capt_arg_payload $--> C.malloc_not_null
-        ; +PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null
-        ; +PatternMatch.ObjectiveC.is_core_graphics_release
+        ; +map_context_tenv PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null
+        ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_release
           <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
         ; -"CFRelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
-        ; +PatternMatch.ObjectiveC.is_modelled_as_release
+        ; +map_context_tenv PatternMatch.ObjectiveC.is_modelled_as_release
           <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
         ; -"CFAutorelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
         ; -"CFBridgingRelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
         ; +match_builtin BuiltinDecl.__objc_bridge_transfer
           <>$ 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 ] )
+        ; -"NSObject" &:: "init" <>$ capt_arg_payload $--> Misc.id_first_arg
+        ; +match_regexp_opt Config.pulse_model_skip_pattern
+          &::.*++> Misc.skip "modelled as skip due to configuration option" ] )
 end
 
-let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args
+let dispatch tenv proc_name args = ProcNameDispatcher.dispatch (tenv, proc_name) proc_name args

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

@@ -0,0 +1,3 @@
+{
+  "pulse-model-skip-pattern": "skip_model::SkipAll::.*\\|.*SkipSome<.*>::skip_me"
+}

infer/tests/codetoanalyze/cpp/pulse/skip_config.cpp

@@ -0,0 +1,49 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+namespace skip_model {
+struct SkipAll {
+  int* foo() { return nullptr; }
+  static int* goo() { return nullptr; }
+};
+
+template <typename T>
+struct SkipSome {
+  int* skip_me(int**) { return nullptr; }
+  static int no_skip() { return 42; }
+};
+
+void test_config_no_skip_ok() {
+  if (SkipSome<SkipSome<int>>::no_skip() != 42) {
+    int* p = nullptr;
+    *p = 42;
+  }
+}
+
+void test_config_skip_me_ok() {
+  int* may_be_mutated = nullptr;
+  int* p = nullptr;
+  SkipSome<SkipSome<int>> x;
+  p = x.skip_me(&may_be_mutated);
+  *p = 42;
+  *may_be_mutated = 42;
+}
+} // namespace skip_model
+
+namespace skip_another_namespace {
+void test_config_foo_ok() {
+  int* p = nullptr;
+  skip_model::SkipAll x;
+  p = x.foo();
+  *p = 42;
+}
+void test_config_goo_ok() {
+  int* p = skip_model::SkipAll::goo();
+  *p = 42;
+}
+
+} // namespace skip_another_namespace