[pulse] move PulseInvalidation inside PulseDomain

Summary:
Just moving code around.

This is needed later to make some types in `PulseInvalidation` depend on
a new type that I'll have to define in `PulseDomain`.

Reviewed By: mbouaziz

Differential Revision: D15824962

fbshipit-source-id: 86cba2bfb

infer/src/pulse/PulseAbductiveDomain.mli

@@ -46,14 +46,17 @@ module Memory : sig
        HilExp.AccessExpression.t PulseTrace.action
     -> AbstractAddress.t
     -> t
-    -> (t, PulseInvalidation.t PulseTrace.t) result
+    -> (t, PulseDomain.Invalidation.t PulseTrace.t) result
 
   val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option
 
   val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t
 
   val invalidate :
-    AbstractAddress.t * PulseTrace.breadcrumbs -> PulseInvalidation.t PulseTrace.action -> t -> t
+       AbstractAddress.t * PulseTrace.breadcrumbs
+    -> PulseDomain.Invalidation.t PulseTrace.action
+    -> t
+    -> t
 
   val is_std_vector_reserved : AbstractAddress.t -> t -> bool
 

infer/src/pulse/PulseDiagnostic.ml

@@ -11,7 +11,7 @@ module F = Format
 type t =
   | AccessToInvalidAddress of
       { access: HilExp.AccessExpression.t
-      ; invalidated_by: PulseInvalidation.t PulseTrace.t
+      ; invalidated_by: PulseDomain.Invalidation.t PulseTrace.t
       ; accessed_by: HilExp.AccessExpression.t PulseTrace.t }
   | StackVariableAddressEscape of
       { variable: Var.t
@@ -86,10 +86,10 @@ let get_message = function
       let pp_invalidation_trace line f trace =
         match trace.PulseTrace.action with
         | Immediate {imm= invalidation; _} ->
-            F.fprintf f "%a on line %d" PulseInvalidation.describe invalidation line
+            F.fprintf f "%a on line %d" PulseDomain.Invalidation.describe invalidation line
         | ViaCall {action; proc_name; _} ->
             F.fprintf f "%a on line %d indirectly during the call to `%a`"
-              PulseInvalidation.describe
+              PulseDomain.Invalidation.describe
               (PulseTrace.immediate_of_action action)
               line Typ.Procname.describe proc_name
       in
@@ -112,7 +112,8 @@ let get_message = function
 let get_trace = function
   | AccessToInvalidAddress {accessed_by; invalidated_by} ->
       PulseTrace.add_to_errlog ~header:"invalidation part of the trace starts here"
-        (fun f invalidation -> F.fprintf f "memory %a" PulseInvalidation.describe invalidation)
+        (fun f invalidation ->
+          F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation )
         invalidated_by
       @@ PulseTrace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here"
            (fun f access -> F.fprintf f "invalid access to `%a`" HilExp.AccessExpression.pp access)
@@ -127,6 +128,7 @@ let get_trace = function
 
 let get_issue_type = function
   | AccessToInvalidAddress {invalidated_by} ->
-      PulseTrace.immediate_of_action invalidated_by.action |> PulseInvalidation.issue_type_of_cause
+      PulseTrace.immediate_of_action invalidated_by.action
+      |> PulseDomain.Invalidation.issue_type_of_cause
   | StackVariableAddressEscape _ ->
       IssueType.stack_variable_address_escape

infer/src/pulse/PulseDiagnostic.mli

@@ -11,7 +11,7 @@ open! IStd
 type t =
   | AccessToInvalidAddress of
       { access: HilExp.AccessExpression.t
-      ; invalidated_by: PulseInvalidation.t PulseTrace.t
+      ; invalidated_by: PulseDomain.Invalidation.t PulseTrace.t
       ; accessed_by: HilExp.AccessExpression.t PulseTrace.t }
   | StackVariableAddressEscape of
       { variable: Var.t

infer/src/pulse/PulseDomain.ml

@@ -7,10 +7,95 @@
 open! IStd
 module F = Format
 module L = Logging
-module Invalidation = PulseInvalidation
 
 (* {2 Abstract domain description } *)
 
+module Invalidation = struct
+  type std_vector_function =
+    | Assign
+    | Clear
+    | Emplace
+    | EmplaceBack
+    | Insert
+    | PushBack
+    | Reserve
+    | ShrinkToFit
+  [@@deriving compare]
+
+  let pp_std_vector_function f = function
+    | Assign ->
+        F.fprintf f "std::vector::assign"
+    | Clear ->
+        F.fprintf f "std::vector::clear"
+    | Emplace ->
+        F.fprintf f "std::vector::emplace"
+    | EmplaceBack ->
+        F.fprintf f "std::vector::emplace_back"
+    | Insert ->
+        F.fprintf f "std::vector::insert"
+    | PushBack ->
+        F.fprintf f "std::vector::push_back"
+    | Reserve ->
+        F.fprintf f "std::vector::reserve"
+    | ShrinkToFit ->
+        F.fprintf f "std::vector::shrink_to_fit"
+
+
+  type t =
+    | CFree of HilExp.AccessExpression.t
+    | CppDelete of HilExp.AccessExpression.t
+    | GoneOutOfScope of Pvar.t * Typ.t
+    | Nullptr
+    | StdVector of std_vector_function * HilExp.AccessExpression.t
+  [@@deriving compare]
+
+  let issue_type_of_cause = function
+    | CFree _ ->
+        IssueType.use_after_free
+    | CppDelete _ ->
+        IssueType.use_after_delete
+    | GoneOutOfScope _ ->
+        IssueType.use_after_lifetime
+    | Nullptr ->
+        IssueType.null_dereference
+    | StdVector _ ->
+        IssueType.vector_invalidation
+
+
+  let describe f = function
+    | CFree access_expr ->
+        F.fprintf f "was invalidated by call to `free()` on `%a`" HilExp.AccessExpression.pp
+          access_expr
+    | CppDelete access_expr ->
+        F.fprintf f "was invalidated by `delete` on `%a`" HilExp.AccessExpression.pp access_expr
+    | GoneOutOfScope (pvar, typ) ->
+        let pp_var f pvar =
+          if Pvar.is_cpp_temporary pvar then
+            F.fprintf f "is the address of a C++ temporary of type `%a`" (Typ.pp_full Pp.text) typ
+          else F.fprintf f "is the address of a stack variable `%a`" Pvar.pp_value pvar
+        in
+        F.fprintf f "%a whose lifetime has ended" pp_var pvar
+    | Nullptr ->
+        F.fprintf f "is the null pointer"
+    | StdVector (std_vector_f, access_expr) ->
+        F.fprintf f "was potentially invalidated by `%a()` on `%a`" pp_std_vector_function
+          std_vector_f HilExp.AccessExpression.pp access_expr
+
+
+  let pp f invalidation =
+    match invalidation with
+    | CFree _ ->
+        F.fprintf f "CFree(%a)" describe invalidation
+    | CppDelete _ ->
+        F.fprintf f "CppDelete(%a)" describe invalidation
+    | GoneOutOfScope _ ->
+        describe f invalidation
+    | Nullptr ->
+        describe f invalidation
+    | StdVector _ ->
+        F.fprintf f "StdVector(%a)" describe invalidation
+end
+
 (** Purposefully declared before [AbstractAddress] to avoid attributes depending on
     addresses. Otherwise they become a pain to handle when comparing memory states. *)
 module Attribute = struct

infer/src/pulse/PulseDomain.mli

@@ -8,9 +8,36 @@
 open! IStd
 module F = Format
 
+module Invalidation : sig
+  type std_vector_function =
+    | Assign
+    | Clear
+    | Emplace
+    | EmplaceBack
+    | Insert
+    | PushBack
+    | Reserve
+    | ShrinkToFit
+  [@@deriving compare]
+
+  val pp_std_vector_function : Format.formatter -> std_vector_function -> unit
+
+  type t =
+    | CFree of HilExp.AccessExpression.t
+    | CppDelete of HilExp.AccessExpression.t
+    | GoneOutOfScope of Pvar.t * Typ.t
+    | Nullptr
+    | StdVector of std_vector_function * HilExp.AccessExpression.t
+  [@@deriving compare]
+
+  val issue_type_of_cause : t -> IssueType.t
+
+  val describe : Format.formatter -> t -> unit
+end
+
 module Attribute : sig
   type t =
-    | Invalid of PulseInvalidation.t PulseTrace.t
+    | Invalid of Invalidation.t PulseTrace.t
     | MustBeValid of HilExp.AccessExpression.t PulseTrace.action
     | AddressOfCppTemporary of Var.t * Location.t option
     | Closure of Typ.Procname.t
@@ -94,9 +121,9 @@ module Memory : sig
   val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
 
   val invalidate :
-    AbstractAddress.t * PulseTrace.breadcrumbs -> PulseInvalidation.t PulseTrace.action -> t -> t
+    AbstractAddress.t * PulseTrace.breadcrumbs -> Invalidation.t PulseTrace.action -> t -> t
 
-  val check_valid : AbstractAddress.t -> t -> (unit, PulseInvalidation.t PulseTrace.t) result
+  val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t PulseTrace.t) result
 
   val std_vector_reserve : AbstractAddress.t -> t -> t
 

infer/src/pulse/PulseInvalidation.ml

@@ -1,92 +0,0 @@
-(*
- * 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 std_vector_function =
-  | Assign
-  | Clear
-  | Emplace
-  | EmplaceBack
-  | Insert
-  | PushBack
-  | Reserve
-  | ShrinkToFit
-[@@deriving compare]
-
-let pp_std_vector_function f = function
-  | Assign ->
-      F.fprintf f "std::vector::assign"
-  | Clear ->
-      F.fprintf f "std::vector::clear"
-  | Emplace ->
-      F.fprintf f "std::vector::emplace"
-  | EmplaceBack ->
-      F.fprintf f "std::vector::emplace_back"
-  | Insert ->
-      F.fprintf f "std::vector::insert"
-  | PushBack ->
-      F.fprintf f "std::vector::push_back"
-  | Reserve ->
-      F.fprintf f "std::vector::reserve"
-  | ShrinkToFit ->
-      F.fprintf f "std::vector::shrink_to_fit"
-
-
-type t =
-  | CFree of HilExp.AccessExpression.t
-  | CppDelete of HilExp.AccessExpression.t
-  | GoneOutOfScope of Pvar.t * Typ.t
-  | Nullptr
-  | StdVector of std_vector_function * HilExp.AccessExpression.t
-[@@deriving compare]
-
-let issue_type_of_cause = function
-  | CFree _ ->
-      IssueType.use_after_free
-  | CppDelete _ ->
-      IssueType.use_after_delete
-  | GoneOutOfScope _ ->
-      IssueType.use_after_lifetime
-  | Nullptr ->
-      IssueType.null_dereference
-  | StdVector _ ->
-      IssueType.vector_invalidation
-
-
-let describe f = function
-  | CFree access_expr ->
-      F.fprintf f "was invalidated by call to `free()` on `%a`" HilExp.AccessExpression.pp
-        access_expr
-  | CppDelete access_expr ->
-      F.fprintf f "was invalidated by `delete` on `%a`" HilExp.AccessExpression.pp access_expr
-  | GoneOutOfScope (pvar, typ) ->
-      let pp_var f pvar =
-        if Pvar.is_cpp_temporary pvar then
-          F.fprintf f "is the address of a C++ temporary of type `%a`" (Typ.pp_full Pp.text) typ
-        else F.fprintf f "is the address of a stack variable `%a`" Pvar.pp_value pvar
-      in
-      F.fprintf f "%a whose lifetime has ended" pp_var pvar
-  | Nullptr ->
-      F.fprintf f "is the null pointer"
-  | StdVector (std_vector_f, access_expr) ->
-      F.fprintf f "was potentially invalidated by `%a()` on `%a`" pp_std_vector_function
-        std_vector_f HilExp.AccessExpression.pp access_expr
-
-
-let pp f invalidation =
-  match invalidation with
-  | CFree _ ->
-      F.fprintf f "CFree(%a)" describe invalidation
-  | CppDelete _ ->
-      F.fprintf f "CppDelete(%a)" describe invalidation
-  | GoneOutOfScope _ ->
-      describe f invalidation
-  | Nullptr ->
-      describe f invalidation
-  | StdVector _ ->
-      F.fprintf f "StdVector(%a)" describe invalidation

infer/src/pulse/PulseInvalidation.mli

@@ -1,34 +0,0 @@
-(*
- * 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
-
-type std_vector_function =
-  | Assign
-  | Clear
-  | Emplace
-  | EmplaceBack
-  | Insert
-  | PushBack
-  | Reserve
-  | ShrinkToFit
-[@@deriving compare]
-
-val pp_std_vector_function : Format.formatter -> std_vector_function -> unit
-
-type t =
-  | CFree of HilExp.AccessExpression.t
-  | CppDelete of HilExp.AccessExpression.t
-  | GoneOutOfScope of Pvar.t * Typ.t
-  | Nullptr
-  | StdVector of std_vector_function * HilExp.AccessExpression.t
-[@@deriving compare]
-
-val issue_type_of_cause : t -> IssueType.t
-
-val describe : Format.formatter -> t -> unit
-
-val pp : Format.formatter -> t -> unit

infer/src/pulse/PulseModels.ml

@@ -26,7 +26,7 @@ module C = struct
     match actuals with
     | [AccessExpression deleted_access] ->
         PulseOperations.invalidate
-          (PulseTrace.Immediate {imm= PulseInvalidation.CFree deleted_access; location})
+          (PulseTrace.Immediate {imm= PulseDomain.Invalidation.CFree deleted_access; location})
           location deleted_access astate
         >>| List.return
     | _ ->
@@ -41,7 +41,7 @@ module Cplusplus = struct
     match actuals with
     | [AccessExpression deleted_access] ->
         PulseOperations.invalidate
-          (PulseTrace.Immediate {imm= PulseInvalidation.CppDelete deleted_access; location})
+          (PulseTrace.Immediate {imm= PulseDomain.Invalidation.CppDelete deleted_access; location})
           location deleted_access astate
         >>| List.return
     | _ ->
@@ -104,7 +104,7 @@ module StdVector = struct
     let array_address = to_internal_array vector in
     let array = deref_internal_array vector in
     let invalidation =
-      PulseTrace.Immediate {imm= PulseInvalidation.StdVector (vector_f, vector); location}
+      PulseTrace.Immediate {imm= PulseDomain.Invalidation.StdVector (vector_f, vector); location}
     in
     PulseOperations.invalidate_array_elements invalidation location array astate
     >>= PulseOperations.invalidate invalidation location array
@@ -117,7 +117,9 @@ module StdVector = struct
     | AccessExpression vector :: _ ->
         let crumb =
           PulseTrace.Call
-            { f= `Model (Format.asprintf "%a" PulseInvalidation.pp_std_vector_function vector_f)
+            { f=
+                `Model
+                  (Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f)
             ; actuals
             ; location }
         in

infer/src/pulse/PulseOperations.mli

@@ -62,14 +62,14 @@ val write :
   -> t access_result
 
 val invalidate :
-     PulseInvalidation.t PulseTrace.action
+     PulseDomain.Invalidation.t PulseTrace.action
   -> Location.t
   -> HilExp.AccessExpression.t
   -> t
   -> t access_result
 
 val invalidate_array_elements :
-     PulseInvalidation.t PulseTrace.action
+     PulseDomain.Invalidation.t PulseTrace.action
   -> Location.t
   -> HilExp.AccessExpression.t
   -> t