diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 7730379b9..a753db5d6 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -122,8 +122,8 @@ let extract_impurity tenv pdesc pre_post : ImpurityDomain.t = false in let skipped_calls = - post.BaseDomain.skipped_calls - |> BaseDomain.SkippedCalls.filter (fun proc_name _ -> + AbductiveDomain.extract_skipped_calls pre_post + |> PulseAbductiveDomain.SkippedCalls.filter (fun proc_name _ -> Purity.should_report proc_name && not (is_modeled_pure proc_name) ) in {modified_globals; modified_params; skipped_calls} @@ -144,7 +144,7 @@ let report_errors summary proc_name pname_loc modified_opt = set acc in let skipped_functions = - PulseBaseDomain.SkippedCalls.fold + PulseAbductiveDomain.SkippedCalls.fold (fun proc_name trace acc -> PulseTrace.add_to_errlog ~nesting:1 ~pp_immediate:(fun fmt -> diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index 87473f012..e4dae48b6 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -7,6 +7,7 @@ open! IStd module F = Format +module SkippedCalls = PulseAbductiveDomain.SkippedCalls type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * PulseTrace.t) [@@deriving compare] @@ -24,18 +25,18 @@ module ModifiedVarSet = AbstractDomain.FiniteSet (ModifiedVar) type t = { modified_params: ModifiedVarSet.t ; modified_globals: ModifiedVarSet.t - ; skipped_calls: PulseBaseDomain.SkippedCalls.t } + ; skipped_calls: SkippedCalls.t } let is_pure {modified_globals; modified_params; skipped_calls} = ModifiedVarSet.is_empty modified_globals && ModifiedVarSet.is_empty modified_params - && PulseBaseDomain.SkippedCalls.is_empty skipped_calls + && SkippedCalls.is_empty skipped_calls let pure = { modified_params= ModifiedVarSet.empty ; modified_globals= ModifiedVarSet.empty - ; skipped_calls= PulseBaseDomain.SkippedCalls.empty } + ; skipped_calls= SkippedCalls.empty } let join astate1 astate2 = @@ -47,7 +48,7 @@ let join astate1 astate2 = ~res: { modified_globals= ModifiedVarSet.join mg1 mg2 ; modified_params= ModifiedVarSet.join mp1 mp2 - ; skipped_calls= PulseBaseDomain.SkippedCalls.union (fun _pname t1 _ -> Some t1) uk1 uk2 } + ; skipped_calls= 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 fa91e56f2..d5c58e725 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: PulseBaseDomain.SkippedCalls.t } + ; skipped_calls: PulseAbductiveDomain.SkippedCalls.t } val pure : t diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 9504c067c..77b7a678f 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -11,7 +11,6 @@ open PulseBasicInterface module BaseDomain = PulseBaseDomain module BaseStack = PulseBaseStack module BaseMemory = PulseBaseMemory -module BaseSkippedCalls = BaseDomain.SkippedCalls module BaseAddressAttributes = PulseBaseAddressAttributes (** signature common to the "normal" [Domain], representing the post at the current program point, @@ -23,13 +22,7 @@ module type BaseDomain = sig val empty : t - val update : - ?stack:BaseStack.t - -> ?heap:BaseMemory.t - -> ?skipped_calls:BaseSkippedCalls.t - -> ?attrs:BaseAddressAttributes.t - -> t - -> t + val update : ?stack:BaseStack.t -> ?heap:BaseMemory.t -> ?attrs:BaseAddressAttributes.t -> t -> t val filter_addr : f:(AbstractValue.t -> bool) -> t -> t (**filter both heap and attrs *) @@ -40,26 +33,21 @@ end (* just to expose record field names without having to type [BaseDomain.heap] *) type base_domain = BaseDomain.t = - { heap: BaseMemory.t - ; stack: BaseStack.t - ; skipped_calls: BaseSkippedCalls.t - ; attrs: BaseAddressAttributes.t } + {heap: BaseMemory.t; stack: BaseStack.t; attrs: BaseAddressAttributes.t} (** operations common to [Domain] and [InvertedDomain], see also the [BaseDomain] signature *) module BaseDomainCommon = struct - let update ?stack ?heap ?skipped_calls ?attrs foot = - let new_stack, new_heap, new_skipped_calls, new_attrs = + let update ?stack ?heap ?attrs foot = + let new_stack, new_heap, new_attrs = ( Option.value ~default:foot.stack stack , Option.value ~default:foot.heap heap - , 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 foot.skipped_calls && phys_equal new_attrs foot.attrs then foot - else {stack= new_stack; heap= new_heap; skipped_calls= new_skipped_calls; attrs= new_attrs} + else {stack= new_stack; heap= new_heap; attrs= new_attrs} let filter_addr ~f foot = @@ -85,18 +73,33 @@ module InvertedDomain : BaseDomain = struct let pp = BaseDomain.pp end -(** biabduction-style pre/post state *) +module SkippedTrace = struct + type t = PulseTrace.t [@@deriving compare] + + let pp fmt = + PulseTrace.pp fmt ~pp_immediate:(fun fmt -> + F.pp_print_string fmt "call to skipped function occurs here" ) + + + let leq ~lhs ~rhs = phys_equal lhs rhs + + let join s1 _ = s1 + + let widen ~prev ~next ~num_iters:_ = join prev next +end + +module SkippedCalls = AbstractDomain.Map (Procname) (SkippedTrace) + +(** biabduction-style pre/post state + skipped calls *) type t = { post: Domain.t (** state at the current program point*) - ; pre: InvertedDomain.t (** inferred pre at the current program point *) } + ; pre: InvertedDomain.t (** inferred pre at the current program point *) + ; skipped_calls: SkippedCalls.t (** set of skipped calls *) } let pp f {post; pre} = F.fprintf f "@[%a@;PRE=[%a]@]" Domain.pp post InvertedDomain.pp pre let leq ~lhs ~rhs = - (* We only care about post state for skipped calls. TODO: Pull - skipped calls out of BaseDomain to here. *) - BaseDomain.SkippedCalls.leq ~lhs:(lhs.post :> BaseDomain.t).skipped_calls - ~rhs:(rhs.post :> BaseDomain.t).skipped_calls + SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls && match BaseDomain.isograph_map BaseDomain.empty_mapping @@ -141,7 +144,10 @@ module Stack = struct InvertedDomain.update ~stack:foot_stack ~heap:foot_heap astate.pre else astate.pre in - ({post= Domain.update astate.post ~stack:post_stack; pre}, addr_hist) + ( { post= Domain.update astate.post ~stack:post_stack + ; pre + ; skipped_calls= astate.skipped_calls } + , addr_hist ) let add var addr_loc_opt astate = @@ -271,7 +277,8 @@ module Memory = struct else (astate.pre :> base_domain).heap in ( { post= Domain.update astate.post ~heap:post_heap - ; pre= InvertedDomain.update astate.pre ~heap:foot_heap } + ; pre= InvertedDomain.update astate.pre ~heap:foot_heap + ; skipped_calls= astate.skipped_calls } , addr_hist_dst ) @@ -302,20 +309,14 @@ let mk_initial proc_desc = InvertedDomain.update ~stack:initial_stack ~heap:initial_heap InvertedDomain.empty in let post = Domain.update ~stack:initial_stack Domain.empty in - {pre; post} - - -(** [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:(f (astate.post :> base_domain).skipped_calls) - in - if phys_equal new_post astate.post then astate else {astate with post= new_post} + let skipped_calls = SkippedCalls.empty in + {pre; post; skipped_calls} 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 new_skipped_calls = SkippedCalls.add pname trace astate.skipped_calls in + if phys_equal new_skipped_calls astate.skipped_calls then astate + else {astate with skipped_calls= new_skipped_calls} let discard_unreachable ({pre; post} as astate) = @@ -329,7 +330,7 @@ let discard_unreachable ({pre; post} as astate) = Domain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address all_addresses) post in if phys_equal pre_new pre && phys_equal post_new post then astate - else {pre= pre_new; post= post_new} + else {astate with pre= pre_new; post= post_new} let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var) @@ -362,7 +363,8 @@ module PrePost = struct in let pre_heap = deregister_empty (astate.pre :> base_domain).heap in let post_heap = deregister_empty (astate.post :> base_domain).heap in - { pre= InvertedDomain.update astate.pre ~heap:pre_heap + { astate with + pre= InvertedDomain.update astate.pre ~heap:pre_heap ; post= Domain.update ~stack:post_stack ~heap:post_heap astate.post } @@ -395,7 +397,7 @@ module PrePost = struct attrs attrs in if phys_equal attrs attrs' then astate - else {pre= astate.pre; post= Domain.update astate.post ~attrs:attrs'} + else {astate with pre= astate.pre; post= Domain.update astate.post ~attrs:attrs'} let of_post pdesc astate = @@ -971,18 +973,17 @@ 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 in + let callee_skipped_map = pre_post.skipped_calls in let caller_skipped_map = - BaseSkippedCalls.map + SkippedCalls.map (fun trace -> add_call_to_trace callee_proc_name call_loc [] trace) callee_skipped_map |> (* favor calls we already knew about somewhat arbitrarily *) - BaseSkippedCalls.union + SkippedCalls.union (fun _ orig_call _callee_call -> Some orig_call) - (call_state.astate.post :> BaseDomain.t).skipped_calls + call_state.astate.skipped_calls in - { call_state with - astate= map_post_skipped_calls ~f:(fun _ -> caller_skipped_map) call_state.astate } + {call_state with astate= {call_state.astate with skipped_calls= caller_skipped_map}} let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state = @@ -1081,3 +1082,5 @@ end let extract_pre {pre} = (pre :> BaseDomain.t) let extract_post {post} = (post :> BaseDomain.t) + +let extract_skipped_calls {skipped_calls} = skipped_calls diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index b841a5cfe..0ec3674b3 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -95,6 +95,12 @@ val find_post_cell_opt : AbstractValue.t -> t -> BaseDomain.cell option val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t +module SkippedTrace : sig + type t = PulseTrace.t +end + +module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t + module PrePost : sig type domain_t = t @@ -125,3 +131,5 @@ val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t val extract_pre : PrePost.t -> BaseDomain.t val extract_post : PrePost.t -> BaseDomain.t + +val extract_skipped_calls : PrePost.t -> SkippedCalls.t diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index 9daaa302f..a73277bb5 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -12,26 +12,9 @@ module Memory = PulseBaseMemory module Stack = PulseBaseStack module AddressAttributes = PulseBaseAddressAttributes -module SkippedTrace = struct - type t = PulseTrace.t [@@deriving compare] - - let pp fmt = - PulseTrace.pp fmt ~pp_immediate:(fun fmt -> - F.pp_print_string fmt "call to skipped function occurs here" ) - - - let leq ~lhs ~rhs = phys_equal lhs rhs - - let join _ _ = assert false - - let widen ~prev:_ ~next:_ ~num_iters:_ = assert false -end - -module SkippedCalls = AbstractDomain.Map (Procname) (SkippedTrace) - (* {2 Abstract domain description } *) -type t = {heap: Memory.t; stack: Stack.t; skipped_calls: SkippedCalls.t; attrs: AddressAttributes.t} +type t = {heap: Memory.t; stack: Stack.t; attrs: AddressAttributes.t} let empty = { heap= @@ -39,7 +22,6 @@ 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= SkippedCalls.empty ; attrs= AddressAttributes.empty } @@ -197,10 +179,9 @@ module GraphComparison = struct match isograph_map ~lhs ~rhs mapping with IsomorphicUpTo _ -> true | NotIsomorphic -> false end -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 SkippedCalls.pp skipped_calls +let pp fmt {heap; stack; attrs} = + F.fprintf fmt "{@[ roots=@[%a@];@;mem =@[%a@];@;attrs=@[%a@];@]}" Stack.pp stack + Memory.pp heap AddressAttributes.pp attrs module GraphVisit : sig diff --git a/infer/src/pulse/PulseBaseDomain.mli b/infer/src/pulse/PulseBaseDomain.mli index 95b3e9256..75cff7f9f 100644 --- a/infer/src/pulse/PulseBaseDomain.mli +++ b/infer/src/pulse/PulseBaseDomain.mli @@ -9,17 +9,7 @@ open! IStd open PulseBasicInterface module F = Format -module SkippedTrace : sig - type t = PulseTrace.t -end - -module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t - -type t = - { heap: PulseBaseMemory.t - ; stack: PulseBaseStack.t - ; skipped_calls: SkippedCalls.t - ; attrs: PulseBaseAddressAttributes.t } +type t = {heap: PulseBaseMemory.t; stack: PulseBaseStack.t; attrs: PulseBaseAddressAttributes.t} type cell = PulseBaseMemory.Edges.t * Attributes.t