[ai] No need to create a domain for a bottom_lifted type

Summary: Makes `type 'astate bottom_lifted` accessible without invoking `BottomLifted`

Reviewed By: jvillard, sblackshear

Differential Revision: D5920660

fbshipit-source-id: 40fca97

infer/src/absint/AbstractDomain.ml

@@ -10,6 +10,14 @@
 open! IStd
 module F = Format
 
+module Types = struct
+  type 'astate bottom_lifted = Bottom | NonBottom of 'astate
+
+  type 'astate top_lifted = Top | NonTop of 'astate
+end
+
+open! Types
+
 module type S = sig
   type astate
 
@@ -39,7 +47,7 @@ module type WithTop = sig
 end
 
 module BottomLifted (Domain : S) = struct
-  type astate = Bottom | NonBottom of Domain.astate
+  type astate = Domain.astate bottom_lifted
 
   let empty = Bottom
 
@@ -82,7 +90,7 @@ module BottomLifted (Domain : S) = struct
 end
 
 module TopLifted (Domain : S) = struct
-  type astate = Top | NonTop of Domain.astate
+  type astate = Domain.astate top_lifted
 
   let top = Top
 

infer/src/absint/AbstractDomain.mli

@@ -10,6 +10,14 @@
 open! IStd
 module F = Format
 
+module Types : sig
+  type 'astate bottom_lifted = Bottom | NonBottom of 'astate
+
+  type 'astate top_lifted = Top | NonTop of 'astate
+end
+
+open! Types
+
 (** Abstract domains and domain combinators *)
 
 module type S = sig
@@ -47,14 +55,14 @@ end
 
 (** Lift a pre-domain to a domain *)
 module BottomLifted (Domain : S) : sig
-  type astate = Bottom | NonBottom of Domain.astate
+  type astate = Domain.astate bottom_lifted
 
   include WithBottom with type astate := astate
 end
 
 (** Create a domain with Top element from a pre-domain *)
 module TopLifted (Domain : S) : sig
-  type astate = Top | NonTop of Domain.astate
+  type astate = Domain.astate top_lifted
 
   include WithTop with type astate := astate
 end

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -12,6 +12,7 @@
 
 open! IStd
 open AbsLoc
+open! AbstractDomain.Types
 module F = Format
 module L = Logging
 module Dom = BufferOverrunDomain
@@ -134,7 +135,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | "__inferbo_min"
        -> model_min ret params loc mem
       | "__exit" | "exit"
-       -> Dom.Mem.Bottom
+       -> Bottom
       | "fgetc"
        -> model_by_value Dom.Val.Itv.m1_255 ret mem
       | "infer_print"

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -12,6 +12,7 @@
 
 open! IStd
 open AbsLoc
+open! AbstractDomain.Types
 module F = Format
 module L = Logging
 module MF = MarkupFormatter

infer/src/bufferoverrun/itv.ml

@@ -11,6 +11,7 @@
  *)
 
 open! IStd
+open! AbstractDomain.Types
 module F = Format
 module L = Logging
 

infer/src/checkers/Siof.ml

@@ -8,6 +8,7 @@
  *)
 
 open! IStd
+open! AbstractDomain.Types
 module F = Format
 module L = Logging
 module GlobalsAccesses = SiofTrace.GlobalsAccesses
@@ -63,7 +64,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let is_compile_time_constructed pdesc pv =
     let init_pname = Pvar.get_initializer_pname pv in
     match Option.bind init_pname ~f:(Summary.read_summary pdesc) with
-    | Some (Domain.BottomSiofTrace.Bottom, _)
+    | Some (Bottom, _)
      -> (* we analyzed the initializer for this global and found that it doesn't require any runtime
            initialization so cannot participate in SIOF *)
         true
@@ -94,13 +95,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let add_globals astate outer_loc globals =
     if GlobalsAccesses.is_empty globals then astate
     else
-      let trace =
+      let trace = match fst astate with Bottom -> SiofTrace.empty | NonBottom t -> t in
-        match fst astate with
-        | Domain.BottomSiofTrace.Bottom
-         -> SiofTrace.empty
-        | Domain.BottomSiofTrace.NonBottom t
-         -> t
-      in
       (* filter out variables that are known to be already initialized *)
       let non_init_globals =
         let initialized = snd astate in
@@ -109,15 +104,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       let globals_trace =
         SiofTrace.add_sink (SiofTrace.make_access non_init_globals outer_loc) trace
       in
-      (Domain.BottomSiofTrace.NonBottom globals_trace, snd astate)
+      (NonBottom globals_trace, snd astate)
 
   let add_params_globals astate pdesc call_loc params =
     List.map ~f:(fun (e, _) -> get_globals pdesc call_loc e) params
     |> List.fold ~f:GlobalsAccesses.union ~init:GlobalsAccesses.empty
     |> add_globals astate (Procdesc.get_loc pdesc)
 
-  let at_least_nonbottom =
+  let at_least_nonbottom = Domain.join (NonBottom SiofTrace.empty, Domain.VarNames.empty)
-    Domain.join (Domain.BottomSiofTrace.NonBottom SiofTrace.empty, Domain.VarNames.empty)
 
   let exec_instr astate {ProcData.pdesc} _ (instr: Sil.instr) =
     match instr with
@@ -135,8 +129,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               then Some initialized_globals
               else None )
         in
-        Domain.join astate
+        Domain.join astate (NonBottom SiofTrace.empty, Domain.VarNames.of_list init)
-          (Domain.BottomSiofTrace.NonBottom SiofTrace.empty, Domain.VarNames.of_list init)
     | Call (_, Const Cfun callee_pname, _ :: params_without_self, loc, _)
       when Typ.Procname.is_c_method callee_pname && Typ.Procname.is_constructor callee_pname
            && Typ.Procname.is_constexpr callee_pname
@@ -145,7 +138,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
      -> let callsite = CallSite.make callee_pname loc in
         let callee_astate =
           match Summary.read_summary pdesc callee_pname with
-          | Some (Domain.BottomSiofTrace.NonBottom trace, initialized_globals)
+          | Some (NonBottom trace, initialized_globals)
            -> let trace_without_initialized_globals =
                 let sinks_with_non_init_globals =
                   SiofTrace.Sinks.filter
@@ -156,13 +149,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                 in
                 SiofTrace.update_sinks trace sinks_with_non_init_globals
               in
-              ( Domain.BottomSiofTrace.NonBottom
+              ( NonBottom (SiofTrace.with_callsite trace_without_initialized_globals callsite)
-                  (SiofTrace.with_callsite trace_without_initialized_globals callsite)
               , initialized_globals )
-          | Some (Domain.BottomSiofTrace.Bottom, _ as astate)
+          | Some (Bottom, _ as astate)
            -> astate
           | None
-           -> (Domain.BottomSiofTrace.Bottom, Domain.VarNames.empty)
+           -> (Bottom, Domain.VarNames.empty)
         in
         add_params_globals astate pdesc loc params |> Domain.join callee_astate
         |> (* make sure it's not Bottom: we made a function call so this needs initialization *)
@@ -193,7 +185,7 @@ let report_siof summary trace pdesc gname loc =
   in
   let trace_of_pname pname =
     match Summary.read_summary pdesc pname with
-    | Some (SiofDomain.BottomSiofTrace.NonBottom summary, _)
+    | Some (NonBottom summary, _)
      -> summary
     | _
      -> SiofTrace.empty
@@ -233,7 +225,7 @@ let report_siof summary trace pdesc gname loc =
 
 let siof_check pdesc gname (summary: Specs.summary) =
   match summary.payload.siof with
-  | Some (SiofDomain.BottomSiofTrace.NonBottom post, _)
+  | Some (NonBottom post, _)
    -> let attrs = Procdesc.get_attributes pdesc in
       let all_globals =
         SiofTrace.Sinks.fold
@@ -246,12 +238,12 @@ let siof_check pdesc gname (summary: Specs.summary) =
       in
       if GlobalsAccesses.exists (is_foreign tu_opt) all_globals then
         report_siof summary post pdesc gname attrs.ProcAttributes.loc
-  | Some (SiofDomain.BottomSiofTrace.Bottom, _) | None
+  | Some (Bottom, _) | None
    -> ()
 
 let checker {Callbacks.proc_desc; tenv; summary} : Specs.summary =
   let proc_data = ProcData.make_default proc_desc tenv in
-  let initial = (SiofDomain.BottomSiofTrace.Bottom, SiofDomain.VarNames.empty) in
+  let initial = (Bottom, SiofDomain.VarNames.empty) in
   let updated_summary =
     match Analyzer.compute_post proc_data ~initial with
     | Some post

infer/src/checkers/SiofDomain.ml

@@ -8,6 +8,7 @@
  *)
 
 open! IStd
+open! AbstractDomain.Types
 module VarNames = AbstractDomain.FiniteSet (String)
 module BottomSiofTrace = AbstractDomain.BottomLifted (SiofTrace)
 include AbstractDomain.Pair (BottomSiofTrace) (VarNames)
@@ -15,9 +16,9 @@ include AbstractDomain.Pair (BottomSiofTrace) (VarNames)
 (** group together procedure-local accesses *)
 let normalize (trace, initialized as astate) =
   match trace with
-  | BottomSiofTrace.Bottom
+  | Bottom
    -> astate
-  | BottomSiofTrace.NonBottom trace
+  | NonBottom trace
    -> let elems = SiofTrace.Sinks.elements (SiofTrace.sinks trace) in
       let direct, indirect = List.partition_tf ~f:SiofTrace.is_intraprocedural_access elems in
       match direct with
@@ -35,4 +36,4 @@ let normalize (trace, initialized as astate) =
             SiofTrace.make_access kind loc :: indirect |> SiofTrace.Sinks.of_list
             |> SiofTrace.update_sinks trace
           in
-          (BottomSiofTrace.NonBottom trace', initialized)
+          (NonBottom trace', initialized)

infer/src/checkers/annotationReachability.ml

@@ -8,6 +8,7 @@
  *)
 
 open! IStd
+open! AbstractDomain.Types
 module F = Format
 module L = Logging
 module MF = MarkupFormatter
@@ -21,9 +22,9 @@ module Domain = struct
 
   let add_call_site annot sink call_site (annot_map, previous_vstate as astate) =
     match previous_vstate with
-    | TrackingDomain.Bottom
+    | Bottom
      -> astate
-    | TrackingDomain.NonBottom _
+    | NonBottom _
      -> let sink_map =
           try AnnotReachabilityDomain.find annot annot_map
           with Not_found -> AnnotReachabilityDomain.SinkMap.empty
@@ -37,28 +38,24 @@ module Domain = struct
         if phys_equal sink_map' sink_map then astate
         else (AnnotReachabilityDomain.add annot sink_map' annot_map, previous_vstate)
 
-  let stop_tracking ((annot_map, _): astate) = (annot_map, TrackingDomain.Bottom)
+  let stop_tracking ((annot_map, _): astate) = (annot_map, Bottom)
 
   let add_tracking_var var (annot_map, previous_vstate as astate) =
     match previous_vstate with
-    | TrackingDomain.Bottom
+    | Bottom
      -> astate
-    | TrackingDomain.NonBottom vars
+    | NonBottom vars
-     -> (annot_map, TrackingDomain.NonBottom (TrackingVar.add var vars))
+     -> (annot_map, NonBottom (TrackingVar.add var vars))
 
   let remove_tracking_var var (annot_map, previous_vstate as astate) =
     match previous_vstate with
-    | TrackingDomain.Bottom
+    | Bottom
      -> astate
-    | TrackingDomain.NonBottom vars
+    | NonBottom vars
-     -> (annot_map, TrackingDomain.NonBottom (TrackingVar.remove var vars))
+     -> (annot_map, NonBottom (TrackingVar.remove var vars))
 
   let is_tracked_var var (_, vstate) =
-    match vstate with
+    match vstate with Bottom -> false | NonBottom vars -> TrackingVar.mem var vars
-    | TrackingDomain.Bottom
-     -> false
-    | TrackingDomain.NonBottom vars
-     -> TrackingVar.mem var vars
 end
 
 module Summary = Summary.Make (struct
@@ -434,9 +431,7 @@ end
 module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions)
 
 let checker ({Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary =
-  let initial =
+  let initial = (AnnotReachabilityDomain.empty, NonBottom Domain.TrackingVar.empty) in
-    (AnnotReachabilityDomain.empty, Domain.TrackingDomain.NonBottom Domain.TrackingVar.empty)
-  in
   let proc_data = ProcData.make_default proc_desc tenv in
   match Analyzer.compute_post proc_data ~initial with
   | Some (annot_map, _)