From 4677584018f0c9e592f2df0f3eb0a928e48ea7b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 28 Jan 2020 07:39:50 -0800 Subject: [PATCH] [pulse] Remove map suffix from SkippedCalls Reviewed By: jvillard Differential Revision: D19555827 fbshipit-source-id: 8ebc2f41d --- infer/src/checkers/impurity.ml | 14 ++++----- infer/src/checkers/impurityDomain.ml | 15 +++++---- infer/src/checkers/impurityDomain.mli | 2 +- infer/src/pulse/PulseAbductiveDomain.ml | 39 ++++++++++++------------ infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseBaseDomain.ml | 11 +++---- infer/src/pulse/PulseBaseDomain.mli | 4 +-- infer/src/pulse/PulseOperations.ml | 2 +- 8 files changed, 43 insertions(+), 46 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index ff22729be..7730379b9 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -121,12 +121,12 @@ let extract_impurity tenv pdesc pre_post : ImpurityDomain.t = | None -> false in - let skipped_calls_map = - post.BaseDomain.skipped_calls_map - |> BaseDomain.SkippedCallsMap.filter (fun proc_name _ -> + let skipped_calls = + post.BaseDomain.skipped_calls + |> BaseDomain.SkippedCalls.filter (fun proc_name _ -> Purity.should_report proc_name && not (is_modeled_pure proc_name) ) in - {modified_globals; modified_params; skipped_calls_map} + {modified_globals; modified_params; skipped_calls} let report_errors summary proc_name pname_loc modified_opt = @@ -136,7 +136,7 @@ let report_errors summary proc_name pname_loc modified_opt = | None -> Reporting.log_error summary ~loc:pname_loc ~ltr:[impure_fun_ltr] IssueType.impure_function impure_fun_desc - | Some (ImpurityDomain.{modified_globals; modified_params; skipped_calls_map} as astate) -> + | Some (ImpurityDomain.{modified_globals; modified_params; skipped_calls} as astate) -> if Purity.should_report proc_name && not (ImpurityDomain.is_pure astate) then let modified_ltr param_source set acc = ImpurityDomain.ModifiedVarSet.fold @@ -144,13 +144,13 @@ let report_errors summary proc_name pname_loc modified_opt = set acc in let skipped_functions = - PulseBaseDomain.SkippedCallsMap.fold + PulseBaseDomain.SkippedCalls.fold (fun proc_name trace acc -> PulseTrace.add_to_errlog ~nesting:1 ~pp_immediate:(fun fmt -> F.fprintf fmt "call to skipped function %a occurs here" Procname.pp proc_name ) trace acc ) - skipped_calls_map [] + skipped_calls [] in let ltr = impure_fun_ltr diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index 3da3cfaa7..87473f012 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -24,31 +24,30 @@ module ModifiedVarSet = AbstractDomain.FiniteSet (ModifiedVar) type t = { modified_params: ModifiedVarSet.t ; modified_globals: ModifiedVarSet.t - ; skipped_calls_map: PulseBaseDomain.SkippedCallsMap.t } + ; skipped_calls: PulseBaseDomain.SkippedCalls.t } -let is_pure {modified_globals; modified_params; skipped_calls_map} = +let is_pure {modified_globals; modified_params; skipped_calls} = ModifiedVarSet.is_empty modified_globals && ModifiedVarSet.is_empty modified_params - && PulseBaseDomain.SkippedCallsMap.is_empty skipped_calls_map + && PulseBaseDomain.SkippedCalls.is_empty skipped_calls let pure = { modified_params= ModifiedVarSet.empty ; modified_globals= ModifiedVarSet.empty - ; skipped_calls_map= PulseBaseDomain.SkippedCallsMap.empty } + ; skipped_calls= PulseBaseDomain.SkippedCalls.empty } let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else - let {modified_globals= mg1; modified_params= mp1; skipped_calls_map= uk1} = astate1 in - let {modified_globals= mg2; modified_params= mp2; skipped_calls_map= uk2} = astate2 in + let {modified_globals= mg1; modified_params= mp1; skipped_calls= uk1} = astate1 in + let {modified_globals= mg2; modified_params= mp2; skipped_calls= uk2} = astate2 in PhysEqual.optim2 ~res: { modified_globals= ModifiedVarSet.join mg1 mg2 ; modified_params= ModifiedVarSet.join mp1 mp2 - ; skipped_calls_map= - PulseBaseDomain.SkippedCallsMap.union (fun _pname t1 _ -> Some t1) uk1 uk2 } + ; skipped_calls= PulseBaseDomain.SkippedCalls.union (fun _pname t1 _ -> Some t1) uk1 uk2 } astate1 astate2 diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 629876dde..fa91e56f2 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -21,7 +21,7 @@ end type t = { modified_params: ModifiedVarSet.t ; modified_globals: ModifiedVarSet.t - ; skipped_calls_map: PulseBaseDomain.SkippedCallsMap.t } + ; skipped_calls: PulseBaseDomain.SkippedCalls.t } val pure : t diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 1e2fd55a9..fc23c04c9 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -11,7 +11,7 @@ open PulseBasicInterface module BaseDomain = PulseBaseDomain module BaseStack = PulseBaseStack module BaseMemory = PulseBaseMemory -module BaseSkippedCallsMap = BaseDomain.SkippedCallsMap +module BaseSkippedCalls = BaseDomain.SkippedCalls module BaseAddressAttributes = PulseBaseAddressAttributes (** signature common to the "normal" [Domain], representing the post at the current program point, @@ -26,7 +26,7 @@ module type BaseDomain = sig val update : ?stack:BaseStack.t -> ?heap:BaseMemory.t - -> ?skipped_calls_map:BaseSkippedCallsMap.t + -> ?skipped_calls:BaseSkippedCalls.t -> ?attrs:BaseAddressAttributes.t -> t -> t @@ -42,25 +42,24 @@ end type base_domain = BaseDomain.t = { heap: BaseMemory.t ; stack: BaseStack.t - ; skipped_calls_map: BaseSkippedCallsMap.t + ; skipped_calls: BaseSkippedCalls.t ; attrs: BaseAddressAttributes.t } (** operations common to [Domain] and [InvertedDomain], see also the [BaseDomain] signature *) module BaseDomainCommon = struct - let update ?stack ?heap ?skipped_calls_map ?attrs foot = - let new_stack, new_heap, new_skipped_calls_map, new_attrs = + let update ?stack ?heap ?skipped_calls ?attrs foot = + let new_stack, new_heap, new_skipped_calls, new_attrs = ( Option.value ~default:foot.stack stack , Option.value ~default:foot.heap heap - , Option.value ~default:foot.skipped_calls_map skipped_calls_map + , Option.value ~default:foot.skipped_calls skipped_calls , Option.value ~default:foot.attrs attrs ) in if phys_equal new_stack foot.stack && phys_equal new_heap foot.heap - && phys_equal new_skipped_calls_map foot.skipped_calls_map + && phys_equal new_skipped_calls foot.skipped_calls && phys_equal new_attrs foot.attrs then foot - else - {stack= new_stack; heap= new_heap; skipped_calls_map= new_skipped_calls_map; attrs= new_attrs} + else {stack= new_stack; heap= new_heap; skipped_calls= new_skipped_calls; attrs= new_attrs} let filter_addr ~f foot = @@ -305,17 +304,17 @@ let mk_initial proc_desc = {pre; post} -(** [astate] with [astate.post.skipped_calls_map = f astate.post.skipped_calls_map] *) -let map_post_skipped_calls_map ~f astate = +(** [astate] with [astate.post.skipped_calls = f astate.post.skipped_calls] *) +let map_post_skipped_calls ~f astate = let new_post = - Domain.update astate.post ~skipped_calls_map:(f (astate.post :> base_domain).skipped_calls_map) + Domain.update astate.post ~skipped_calls:(f (astate.post :> base_domain).skipped_calls) in if phys_equal new_post astate.post then astate else {astate with post= new_post} -let add_skipped_calls_map pname trace astate = - map_post_skipped_calls_map astate ~f:(fun skipped_call_map -> - BaseSkippedCallsMap.add pname trace skipped_call_map ) +let add_skipped_calls pname trace astate = + map_post_skipped_calls astate ~f:(fun skipped_call_map -> + BaseSkippedCalls.add pname trace skipped_call_map ) let discard_unreachable ({pre; post} as astate) = @@ -968,18 +967,18 @@ module PrePost = struct let record_skipped_calls callee_proc_name call_loc pre_post call_state = - let callee_skipped_map = (pre_post.post :> BaseDomain.t).skipped_calls_map in + let callee_skipped_map = (pre_post.post :> BaseDomain.t).skipped_calls in let caller_skipped_map = - BaseSkippedCallsMap.map + BaseSkippedCalls.map (fun trace -> add_call_to_trace callee_proc_name call_loc [] trace) callee_skipped_map |> (* favor calls we already knew about somewhat arbitrarily *) - BaseSkippedCallsMap.union + BaseSkippedCalls.union (fun _ orig_call _callee_call -> Some orig_call) - (call_state.astate.post :> BaseDomain.t).skipped_calls_map + (call_state.astate.post :> BaseDomain.t).skipped_calls in { call_state with - astate= map_post_skipped_calls_map ~f:(fun _ -> caller_skipped_map) call_state.astate } + astate= map_post_skipped_calls ~f:(fun _ -> caller_skipped_map) call_state.astate } let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 505d3c569..b841a5cfe 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -120,7 +120,7 @@ val discard_unreachable : t -> t (** garbage collect unreachable addresses in the state to make it smaller, just for convenience and keep its size down *) -val add_skipped_calls_map : Procname.t -> PulseTrace.t -> t -> t +val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t val extract_pre : PrePost.t -> BaseDomain.t diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index a3c6c047d..7e2938de0 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -20,12 +20,11 @@ module SkippedTrace = struct F.pp_print_string fmt "call to skipped function occurs here" ) end -module SkippedCallsMap = PrettyPrintable.MakePPMonoMap (Procname) (SkippedTrace) +module SkippedCalls = PrettyPrintable.MakePPMonoMap (Procname) (SkippedTrace) (* {2 Abstract domain description } *) -type t = - {heap: Memory.t; stack: Stack.t; skipped_calls_map: SkippedCallsMap.t; attrs: AddressAttributes.t} +type t = {heap: Memory.t; stack: Stack.t; skipped_calls: SkippedCalls.t; attrs: AddressAttributes.t} let empty = { heap= @@ -33,7 +32,7 @@ let empty = (* TODO: we could record that 0 is an invalid address at this point but this makes the analysis go a bit overboard with the Nullptr reports. *) ; stack= Stack.empty - ; skipped_calls_map= SkippedCallsMap.empty + ; skipped_calls= SkippedCalls.empty ; attrs= AddressAttributes.empty } @@ -195,10 +194,10 @@ let leq ~lhs ~rhs = phys_equal lhs rhs || GraphComparison.is_isograph ~lhs ~rhs GraphComparison.empty_mapping -let pp fmt {heap; stack; skipped_calls_map; attrs} = +let pp fmt {heap; stack; skipped_calls; attrs} = F.fprintf fmt "{@[ roots=@[%a@];@;mem =@[%a@];@;attrs=@[%a@];@;skipped_calls=@[%a@];@]}" - Stack.pp stack Memory.pp heap AddressAttributes.pp attrs SkippedCallsMap.pp skipped_calls_map + Stack.pp stack Memory.pp heap AddressAttributes.pp attrs SkippedCalls.pp skipped_calls module GraphVisit : sig diff --git a/infer/src/pulse/PulseBaseDomain.mli b/infer/src/pulse/PulseBaseDomain.mli index 54407fff9..2fbac7aaa 100644 --- a/infer/src/pulse/PulseBaseDomain.mli +++ b/infer/src/pulse/PulseBaseDomain.mli @@ -12,13 +12,13 @@ module SkippedTrace : sig type t = PulseTrace.t end -module SkippedCallsMap : +module SkippedCalls : PrettyPrintable.PPMonoMap with type key = Procname.t and type value = SkippedTrace.t type t = { heap: PulseBaseMemory.t ; stack: PulseBaseStack.t - ; skipped_calls_map: SkippedCallsMap.t + ; skipped_calls: SkippedCalls.t ; attrs: PulseBaseAddressAttributes.t } type cell = PulseBaseMemory.Edges.t * Attributes.t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 0b3fa4051..51d593cb6 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -510,7 +510,7 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = let add_skipped_proc astate = match reason with | PulseCallEvent.SkippedKnownCall proc_name -> - AbductiveDomain.add_skipped_calls_map proc_name + AbductiveDomain.add_skipped_calls proc_name (Trace.Immediate {location= call_loc; history= []}) astate | _ ->