From fd9d963b1cc378faaf3d1cd3da3bcbbfd7d55977 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Wed, 11 Dec 2019 04:40:45 -0800
Subject: [PATCH] [inferbo] generalise `prune_comp` to `prune_binop`

Summary:
This exposes a more general interface to other modules, at the cost of
hiding the fact that it won't deal with all binary operations with equal
precision.

Reviewed By: ezgicicek

Differential Revision: D18908095

fbshipit-source-id: 0c0653bb6
---
 infer/src/bufferoverrun/arrayBlk.ml           |  6 +--
 infer/src/bufferoverrun/arrayBlk.mli          |  5 +--
 .../src/bufferoverrun/bufferOverrunDomain.ml  |  4 +-
 .../bufferoverrun/bufferOverrunSemantics.ml   | 22 +++++------
 infer/src/bufferoverrun/itv.ml                | 37 ++++++++++++++++---
 infer/src/bufferoverrun/itv.mli               |  2 +-
 6 files changed, 51 insertions(+), 25 deletions(-)

diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml
index 215e48990..a5cf834a1 100644
--- a/infer/src/bufferoverrun/arrayBlk.ml
+++ b/infer/src/bufferoverrun/arrayBlk.ml
@@ -189,8 +189,8 @@ module ArrInfo = struct
         arr1
 
 
-  let prune_comp : Binop.t -> t -> t -> t =
-   fun c arr1 arr2 -> prune_offset arr1 arr2 ~f:(Itv.prune_comp c)
+  let prune_binop : Binop.t -> t -> t -> t =
+   fun c arr1 arr2 -> prune_offset arr1 arr2 ~f:(Itv.prune_binop c)
 
 
   let prune_eq : t -> t -> t = fun arr1 arr2 -> prune_offset arr1 arr2 ~f:Itv.prune_eq
@@ -378,7 +378,7 @@ let do_prune : (ArrInfo.t -> ArrInfo.t -> ArrInfo.t) -> t -> t -> t =
       a1
 
 
-let prune_comp : Binop.t -> t -> t -> t = fun c a1 a2 -> do_prune (ArrInfo.prune_comp c) a1 a2
+let prune_binop : Binop.t -> t -> t -> t = fun c a1 a2 -> do_prune (ArrInfo.prune_binop c) a1 a2
 
 let prune_eq : t -> t -> t = fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2
 
diff --git a/infer/src/bufferoverrun/arrayBlk.mli b/infer/src/bufferoverrun/arrayBlk.mli
index 863577baf..d938219c4 100644
--- a/infer/src/bufferoverrun/arrayBlk.mli
+++ b/infer/src/bufferoverrun/arrayBlk.mli
@@ -49,9 +49,8 @@ val lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t ->
 val transform_length : f:(Itv.t -> Itv.t) -> t -> t
 (** Apply [f] to all sizes *)
 
-val prune_comp : Binop.t -> t -> t -> t
-(** [prune_comp comp x y] returns a pruned value of [x] by [comp] and [y]. [comp] should be
-    [Binop.Le], [Ge], [Lt], or [Gt]. *)
+val prune_binop : Binop.t -> t -> t -> t
+(** [prune_binop bop x y] returns a pruned value of [x] by [bop] and [y]. *)
 
 val prune_eq : t -> t -> t
 (** [prune_eq x y] returns a pruned value of [x] by [== y]. *)
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 8b8be2ed4..786488dd1 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -432,8 +432,8 @@ module Val = struct
 
   let prune_length_ge_one : t -> t = lift_prune_length1 Itv.prune_ge_one
 
-  let prune_comp : Binop.t -> t -> t -> t =
-   fun c -> lift_prune2 (Itv.prune_comp c) (ArrayBlk.prune_comp c)
+  let prune_binop : Binop.t -> t -> t -> t =
+   fun c -> lift_prune2 (Itv.prune_binop c) (ArrayBlk.prune_binop c)
 
 
   let is_null : t -> bool =
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 16a1c97da..6c3f8dde9 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -589,27 +589,27 @@ module Prune = struct
   let gen_prune_alias_functions ~prune_alias_core integer_type_widths comp x e astate =
     (* [val_prune_eq] is applied when the alias type is [AliasTarget.Eq]. *)
     let val_prune_eq =
-      match comp with
-      | Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge ->
-          Val.prune_comp comp
-      | Binop.Eq ->
+      match (comp : Binop.t) with
+      | Lt | Gt | Le | Ge ->
+          Val.prune_binop comp
+      | Eq ->
           Val.prune_eq
-      | Binop.Ne ->
+      | Ne ->
           Val.prune_ne
       | _ ->
           assert false
     in
     (* [val_prune_le] is applied when the alias type is [AliasTarget.Le]. *)
     let val_prune_le =
-      match comp with
-      | Binop.Lt ->
+      match (comp : Binop.t) with
+      | Lt ->
           (* when [alias_target <= alias_key < e], prune [alias_target] with [alias_target < e] *)
-          Some (Val.prune_comp comp)
-      | Binop.Le | Binop.Eq ->
+          Some (Val.prune_binop comp)
+      | Le | Eq ->
           (* when [alias_target <= alias_key = e] or [alias_target <= alias_key <= e], prune
              [alias_target] with [alias_target <= e] *)
-          Some (Val.prune_comp Binop.Le)
-      | Binop.Ne | Binop.Gt | Binop.Ge ->
+          Some (Val.prune_binop Le)
+      | Ne | Gt | Ge ->
           (* when [alias_target <= alias_key != e], [alias_target <= alias_key > e] or [alias_target
              <= alias_key >= e], no prune *)
           None
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 843847bcf..5f4eab64b 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -484,13 +484,13 @@ module ItvPure = struct
     else
       let x =
         match c with
-        | Binop.Le ->
+        | Le ->
             prune_le x y
-        | Binop.Ge ->
+        | Ge ->
             prune_ge x y
-        | Binop.Lt ->
+        | Lt ->
             prune_lt x y
-        | Binop.Gt ->
+        | Gt ->
             prune_gt x y
         | _ ->
             assert false
@@ -516,6 +516,33 @@ module ItvPure = struct
 
   let prune_ge_one : t -> t bottom_lifted = fun x -> prune_comp Binop.Ge x one
 
+  let prune_binop : Binop.t -> t -> t -> t bottom_lifted =
+   fun bop x y ->
+    match bop with
+    | Lt | Gt | Le | Ge ->
+        prune_comp bop x y
+    | Eq ->
+        prune_eq x y
+    | Ne ->
+        prune_ne x y
+    | PlusA _
+    | PlusPI
+    | MinusA _
+    | MinusPI
+    | MinusPP
+    | Mult _
+    | Div
+    | Mod
+    | Shiftlt
+    | Shiftrt
+    | BAnd
+    | BXor
+    | BOr
+    | LAnd
+    | LOr ->
+        NonBottom x
+
+
   let get_symbols : t -> SymbolSet.t =
    fun (l, u) -> SymbolSet.union (Bound.get_symbols l) (Bound.get_symbols u)
 
@@ -772,7 +799,7 @@ let prune_ne_zero : t -> t = bind1 ItvPure.prune_ne_zero
 
 let prune_ge_one : t -> t = bind1 ItvPure.prune_ge_one
 
-let prune_comp : Binop.t -> t -> t -> t = fun comp -> bind2 (ItvPure.prune_comp comp)
+let prune_binop : Binop.t -> t -> t -> t = fun comp -> bind2 (ItvPure.prune_binop comp)
 
 let prune_lt : t -> t -> t = lift2 ItvPure.prune_lt
 
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index 9bba1cf70..bf1fd05f7 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -245,7 +245,7 @@ val prune_ne_zero : t -> t
 
 val prune_ge_one : t -> t
 
-val prune_comp : Binop.t -> t -> t -> t
+val prune_binop : Binop.t -> t -> t -> t
 
 val prune_eq : t -> t -> t