pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse] Move models to ProcnameDispatcher style

Browse Source 
Summary: Rather than repeatedly matching actuals, let's use `ProcnameDispatcher.ModeledCall` to pick up the actual arguments with their corresponding values. This simplifies the models.

Reviewed By: jvillard

Differential Revision: D18685855

fbshipit-source-id: 7788bd8bb
master
Ezgi Çiçek 5 years ago committed by Facebook Github Bot
parent 766fc2c072
commit eb8c8af117
5 changed files with 168 additions and 192 deletions
Show Stats Download Patch File Download Diff File

11
infer/src/IR/ProcnameDispatcher.ml
Unescape View File

@ -691,6 +691,11 @@ module Call = struct
{one_arg_matcher= match_any_arg; capture= capture_arg} {one_arg_matcher= match_any_arg; capture= capture_arg}
let all_args : ('context, 'value FuncArg.t list -> 'f_out, 'f_out, 'value) func_arg =
let eat_func_arg _context (f, args) = Some (f args, []) in
{eat_func_arg}
let capt_value : ('context, 'value, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, 'value) one_arg = let capt_value : ('context, 'value, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, 'value) one_arg =
{one_arg_matcher= match_any_arg; capture= capture_arg_val} {one_arg_matcher= match_any_arg; capture= capture_arg_val}
@ -785,6 +790,8 @@ module Call = struct
let ( $+ ) args_matcher one_arg = args_matcher $+! (one_arg $!! ()) let ( $+ ) args_matcher one_arg = args_matcher $+! (one_arg $!! ())
let ( $++ ) args_matcher () = args_matcher $+! all_args
let ( $+? ) args_matcher one_arg = args_matcher $+! (one_arg $?! ()) let ( $+? ) args_matcher one_arg = args_matcher $+! (one_arg $?! ())
let ( >$ ) templ_matcher one_arg = templ_matcher >$! () $+ one_arg let ( >$ ) templ_matcher one_arg = templ_matcher >$! () $+ one_arg
@ -799,6 +806,8 @@ module Call = struct
let ( $+...$--> ) args_matcher f = args_matcher $* any_func_args $*--> f let ( $+...$--> ) args_matcher f = args_matcher $* any_func_args $*--> f
let ( $++$--> ) args_matcher f = args_matcher $++ () $--> f
let ( >--> ) templ_matcher f = templ_matcher >$! () $+...$--> f let ( >--> ) templ_matcher f = templ_matcher >$! () $+...$--> f
let ( >$$--> ) templ_matcher f = templ_matcher >$! () $--> f let ( >$$--> ) templ_matcher f = templ_matcher >$! () $--> f
@ -809,6 +818,8 @@ module Call = struct
let ( &--> ) name_matcher f = name_matcher <...>! () $! () $+...$--> f let ( &--> ) name_matcher f = name_matcher <...>! () $! () $+...$--> f
let ( &++> ) name_matcher f = name_matcher <...>! () $! () $++$--> f
let ( <>--> ) name_matcher f = name_matcher <! () >--> f let ( <>--> ) name_matcher f = name_matcher <! () >--> f
let ( &::.*--> ) name_matcher f = name_matcher <...>! () &::.*! () $! () $+...$--> f let ( &::.*--> ) name_matcher f = name_matcher <...>! () &::.*! () $! () $+...$--> f

13
infer/src/IR/ProcnameDispatcher.mli
Unescape View File

@ -242,6 +242,12 @@ module Call : sig
('context, 'f_in, _, 'f_out, 'value) args_matcher -> 'f_in -> ('context, 'f_out, 'value) matcher ('context, 'f_in, _, 'f_out, 'value) args_matcher -> 'f_in -> ('context, 'f_out, 'value) matcher
(** Ends function arguments with eats-ALL and binds the function *) (** Ends function arguments with eats-ALL and binds the function *)
val ( $++$--> ) :
('context, 'f_in, _, 'value FuncArg.t list -> 'f_out, 'value) args_matcher
-> 'f_in
-> ('context, 'f_out, 'value) matcher
(** Ends and captures ALL function arguments as a list and binds the function *)
val ( >$$--> ) : val ( >$$--> ) :
('context, 'f_in, 'f_out, _, 'value) templ_matcher ('context, 'f_in, 'f_out, _, 'value) templ_matcher
-> 'f_in -> 'f_in
@ -264,6 +270,13 @@ module Call : sig
('context, 'f_in, 'f_out, 'value) name_matcher -> 'f_in -> ('context, 'f_out, 'value) matcher ('context, 'f_in, 'f_out, 'value) name_matcher -> 'f_in -> ('context, 'f_out, 'value) matcher
(** After a name, accepts NO template arguments, accepts ALL function arguments, binds the function *) (** After a name, accepts NO template arguments, accepts ALL function arguments, binds the function *)
val ( &++> ) :
('context, 'f_in, 'value FuncArg.t list -> 'f_out, 'value) name_matcher
-> 'f_in
-> ('context, 'f_out, 'value) matcher
(** After a name, accepts ALL template arguments, captures ALL function arguments as a list, binds
the function *)
val ( &::.*--> ) : val ( &::.*--> ) :
('context, 'f_in, 'f_out, 'value) name_matcher -> 'f_in -> ('context, 'f_out, 'value) matcher ('context, 'f_in, 'f_out, 'value) name_matcher -> 'f_in -> ('context, 'f_out, 'value) matcher
(** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates), (** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates),

21
infer/src/pulse/Pulse.ml
Unescape View File

@ -101,16 +101,18 @@ module PulseTransferFunctions = struct
let dispatch_call tenv summary ret call_exp actuals call_loc flags astate = let dispatch_call tenv summary ret call_exp actuals call_loc flags astate =
(* evaluate all actuals *) (* evaluate all actuals *)
List.fold_result actuals ~init:(astate, []) List.fold_result actuals ~init:(astate, [])
~f:(fun (astate, rev_actuals_evaled) (actual_exp, actual_typ) -> ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) ->
PulseOperations.eval call_loc actual_exp astate PulseOperations.eval call_loc actual_exp astate
>>| fun (astate, actual_evaled) -> >>| fun (astate, actual_evaled) ->
(astate, (actual_evaled, actual_typ) :: rev_actuals_evaled) ) ( astate
>>= fun (astate, rev_actuals_evaled) -> , ProcnameDispatcher.Call.FuncArg.{exp= actual_exp; value= actual_evaled; typ= actual_typ}
let actuals_evaled = List.rev rev_actuals_evaled in :: rev_func_args ) )
>>= fun (astate, rev_func_args) ->
let func_args = List.rev rev_func_args in
let model = let model =
match proc_name_of_call call_exp with match proc_name_of_call call_exp with
| Some callee_pname -> | Some callee_pname ->
PulseModels.dispatch tenv callee_pname PulseModels.dispatch tenv callee_pname func_args
| None -> | None ->
(* function pointer, etc.: skip for now *) (* function pointer, etc.: skip for now *)
None None
@ -120,10 +122,15 @@ module PulseTransferFunctions = struct
match model with match model with
| Some model -> | Some model ->
L.d_printfln "Found model for call@\n" ; L.d_printfln "Found model for call@\n" ;
model ~caller_summary:summary call_loc ~ret ~actuals:actuals_evaled astate model ~caller_summary:summary call_loc ~ret astate
| None -> | None ->
PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
let r = interprocedural_call summary ret call_exp actuals_evaled flags call_loc astate in let only_actuals_evaled =
List.map ~f:(fun ProcnameDispatcher.Call.FuncArg.{value; typ} -> (value, typ)) func_args
in
let r =
interprocedural_call summary ret call_exp only_actuals_evaled flags call_loc astate
in
PerfEvent.(log (fun logger -> log_end_event logger ())) ; PerfEvent.(log (fun logger -> log_end_event logger ())) ;
r r
in in

308
infer/src/pulse/PulseModels.ml
Unescape View File

@ -9,38 +9,35 @@ open Result.Monad_infix
open PulseBasicInterface open PulseBasicInterface
open PulseDomainInterface open PulseDomainInterface
type arg_payload = AbstractValue.t * ValueHistory.t
type exec_fun = type exec_fun =
caller_summary:Summary.t caller_summary:Summary.t
-> Location.t -> Location.t
-> ret:Ident.t * Typ.t -> ret:Ident.t * Typ.t
-> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
-> PulseAbductiveDomain.t -> PulseAbductiveDomain.t
-> PulseAbductiveDomain.t list PulseOperations.access_result -> PulseAbductiveDomain.t list PulseOperations.access_result
type model = exec_fun type model = exec_fun
module Misc = struct module Misc = struct
let shallow_copy model_desc : model = let shallow_copy model_desc dest_pointer_hist src_pointer_hist : model =
fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in
( match actuals with PulseOperations.eval_access location src_pointer_hist Dereference astate
| [(dest_pointer_hist, _); (src_pointer_hist, _)] -> >>= fun (astate, obj) ->
PulseOperations.eval_access location src_pointer_hist Dereference astate PulseOperations.shallow_copy location obj astate
>>= fun (astate, obj) -> >>= fun (astate, obj_copy) ->
PulseOperations.shallow_copy location obj astate PulseOperations.write_deref location ~ref:dest_pointer_hist
>>= fun (astate, obj_copy) -> ~obj:(fst obj_copy, event :: snd obj_copy)
PulseOperations.write_deref location ~ref:dest_pointer_hist astate
~obj:(fst obj_copy, event :: snd obj_copy)
astate
| _ ->
Ok astate )
>>| fun astate -> [PulseOperations.havoc_id ret_id [event] astate] >>| fun astate -> [PulseOperations.havoc_id ret_id [event] astate]
let early_exit : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ _ -> Ok [] let early_exit : model = fun ~caller_summary:_ _ ~ret:_ _ -> Ok []
let return_int : Int64.t -> model = let return_int : Int64.t -> model =
fun i64 ~caller_summary:_ location ~ret:(ret_id, _) ~actuals:_ astate -> fun i64 ~caller_summary:_ location ~ret:(ret_id, _) astate ->
let ret_addr = AbstractValue.mk_fresh () in let ret_addr = AbstractValue.mk_fresh () in
let astate = let astate =
Memory.add_attribute ret_addr Memory.add_attribute ret_addr
@ -50,43 +47,30 @@ module Misc = struct
Ok [PulseOperations.write_id ret_id (ret_addr, []) astate] Ok [PulseOperations.write_id ret_id (ret_addr, []) astate]
let skip : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ astate -> Ok [astate] let skip : model = fun ~caller_summary:_ _ ~ret:_ astate -> Ok [astate]
let id_first_arg : model = let id_first_arg arg_access_hist : model =
fun ~caller_summary:_ _ ~ret ~actuals astate -> fun ~caller_summary:_ _ ~ret astate ->
match actuals with Ok [PulseOperations.write_id (fst ret) arg_access_hist astate]
| (arg_access_hist, _) :: _ ->
Ok [PulseOperations.write_id (fst ret) arg_access_hist astate]
| _ ->
Ok [astate]
end end
module C = struct module C = struct
let free : model = let free deleted_access : model =
fun ~caller_summary:_ location ~ret:_ ~actuals astate -> fun ~caller_summary:_ location ~ret:_ astate ->
match actuals with PulseOperations.invalidate location Invalidation.CFree deleted_access astate >>| List.return
| [(deleted_access, _)] ->
PulseOperations.invalidate location Invalidation.CFree deleted_access astate >>| List.return
| _ ->
Ok [astate]
end end
module Cplusplus = struct module Cplusplus = struct
let delete : model = let delete deleted_access : model =
fun ~caller_summary:_ location ~ret:_ ~actuals astate -> fun ~caller_summary:_ location ~ret:_ astate ->
match actuals with PulseOperations.invalidate location Invalidation.CppDelete deleted_access astate >>| List.return
| [(deleted_access, _)] ->
PulseOperations.invalidate location Invalidation.CppDelete deleted_access astate
>>| List.return
| _ ->
Ok [astate]
let placement_new : model = let placement_new actuals : model =
fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
let event = ValueHistory.Call {f= Model "<placement new>()"; location; in_call= []} in let event = ValueHistory.Call {f= Model "<placement new>()"; location; in_call= []} in
match List.rev actuals with match List.rev actuals with
| ((address, hist), _) :: _ -> | ProcnameDispatcher.Call.FuncArg.{value= address, hist} :: _ ->
Ok [PulseOperations.write_id ret_id (address, event :: hist) astate] Ok [PulseOperations.write_id ret_id (address, event :: hist) astate]
| _ -> | _ ->
Ok [PulseOperations.havoc_id ret_id [event] astate] Ok [PulseOperations.havoc_id ret_id [event] astate]
@ -105,57 +89,47 @@ module StdBasicString = struct
PulseOperations.eval_access location bstring internal_string_access astate PulseOperations.eval_access location bstring internal_string_access astate
let data : model = let data this_hist : model =
fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in
match actuals with to_internal_string location this_hist astate
| [(this_hist, _)] -> >>= fun (astate, string_addr_hist) ->
to_internal_string location this_hist astate PulseOperations.eval_access location string_addr_hist Dereference astate
>>= fun (astate, string_addr_hist) -> >>| fun (astate, (string, hist)) ->
PulseOperations.eval_access location string_addr_hist Dereference astate [PulseOperations.write_id ret_id (string, event :: hist) astate]
>>| fun (astate, (string, hist)) ->
[PulseOperations.write_id ret_id (string, event :: hist) astate]
| _ ->
Ok [PulseOperations.havoc_id ret_id [event] astate]
let destructor : model = let destructor this_hist : model =
fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> fun ~caller_summary:_ location ~ret:_ astate ->
let model = CallEvent.Model "std::basic_string::~basic_string()" in let model = CallEvent.Model "std::basic_string::~basic_string()" in
let call_event = ValueHistory.Call {f= model; location; in_call= []} in let call_event = ValueHistory.Call {f= model; location; in_call= []} in
match actuals with to_internal_string location this_hist astate
| [(this_hist, _)] -> >>= fun (astate, (string_addr, string_hist)) ->
to_internal_string location this_hist astate let string_addr_hist = (string_addr, call_event :: string_hist) in
>>= fun (astate, (string_addr, string_hist)) -> PulseOperations.invalidate_deref location CppDelete string_addr_hist astate
let string_addr_hist = (string_addr, call_event :: string_hist) in >>= fun astate ->
PulseOperations.invalidate_deref location CppDelete string_addr_hist astate PulseOperations.invalidate location CppDelete string_addr_hist astate >>| fun astate -> [astate]
>>= fun astate ->
PulseOperations.invalidate location CppDelete string_addr_hist astate
>>| fun astate -> [astate]
| _ ->
Ok [PulseOperations.havoc_id ret_id [call_event] astate]
end end
module StdFunction = struct module StdFunction = struct
let operator_call : model = let operator_call lambda_ptr_hist actuals : model =
fun ~caller_summary location ~ret ~actuals astate -> fun ~caller_summary location ~ret astate ->
let havoc_ret (ret_id, _) astate = let havoc_ret (ret_id, _) astate =
let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in
[PulseOperations.havoc_id ret_id [event] astate] [PulseOperations.havoc_id ret_id [event] astate]
in in
match actuals with PulseOperations.eval_access location lambda_ptr_hist Dereference astate
| [] -> >>= fun (astate, (lambda, _)) ->
Ok (havoc_ret ret astate) PulseOperations.Closures.check_captured_addresses location lambda astate
| (lambda_ptr_hist, _) :: actuals -> ( >>= fun astate ->
PulseOperations.eval_access location lambda_ptr_hist Dereference astate match PulseAbductiveDomain.Memory.get_closure_proc_name lambda astate with
>>= fun (astate, (lambda, _)) -> | None ->
PulseOperations.Closures.check_captured_addresses location lambda astate (* we don't know what proc name this lambda resolves to *) Ok (havoc_ret ret astate)
>>= fun astate -> | Some callee_proc_name ->
match PulseAbductiveDomain.Memory.get_closure_proc_name lambda astate with let actuals =
| None -> List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{value; typ} -> (value, typ))
(* we don't know what proc name this lambda resolves to *) Ok (havoc_ret ret astate) in
| Some callee_proc_name -> PulseOperations.call ~caller_summary location callee_proc_name ~ret ~actuals astate
PulseOperations.call ~caller_summary location callee_proc_name ~ret ~actuals astate )
end end
module StdVector = struct module StdVector = struct
@ -187,118 +161,86 @@ module StdVector = struct
>>= PulseOperations.havoc_field location vector internal_array trace >>= PulseOperations.havoc_field location vector internal_array trace
let invalidate_references vector_f : model = let invalidate_references vector_f vector : model =
fun ~caller_summary:_ location ~ret:_ ~actuals astate -> fun ~caller_summary:_ location ~ret:_ astate ->
match actuals with let crumb =
| (vector, _) :: _ -> ValueHistory.Call
let crumb = { f= Model (Format.asprintf "%a()" Invalidation.pp_std_vector_function vector_f)
ValueHistory.Call ; location
{ f= Model (Format.asprintf "%a()" Invalidation.pp_std_vector_function vector_f) ; in_call= [] }
; location in
; in_call= [] } reallocate_internal_array [crumb] vector vector_f location astate >>| List.return
in
reallocate_internal_array [crumb] vector vector_f location astate >>| List.return
| _ ->
Ok [astate]
let at ~desc : model = let at ~desc vector index : model =
fun ~caller_summary:_ location ~ret ~actuals astate -> fun ~caller_summary:_ location ~ret astate ->
let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
match actuals with element_of_internal_array location vector (fst index) astate
| [(vector, _); (index, _)] -> >>| fun (astate, (addr, hist)) ->
element_of_internal_array location vector (fst index) astate [PulseOperations.write_id (fst ret) (addr, event :: hist) astate]
>>| fun (astate, (addr, hist)) ->
[PulseOperations.write_id (fst ret) (addr, event :: hist) astate]
| _ -> let reserve vector : model =
Ok [PulseOperations.havoc_id (fst ret) [event] astate] fun ~caller_summary:_ location ~ret:_ astate ->
let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in
reallocate_internal_array [crumb] vector Reserve location astate
let reserve : model = >>| PulseAbductiveDomain.Memory.std_vector_reserve (fst vector)
fun ~caller_summary:_ location ~ret:_ ~actuals astate -> >>| List.return
match actuals with
| [(vector, _); _value] ->
let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in let push_back vector : model =
reallocate_internal_array [crumb] vector Reserve location astate fun ~caller_summary:_ location ~ret:_ astate ->
>>| PulseAbductiveDomain.Memory.std_vector_reserve (fst vector) let crumb = ValueHistory.Call {f= Model "std::vector::push_back()"; location; in_call= []} in
>>| List.return if PulseAbductiveDomain.Memory.is_std_vector_reserved (fst vector) astate then
| _ -> (* assume that any call to [push_back] is ok after one called [reserve] on the same vector
Ok [astate] (a perfect analysis would also make sure we don't exceed the reserved size) *)
Ok [astate]
else
let push_back : model = (* simulate a re-allocation of the underlying array every time an element is added *)
fun ~caller_summary:_ location ~ret:_ ~actuals astate -> reallocate_internal_array [crumb] vector PushBack location astate >>| List.return
match actuals with
| [(vector, _); _value] ->
let crumb =
ValueHistory.Call {f= Model "std::vector::push_back()"; location; in_call= []}
in
if PulseAbductiveDomain.Memory.is_std_vector_reserved (fst vector) astate then
(* assume that any call to [push_back] is ok after one called [reserve] on the same vector
(a perfect analysis would also make sure we don't exceed the reserved size) *)
Ok [astate]
else
(* simulate a re-allocation of the underlying array every time an element is added *)
reallocate_internal_array [crumb] vector PushBack location astate >>| List.return
| _ ->
Ok [astate]
end end
module ProcNameDispatcher = struct module ProcNameDispatcher = struct
let dispatch : (Tenv.t, model, unit) ProcnameDispatcher.ProcName.dispatcher = let dispatch : (Tenv.t, model, arg_payload) ProcnameDispatcher.Call.dispatcher =
let open ProcnameDispatcher.ProcName in let open ProcnameDispatcher.Call in
let match_builtin builtin _ s = String.equal s (Typ.Procname.get_method builtin) in
make_dispatcher make_dispatcher
[ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip [ +match_builtin BuiltinDecl.free <>$ capt_value $--> C.free
; +match_builtin BuiltinDecl.__delete <>$ capt_value $--> Cplusplus.delete
; +match_builtin BuiltinDecl.__placement_new &++> Cplusplus.placement_new
; +match_builtin BuiltinDecl.objc_cpp_throw <>--> Misc.early_exit
; +match_builtin BuiltinDecl.__cast <>$ capt_value $+...$--> Misc.id_first_arg
; +match_builtin BuiltinDecl.abort <>--> Misc.early_exit
; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit
; -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip
; -"folly" &:: "Optional" &:: "reset" &--> Misc.skip ; -"folly" &:: "Optional" &:: "reset" &--> Misc.skip
; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip
; -"std" &:: "basic_string" &:: "data" &--> StdBasicString.data ; -"std" &:: "basic_string" &:: "data" <>$ capt_value $--> StdBasicString.data
; -"std" &:: "basic_string" &:: "~basic_string" &--> StdBasicString.destructor ; -"std" &:: "basic_string" &:: "~basic_string" <>$ capt_value $--> StdBasicString.destructor
; -"std" &:: "function" &:: "operator()" &--> StdFunction.operator_call ; -"std" &:: "function" &:: "operator()" $ capt_value $++$--> StdFunction.operator_call
; -"std" &:: "function" &:: "operator=" &--> Misc.shallow_copy "std::function::operator=" ; -"std" &:: "function" &:: "operator=" $ capt_value $+ capt_value
$--> Misc.shallow_copy "std::function::operator="
; -"std" &:: "integral_constant" < any_typ &+ capt_int ; -"std" &:: "integral_constant" < any_typ &+ capt_int
>::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name) >::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name)
&--> Misc.return_int <>--> Misc.return_int
; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign ; -"std" &:: "vector" &:: "assign" <>$ capt_value
; -"std" &:: "vector" &:: "clear" &--> StdVector.invalidate_references Clear $+...$--> StdVector.invalidate_references Assign
; -"std" &:: "vector" &:: "emplace" &--> StdVector.invalidate_references Emplace ; -"std" &:: "vector" &:: "clear" <>$ capt_value $--> StdVector.invalidate_references Clear
; -"std" &:: "vector" &:: "emplace_back" &--> StdVector.invalidate_references EmplaceBack ; -"std" &:: "vector" &:: "emplace" $ capt_value
; -"std" &:: "vector" &:: "insert" &--> StdVector.invalidate_references Insert $+...$--> StdVector.invalidate_references Emplace
; -"std" &:: "vector" &:: "operator[]" &--> StdVector.at ~desc:"std::vector::at()" ; -"std" &:: "vector" &:: "emplace_back" $ capt_value
; -"std" &:: "vector" &:: "push_back" &--> StdVector.push_back $+...$--> StdVector.invalidate_references EmplaceBack
; -"std" &:: "vector" &:: "reserve" &--> StdVector.reserve ; -"std" &:: "vector" &:: "insert" <>$ capt_value
; -"std" &:: "vector" &:: "shrink_to_fit" &--> StdVector.invalidate_references ShrinkToFit $+...$--> StdVector.invalidate_references Insert
; +PatternMatch.implements_collection &:: "get" <>--> StdVector.at ~desc:"Collection.get()" ; -"std" &:: "vector" &:: "operator[]" <>$ capt_value $+ capt_value
; -"__cast" <>--> Misc.id_first_arg ] $--> StdVector.at ~desc:"std::vector::at()"
; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_value
$--> StdVector.invalidate_references ShrinkToFit
; -"std" &:: "vector" &:: "push_back" <>$ capt_value $+...$--> StdVector.push_back
; -"std" &:: "vector" &:: "reserve" <>$ capt_value $+...$--> StdVector.reserve
; +PatternMatch.implements_collection
&:: "get" <>$ capt_value $+ capt_value
$--> StdVector.at ~desc:"Collection.get()" ]
end end
let builtins_dispatcher = let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args
let builtins =
[ (BuiltinDecl.__delete, Cplusplus.delete)
; (BuiltinDecl.__placement_new, Cplusplus.placement_new)
; (BuiltinDecl.abort, Misc.early_exit)
; (BuiltinDecl.exit, Misc.early_exit)
; (BuiltinDecl.free, C.free)
; (BuiltinDecl.objc_cpp_throw, Misc.early_exit) ]
in
let builtins_map =
Hashtbl.create
( module struct
include Typ.Procname
let hash = Caml.Hashtbl.hash
let sexp_of_t _ = assert false
end )
in
List.iter builtins ~f:(fun (builtin, model) ->
let open PolyVariantEqual in
assert (Hashtbl.add builtins_map ~key:builtin ~data:model = `Ok) ) ;
fun proc_name -> Hashtbl.find builtins_map proc_name
let dispatch tenv proc_name =
match builtins_dispatcher proc_name with
| Some _ as result ->
result
| None ->
ProcNameDispatcher.dispatch tenv proc_name

7
infer/src/pulse/PulseModels.mli
Unescape View File

@ -11,10 +11,13 @@ type exec_fun =
caller_summary:Summary.t caller_summary:Summary.t
-> Location.t -> Location.t
-> ret:Ident.t * Typ.t -> ret:Ident.t * Typ.t
-> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
-> PulseAbductiveDomain.t -> PulseAbductiveDomain.t
-> PulseAbductiveDomain.t list PulseOperations.access_result -> PulseAbductiveDomain.t list PulseOperations.access_result
type model = exec_fun type model = exec_fun
val dispatch : Tenv.t -> Typ.Procname.t -> model option val dispatch :
Tenv.t
-> Typ.Procname.t
-> (AbstractValue.t * ValueHistory.t) ProcnameDispatcher.Call.FuncArg.t list
-> model option

Write Preview
Loading…
Cancel
Save