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