Cost: improve NonNegativePolynomial.(<=)

Reviewed By: ezgicicek

Differential Revision: D8531865

fbshipit-source-id: b5c9293

infer/src/bufferoverrun/itv.ml

@@ -156,6 +156,8 @@ module Ints : sig
 
     val one : t
 
+    val of_int : int -> t option
+
     val of_int_exn : int -> t
 
     val is_zero : t -> bool
@@ -196,6 +198,8 @@ end = struct
 
     let is_one = function 1 -> true | _ -> false
 
+    let of_int i = if i < 0 then None else Some i
+
     let of_int_exn i =
       assert (i >= 0) ;
       i
@@ -372,6 +376,13 @@ module SymLinear = struct
 
   let get_symbols : t -> Symbol.t list =
    fun x -> M.fold (fun symbol _coeff acc -> symbol :: acc) x []
+
+
+  (* we can give integer bounds (obviously 0) only when all symbols are unsigned *)
+
+  let int_lb x = if is_ge_zero x then Some 0 else None
+
+  let int_ub x = if is_le_zero x then Some 0 else None
 end
 
 module Bound = struct
@@ -616,6 +627,28 @@ module Bound = struct
         assert false
 
 
+  let int_lb = function
+    | MInf ->
+        None
+    | PInf ->
+        assert false
+    | MinMax _ as b ->
+        int_lb_of_minmax b
+    | Linear (c, se) ->
+        SymLinear.int_lb se |> Option.map ~f:(( + ) c)
+
+
+  let int_ub = function
+    | MInf ->
+        assert false
+    | PInf ->
+        None
+    | MinMax _ as b ->
+        int_ub_of_minmax b
+    | Linear (c, se) ->
+        SymLinear.int_ub se |> Option.map ~f:(( + ) c)
+
+
   let linear_ub_of_minmax = function
     | MinMax (c, Plus, Min, _, x) ->
         Some (Linear (c, SymLinear.singleton_one x))
@@ -970,6 +1003,13 @@ module NonNegativeBound = struct
 
   let of_bound b = if Bound.le b Bound.zero then Bound.zero else b
 
+  let int_lb b =
+    Bound.int_lb b |> Option.bind ~f:NonNegativeInt.of_int
+    |> Option.value ~default:NonNegativeInt.zero
+
+
+  let int_ub b = Bound.int_ub b |> Option.map ~f:NonNegativeInt.of_int_exn
+
   let classify = function
     | Bound.PInf ->
         ValTop
@@ -994,6 +1034,10 @@ end
 module type NonNegativeSymbol = sig
   type t [@@deriving compare]
 
+  val int_lb : t -> NonNegativeInt.t
+
+  val int_ub : t -> NonNegativeInt.t option
+
   val subst : t -> Bound.t bottom_lifted SymbolMap.t -> (NonNegativeInt.t, t) valclass
 
   val pp : F.formatter -> t -> unit
@@ -1141,12 +1185,33 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
       mult_const p1 p2.const |> M.fold (fun s p acc -> plus (mult_symb (mult p p1) s) acc) p2.terms
 
 
+  let rec int_lb {const; terms} =
+    M.fold
+      (fun symbol polynomial acc ->
+        let s_lb = S.int_lb symbol in
+        let p_lb = int_lb polynomial in
+        NonNegativeInt.((s_lb * p_lb) + acc) )
+      terms const
+
+
+  let rec int_ub {const; terms} =
+    M.fold
+      (fun symbol polynomial acc ->
+        Option.bind acc ~f:(fun acc ->
+            Option.bind (S.int_ub symbol) ~f:(fun s_ub ->
+                Option.map (int_ub polynomial) ~f:(fun p_ub -> NonNegativeInt.((s_ub * p_ub) + acc))
+            ) ) )
+      terms (Some const)
+
+
   (* assumes symbols are not comparable *)
   let rec ( <= ) : lhs:t -> rhs:t -> bool =
    fun ~lhs ~rhs ->
     phys_equal lhs rhs
     || NonNegativeInt.( <= ) ~lhs:lhs.const ~rhs:rhs.const
        && M.le ~le_elt:( <= ) lhs.terms rhs.terms
+    || Option.exists (int_ub lhs) ~f:(fun lhs_ub ->
+           NonNegativeInt.( <= ) ~lhs:lhs_ub ~rhs:(int_lb rhs) )
 
 
   let rec xcompare ~lhs ~rhs =

infer/tests/codetoanalyze/c/performance/cost_test.c

@@ -125,4 +125,4 @@ void call_while_upto20_minus100_bad() { while_upto20_bad(-100); }
 
 void call_while_upto20_10_good() { while_upto20_bad(10); }
 
-void call_while_upto20_unsigned_good_FP(unsigned x) { while_upto20_bad(x); }
+void call_while_upto20_unsigned_good(unsigned x) { while_upto20_bad(x); }

infer/tests/codetoanalyze/c/performance/issues.exp

@@ -33,7 +33,6 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13,
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 604]
-codetoanalyze/c/performance/cost_test.c, call_while_upto20_unsigned_good_FP, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * (-u$0 + 20)]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1002]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1002]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004]