From 7c0059174768c86e8268575758fc0da1661cd754 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Fri, 16 Nov 2018 08:18:31 -0800
Subject: [PATCH] [inferbo] Type name for eval_sym

Reviewed By: skcho

Differential Revision: D13071774

fbshipit-source-id: 1dc412646
---
 infer/src/bufferoverrun/arrayBlk.ml                  |  4 ++--
 infer/src/bufferoverrun/bounds.ml                    |  5 +++--
 infer/src/bufferoverrun/bounds.mli                   | 12 ++++--------
 infer/src/bufferoverrun/bufferOverrunDomain.ml       |  6 +-----
 .../bufferoverrun/bufferOverrunProofObligations.ml   |  7 +------
 .../bufferoverrun/bufferOverrunProofObligations.mli  |  2 +-
 infer/src/bufferoverrun/itv.ml                       |  6 +++---
 infer/src/bufferoverrun/itv.mli                      |  6 +++---
 infer/src/bufferoverrun/symb.ml                      |  2 ++
 infer/src/bufferoverrun/symb.mli                     |  2 ++
 10 files changed, 22 insertions(+), 30 deletions(-)

diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml
index 16d4402c6..f25c8c8ce 100644
--- a/infer/src/bufferoverrun/arrayBlk.ml
+++ b/infer/src/bufferoverrun/arrayBlk.ml
@@ -56,7 +56,7 @@ module ArrInfo = struct
 
   let diff : t -> t -> Itv.astate = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset
 
-  let subst : t -> (Symb.Symbol.t -> Bounds.Bound.t bottom_lifted) -> t =
+  let subst : t -> Bound.eval_sym -> t =
    fun arr eval_sym ->
     {arr with offset= Itv.subst arr.offset eval_sym; size= Itv.subst arr.size eval_sym}
 
@@ -141,7 +141,7 @@ let get_pow_loc : astate -> PowLoc.t =
   fold pow_loc_of_allocsite array PowLoc.bot
 
 
-let subst : astate -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> astate =
+let subst : astate -> Bound.eval_sym -> astate =
  fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a
 
 
diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 78a1c7cb8..1f248cc78 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -229,6 +229,8 @@ module Bound = struct
     | PInf
   [@@deriving compare]
 
+  type eval_sym = t Symb.Symbol.eval
+
   let equal = [%compare.equal: t]
 
   let pp : F.formatter -> t -> unit =
@@ -812,8 +814,7 @@ module Bound = struct
 
 
   (** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as possible according to [subst_pos]. *)
-  let subst :
-      subst_pos:Symb.BoundEnd.t -> t -> (Symb.Symbol.t -> t bottom_lifted) -> t bottom_lifted =
+  let subst : subst_pos:Symb.BoundEnd.t -> t -> eval_sym -> t bottom_lifted =
    fun ~subst_pos x eval_sym ->
     let get s =
       match eval_sym s with
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index 610973af3..ce0c137d6 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/infer/src/bufferoverrun/bounds.mli
@@ -35,6 +35,8 @@ module Bound : sig
     | MinMax of Z.t * sign * min_max * Z.t * Symb.Symbol.t
     | PInf
 
+  type eval_sym = t Symb.Symbol.eval
+
   val compare : t -> t -> int
 
   val equal : t -> t -> bool
@@ -109,15 +111,9 @@ module Bound : sig
 
   val is_not_infty : t -> bool
 
-  val subst_lb :
-       t
-    -> (Symb.Symbol.t -> t AbstractDomain.Types.bottom_lifted)
-    -> t AbstractDomain.Types.bottom_lifted
+  val subst_lb : t -> eval_sym -> t AbstractDomain.Types.bottom_lifted
 
-  val subst_ub :
-       t
-    -> (Symb.Symbol.t -> t AbstractDomain.Types.bottom_lifted)
-    -> t AbstractDomain.Types.bottom_lifted
+  val subst_ub : t -> eval_sym -> t AbstractDomain.Types.bottom_lifted
 
   val simplify_bound_ends_from_paths : t -> t
 
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 4b63ade58..dc0478d55 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -295,11 +295,7 @@ module Val = struct
    fun x -> {x with itv= Itv.normalize x.itv; arrayblk= ArrayBlk.normalize x.arrayblk}
 
 
-  let subst :
-         t
-      -> (Symb.Symbol.t -> Bounds.Bound.t bottom_lifted) * (Symb.Symbol.t -> TraceSet.t)
-      -> Location.t
-      -> t =
+  let subst : t -> Bounds.Bound.eval_sym * (Symb.Symbol.t -> TraceSet.t) -> Location.t -> t =
    fun x (eval_sym, trace_of_sym) location ->
     let symbols = get_symbols x in
     let traces_caller =
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index 70ede1850..10e7f4d56 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -289,12 +289,7 @@ module ArrayAccessCondition = struct
       {report_issue_type; propagate= is_symbolic}
 
 
-  let subst :
-         (Symb.Symbol.t -> Bound.t bottom_lifted)
-      -> Relation.SubstMap.t
-      -> Relation.astate
-      -> t
-      -> t option =
+  let subst : Bound.eval_sym -> Relation.SubstMap.t -> Relation.astate -> t -> t option =
    fun eval_sym rel_map caller_relation c ->
     match
       (ItvPure.subst c.offset eval_sym, ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym)
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli
index bccc99529..9c9812b0b 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli
@@ -63,7 +63,7 @@ module ConditionSet : sig
 
   val subst :
        summary_t
-    -> (Symb.Symbol.t -> Bounds.Bound.t bottom_lifted) * (Symb.Symbol.t -> ValTraceSet.t)
+    -> Bounds.Bound.eval_sym * (Symb.Symbol.t -> ValTraceSet.t)
     -> Relation.SubstMap.t
     -> Relation.astate
     -> Typ.Procname.t
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index b4120bd11..c0fe16217 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -79,7 +79,7 @@ module type NonNegativeSymbol = sig
 
   val int_ub : t -> NonNegativeInt.t option
 
-  val subst : t -> (Symb.Symbol.t -> t bottom_lifted) -> (NonNegativeInt.t, t) Bounds.valclass
+  val subst : t -> t Symb.Symbol.eval -> (NonNegativeInt.t, t) Bounds.valclass
 
   val pp : F.formatter -> t -> unit
 end
@@ -780,7 +780,7 @@ module ItvPure = struct
 
   let normalize : t -> t bottom_lifted = fun x -> if is_invalid x then Bottom else NonBottom x
 
-  let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted =
+  let subst : t -> Bound.eval_sym -> t bottom_lifted =
    fun (l, u) eval_sym ->
     match (Bound.subst_lb l eval_sym, Bound.subst_ub u eval_sym) with
     | NonBottom l, NonBottom u ->
@@ -1025,7 +1025,7 @@ let prune_eq : t -> t -> t = bind2 ItvPure.prune_eq
 
 let prune_ne : t -> t -> t = bind2 ItvPure.prune_ne
 
-let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t =
+let subst : t -> Bound.eval_sym -> t =
  fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x
 
 
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index 5018894d5..5f8e30b39 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -50,7 +50,7 @@ module NonNegativePolynomial : sig
 
   val min_default_left : astate -> astate -> astate
 
-  val subst : astate -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> astate
+  val subst : astate -> Bound.eval_sym -> astate
 
   val degree : astate -> int option
 
@@ -138,7 +138,7 @@ module ItvPure : sig
 
   val get_symbols : t -> SymbolSet.t
 
-  val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted
+  val subst : t -> Bound.eval_sym -> t bottom_lifted
 
   val neg : t -> t
 
@@ -253,4 +253,4 @@ val prune_eq : t -> t -> t
 
 val prune_ne : t -> t -> t
 
-val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t
+val subst : t -> Bound.eval_sym -> t
diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml
index 915accd5a..ca061abc7 100644
--- a/infer/src/bufferoverrun/symb.ml
+++ b/infer/src/bufferoverrun/symb.ml
@@ -57,6 +57,8 @@ module Symbol = struct
   type t =
     {id: int; pname: Typ.Procname.t; unsigned: bool; path: SymbolPath.t; bound_end: BoundEnd.t}
 
+  type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
+
   let compare s1 s2 =
     (* Symbols only make sense within a given function, so shouldn't be compared across function boundaries. *)
     assert (phys_equal s1.pname s2.pname) ;
diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli
index c9ccbad3d..745e58821 100644
--- a/infer/src/bufferoverrun/symb.mli
+++ b/infer/src/bufferoverrun/symb.mli
@@ -38,6 +38,8 @@ end
 module Symbol : sig
   type t
 
+  type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
+
   val compare : t -> t -> int
 
   val is_unsigned : t -> bool