From a93e05e9fe2913f21e4a9633d8ba4d79fb281564 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Thu, 22 Nov 2018 08:33:48 -0800
Subject: [PATCH] [inferbo] AliasRet: use AbstractDomain.Flat

Reviewed By: skcho

Differential Revision: D13164265

fbshipit-source-id: 66aad24fa
---
 infer/src/absint/AbstractDomain.ml            | 47 ++++++++++++++++
 infer/src/absint/AbstractDomain.mli           | 11 ++++
 .../src/bufferoverrun/bufferOverrunDomain.ml  | 54 ++-----------------
 infer/src/istd/PrettyPrintable.ml             |  8 +++
 infer/src/istd/PrettyPrintable.mli            |  8 +++
 5 files changed, 79 insertions(+), 49 deletions(-)

diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml
index af4269cec..ab4041f02 100644
--- a/infer/src/absint/AbstractDomain.ml
+++ b/infer/src/absint/AbstractDomain.ml
@@ -172,6 +172,53 @@ module Pair (Domain1 : S) (Domain2 : S) = struct
   let pp fmt astate = Pp.pair ~fst:Domain1.pp ~snd:Domain2.pp fmt astate
 end
 
+module Flat (V : PrettyPrintable.PrintableEquatableType) = struct
+  type astate = Bot | V of V.t | Top
+
+  let empty = Bot
+
+  let is_empty = function Bot -> true | _ -> false
+
+  let top = Top
+
+  let ( <= ) ~lhs ~rhs =
+    phys_equal lhs rhs
+    ||
+    match (lhs, rhs) with
+    | Bot, _ | _, Top ->
+        true
+    | Top, _ | _, Bot ->
+        false
+    | V v1, V v2 ->
+        V.equal v1 v2
+
+
+  let join a1 a2 =
+    match (a1, a2) with
+    | Top, _ | _, Top ->
+        Top
+    | Bot, a | a, Bot ->
+        a
+    | V v1, V v2 ->
+        if V.equal v1 v2 then a1 else Top
+
+
+  let widen ~prev ~next ~num_iters:_ = join prev next
+
+  let pp f = function
+    | Bot ->
+        F.pp_print_string f "_|_"
+    | V v ->
+        V.pp f v
+    | Top ->
+        F.pp_print_char f 'T'
+
+
+  let v x = V x
+
+  let get = function V v -> Some v | Bot | Top -> None
+end
+
 module FiniteSetOfPPSet (S : PrettyPrintable.PPSet) = struct
   include S
 
diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli
index 0c9021ac5..b68cc5d38 100644
--- a/infer/src/absint/AbstractDomain.mli
+++ b/infer/src/absint/AbstractDomain.mli
@@ -88,6 +88,17 @@ end
 (** Cartesian product of two domains. *)
 module Pair (Domain1 : S) (Domain2 : S) : S with type astate = Domain1.astate * Domain2.astate
 
+(** Flat abstract domain: Bottom, Top, and non-comparable elements in between *)
+module Flat (V : PrettyPrintable.PrintableEquatableType) : sig
+  include WithBottom
+
+  include WithTop with type astate := astate
+
+  val v : V.t -> astate
+
+  val get : astate -> V.t option
+end
+
 (** Lift a PPSet to a powerset domain ordered by subset. The elements of the set should be drawn from
     a *finite* collection of possible values, since the widening operator here is just union. *)
 module FiniteSetOfPPSet (PPSet : PrettyPrintable.PPSet) : sig
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index ca4b96c20..7e0205084 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -434,56 +434,12 @@ module AliasMap = struct
   let find : Ident.t -> astate -> AliasTarget.astate option = find_opt
 end
 
-module AliasRet = struct
-  type astate = Bot | L of AliasTarget.astate | Top
-
-  let bot = Bot
-
-  let ( <= ) : lhs:astate -> rhs:astate -> bool =
-   fun ~lhs ~rhs ->
-    match (lhs, rhs) with
-    | Bot, _ | _, Top ->
-        true
-    | Top, _ | _, Bot ->
-        false
-    | L loc1, L loc2 ->
-        AliasTarget.equal loc1 loc2
-
-
-  let join : astate -> astate -> astate =
-   fun x y ->
-    match (x, y) with
-    | Top, _ | _, Top ->
-        Top
-    | Bot, a | a, Bot ->
-        a
-    | L loc1, L loc2 ->
-        if AliasTarget.equal loc1 loc2 then x else Top
-
-
-  let widen : prev:astate -> next:astate -> num_iters:int -> astate =
-   fun ~prev ~next ~num_iters:_ -> join prev next
-
-
-  let pp : F.formatter -> astate -> unit =
-   fun fmt x ->
-    match x with
-    | Top ->
-        F.pp_print_char fmt 'T'
-    | L loc ->
-        AliasTarget.pp fmt loc
-    | Bot ->
-        F.pp_print_string fmt "_|_"
-
-
-  let find : astate -> AliasTarget.astate option =
-   fun x -> match x with L loc -> Some loc | _ -> None
-end
+module AliasRet = AbstractDomain.Flat (AliasTarget)
 
 module Alias = struct
   include AbstractDomain.Pair (AliasMap) (AliasRet)
 
-  let bot : astate = (AliasMap.empty, AliasRet.bot)
+  let bot : astate = (AliasMap.empty, AliasRet.empty)
 
   let lift : (AliasMap.astate -> AliasMap.astate) -> astate -> astate =
    fun f a -> (f (fst a), snd a)
@@ -493,7 +449,7 @@ module Alias = struct
 
   let find : Ident.t -> astate -> AliasTarget.astate option = fun x -> lift_v (AliasMap.find x)
 
-  let find_ret : astate -> AliasTarget.astate option = fun x -> AliasRet.find (snd x)
+  let find_ret : astate -> AliasTarget.astate option = fun x -> AliasRet.get (snd x)
 
   let load : Ident.t -> AliasTarget.astate -> astate -> astate =
    fun id loc -> lift (AliasMap.load id loc)
@@ -504,7 +460,7 @@ module Alias = struct
     let a = lift (AliasMap.store loc e) a in
     match e with
     | Exp.Var l when Loc.is_return loc ->
-        let update_ret retl = (fst a, AliasRet.L retl) in
+        let update_ret retl = (fst a, AliasRet.v retl) in
         Option.value_map (find l a) ~default:a ~f:update_ret
     | _ ->
         a
@@ -516,7 +472,7 @@ module Alias = struct
     let locs = Val.get_all_locs formal in
     match PowLoc.is_singleton_or_more locs with
     | IContainer.Singleton loc ->
-        (fst a, AliasRet.L (AliasTarget.of_empty loc))
+        (fst a, AliasRet.v (AliasTarget.of_empty loc))
     | _ ->
         a
 
diff --git a/infer/src/istd/PrettyPrintable.ml b/infer/src/istd/PrettyPrintable.ml
index 5e9532d1c..eeb76ad0b 100644
--- a/infer/src/istd/PrettyPrintable.ml
+++ b/infer/src/istd/PrettyPrintable.ml
@@ -10,6 +10,14 @@ module F = Format
 
 (** Wrappers for making pretty-printable modules *)
 
+module type PrintableEquatableType = sig
+  type t
+
+  val equal : t -> t -> bool
+
+  val pp : F.formatter -> t -> unit
+end
+
 module type PrintableOrderedType = sig
   include Caml.Set.OrderedType
 
diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli
index a2e8523e0..a021794e5 100644
--- a/infer/src/istd/PrettyPrintable.mli
+++ b/infer/src/istd/PrettyPrintable.mli
@@ -12,6 +12,14 @@ module F = Format
 
 val pp_collection : pp_item:(F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
 
+module type PrintableEquatableType = sig
+  type t
+
+  val equal : t -> t -> bool
+
+  val pp : F.formatter -> t -> unit
+end
+
 module type PrintableOrderedType = sig
   include Caml.Set.OrderedType