From 7b3bf7b4b591717f99692683f011ddd7aa08842c Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Tue, 16 Jan 2018 13:04:08 -0800
Subject: [PATCH] [dispatcher] Match all suffixes

Summary:
`&::.*-->` allows to match any path end.
Used for models of `std::array` to force unmodelled functions (and types) to have a Skip summary

Depends on D6408415

Reviewed By: jvillard

Differential Revision: D6611203

fbshipit-source-id: 6663b2c
---
 infer/src/IR/ProcnameDispatcher.ml            | 46 ++++++++++++++++---
 infer/src/IR/ProcnameDispatcher.mli           | 10 ++++
 .../src/bufferoverrun/bufferOverrunModels.ml  | 32 ++++++++++++-
 3 files changed, 80 insertions(+), 8 deletions(-)

diff --git a/infer/src/IR/ProcnameDispatcher.ml b/infer/src/IR/ProcnameDispatcher.ml
index e70066943..63fc627ae 100644
--- a/infer/src/IR/ProcnameDispatcher.ml
+++ b/infer/src/IR/ProcnameDispatcher.ml
@@ -199,6 +199,34 @@ let name_cons
     {on_objc_cpp; on_qual_name; get_markers}
 
 
+let all_names_cons
+    : ('f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, non_empty) path_matcher
+      -> ('f_in, 'f_out, 'captured_tpes, 'markers_in, 'markers_out, non_empty) path_matcher =
+  fun m ->
+    let {on_templated_name; get_markers; path_extra= PathNonEmpty {on_objc_cpp}} = m in
+    let rec on_templated_name_rec f templated_name =
+      match on_templated_name f templated_name with
+      | Some _ as some ->
+          some
+      | None ->
+          let qual_name, _template_args = templated_name in
+          match QualifiedCppName.extract_last qual_name with
+          | None ->
+              None
+          | Some (_last, rest) ->
+              on_templated_name_rec f (rest, [])
+    in
+    let on_templated_name = on_templated_name_rec in
+    let on_objc_cpp f objc_cpp =
+      match on_objc_cpp f objc_cpp with
+      | Some _ as some ->
+          some
+      | None ->
+          on_templated_name f (templated_name_of_class_name objc_cpp.Typ.Procname.class_name)
+    in
+    {on_templated_name; get_markers; path_extra= PathNonEmpty {on_objc_cpp}}
+
+
 let templ_begin
     : ('f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
       -> ('f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, accept_more) templ_matcher =
@@ -496,6 +524,8 @@ module Common = struct
 
   let ( &::! ) path_matcher name = name_cons path_matcher name
 
+  let ( &::.*! ) path_matcher () = all_names_cons path_matcher
+
   let ( ~- ) name = empty &::! name
 
   let ( &+ ) templ_matcher template_arg = templ_cons templ_matcher template_arg
@@ -508,9 +538,9 @@ module Common = struct
 
   let ( >:: ) templ_matcher name = templ_matcher >! () &::! name
 
-  let ( &+...>:: ) templ_matcher name = templ_matcher &+ any_template_args >:: name
+  let ( &+...>:: ) templ_matcher name = templ_matcher &+...>! () &::! name
 
-  let ( &:: ) path_matcher name = path_matcher < any_template_args >:: name
+  let ( &:: ) name_matcher name = name_matcher <...>! () &::! name
 
   let ( <>:: ) name_matcher name = name_matcher <! () >:: name
 end
@@ -734,7 +764,7 @@ module Procname = struct
 
   let ( $--> ) args_matcher f = args_matcher $* no_args_left $*--> f
 
-  let ( $ ) name_matcher one_arg = name_matcher < any_template_args >$ one_arg
+  let ( $ ) name_matcher func_arg = name_matcher <...>! () $! () $+ func_arg
 
   let ( <>$ ) name_matcher one_arg = name_matcher <! () >$ one_arg
 
@@ -744,14 +774,16 @@ module Procname = struct
 
   let ( >$$--> ) templ_matcher f = templ_matcher >$! () $--> f
 
-  let ( $$--> ) name_matcher f = name_matcher < any_template_args >$$--> f
+  let ( $$--> ) name_matcher f = name_matcher <...>! () $! () $--> f
 
   let ( <>$$--> ) name_matcher f = name_matcher <! () >$$--> f
 
-  let ( &--> ) name_matcher f = name_matcher < any_template_args >--> f
+  let ( &--> ) name_matcher f = name_matcher <...>! () $! () $+...$--> f
 
   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
@@ -777,5 +809,7 @@ module TypName = struct
 
   let ( <>--> ) name_matcher f = name_matcher <! () >--> f
 
-  let ( &--> ) name_matcher f = name_matcher < any_template_args >--> f
+  let ( &--> ) name_matcher f = name_matcher <...>! () &-->! f
+
+  let ( &::.*--> ) name_matcher f = name_matcher <...>! () &::.*! () &-->! f
 end
diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli
index d75b2ff36..a152ebc32 100644
--- a/infer/src/IR/ProcnameDispatcher.mli
+++ b/infer/src/IR/ProcnameDispatcher.mli
@@ -265,6 +265,11 @@ module Procname : sig
     ('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in -> 'f_out matcher
   (** After a name, accepts NO template arguments, accepts ALL function arguments, binds the function *)
 
+  val ( &::.*--> ) :
+    ('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in -> 'f_out matcher
+  (** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates),
+      accepts ALL function arguments, binds the function *)
+
   val ( $!--> ) :
     ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher
   (** Ends function arguments, accepts NO more function arguments.
@@ -287,5 +292,10 @@ module TypName : sig
 
   val ( &--> ) :
     ('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in -> 'f_out typ_matcher
+
+  val ( &::.*--> ) :
+    ('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in -> 'f_out typ_matcher
+  (** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates),
+        accepts ALL function arguments, binds the function *)
 end
 [@@warning "-32"]
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index cb8fbbf36..b03efa6ca 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -242,6 +242,31 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
         BoUtils.Check.lindex ~array_exp ~index_exp mem pname location cond_set
       in
       {exec; check}
+
+
+    let no_model =
+      let exec pname ret _node location mem =
+        L.(debug BufferOverrun Verbose)
+          "No model for %a at %a" Typ.Procname.pp pname Location.pp location ;
+        mem
+      in
+      {exec; check= no_check}
+
+
+    let no_typ_model =
+      let no_model kind pname location mem =
+        L.(debug BufferOverrun Verbose)
+          "No %s type model in %a at %a" kind Typ.Procname.pp pname Location.pp location ;
+        mem
+      in
+      let declare_local ~decl_local:_ pname _node location _loc ~inst_num ~dimension:_ mem =
+        (no_model "local" pname location mem, inst_num)
+      in
+      let declare_symbolic ~decl_sym_val:_ pname _tenv _node location ~depth:_ _loc ~inst_num:_
+          ~new_sym_num:_ ~new_alloc_num:_ mem =
+        no_model "symbolic" pname location mem
+      in
+      {declare_local; declare_symbolic}
   end
 
   module Procname = struct
@@ -268,12 +293,15 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
           $+? capt_exp $--> Folly.Split.std_vector
         ; std_array0 >:: "array" &--> StdArray.constructor
         ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at
-        ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at ]
+        ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at
+        ; -"std" &:: "array" &::.*--> StdArray.no_model ]
   end
 
   module TypName = struct
     let dispatch : typ_model ProcnameDispatcher.typ_dispatcher =
       let open ProcnameDispatcher.TypName in
-      make_dispatcher [-"std" &:: "array" < capt_typ `T &+ capt_int >--> StdArray.typ]
+      make_dispatcher
+        [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> StdArray.typ
+        ; -"std" &:: "array" &::.*--> StdArray.no_typ_model ]
   end
 end