[cost] Simplify range of min(1,x)

Summary: When a positive bound is expected, min(1,x) can be simplified to 1.

Reviewed By: ezgicicek

Differential Revision: D17091884

fbshipit-source-id: 3a89a44fa

infer/src/bufferoverrun/bounds.ml

@@ -1052,6 +1052,15 @@ module Bound = struct
 
   let subst_ub x eval_sym = subst ~subst_pos:Symb.BoundEnd.UpperBound x eval_sym
 
+  (* When a positive bound is expected, min(1,x) can be simplified to 1. *)
+  let simplify_min_one b =
+    match b with
+    | MinMax (c, Plus, Min, d, _x) when Z.(equal c zero) && Z.(equal d one) ->
+        Linear (d, SymLinear.zero)
+    | _ ->
+        b
+
+
   let simplify_bound_ends_from_paths x =
     match x with
     | MInf | PInf | MinMax _ ->

infer/src/bufferoverrun/bounds.mli

@@ -112,6 +112,8 @@ module Bound : sig
 
   val simplify_bound_ends_from_paths : t -> t
 
+  val simplify_min_one : t -> t
+
   val is_same_symbol : t -> t -> Symb.SymbolPath.t option
 
   val exists_str : f:(string -> bool) -> t -> bool

infer/src/bufferoverrun/itv.ml

@@ -24,7 +24,7 @@ module ItvRange = struct
    fun ~loop_head_loc ~lb ~ub ->
     Bound.plus_u ub Bound.one
     |> Bound.plus_u (Bound.neg lb)
-    |> Bound.simplify_bound_ends_from_paths
+    |> Bound.simplify_min_one |> Bound.simplify_bound_ends_from_paths
     |> Bounds.NonNegativeBound.of_loop_bound loop_head_loc