[pulse][1/9] create PulseBasicInterface, with CallEvent

Summary:
Problem: PulseDomain.ml is pretty big, and contains lots of small
modules. The Infer build being a bit monolithic at the moment, it is
hard to split all these small modules off without creating some
confusion about which abstraction barries lay where. For instance, it's
fine to use `PulseDomain.ValueHistory` anywhere, but using `PulseDomain`
itself is sometimes bad when one should use `PulseAbductiveDomain`
instead.

Proposal: a poorman's library mechanism based on module aliasing. This
stack of diffs creates new Pulse* modules for all these small, safe to
use modules, together with `PulseBasicInterface.ml`, which aliases these
modules to remove the `Pulse` prefix. At the end of the stack, it will
contain:

```
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
```

This "interface" module can be opened in other pulse modules freely.

Reviewed By: ezgicicek

Differential Revision: D17955104

fbshipit-source-id: 13d3aa2b5

infer/src/pulse/PulseBasicInterface.ml

@@ -0,0 +1,11 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+(** Basic Pulse modules that are safe to use in any module *)
+
+module CallEvent = PulseCallEvent

infer/src/pulse/PulseCallEvent.ml

@@ -0,0 +1,32 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+
+type t =
+  | Call of Typ.Procname.t
+  | Model of string
+  | SkippedKnownCall of Typ.Procname.t
+  | SkippedUnknownCall of Exp.t
+[@@deriving compare]
+
+let pp_config ~verbose fmt =
+  let pp_proc_name = if verbose then Typ.Procname.pp else Typ.Procname.describe in
+  function
+  | Call proc_name ->
+      F.fprintf fmt "`%a`" pp_proc_name proc_name
+  | Model model ->
+      F.fprintf fmt "`%s` (modelled)" model
+  | SkippedKnownCall proc_name ->
+      F.fprintf fmt "function `%a` with no summary" pp_proc_name proc_name
+  | SkippedUnknownCall call_exp ->
+      F.fprintf fmt "unresolved call expression `%a`" Exp.pp call_exp
+
+
+let pp = pp_config ~verbose:true
+
+let describe = pp_config ~verbose:false

infer/src/pulse/PulseCallEvent.mli

@@ -0,0 +1,20 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module F = Format
+
+type t =
+  | Call of Typ.Procname.t  (** known function with summary *)
+  | Model of string  (** hardcoded model *)
+  | SkippedKnownCall of Typ.Procname.t  (** known function without summary *)
+  | SkippedUnknownCall of Exp.t  (** couldn't link the expression to a proc name *)
+[@@deriving compare]
+
+val pp : F.formatter -> t -> unit
+
+val describe : F.formatter -> t -> unit

infer/src/pulse/PulseDiagnostic.ml

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

infer/src/pulse/PulseDomain.ml

@@ -7,35 +7,10 @@
 open! IStd
 module F = Format
 module L = Logging
+open PulseBasicInterface
 
 (* {2 Abstract domain description } *)
 
-module CallEvent = struct
-  type t =
-    | Call of Typ.Procname.t
-    | Model of string
-    | SkippedKnownCall of Typ.Procname.t
-    | SkippedUnknownCall of Exp.t
-  [@@deriving compare]
-
-  let pp_config ~verbose fmt =
-    let pp_proc_name = if verbose then Typ.Procname.pp else Typ.Procname.describe in
-    function
-    | Call proc_name ->
-        F.fprintf fmt "`%a`" pp_proc_name proc_name
-    | Model model ->
-        F.fprintf fmt "`%s` (modelled)" model
-    | SkippedKnownCall proc_name ->
-        F.fprintf fmt "function `%a` with no summary" pp_proc_name proc_name
-    | SkippedUnknownCall call_exp ->
-        F.fprintf fmt "unresolved call expression `%a`" Exp.pp call_exp
-
-
-  let pp = pp_config ~verbose:true
-
-  let describe = pp_config ~verbose:false
-end
-
 module Invalidation = struct
   type std_vector_function =
     | Assign

infer/src/pulse/PulseDomain.mli

@@ -7,16 +7,7 @@
 
 open! IStd
 module F = Format
-
-module CallEvent : sig
-  type t =
-    | Call of Typ.Procname.t  (** known function with summary *)
-    | Model of string  (** hardcoded model *)
-    | SkippedKnownCall of Typ.Procname.t  (** known function without summary *)
-    | SkippedUnknownCall of Exp.t  (** couldn't link the expression to a proc name *)
-
-  val describe : F.formatter -> t -> unit
-end
+open PulseBasicInterface
 
 module Invalidation : sig
   type std_vector_function =

infer/src/pulse/PulseModels.ml

@@ -6,6 +6,7 @@
  *)
 open! IStd
 open Result.Monad_infix
+open PulseBasicInterface
 
 type exec_fun =
      caller_summary:Summary.t
@@ -106,7 +107,7 @@ module StdBasicString = struct
 
   let destructor : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
-    let model = PulseDomain.CallEvent.Model "std::basic_string::~basic_string()" in
+    let model = CallEvent.Model "std::basic_string::~basic_string()" in
     let call_event = PulseDomain.ValueHistory.Call {f= model; location; in_call= []} in
     match actuals with
     | [(this_hist, _)] ->