From 3792b9b17a6eaabdd4278d1d6d609d805387183c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 26 Nov 2019 05:33:26 -0800 Subject: [PATCH] [infer] Record the value of function arguments in ProcnameDispatcher calls Summary: Preperation diff to use `ProcnameDispatcher` for Pulse: it changes function arguments, i.e. `ProcnameDispatcher.Call.FuncArg`, to a record in order to track the value of arguments. To do that, it changes `ProcnameDispatcher.Call` into a functor so that we can parametrize over the type of the value without making changes upwards. Reviewed By: jvillard Differential Revision: D18590224 fbshipit-source-id: 6a13fbc1a --- infer/src/IR/ProcnameDispatcher.ml | 31 ++++++++--- infer/src/IR/ProcnameDispatcher.mli | 11 +++- .../bufferoverrun/bufferOverrunAnalysis.ml | 5 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 5 +- .../src/bufferoverrun/bufferOverrunModels.ml | 53 +++++++++++-------- infer/src/checkers/cost.ml | 6 ++- infer/src/checkers/costModels.ml | 4 +- infer/src/checkers/hoisting.ml | 6 ++- infer/src/opensource/FbCostModels.ml | 2 +- infer/src/opensource/FbCostModels.mli | 2 +- 10 files changed, 85 insertions(+), 40 deletions(-) diff --git a/infer/src/IR/ProcnameDispatcher.ml b/infer/src/IR/ProcnameDispatcher.ml index 1be9a8a5d..102fcd964 100644 --- a/infer/src/IR/ProcnameDispatcher.ml +++ b/infer/src/IR/ProcnameDispatcher.ml @@ -529,23 +529,29 @@ module Common = struct let ( <>:: ) name_matcher name = name_matcher :: name end -module Call = struct +module type VALUE = sig + type t +end + +module MakeCall (Val : VALUE) = struct include Common (** Little abstraction over arguments: currently actual args, we'll want formal args later *) module FuncArg = struct - type t = Exp.t * Typ.t + type t = {exp: Exp.t; typ: Typ.t; value: Val.t} + + let typ {typ} = typ - let typ (_, ty) = ty + let exp {exp} = exp - let exp (e, _) = e + let value {value} = value - let get_var_exn arg = - match exp arg with + let get_var_exn {exp; typ} = + match exp with | Exp.Var v -> v | e -> - Logging.(die InternalError) "Expected Lvar, got %a:%a" Exp.pp e (Typ.pp Pp.text) (typ arg) + Logging.(die InternalError) "Expected Lvar, got %a:%a" Exp.pp e (Typ.pp Pp.text) typ end type ('context, 'f_in, 'f_out, 'captured_types) proc_matcher = @@ -814,6 +820,13 @@ module Call = struct {get_captured_value; do_capture} + (** Capture the argument value *) + let capture_arg_val : (Val.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f) arg_capture = + let get_captured_value arg = FuncArg.value arg in + let do_capture f v = f v in + {get_captured_value; do_capture} + + (** Capture the argument expression *) let capture_arg_exp : (Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f) arg_capture = let get_captured_value arg = FuncArg.exp arg in @@ -869,6 +882,10 @@ module Call = struct {one_arg_matcher= match_any_arg; capture= capture_arg} + let capt_value : ('context, Val.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg = + {one_arg_matcher= match_any_arg; capture= capture_arg_val} + + let capt_exp : ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg = {one_arg_matcher= match_any_arg; capture= capture_arg_exp} diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli index 33a8fd493..70277bed5 100644 --- a/infer/src/IR/ProcnameDispatcher.mli +++ b/infer/src/IR/ProcnameDispatcher.mli @@ -224,10 +224,14 @@ module ProcName : module TypName : NameCommon with type ('context, 'f) dispatcher = 'context -> Typ.name -> 'f option -module Call : sig +module type VALUE = sig + type t +end + +module MakeCall (Val : VALUE) : sig (** Little abstraction over arguments: currently actual args, we'll want formal args later *) module FuncArg : sig - type t = Exp.t * Typ.t + type t = {exp: Exp.t; typ: Typ.t; value: Val.t} end include @@ -251,6 +255,9 @@ module Call : sig val capt_arg : ('context, FuncArg.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg (** Captures one arg *) + val capt_value : ('context, Val.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg + (** Captures the value of one arg at current state *) + val capt_exp : ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg (** Captures one arg expression *) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 89c57d3a7..1141cfd8f 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -362,7 +362,10 @@ module TransferFunctions = struct if is_java_enum_values ~caller_pname:(Summary.get_proc_name summary) ~callee_pname then assign_java_enum_values id callee_pname mem else - match Models.Call.dispatch tenv callee_pname params with + let fun_arg_list = + List.map params ~f:(fun (exp, typ) -> Models.ModeledCall.FuncArg.{exp; typ; value= ()}) + in + match Models.Call.dispatch tenv callee_pname fun_arg_list with | Some {Models.exec} -> let model_env = let node_hash = CFG.Node.hash node in diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index dde20617a..f3938172f 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -294,7 +294,10 @@ let check_instr : List.fold params ~init:cond_set ~f:(fun cond_set (exp, _) -> check_expr_for_integer_overflow integer_type_widths exp location mem cond_set ) in - match Models.Call.dispatch tenv callee_pname params with + let fun_arg_list = + List.map params ~f:(fun (exp, typ) -> Models.ModeledCall.FuncArg.{exp; typ; value= ()}) + in + match Models.Call.dispatch tenv callee_pname fun_arg_list with | Some {Models.check} -> let model_env = let node_hash = CFG.Node.hash node in diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index ad8af075e..b9d04f81e 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -17,6 +17,13 @@ module Relation = BufferOverrunDomainRelation module Trace = BufferOverrunTrace open BoUtils.ModelEnv +module Val = struct + type t = unit +end + +module ModeledCall = ProcnameDispatcher.MakeCall (Val) +open ModeledCall.FuncArg + type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.t -> Dom.Mem.t type check_fun = model_env -> Dom.Mem.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t @@ -282,9 +289,9 @@ let realloc src_exp size_exp = {exec; check} -let placement_new size_exp (src_exp1, t1) src_arg2_opt = +let placement_new size_exp {exp= src_exp1; typ= t1} src_arg2_opt = match (t1.Typ.desc, src_arg2_opt) with - | Tint _, None | Tint _, Some (_, {Typ.desc= Tint _}) -> + | Tint _, None | Tint _, Some {typ= {Typ.desc= Tint _}} -> malloc ~can_be_zero:true (Exp.BinOp (Binop.PlusA (Some Typ.size_t), size_exp, src_exp1)) | Tstruct (CppClass (name, _)), None when [%compare.equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] -> @@ -295,7 +302,7 @@ let placement_new size_exp (src_exp1, t1) src_arg2_opt = if Typ.is_pointer_to_void t1 then src_exp1 else match src_arg2_opt with - | Some (src_exp2, t2) when Typ.is_pointer_to_void t2 -> + | Some {exp= src_exp2; typ= t2} when Typ.is_pointer_to_void t2 -> src_exp2 | _ -> (* TODO: Raise an exception when given unexpected arguments. Before that, we need @@ -403,9 +410,9 @@ let get_array_length array_exp = (* Clang only *) -let set_array_length array length_exp = +let set_array_length {exp; typ} length_exp = let exec {pname; node_hash; location; integer_type_widths} ~ret:_ mem = - match array with + match (exp, typ) with | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {stride}} -> let length = Sem.eval integer_type_widths length_exp mem in let stride = Option.map ~f:IntLit.to_int_exn stride in @@ -460,7 +467,7 @@ module CFArray = struct {exec; check} - let at (array_exp, _) (index_exp, _) = at ?size:None array_exp index_exp + let at {exp= array_exp} {exp= index_exp} = at ?size:None array_exp index_exp let length e = let exec {integer_type_widths} ~ret:(ret_id, _) mem = @@ -472,7 +479,7 @@ module CFArray = struct end module Split = struct - let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem = + let std_vector ~adds_at_least_one {exp= vector_exp; typ= vector_typ} location mem = let increment = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in let size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in @@ -515,9 +522,9 @@ module StdArray = struct {exec; check= no_check} - let at size (array_exp, _) (index_exp, _) = at ~size array_exp index_exp + let at size {exp= array_exp} {exp= index_exp} = at ~size array_exp index_exp - let begin_ _size (array_exp, _) = + let begin_ _size {exp= array_exp} = let exec {location; integer_type_widths} ~ret:(id, _) mem = let v = Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location Itv.zero @@ -527,7 +534,7 @@ module StdArray = struct {exec; check= no_check} - let end_ size (array_exp, _) = + let end_ size {exp= array_exp} = let exec {location; integer_type_widths} ~ret:(id, _) mem = let v = let offset = Itv.of_int_lit (IntLit.of_int64 size) in @@ -538,7 +545,7 @@ module StdArray = struct {exec; check= no_check} - let back size (array_exp, _) = + let back size {exp= array_exp} = let exec {location; integer_type_widths} ~ret:(id, _) mem = let v = let offset = Itv.of_int_lit (IntLit.of_int64 Int64.(size - one)) in @@ -607,13 +614,13 @@ module StdVector = struct PowLoc.append_field locs ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ) - let deref_of model_env elt_typ (vec_exp, vec_typ) mem = + let deref_of model_env elt_typ {exp= vec_exp; typ= vec_typ} mem = let fn = BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ in ArrObjCommon.deref_of model_env vec_exp ~fn mem (* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *) - let constructor_size elt_typ (vec_exp, vec_typ) size_exp = + let constructor_size elt_typ {exp= vec_exp; typ= vec_typ} size_exp = let {exec= malloc_exec; check} = malloc ~can_be_zero:true size_exp in let exec ({pname; node_hash; integer_type_widths; location} as model_env) ~ret:((id, _) as ret) mem = @@ -639,7 +646,7 @@ module StdVector = struct let constructor_empty elt_typ vec = constructor_size elt_typ vec Exp.zero (* The (5) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *) - let constructor_copy elt_typ (vec_exp, vec_typ) src_exp = + let constructor_copy elt_typ {exp= vec_exp; typ= vec_typ} src_exp = let exec ({integer_type_widths} as model_env) ~ret:_ mem = let vec_locs, traces = let v = Sem.eval integer_type_widths vec_exp mem in @@ -654,7 +661,7 @@ module StdVector = struct {exec; check= no_check} - let at elt_typ (vec_exp, vec_typ) index_exp = + let at elt_typ {exp= vec_exp; typ= vec_typ} index_exp = ArrObjCommon.at vec_exp ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ) index_exp @@ -703,7 +710,7 @@ module StdVector = struct {exec; check= no_check} - let size elt_typ (vec_exp, vec_typ) = + let size elt_typ {exp= vec_exp; typ= vec_typ} = let exec = ArrObjCommon.size_exec vec_exp ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ) in @@ -711,7 +718,7 @@ module StdVector = struct end module StdBasicString = struct - let constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src ~len_opt = + let constructor_from_char_ptr char_typ {exp= tgt_exp; typ= tgt_typ} src ~len_opt = let exec ({pname; node_hash} as model_env) ~ret mem = let mem = Option.value_map len_opt ~default:mem ~f:(fun len -> @@ -743,13 +750,13 @@ module StdBasicString = struct (* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) - let constructor_from_char_ptr_with_len char_typ (tgt_exp, tgt_typ) src len = - constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src ~len_opt:(Some len) + let constructor_from_char_ptr_with_len char_typ tgt_arg src len = + constructor_from_char_ptr char_typ tgt_arg src ~len_opt:(Some len) (* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) - let constructor_from_char_ptr_without_len char_typ (tgt_exp, tgt_typ) src = - constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src ~len_opt:None + let constructor_from_char_ptr_without_len char_typ tgt_arg src = + constructor_from_char_ptr char_typ tgt_arg src ~len_opt:None (* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) @@ -1169,8 +1176,8 @@ module Object = struct end module Call = struct - let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher = - let open ProcnameDispatcher.Call in + let dispatch : (Tenv.t, model) ModeledCall.dispatcher = + let open ModeledCall in let mk_std_array () = -"std" &:: "array" < any_typ &+ capt_int in let std_array0 = mk_std_array () in let std_array1 = mk_std_array () in diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 4be1760c9..9accab4ec 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -563,7 +563,11 @@ module InstrBasicCost = struct CostDomain.unit_cost_atomic_operation | Some inferbo_mem -> ( let loc = InstrCFG.Node.loc instr_node in - match CostModels.Call.dispatch tenv callee_pname params with + let fun_arg_list = + List.map params ~f:(fun (exp, typ) -> + BufferOverrunModels.ModeledCall.FuncArg.{exp; typ; value= ()} ) + in + match CostModels.Call.dispatch tenv callee_pname fun_arg_list with | Some model -> let node_hash = InstrCFG.Node.hash instr_node in let model_env = diff --git a/infer/src/checkers/costModels.ml b/infer/src/checkers/costModels.ml index 2b8f21b48..c1b2760f8 100644 --- a/infer/src/checkers/costModels.ml +++ b/infer/src/checkers/costModels.ml @@ -118,8 +118,8 @@ module ImmutableSet = struct end module Call = struct - let dispatch : (Tenv.t, CostUtils.model) ProcnameDispatcher.Call.dispatcher = - let open ProcnameDispatcher.Call in + let dispatch : (Tenv.t, CostUtils.model) BufferOverrunModels.ModeledCall.dispatcher = + let open BufferOverrunModels.ModeledCall in let int_typ = Typ.mk (Typ.Tint Typ.IInt) in let dispatcher = make_dispatcher diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index e7a9049b1..d680c2f2d 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -116,7 +116,11 @@ let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_f ~callee_pname:pname ~callee_formals ~params ~callee_cost ~loc) else None | None -> - CostModels.Call.dispatch tenv pname params + let fun_arg_list = + List.map params ~f:(fun (exp, typ) -> + BufferOverrunModels.ModeledCall.FuncArg.{exp; typ; value= ()} ) + in + CostModels.Call.dispatch tenv pname fun_arg_list |> Option.map ~f:(fun model -> let model_env = let node_hash = InstrCFG.Node.hash last_node in diff --git a/infer/src/opensource/FbCostModels.ml b/infer/src/opensource/FbCostModels.ml index eb60fb8f0..2f572a0bc 100644 --- a/infer/src/opensource/FbCostModels.ml +++ b/infer/src/opensource/FbCostModels.ml @@ -8,5 +8,5 @@ open! IStd module Call = struct - let dispatch = ProcnameDispatcher.Call.make_dispatcher [] + let dispatch = BufferOverrunModels.ModeledCall.make_dispatcher [] end diff --git a/infer/src/opensource/FbCostModels.mli b/infer/src/opensource/FbCostModels.mli index 3a3b3f615..101451918 100644 --- a/infer/src/opensource/FbCostModels.mli +++ b/infer/src/opensource/FbCostModels.mli @@ -8,5 +8,5 @@ open! IStd module Call : sig - val dispatch : (Tenv.t, CostUtils.model) ProcnameDispatcher.Call.dispatcher + val dispatch : (Tenv.t, CostUtils.model) BufferOverrunModels.ModeledCall.dispatcher end