From a73162d8e4786c441dc724868004c0b356eede41 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 20 Nov 2017 04:47:38 -0800 Subject: [PATCH] [dispatcher] + Capture function argument Summary: Allow capturing function arguments. Model functions don't have to match on a list any more. Depends on D6347829 Reviewed By: jvillard Differential Revision: D6350628 fbshipit-source-id: e88b758 --- infer/src/IR/ProcnameDispatcher.ml | 77 ++++++++++--------- infer/src/IR/ProcnameDispatcher.mli | 45 ++++++----- .../src/bufferoverrun/bufferOverrunChecker.ml | 4 +- .../src/bufferoverrun/bufferOverrunModels.ml | 74 ++++++++---------- 4 files changed, 101 insertions(+), 99 deletions(-) diff --git a/infer/src/IR/ProcnameDispatcher.ml b/infer/src/IR/ProcnameDispatcher.ml index e1df6a67b..439e61b03 100644 --- a/infer/src/IR/ProcnameDispatcher.ml +++ b/infer/src/IR/ProcnameDispatcher.ml @@ -100,15 +100,16 @@ type ('f_in, 'f_out, 'captured_types) proc_matcher = { on_objc_cpp: 'f_in -> objc_cpp -> ('f_out * 'captured_types) option ; on_c: 'f_in -> c -> ('f_out * 'captured_types) option } -type 'captured_types on_args = 'captured_types -> FuncArg.t list -> FuncArg.t list option +type ('f_in, 'f_out, 'captured_types) on_args = + 'captured_types -> 'f_in * FuncArg.t list -> ('f_out * FuncArg.t list) option -type ('f_in, 'f_out, 'captured_types, 'markers) args_matcher = - { on_proc: ('f_in, 'f_out, 'captured_types) proc_matcher - ; on_args: 'captured_types on_args +type ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher = + { on_proc: ('f_in, 'f_proc_out, 'captured_types) proc_matcher + ; on_args: ('f_proc_out, 'f_out, 'captured_types) on_args ; markers: 'markers } -type ('captured_types, 'markers) func_arg = - {eat_func_arg: 'captured_types on_args; marker_static_checker: 'markers -> bool} +type ('f_in, 'f_out, 'captured_types, 'markers) func_arg = + {eat_func_arg: ('f_in, 'f_out, 'captured_types) on_args; marker_static_checker: 'markers -> bool} type 'f matcher = Typ.Procname.t -> FuncArg.t list -> 'f option @@ -127,8 +128,9 @@ let pre_to_opt procname args = function f procname args -type ('f, 'captured_types) func_args_end = - on_args:'captured_types on_args -> FuncArg.t list -> 'f * 'captured_types -> 'f pre_result +type ('f_in, 'f_out, 'captured_types) func_args_end = + on_args:('f_in, 'f_out, 'captured_types) on_args -> FuncArg.t list -> 'f_in * 'captured_types + -> 'f_out pre_result type ('f_in, 'f_out) all_args_matcher = { on_objc_cpp: 'f_in -> objc_cpp -> FuncArg.t list -> 'f_out pre_result @@ -244,8 +246,8 @@ let templ_end let args_begin : ('f_in, 'f_out, 'captured_types, unit, 'markers, non_empty) path_matcher - -> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher = - let on_args _capt args = Some args in + -> ('f_in, 'f_out, 'f_out, 'captured_types, 'markers) args_matcher = + let on_args _capt f_args = Some f_args in fun m -> let {on_templated_name; path_extra= PathNonEmpty {on_objc_cpp}; get_markers} = m in let markers = get_markers () in @@ -260,20 +262,20 @@ let args_begin let args_cons - : ('f_in, 'f_out, 'captured_types, 'markers) args_matcher - -> ('captured_types, 'markers) func_arg - -> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher = + : ('f_in, 'f_proc_out, 'f_interm, 'captured_types, 'markers) args_matcher + -> ('f_interm, 'f_out, 'captured_types, 'markers) func_arg + -> ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher = fun m func_arg -> let {on_proc; on_args; markers} = m in let {marker_static_checker; eat_func_arg} = func_arg in assert (marker_static_checker markers) ; - let on_args capt args = on_args capt args |> Option.bind ~f:(eat_func_arg capt) in + let on_args capt f_args = on_args capt f_args |> Option.bind ~f:(eat_func_arg capt) in {on_proc; on_args; markers} let args_end - : ('f_in, 'f_out, 'captured_types, 'markers) args_matcher - -> ('f_out, 'captured_types) func_args_end -> ('f_in, 'f_out) all_args_matcher = + : ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher + -> ('f_proc_out, 'f_out, 'captured_types) func_args_end -> ('f_in, 'f_out) all_args_matcher = fun m func_args_end -> let {on_proc= {on_c; on_objc_cpp}; on_args} = m in let on_c f c args = on_c f c |> pre_bind_opt ~f:(func_args_end ~on_args args) in @@ -381,22 +383,19 @@ let capt_all let no_checker _ = true -let eat_one_func_arg ~match_if capt = function - | arg :: rest when match_if capt arg -> - Some rest - | _ -> - None +let eat_one_func_arg ~match_if capt (f, args) = + match args with arg :: rest when match_if capt arg -> Some (f, rest) | _ -> None (** Eats one arg *) -let any_arg : (_, _) func_arg = +let any_arg : ('f, 'f, _, _) func_arg = let eat_func_arg capt = eat_one_func_arg ~match_if:(fun _ _ -> true) capt in {eat_func_arg; marker_static_checker= no_checker} let mk_typ_nth : ('markers -> 'marker) -> ('captured_types -> 'marker mtyp) -> 'marker - -> ('captured_types, 'markers) func_arg = + -> ('f, 'f, 'captured_types, 'markers) func_arg = fun get_m get_c marker -> let marker_static_checker markers = Polymorphic_compare.( = ) marker (get_m markers) in let eat_func_arg = @@ -407,40 +406,48 @@ let mk_typ_nth (** Matches first captured type *) -let typ1 : 'marker -> ('marker mtyp * _, 'marker * _) func_arg = +let typ1 : 'marker -> ('f, 'f, 'marker mtyp * _, 'marker * _) func_arg = let pos1 (x, _) = x in fun marker -> mk_typ_nth pos1 pos1 marker (** Matches second captured type *) -let typ2 : 'marker -> (_ * ('marker mtyp * _), _ * ('marker * _)) func_arg = +let typ2 : 'marker -> ('f, 'f, _ * ('marker mtyp * _), _ * ('marker * _)) func_arg = let pos2 (_, (x, _)) = x in fun marker -> mk_typ_nth pos2 pos2 marker (** Matches third captured type *) -let typ3 : 'marker -> (_ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) func_arg = +let typ3 : 'marker -> ('f, 'f, _ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) func_arg = let pos3 (_, (_, (x, _))) = x in fun marker -> mk_typ_nth pos3 pos3 marker +let capt_arg : (FuncArg.t -> 'f, 'f, _, _) func_arg = + let eat_func_arg _capt (f, args) = + match args with arg :: rest -> Some (f arg, rest) | _ -> None + in + {eat_func_arg; marker_static_checker= no_checker} + + (* Function args end *) (** Matches if there is no function arguments left *) -let no_args_left : (_, _) func_args_end = - let match_empty_args f = function Some [] -> Matches f | _ -> DoesNotMatch in - fun ~on_args args (f, capt) -> on_args capt args |> match_empty_args f +let no_args_left : (_, _, _) func_args_end = + let match_empty_args = function Some (f, []) -> Matches f | _ -> DoesNotMatch in + fun ~on_args args (f, capt) -> on_args capt (f, args) |> match_empty_args (** Matches any function arguments *) -let any_func_args : (_, _) func_args_end = - fun ~on_args args (f, capt) -> on_args capt args |> pre_map_opt ~f:(fun _ -> f) +let any_func_args : (_, _, _) func_args_end = + fun ~on_args args (f, capt) -> on_args capt (f, args) |> pre_map_opt ~f:fst (** If [func_args_end1] does not match, use [func_args_end2] *) let alternative_args_end - : ('f, 'captured_types) func_args_end -> ('f, 'captured_types) func_args_end - -> ('f, 'captured_types) func_args_end = + : ('f_in, 'f_out, 'captured_types) func_args_end + -> ('f_in, 'f_out, 'captured_types) func_args_end + -> ('f_in, 'f_out, 'captured_types) func_args_end = fun func_args_end1 func_args_end2 ~on_args args f_capt -> match func_args_end1 ~on_args args f_capt with | DoesNotMatch -> @@ -450,11 +457,11 @@ let alternative_args_end (** Retries matching with another matcher *) -let args_end_retry : _ -> (_, _) func_args_end = fun f ~on_args:_ _args _f_capt -> RetryWith f +let args_end_retry : _ -> (_, _, _) func_args_end = fun f ~on_args:_ _args _f_capt -> RetryWith f (** Retries matching with another matcher if the function does not have the exact number/types of args *) -let exact_args_or_retry : 'f -> (_, _) func_args_end = +let exact_args_or_retry : 'f -> (_, _, _) func_args_end = fun f -> alternative_args_end no_args_left (args_end_retry f) diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli index 63a8cd5d1..6d582a0f7 100644 --- a/infer/src/IR/ProcnameDispatcher.mli +++ b/infer/src/IR/ProcnameDispatcher.mli @@ -46,9 +46,9 @@ type ( 'f_in type ('f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, 'list_constraint) templ_matcher -type ('f_in, 'f_out, 'captured_types, 'markers) args_matcher +type ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher -type ('captured_types, 'markers) func_arg +type ('f_in, 'f_out, 'captured_types, 'markers) func_arg type 'f matcher = Typ.Procname.t -> FuncArg.t list -> 'f option @@ -99,16 +99,19 @@ val capt_all : (* Function args *) -val any_arg : (_, _) func_arg +val any_arg : ('f, 'f, _, _) func_arg (** Eats one arg *) -val typ1 : 'marker -> ('marker mtyp * _, 'marker * _) func_arg +val capt_arg : (FuncArg.t -> 'f, 'f, _, _) func_arg +(** Captures one arg *) + +val typ1 : 'marker -> ('f, 'f, 'marker mtyp * _, 'marker * _) func_arg (** Matches first captured type *) -val typ2 : 'marker -> (_ * ('marker mtyp * _), _ * ('marker * _)) func_arg +val typ2 : 'marker -> ('f, 'f, _ * ('marker mtyp * _), _ * ('marker * _)) func_arg (** Matches second captured type *) -val typ3 : 'marker -> (_ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) func_arg +val typ3 : 'marker -> ('f, 'f, _ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) func_arg (** Matches third captured type *) (* A matcher is a rule associating a function [f] to a [C/C++ function/method]: @@ -161,17 +164,18 @@ val ( >:: ) : (** Ends template arguments and starts a name *) val ( $+ ) : - ('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> ('captured_types, 'markers) func_arg - -> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher + ('f_in, 'f_proc_out, 'f_interm, 'captured_types, 'markers) args_matcher + -> ('f_interm, 'f_out, 'captured_types, 'markers) func_arg + -> ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher (** Separate function arguments *) val ( >$ ) : - ('f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher - -> ('captured_types, 'markers) func_arg - -> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher + ('f_in, 'f_proc_out, 'ct, unit, 'cm, _) templ_matcher -> ('f_proc_out, 'f_out, 'ct, 'cm) func_arg + -> ('f_in, 'f_proc_out, 'f_out, 'ct, 'cm) args_matcher (** Ends template arguments and starts function arguments *) -val ( $--> ) : ('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher +val ( $--> ) : + ('f_in, _, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher (** Ends function arguments, binds the function *) val ( &+...>:: ) : @@ -190,15 +194,15 @@ val ( <>:: ) : (** Separates names (accepts NO template arguments on the left one) *) val ( $ ) : - ('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher - -> ('captured_types, 'markers) func_arg - -> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher + ('f_in, 'f_proc_out, 'captured_types, unit, 'markers) name_matcher + -> ('f_proc_out, 'f_out, 'captured_types, 'markers) func_arg + -> ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher (** Ends a name with accept-ALL template arguments and starts function arguments *) val ( <>$ ) : - ('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher - -> ('captured_types, 'markers) func_arg - -> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher + ('f_in, 'f_proc_out, 'captured_types, unit, 'markers) name_matcher + -> ('f_proc_out, 'f_out, 'captured_types, 'markers) func_arg + -> ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher (** Ends a name with accept-NO template arguments and starts function arguments *) val ( >--> ) : @@ -206,7 +210,7 @@ val ( >--> ) : (** Ends template arguments, accepts ALL function arguments, binds the function *) val ( $+...$--> ) : - ('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher + ('f_in, _, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher (** Ends function arguments with eats-ALL and binds the function *) val ( >$$--> ) : @@ -229,7 +233,8 @@ val ( <>--> ) : ('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, 'markers) args_matcher -> 'f_in -> 'f_out matcher +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. If the args do not match, raise an internal error. *) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 3ab07b53c..78c29abe7 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -266,7 +266,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (ret, Const Cfun callee_pname, params, location, _) -> ( match Models.dispatcher callee_pname params with | Some model -> - model callee_pname ret params node location mem + model callee_pname ret node location mem | None -> match Summary.read_summary pdesc callee_pname with | Some summary -> @@ -276,7 +276,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct L.(debug BufferOverrun Verbose) "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp location ; - Models.model_by_value Dom.Val.unknown callee_pname ret params node location mem + Models.model_by_value Dom.Val.unknown callee_pname ret node location mem |> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown ) | Declare_locals (locals, location) -> (* array allocation in stack e.g., int arr[10] *) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 08ed3140e..c03cf23d2 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -19,8 +19,8 @@ module Make (CFG : ProcCfg.S) = struct module Sem = BufferOverrunSemantics.Make (CFG) type model_fun = - Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node -> Location.t - -> Dom.Mem.astate -> Dom.Mem.astate + Typ.Procname.t -> (Ident.t * Typ.t) option -> CFG.node -> Location.t -> Dom.Mem.astate + -> Dom.Mem.astate let set_uninitialized node (typ: Typ.t) ploc mem = match typ.desc with @@ -44,10 +44,10 @@ module Make (CFG : ProcCfg.S) = struct (Typ.mk (Typ.Tint Typ.IChar), Some 1, x) - let model_malloc pname ret params node location mem = + let model_malloc (size_exp, _) pname ret node location mem = match ret with | Some (id, _) -> - let typ, stride, length0 = get_malloc_info (List.hd_exn params |> fst) in + let typ, stride, length0 = get_malloc_info size_exp in let length = Sem.eval length0 mem in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in let v = @@ -62,13 +62,13 @@ module Make (CFG : ProcCfg.S) = struct mem - let model_realloc pname ret params node location mem = - model_malloc pname ret (List.tl_exn params) node location mem + let model_realloc size_arg pname ret node location mem = + model_malloc size_arg pname ret node location mem - let model_min _pname ret params _node _location mem = - match (ret, params) with - | Some (id, _), [(e1, _); (e2, _)] -> + let model_min (e1, _) (e2, _) _pname ret _node _location mem = + match ret with + | Some (id, _) -> let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in let i2 = Sem.eval e2 mem |> Dom.Val.get_itv in let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in @@ -77,19 +77,15 @@ module Make (CFG : ProcCfg.S) = struct mem - let model_set_size _pname _ret params _node _location mem = - match params with - | [(e1, _); (e2, _)] -> - let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in - let size = Sem.eval e2 mem |> Dom.Val.get_itv in - let arr = Dom.Mem.find_heap_set locs mem in - let arr = Dom.Val.set_array_size size arr in - Dom.Mem.strong_update_heap locs arr mem - | _ -> - mem + let model_set_size (e1, _) (e2, _) _pname _ret _node _location mem = + let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in + let size = Sem.eval e2 mem |> Dom.Val.get_itv in + let arr = Dom.Mem.find_heap_set locs mem in + let arr = Dom.Val.set_array_size size arr in + Dom.Mem.strong_update_heap locs arr mem - let model_by_value value _pname ret _params _node _location mem = + let model_by_value value _pname ret _node _location mem = match ret with | Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) value mem @@ -99,45 +95,39 @@ module Make (CFG : ProcCfg.S) = struct mem - let model_bottom _pname _ret _params _node _location _mem = Bottom + let model_bottom _pname _ret _node _location _mem = Bottom - let model_infer_print _pname _ret params _node location mem = - match params with - | (e, _) :: _ -> - L.(debug BufferOverrun Medium) - "@[=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ; - mem - | _ -> - mem + let model_infer_print (e, _) _pname _ret _node location mem = + L.(debug BufferOverrun Medium) + "@[=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ; + mem - let model_infer_set_array_length pname _ret params node _location mem = - match params with - | [(Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)}); (length_exp, _)] -> + let model_infer_set_array_length array (length_exp, _) pname _ret node _location mem = + match array with + | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)} -> let length = Sem.eval length_exp mem |> Dom.Val.get_itv in let stride = Option.map ~f:IntLit.to_int stride0 in let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v |> set_uninitialized node typ (Dom.Val.get_array_locs v) - | [_; _] -> - L.(die InternalError) "Unexpected type of arguments for __set_array_length()" | _ -> - L.(die InternalError) "Unexpected number of arguments for __set_array_length()" + L.(die InternalError) "Unexpected type of first argument for __set_array_length()" let dispatcher : model_fun ProcnameDispatcher.dispatcher = let open ProcnameDispatcher in make_dispatcher - [ -"__inferbo_min" <>$ any_arg $+ any_arg $!--> model_min - ; -"__inferbo_set_size" <>$ any_arg $+ any_arg $!--> model_set_size + [ -"__inferbo_min" <>$ capt_arg $+ capt_arg $!--> model_min + ; -"__inferbo_set_size" <>$ capt_arg $+ capt_arg $!--> model_set_size ; -"__exit" <>--> model_bottom ; -"exit" <>--> model_bottom ; -"fgetc" <>--> model_by_value Dom.Val.Itv.m1_255 - ; -"infer_print" <>--> model_infer_print - ; -"malloc" <>--> model_malloc - ; -"__new_array" <>--> model_malloc - ; -"realloc" <>--> model_realloc - ; -"__set_array_length" <>$ any_arg $+ any_arg $!--> model_infer_set_array_length + ; -"infer_print" <>$ capt_arg $!--> model_infer_print + ; -"malloc" <>$ capt_arg $+...$--> model_malloc + ; -"__new_array" <>$ capt_arg $+...$--> model_malloc + ; -"realloc" <>$ any_arg $+ capt_arg $+...$--> model_realloc + ; -"__set_array_length" <>$ capt_arg $+ capt_arg $!--> model_infer_set_array_length ; -"strlen" <>--> model_by_value Dom.Val.Itv.nat ] end