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

[pulse] enforce short forms for PulseDomainInterface

Browse Source 
Summary: See previous diff.

Reviewed By: ezgicicek

Differential Revision: D21022923

fbshipit-source-id: b1cab2fdc
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent 94e3b06900
commit bb9726bbd7
11 changed files with 85 additions and 63 deletions
Show Stats Download Patch File Download Diff File

8
infer/src/checkers/impurity.ml
Unescape View File

@ -138,7 +138,7 @@ let is_modeled_pure tenv pname =
(** Given Pulse summary, extract impurity info, i.e. parameters and global variables that are (** Given Pulse summary, extract impurity info, i.e. parameters and global variables that are
modified by the function and skipped functions. *) modified by the function and skipped functions. *)
let extract_impurity tenv pdesc (exec_state : PulseExecutionState.t) : ImpurityDomain.t = let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomain.t =
let astate, exited = let astate, exited =
match exec_state with match exec_state with
| ExitProgram astate -> | ExitProgram astate ->
@ -146,8 +146,8 @@ let extract_impurity tenv pdesc (exec_state : PulseExecutionState.t) : ImpurityD
| AbortProgram astate | ContinueProgram astate -> | AbortProgram astate | ContinueProgram astate ->
(astate, false) (astate, false)
in in
let pre_heap = (PulseAbductiveDomain.get_pre astate).BaseDomain.heap in let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in
let post = PulseAbductiveDomain.get_post astate in let post = AbductiveDomain.get_post astate in
let post_stack = post.BaseDomain.stack in let post_stack = post.BaseDomain.stack in
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
let modified_params = let modified_params =
@ -155,7 +155,7 @@ let extract_impurity tenv pdesc (exec_state : PulseExecutionState.t) : ImpurityD
in in
let modified_globals = get_modified_globals pre_heap post post_stack in let modified_globals = get_modified_globals pre_heap post post_stack in
let skipped_calls = let skipped_calls =
PulseAbductiveDomain.get_skipped_calls astate AbductiveDomain.get_skipped_calls astate
|> SkippedCalls.filter (fun proc_name _ -> |> SkippedCalls.filter (fun proc_name _ ->
Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) ) Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) )
in in

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

@ -10,6 +10,7 @@ module F = Format
module L = Logging module L = Logging
open IResult.Let_syntax open IResult.Let_syntax
open PulseBasicInterface open PulseBasicInterface
open PulseDomainInterface
let report summary diagnostic = let report summary diagnostic =
let open Diagnostic in let open Diagnostic in
@ -22,13 +23,11 @@ let check_error_transform summary ~f = function
f astate f astate
| Error (diagnostic, astate) -> | Error (diagnostic, astate) ->
report summary diagnostic ; report summary diagnostic ;
[PulseExecutionState.AbortProgram astate] [ExecutionDomain.AbortProgram astate]
let check_error_continue summary result = let check_error_continue summary result =
check_error_transform summary check_error_transform summary ~f:(fun astate -> [ExecutionDomain.ContinueProgram astate]) result
~f:(fun astate -> [PulseExecutionState.ContinueProgram astate])
result
let proc_name_of_call call_exp = let proc_name_of_call call_exp =
@ -43,7 +42,7 @@ type get_formals = Procname.t -> (Pvar.t * Typ.t) list option
module PulseTransferFunctions = struct module PulseTransferFunctions = struct
module CFG = ProcCfg.Normal module CFG = ProcCfg.Normal
module Domain = PulseExecutionState module Domain = ExecutionDomain
type extras = get_formals type extras = get_formals
@ -76,13 +75,13 @@ module PulseTransferFunctions = struct
(** [out_of_scope_access_expr] has just gone out of scope and in now invalid *) (** [out_of_scope_access_expr] has just gone out of scope and in now invalid *)
let exec_object_out_of_scope call_loc (pvar, typ) exec_state = let exec_object_out_of_scope call_loc (pvar, typ) exec_state =
match exec_state with match exec_state with
| PulseExecutionState.ContinueProgram astate -> | ExecutionDomain.ContinueProgram astate ->
let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in
let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in
(* invalidate [&x] *) (* invalidate [&x] *)
PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate
>>| PulseExecutionState.continue >>| ExecutionDomain.continue
| PulseExecutionState.AbortProgram _ | PulseExecutionState.ExitProgram _ -> | ExecutionDomain.AbortProgram _ | ExecutionDomain.ExitProgram _ ->
Ok exec_state Ok exec_state
@ -217,7 +216,7 @@ let checker {Callbacks.exe_env; summary} =
AbstractValue.init () ; AbstractValue.init () ;
let pdesc = Summary.get_proc_desc summary in let pdesc = Summary.get_proc_desc summary in
let initial = let initial =
DisjunctiveTransferFunctions.Disjuncts.singleton (PulseExecutionState.mk_initial pdesc) DisjunctiveTransferFunctions.Disjuncts.singleton (ExecutionDomain.mk_initial pdesc)
in in
let get_formals callee_pname = let get_formals callee_pname =
Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals

18
infer/src/pulse/PulseDomainInterface.ml
Unescape View File

@ -4,7 +4,9 @@
* This source code is licensed under the MIT license found in the * This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree. * LICENSE file in the root directory of this source tree.
*) *)
open! IStd open! IStd
module ExecutionDomain = PulseExecutionDomain
module AbductiveDomain = PulseAbductiveDomain module AbductiveDomain = PulseAbductiveDomain
(** if you do any mutations of the state in pulse you probably want this module *) (** if you do any mutations of the state in pulse you probably want this module *)
@ -19,3 +21,19 @@ module BaseDomain = PulseBaseDomain
module BaseStack = PulseBaseStack module BaseStack = PulseBaseStack
module BaseMemory = PulseBaseMemory module BaseMemory = PulseBaseMemory
module BaseAddressAttributes = PulseBaseAddressAttributes module BaseAddressAttributes = PulseBaseAddressAttributes
(** {2 Enforce short form usage} *)
include struct
[@@@warning "-60"]
module PulseAbductiveDomain = PulseAbductiveDomain
[@@deprecated "use the short form AbductiveDomain instead"]
module PulseBaseDomain = PulseBaseDomain [@@deprecated "use the short form BaseDomain instead"]
module PulseBaseStack = PulseBaseStack [@@deprecated "use the short form BaseStack instead"]
module PulseBaseMemory = PulseBaseMemory [@@deprecated "use the short form BaseMemory instead"]
module PulseBaseAddressAttributes = PulseBaseAddressAttributes
[@@deprecated "use the short form BaseAddressAttributes instead"]
module PulseExecutionDomain = PulseExecutionDomain
[@@deprecated "use the short form ExecutionDomain instead"]
end

20
infer/src/pulse/PulseExecutionState.ml → infer/src/pulse/PulseExecutionDomain.ml
Unescape View File

@ -4,37 +4,39 @@
* This source code is licensed under the MIT license found in the * This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree. * LICENSE file in the root directory of this source tree.
*) *)
open! IStd open! IStd
module F = Format module F = Format
module AbductiveDomain = PulseAbductiveDomain
type exec_state = type exec_state =
| AbortProgram of PulseAbductiveDomain.t | AbortProgram of AbductiveDomain.t
| ContinueProgram of PulseAbductiveDomain.t | ContinueProgram of AbductiveDomain.t
| ExitProgram of PulseAbductiveDomain.t | ExitProgram of AbductiveDomain.t
type t = exec_state type t = exec_state
let continue astate = ContinueProgram astate let continue astate = ContinueProgram astate
let mk_initial pdesc = ContinueProgram (PulseAbductiveDomain.mk_initial pdesc) let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc)
let leq ~lhs ~rhs = let leq ~lhs ~rhs =
match (lhs, rhs) with match (lhs, rhs) with
| AbortProgram astate1, AbortProgram astate2 | AbortProgram astate1, AbortProgram astate2
| ContinueProgram astate1, ContinueProgram astate2 | ContinueProgram astate1, ContinueProgram astate2
| ExitProgram astate1, ExitProgram astate2 -> | ExitProgram astate1, ExitProgram astate2 ->
PulseAbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
| _ -> | _ ->
false false
let pp fmt = function let pp fmt = function
| ContinueProgram astate -> | ContinueProgram astate ->
PulseAbductiveDomain.pp fmt astate AbductiveDomain.pp fmt astate
| ExitProgram astate -> | ExitProgram astate ->
F.fprintf fmt "{ExitProgram %a}" PulseAbductiveDomain.pp astate F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp astate
| AbortProgram astate -> | AbortProgram astate ->
F.fprintf fmt "{AbortProgram %a}" PulseAbductiveDomain.pp astate F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp astate
let map ~f exec_state = let map ~f exec_state =
@ -47,4 +49,4 @@ let map ~f exec_state =
ExitProgram (f astate) ExitProgram (f astate)
let of_post pdesc = map ~f:(PulseAbductiveDomain.of_post pdesc) let of_post pdesc = map ~f:(AbductiveDomain.of_post pdesc)

0
infer/src/pulse/PulseExecutionState.mli → infer/src/pulse/PulseExecutionDomain.mli
Unescape View File

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

@ -16,8 +16,8 @@ type model =
-> callee_procname:Procname.t -> callee_procname:Procname.t
-> Location.t -> Location.t
-> ret:Ident.t * Typ.t -> ret:Ident.t * Typ.t
-> PulseAbductiveDomain.t -> AbductiveDomain.t
-> PulseExecutionState.t list PulseOperations.access_result -> ExecutionDomain.t list PulseOperations.access_result
module Misc = struct module Misc = struct
let shallow_copy model_desc dest_pointer_hist src_pointer_hist : model = let shallow_copy model_desc dest_pointer_hist src_pointer_hist : model =
@ -31,12 +31,12 @@ module Misc = struct
astate astate
in in
let astate = PulseOperations.havoc_id ret_id [event] astate in let astate = PulseOperations.havoc_id ret_id [event] astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let early_exit : model = let early_exit : model =
fun ~caller_summary:_ ~callee_procname:_ _ ~ret:_ astate -> fun ~caller_summary:_ ~callee_procname:_ _ ~ret:_ astate ->
Ok [PulseExecutionState.ExitProgram astate] Ok [ExecutionDomain.ExitProgram astate]
let return_int : Int64.t -> model = let return_int : Int64.t -> model =
@ -91,7 +91,7 @@ module C = struct
PulseOperations.ok_continue astate PulseOperations.ok_continue astate
else else
let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let malloc _ : model = let malloc _ : model =
@ -107,7 +107,7 @@ module C = struct
PulseOperations.allocate callee_procname location ret_value astate PulseOperations.allocate callee_procname location ret_value astate
|> AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.pos) |> AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.pos)
|> AddressAttributes.add_one ret_addr (CItv (CItv.ge_to IntLit.one, immediate_hist)) |> AddressAttributes.add_one ret_addr (CItv (CItv.ge_to IntLit.one, immediate_hist))
|> PulseExecutionState.continue |> ExecutionDomain.continue
in in
let+ astate_null = let+ astate_null =
AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit IntLit.zero)) astate AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit IntLit.zero)) astate
@ -115,7 +115,7 @@ module C = struct
|> PulseOperations.invalidate location (Invalidation.ConstantDereference IntLit.zero) |> PulseOperations.invalidate location (Invalidation.ConstantDereference IntLit.zero)
ret_value ret_value
in in
[astate_alloc; PulseExecutionState.ContinueProgram astate_null] [astate_alloc; ExecutionDomain.ContinueProgram astate_null]
end end
module Cplusplus = struct module Cplusplus = struct
@ -124,7 +124,7 @@ module Cplusplus = struct
let+ astate = let+ astate =
PulseOperations.invalidate location Invalidation.CppDelete deleted_access astate PulseOperations.invalidate location Invalidation.CppDelete deleted_access astate
in in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let placement_new actuals : model = let placement_new actuals : model =
@ -163,7 +163,7 @@ module StdAtomicInteger = struct
in in
let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in
let+ astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in let+ astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let arith_bop prepost location event ret_id bop this operand astate = let arith_bop prepost location event ret_id bop this operand astate =
@ -186,7 +186,7 @@ module StdAtomicInteger = struct
arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment) arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment)
astate astate
in in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let fetch_sub this (increment, _) _memory_ordering : model = let fetch_sub this (increment, _) _memory_ordering : model =
@ -196,7 +196,7 @@ module StdAtomicInteger = struct
arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment) arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment)
astate astate
in in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let operator_plus_plus_pre this : model = let operator_plus_plus_pre this : model =
@ -205,7 +205,7 @@ module StdAtomicInteger = struct
let+ astate = let+ astate =
arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate
in in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let operator_plus_plus_post this _int : model = let operator_plus_plus_post this _int : model =
@ -216,7 +216,7 @@ module StdAtomicInteger = struct
let+ astate = let+ astate =
arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate
in in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let operator_minus_minus_pre this : model = let operator_minus_minus_pre this : model =
@ -225,7 +225,7 @@ module StdAtomicInteger = struct
let+ astate = let+ astate =
arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate
in in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let operator_minus_minus_post this _int : model = let operator_minus_minus_post this _int : model =
@ -236,7 +236,7 @@ module StdAtomicInteger = struct
let+ astate = let+ astate =
arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate
in in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let load_instr model_desc this _memory_ordering_opt : model = let load_instr model_desc this _memory_ordering_opt : model =
@ -244,7 +244,7 @@ module StdAtomicInteger = struct
let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in
let+ astate, _int_addr, (int, hist) = load_backing_int location this astate in let+ astate, _int_addr, (int, hist) = load_backing_int location this astate in
let astate = PulseOperations.write_id ret_id (int, event :: hist) astate in let astate = PulseOperations.write_id ret_id (int, event :: hist) astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let load = load_instr "std::atomic<T>::load()" let load = load_instr "std::atomic<T>::load()"
@ -263,7 +263,7 @@ module StdAtomicInteger = struct
fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate ->
let event = ValueHistory.Call {f= Model "std::atomic::store()"; location; in_call= []} in let event = ValueHistory.Call {f= Model "std::atomic::store()"; location; in_call= []} in
let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let exchange this_address (new_value, new_hist) _memory_ordering : model = let exchange this_address (new_value, new_hist) _memory_ordering : model =
@ -272,7 +272,7 @@ module StdAtomicInteger = struct
let* astate, _int_addr, (old_int, old_hist) = load_backing_int location this_address astate in let* astate, _int_addr, (old_int, old_hist) = load_backing_int location this_address astate in
let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in
let astate = PulseOperations.write_id ret_id (old_int, event :: old_hist) astate in let astate = PulseOperations.write_id ret_id (old_int, event :: old_hist) astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
end end
module JavaObject = struct module JavaObject = struct
@ -283,7 +283,7 @@ module JavaObject = struct
let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in
let+ astate, obj_copy = PulseOperations.shallow_copy location obj astate in let+ astate, obj_copy = PulseOperations.shallow_copy location obj astate in
let astate = PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate in let astate = PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
end end
module StdBasicString = struct module StdBasicString = struct
@ -307,7 +307,7 @@ module StdBasicString = struct
PulseOperations.eval_access location string_addr_hist Dereference astate PulseOperations.eval_access location string_addr_hist Dereference astate
in in
let astate = PulseOperations.write_id ret_id (string, event :: hist) astate in let astate = PulseOperations.write_id ret_id (string, event :: hist) astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let destructor this_hist : model = let destructor this_hist : model =
@ -318,7 +318,7 @@ module StdBasicString = struct
let string_addr_hist = (string_addr, call_event :: string_hist) in let string_addr_hist = (string_addr, call_event :: string_hist) in
let* astate = PulseOperations.invalidate_deref location CppDelete string_addr_hist astate in let* astate = PulseOperations.invalidate_deref location CppDelete string_addr_hist astate in
let+ astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in let+ astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
end end
module StdFunction = struct module StdFunction = struct
@ -335,7 +335,7 @@ module StdFunction = struct
match AddressAttributes.get_closure_proc_name lambda astate with match AddressAttributes.get_closure_proc_name lambda astate with
| None -> | None ->
(* we don't know what proc name this lambda resolves to *) (* we don't know what proc name this lambda resolves to *)
Ok (havoc_ret ret astate |> List.map ~f:PulseExecutionState.continue) Ok (havoc_ret ret astate |> List.map ~f:ExecutionDomain.continue)
| Some callee_proc_name -> | Some callee_proc_name ->
let actuals = let actuals =
List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} ->
@ -381,7 +381,7 @@ module StdVector = struct
; in_call= [] } ; in_call= [] }
in in
reallocate_internal_array [crumb] vector vector_f location astate reallocate_internal_array [crumb] vector vector_f location astate
>>| PulseExecutionState.continue >>| List.return >>| ExecutionDomain.continue >>| List.return
let at ~desc vector index : model = let at ~desc vector index : model =
@ -389,7 +389,7 @@ module StdVector = struct
let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
let+ astate, (addr, hist) = element_of_internal_array location vector (fst index) astate in let+ astate, (addr, hist) = element_of_internal_array location vector (fst index) astate in
let astate = PulseOperations.write_id (fst ret) (addr, event :: hist) astate in let astate = PulseOperations.write_id (fst ret) (addr, event :: hist) astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
let reserve vector : model = let reserve vector : model =
@ -397,7 +397,7 @@ module StdVector = struct
let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in
reallocate_internal_array [crumb] vector Reserve location astate reallocate_internal_array [crumb] vector Reserve location astate
>>| AddressAttributes.std_vector_reserve (fst vector) >>| AddressAttributes.std_vector_reserve (fst vector)
>>| PulseExecutionState.continue >>| List.return >>| ExecutionDomain.continue >>| List.return
let push_back vector : model = let push_back vector : model =
@ -410,7 +410,7 @@ module StdVector = struct
else else
(* simulate a re-allocation of the underlying array every time an element is added *) (* simulate a re-allocation of the underlying array every time an element is added *)
reallocate_internal_array [crumb] vector PushBack location astate reallocate_internal_array [crumb] vector PushBack location astate
>>| PulseExecutionState.continue >>| List.return >>| ExecutionDomain.continue >>| List.return
end end
module JavaCollection = struct module JavaCollection = struct
@ -427,7 +427,7 @@ module JavaCollection = struct
>>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem >>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem
in in
let astate = PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate in let astate = PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate in
[PulseExecutionState.ContinueProgram astate] [ExecutionDomain.ContinueProgram astate]
end end
module StringSet = Caml.Set.Make (String) module StringSet = Caml.Set.Make (String)

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

@ -6,14 +6,15 @@
*) *)
open! IStd open! IStd
open PulseBasicInterface open PulseBasicInterface
open PulseDomainInterface
type model = type model =
caller_summary:Summary.t caller_summary:Summary.t
-> callee_procname:Procname.t -> callee_procname:Procname.t
-> Location.t -> Location.t
-> ret:Ident.t * Typ.t -> ret:Ident.t * Typ.t
-> PulseAbductiveDomain.t -> AbductiveDomain.t
-> PulseExecutionState.t list PulseOperations.access_result -> ExecutionDomain.t list PulseOperations.access_result
val dispatch : val dispatch :
Tenv.t Tenv.t

8
infer/src/pulse/PulseOperations.ml
Unescape View File

@ -14,7 +14,7 @@ type t = AbductiveDomain.t
type 'a access_result = ('a, Diagnostic.t * t) result type 'a access_result = ('a, Diagnostic.t * t) result
let ok_continue post = Ok [PulseExecutionState.ContinueProgram post] let ok_continue post = Ok [ExecutionDomain.ContinueProgram post]
(** Check that the [address] is not known to be invalid *) (** Check that the [address] is not known to be invalid *)
let check_addr_access location (address, history) astate = let check_addr_access location (address, history) astate =
@ -495,7 +495,7 @@ let check_memory_leak_unreachable unreachable_attrs location astate =
| _ -> | _ ->
result result
in in
PulseBaseAddressAttributes.fold check_memory_leak unreachable_attrs (Ok ()) BaseAddressAttributes.fold check_memory_leak unreachable_attrs (Ok ())
let remove_vars vars location astate = let remove_vars vars location astate =
@ -592,7 +592,7 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals
in in
Some (f post) Some (f post)
in in
let open PulseExecutionState in let open ExecutionDomain in
match callee_exec_state with match callee_exec_state with
| AbortProgram _ -> | AbortProgram _ ->
(* Callee has failed; don't propagate the failure *) (* Callee has failed; don't propagate the failure *)
@ -604,7 +604,7 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals
let call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt let call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt
(astate : PulseAbductiveDomain.t) : (PulseExecutionState.t list, Diagnostic.t * t) result = (astate : AbductiveDomain.t) : (ExecutionDomain.t list, Diagnostic.t * t) result =
match PulsePayload.read_full ~caller_summary ~callee_pname with match PulsePayload.read_full ~caller_summary ~callee_pname with
| Some (callee_proc_desc, exec_states) -> | Some (callee_proc_desc, exec_states) ->
let formals = let formals =

6
infer/src/pulse/PulseOperations.mli
Unescape View File

@ -9,11 +9,11 @@ open! IStd
open PulseBasicInterface open PulseBasicInterface
open PulseDomainInterface open PulseDomainInterface
type t = PulseAbductiveDomain.t type t = AbductiveDomain.t
type 'a access_result = ('a, Diagnostic.t * t) result type 'a access_result = ('a, Diagnostic.t * t) result
val ok_continue : t -> (PulseExecutionState.exec_state list, 'a) result val ok_continue : t -> (ExecutionDomain.exec_state list, 'a) result
module Closures : sig module Closures : sig
val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t * t) result val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t * t) result
@ -114,7 +114,7 @@ val call :
-> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
-> formals_opt:(Pvar.t * Typ.t) list option -> formals_opt:(Pvar.t * Typ.t) list option
-> t -> t
-> PulseExecutionState.t list access_result -> ExecutionDomain.t list access_result
(** perform an interprocedural call: apply the summary for the call proc name passed as argument if (** perform an interprocedural call: apply the summary for the call proc name passed as argument if
it exists *) it exists *)

7
infer/src/pulse/PulseSummary.ml
Unescape View File

@ -7,14 +7,15 @@
open! IStd open! IStd
module F = Format module F = Format
open PulseDomainInterface
type t = PulseExecutionState.t list type t = ExecutionDomain.t list
let of_posts pdesc posts = List.map posts ~f:(PulseExecutionState.of_post pdesc) let of_posts pdesc posts = List.map posts ~f:(ExecutionDomain.of_post pdesc)
let pp fmt summary = let pp fmt summary =
F.open_vbox 0 ; F.open_vbox 0 ;
F.fprintf fmt "%d pre/post(s)@;" (List.length summary) ; F.fprintf fmt "%d pre/post(s)@;" (List.length summary) ;
List.iteri summary ~f:(fun i pre_post -> List.iteri summary ~f:(fun i pre_post ->
F.fprintf fmt "#%d: @[%a@]@;" i PulseExecutionState.pp pre_post ) ; F.fprintf fmt "#%d: @[%a@]@;" i ExecutionDomain.pp pre_post ) ;
F.close_box () F.close_box ()

5
infer/src/pulse/PulseSummary.mli
Unescape View File

@ -6,9 +6,10 @@
*) *)
open! IStd open! IStd
open PulseDomainInterface
type t = PulseExecutionState.t list type t = ExecutionDomain.t list
val of_posts : Procdesc.t -> PulseExecutionState.t list -> t val of_posts : Procdesc.t -> ExecutionDomain.t list -> t
val pp : Format.formatter -> t -> unit val pp : Format.formatter -> t -> unit

Write Preview
Loading…
Cancel
Save