[cost] Ignore boundends when getting range

Summary: This diff ignores boundends when getting the value range.

Reviewed By: ezgicicek

Differential Revision: D17114363

fbshipit-source-id: cca8745e3

infer/src/bufferoverrun/bounds.ml

@@ -150,16 +150,22 @@ module SymLinear = struct
    fun x -> match get_mone_symbol_opt x with Some _ -> true | None -> false
 
 
-  let is_one_symbol_of : Symb.Symbol.t -> t -> bool =
+  let is_one_symbol_of_common get_symbol_opt ?(weak = false) s x =
-   fun s x -> Option.exists (get_one_symbol_opt x) ~f:(fun s' -> Symb.Symbol.equal s s')
+    Option.exists (get_symbol_opt x) ~f:(fun s' ->
+        (if weak then Symb.Symbol.paths_equal else Symb.Symbol.equal) s s' )
 
 
-  let is_mone_symbol_of : Symb.Symbol.t -> t -> bool =
+  let is_one_symbol_of : ?weak:bool -> Symb.Symbol.t -> t -> bool =
-   fun s x -> Option.exists (get_mone_symbol_opt x) ~f:(fun s' -> Symb.Symbol.equal s s')
+    is_one_symbol_of_common get_one_symbol_opt
 
 
-  let is_signed_one_symbol_of : Sign.t -> Symb.Symbol.t -> t -> bool =
+  let is_mone_symbol_of : ?weak:bool -> Symb.Symbol.t -> t -> bool =
-   fun sign s x -> match sign with Plus -> is_one_symbol_of s x | Minus -> is_mone_symbol_of s x
+    is_one_symbol_of_common get_mone_symbol_opt
+
+
+  let is_signed_one_symbol_of : weak:bool -> Sign.t -> Symb.Symbol.t -> t -> bool =
+   fun ~weak sign s x ->
+    match sign with Plus -> is_one_symbol_of ~weak s x | Minus -> is_mone_symbol_of ~weak s x
 
 
   let get_symbols : t -> Symb.SymbolSet.t =
@@ -797,8 +803,8 @@ module Bound = struct
    fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None
 
 
-  let plus_exact : otherwise:(t -> t -> t) -> t -> t -> t =
+  let plus_exact : weak:bool -> otherwise:(t -> t -> t) -> t -> t -> t =
-   fun ~otherwise x y ->
+   fun ~weak ~otherwise x y ->
     if is_zero x then y
     else if is_zero y then x
     else
@@ -811,14 +817,14 @@ module Bound = struct
           mk_MinMax (Z.(c1 + c2), sign, min_max, d1, x1)
       | MinMax (c1, sign, min_max, d, x1), Linear (c2, x2)
       | Linear (c2, x2), MinMax (c1, sign, min_max, d, x1)
-        when SymLinear.is_signed_one_symbol_of (Sign.neg sign) x1 x2 ->
+        when SymLinear.is_signed_one_symbol_of ~weak (Sign.neg sign) x1 x2 ->
           let c = Sign.eval_big_int sign Z.(c1 + c2) d in
           mk_MinMax (c, Sign.neg sign, MinMax.neg min_max, d, x1)
       | _ ->
           otherwise x y
 
 
-  let plus_l : t -> t -> t =
+  let plus_l : weak:bool -> t -> t -> t =
     plus_exact ~otherwise:(fun x y ->
         match (x, y) with
         | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2)
@@ -831,7 +837,7 @@ module Bound = struct
             MInf )
 
 
-  let plus_u : t -> t -> t =
+  let plus_u : weak:bool -> t -> t -> t =
     plus_exact ~otherwise:(fun x y ->
         match (x, y) with
         | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2)
@@ -844,7 +850,12 @@ module Bound = struct
             PInf )
 
 
-  let plus = function Symb.BoundEnd.LowerBound -> plus_l | Symb.BoundEnd.UpperBound -> plus_u
+  let plus = function
+    | Symb.BoundEnd.LowerBound ->
+        plus_l ~weak:false
+    | Symb.BoundEnd.UpperBound ->
+        plus_u ~weak:false
+
 
   let mult_const : Symb.BoundEnd.t -> NonZeroInt.t -> t -> t =
    fun bound_end n x ->

infer/src/bufferoverrun/bounds.mli

@@ -86,9 +86,9 @@ module Bound : sig
 
   val is_const : t -> Z.t sexp_option
 
-  val plus_l : t -> t -> t
+  val plus_l : weak:bool -> t -> t -> t
 
-  val plus_u : t -> t -> t
+  val plus_u : weak:bool -> t -> t -> t
 
   val mult_const_l : Ints.NonZeroInt.t -> t -> t
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -458,7 +458,7 @@ let mk_eval_sym_trace integer_type_widths callee_formals actual_exps caller_mem
   let eval_sym ~mode s bound_end =
     let sympath = Symb.Symbol.path s in
     let itv, _ = eval_sympath ~mode params sympath caller_mem in
-    Symb.Symbol.assert_bound_end s bound_end ;
+    Symb.Symbol.check_bound_end s bound_end ;
     Itv.get_bound itv bound_end
   in
   let trace_of_sym s =

infer/src/bufferoverrun/itv.ml

@@ -22,8 +22,8 @@ module ItvRange = struct
 
   let of_bounds : loop_head_loc:Location.t -> lb:Bound.t -> ub:Bound.t -> t =
    fun ~loop_head_loc ~lb ~ub ->
-    Bound.plus_u ub Bound.one
+    Bound.plus_u ~weak:true ub Bound.one
-    |> Bound.plus_u (Bound.neg lb)
+    |> Bound.plus_u ~weak:true (Bound.neg lb)
     |> Bound.simplify_min_one |> Bound.simplify_bound_ends_from_paths
     |> Bounds.NonNegativeBound.of_loop_bound loop_head_loc
 
@@ -193,7 +193,9 @@ module ItvPure = struct
 
   let lnot : t -> Boolean.t = fun x -> to_bool x |> Boolean.not_
 
-  let plus : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.plus_l l1 l2, Bound.plus_u u1 u2)
+  let plus : t -> t -> t =
+   fun (l1, u1) (l2, u2) -> (Bound.plus_l ~weak:false l1 l2, Bound.plus_u ~weak:false u1 u2)
+
 
   let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2)
 

infer/src/bufferoverrun/symb.ml

@@ -322,8 +322,17 @@ module Symbol = struct
 
   let path = function OneValue {path} | BoundEnd {path} -> path
 
-  let assert_bound_end s be =
+  (* NOTE: This may not be satisfied in the cost checker for simplifying its results. *)
-    match s with OneValue _ -> () | BoundEnd {bound_end} -> assert (BoundEnd.equal be bound_end)
+  let check_bound_end s be =
+    if Config.bo_debug >= 3 then
+      match s with
+      | OneValue _ ->
+          ()
+      | BoundEnd {bound_end} ->
+          if not (BoundEnd.equal be bound_end) then
+            L.d_printfln_escaped
+              "Mismatch of symbol's boundend and its position: %a is in a place for %s." pp s
+              (BoundEnd.to_string be)
 
 
   let exists_str ~f = function OneValue {path} | BoundEnd {path} -> SymbolPath.exists_str ~f path

infer/src/bufferoverrun/symb.mli

@@ -110,7 +110,7 @@ module Symbol : sig
 
   val path : t -> SymbolPath.t
 
-  val assert_bound_end : t -> BoundEnd.t -> unit
+  val check_bound_end : t -> BoundEnd.t -> unit
 
   type make_t = unsigned:bool -> ?boolean:bool -> SymbolPath.t -> t