[pulse][9/9] add PulseDiagnostic to PulseBasicInterface

Summary: See explanations in D17955104

Reviewed By: ezgicicek

Differential Revision: D17955288

fbshipit-source-id: ac5932cd2

infer/src/pulse/Pulse.ml

@@ -11,7 +11,7 @@ open Result.Monad_infix
 open PulseBasicInterface
 
 let report summary diagnostic =
-  let open PulseDiagnostic in
+  let open Diagnostic in
   Reporting.log_error summary ~loc:(get_location diagnostic) ~ltr:(get_trace diagnostic)
     (get_issue_type diagnostic) (get_message diagnostic)
 

infer/src/pulse/PulseAbductiveDomain.ml

@@ -442,8 +442,7 @@ module PrePost = struct
         let access_trace = add_call callee_access_trace in
         match Memory.check_valid access_trace (fst addr_hist_caller) call_state.astate with
         | Error invalidated_by ->
-            Error
-              (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace})
+            Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace})
         | Ok astate ->
             let call_state = {call_state with astate} in
             Container.fold_result

infer/src/pulse/PulseAbductiveDomain.mli

@@ -95,7 +95,7 @@ module PrePost : sig
     -> formals:Var.t list
     -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
     -> domain_t
-    -> (domain_t * (AbstractValue.t * ValueHistory.t) option, PulseDiagnostic.t) result
+    -> (domain_t * (AbstractValue.t * ValueHistory.t) option, Diagnostic.t) result
   (** return the abstract state after the call along with an optional return value *)
 end
 

infer/src/pulse/PulseBasicInterface.ml

@@ -12,6 +12,7 @@ module AbstractValue = PulseAbstractValue
 module Attribute = PulseAttribute
 module Attributes = PulseAttribute.Attributes
 module CallEvent = PulseCallEvent
+module Diagnostic = PulseDiagnostic
 module Invalidation = PulseInvalidation
 module Trace = PulseTrace
 module ValueHistory = PulseValueHistory

infer/src/pulse/PulseDiagnostic.ml

@@ -7,7 +7,10 @@
 
 open! IStd
 module F = Format
-open PulseBasicInterface
+module CallEvent = PulseCallEvent
+module Invalidation = PulseInvalidation
+module Trace = PulseTrace
+module ValueHistory = PulseValueHistory
 
 type t =
   | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t}

infer/src/pulse/PulseDiagnostic.mli

@@ -6,7 +6,9 @@
  *)
 
 open! IStd
-open PulseBasicInterface
+module Invalidation = PulseInvalidation
+module Trace = PulseTrace
+module ValueHistory = PulseValueHistory
 
 (** an error to report to the user *)
 type t =

infer/src/pulse/PulseOperations.ml

@@ -12,14 +12,14 @@ open PulseDomainInterface
 
 type t = AbductiveDomain.t
 
-type 'a access_result = ('a, PulseDiagnostic.t) result
+type 'a access_result = ('a, Diagnostic.t) result
 
 (** Check that the [address] is not known to be invalid *)
 let check_addr_access location (address, history) astate =
   let accessed_by = Trace.Immediate {imm= (); location; history} in
   Memory.check_valid accessed_by address astate
   |> Result.map_error ~f:(fun invalidated_by ->
-         PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by} )
+         Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by} )
 
 
 module Closures = struct
@@ -304,7 +304,7 @@ let check_address_escape escape_location proc_desc address history astate =
                    (* The returned address corresponds to a C++ temporary. It will have gone out of
                       scope by now except if it was bound to a global. *)
                    Error
-                     (PulseDiagnostic.StackVariableAddressEscape
+                     (Diagnostic.StackVariableAddressEscape
                         {variable; location= escape_location; history})
                | _ ->
                    Ok () ) )
@@ -322,8 +322,7 @@ let check_address_escape escape_location proc_desc address history astate =
           L.d_printfln_escaped "Stack variable address &%a detected at address %a" Var.pp variable
             AbstractValue.pp address ;
           Error
-            (PulseDiagnostic.StackVariableAddressEscape
-               {variable; location= escape_location; history}) )
+            (Diagnostic.StackVariableAddressEscape {variable; location= escape_location; history}) )
         else Ok () )
   in
   check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate

infer/src/pulse/PulseOperations.mli

@@ -11,11 +11,10 @@ open PulseDomainInterface
 
 type t = PulseAbductiveDomain.t
 
-type 'a access_result = ('a, PulseDiagnostic.t) result
+type 'a access_result = ('a, Diagnostic.t) result
 
 module Closures : sig
-  val check_captured_addresses :
-    Location.t -> AbstractValue.t -> t -> (t, PulseDiagnostic.t) result
+  val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t) result
   (** assert the validity of the addresses captured by the lambda *)
 end