[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

@@ -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 )

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
 

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)

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

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
+      let v' = AbstractValue.mk_fresh () in
-      subst := PulseAbstractValue.Map.add v (v', []) !subst ;
+      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)

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