From 94e3b069009610e8260d6eeb0a09542760626c54 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 15 Apr 2020 07:17:36 -0700 Subject: [PATCH] [pulse] enforce short forms for PulseBasicInterface Summary: The "interface" modules define short forms for the internals of pulse and also serve as a guide of which modules you are supposed to use at which "level" in the pulse domains (base domain vs abductive domain vs higher-level PulseOperations.ml). Make sure they are used. Reviewed By: skcho Differential Revision: D21022927 fbshipit-source-id: f890df245 --- infer/src/checkers/impurity.ml | 8 ++++---- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseBaseAddressAttributes.ml | 2 +- infer/src/pulse/PulseBasicInterface.ml | 20 +++++++++++++++++++ infer/src/pulse/PulseInterproc.ml | 8 ++++---- infer/src/pulse/PulseOperations.ml | 2 +- 6 files changed, 31 insertions(+), 11 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 2e25bfeb9..8d6a8a837 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -49,7 +49,7 @@ let add_invalid_and_modified ~var ~access ~check_empty attrs acc : ImpurityDomai in let invalid_and_modified = match Attributes.get_invalid attrs with - | None | Some (PulseInvalidation.ConstantDereference _, _) -> + | None | Some (Invalidation.ConstantDereference _, _) -> modified | Some invalid -> ImpurityDomain.Invalid invalid :: modified @@ -156,7 +156,7 @@ let extract_impurity tenv pdesc (exec_state : PulseExecutionState.t) : ImpurityD let modified_globals = get_modified_globals pre_heap post post_stack in let skipped_calls = PulseAbductiveDomain.get_skipped_calls astate - |> PulseSkippedCalls.filter (fun proc_name _ -> + |> SkippedCalls.filter (fun proc_name _ -> Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) ) in {modified_globals; modified_params; skipped_calls; exited} @@ -195,9 +195,9 @@ let checker {exe_env; Callbacks.summary} : Summary.t = set acc in let skipped_functions = - PulseSkippedCalls.fold + SkippedCalls.fold (fun proc_name trace acc -> - PulseTrace.add_to_errlog ~nesting:1 ~include_value_history:false + Trace.add_to_errlog ~nesting:1 ~include_value_history:false ~pp_immediate:(fun fmt -> F.fprintf fmt "call to skipped function %a occurs here" Procname.pp proc_name ) trace acc ) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index c2d671aed..1997b7f29 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -151,7 +151,7 @@ val discard_unreachable : t -> t * BaseAddressAttributes.t (** [discard_unreachable astate] garbage collects unreachable addresses in the state to make it smaller, and retuns the new state and the attributes of discarded addresses *) -val add_skipped_call : Procname.t -> PulseTrace.t -> t -> t +val add_skipped_call : Procname.t -> Trace.t -> t -> t val add_skipped_calls : SkippedCalls.t -> t -> t diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 414e0b944..b9c34b77e 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -12,7 +12,7 @@ open PulseBasicInterface module AttributesNoRank = struct include Attributes - let pp fmt t : unit = PulseAttribute.Attributes.pp fmt t + let pp fmt t : unit = Attributes.pp ?print_rank:None fmt t end module Graph = PrettyPrintable.MakePPMonoMap (AbstractValue) (AttributesNoRank) diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml index 9a31a304f..1b1ac402d 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -18,3 +18,23 @@ module Invalidation = PulseInvalidation module SkippedCalls = PulseSkippedCalls module Trace = PulseTrace module ValueHistory = PulseValueHistory + +(** {2 Enforce short form usage} *) + +include struct + [@@@warning "-60"] + + module PulseAbstractValue = PulseAbstractValue + [@@deprecated "use the short form AbstractValue instead"] + module PulseAttribute = PulseAttribute [@@deprecated "use the short form Attribute instead"] + module PulseCallEvent = PulseCallEvent [@@deprecated "use the short form CallEvent instead"] + module PulseCItv = PulseCItv [@@deprecated "use the short form CItv instead"] + module PulseDiagnostic = PulseDiagnostic [@@deprecated "use the short form Diagnostic instead"] + module PulseInvalidation = PulseInvalidation + [@@deprecated "use the short form Invalidation instead"] + module PulseSkippedCalls = PulseSkippedCalls + [@@deprecated "use the short form SkippedCalls instead"] + module PulseTrace = PulseTrace [@@deprecated "use the short form Trace instead"] + module PulseValueHistory = PulseValueHistory + [@@deprecated "use the short form ValueHistory instead"] +end diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 51ace5258..8da90694c 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -226,12 +226,12 @@ let materialize_pre_for_globals callee_proc_name call_location pre_post call_sta let eval_sym_of_subst astate subst s bound_end = let v = Symb.Symbol.get_pulse_value_exn s in - match PulseAbstractValue.Map.find_opt v !subst with + match AbstractValue.Map.find_opt v !subst with | Some (v', _) -> Itv.ItvPure.get_bound (AddressAttributes.get_bo_itv v' astate) bound_end | None -> - let v' = PulseAbstractValue.mk_fresh () in - subst := PulseAbstractValue.Map.add v (v', []) !subst ; + let v' = AbstractValue.mk_fresh () in + subst := AbstractValue.Map.add v (v', []) !subst ; Bounds.Bound.of_pulse_value v' @@ -281,7 +281,7 @@ let add_call_to_attributes proc_name call_location ~addr_callee ~addr_caller cal let attrs = Attributes.map attrs ~f:(fun attr -> subst_attribute call_state subst_ref call_state.astate ~addr_callee ~addr_caller attr - |> PulseAttribute.map_trace ~f:(fun trace -> + |> Attribute.map_trace ~f:(fun trace -> add_call_to_trace proc_name call_location caller_history trace ) ) in (!subst_ref, attrs) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index d64c2ceac..0584818d1 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -546,7 +546,7 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = in let add_skipped_proc astate = match reason with - | PulseCallEvent.SkippedKnownCall proc_name -> + | CallEvent.SkippedKnownCall proc_name -> AbductiveDomain.add_skipped_call proc_name (Trace.Immediate {location= call_loc; history= []}) astate