Cost: fix min

Summary: We were wrongly using the underapproximation of `min` rather than the overapproximation

Reviewed By: ddino

Differential Revision: D7844267

fbshipit-source-id: c9d9247

infer/src/bufferoverrun/itv.ml

@@ -622,8 +622,8 @@ module Bound = struct
         x
 
 
-  let rec lb : ?default:t -> t -> t -> t =
+  let rec lb : default:t -> t -> t -> t =
-   fun ?(default= MInf) x y ->
+   fun ~default x y ->
     if le x y then x
     else if le y x then y
     else
@@ -668,6 +668,17 @@ module Bound = struct
           default
 
 
+  (** underapproximation of min b1 b2 *)
+  let min_l b1 b2 = lb ~default:MInf b1 b2
+
+  (** overapproximation of min b1 b2 *)
+  let min_u b1 b2 =
+    lb
+      ~default:
+        (* When the result is not representable, our best effort is to return the first argument. Any other deterministic heuristics would work too. *)
+        b1 b1 b2
+
+
   let ub : ?default:t -> t -> t -> t =
    fun ?(default= PInf) x y ->
     if le x y then y
@@ -688,8 +699,6 @@ module Bound = struct
 
   let join : t -> t -> t = ub ~default:PInf
 
-  let min : t -> t -> t = lb ~default:MInf
-
   let widen_l : t -> t -> t =
    fun x y ->
     match (x, y) with
@@ -896,8 +905,8 @@ module ItvPure = struct
   let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false
 
   let subst : t -> Bound.t bottom_lifted SymbolMap.t -> t bottom_lifted =
-   fun x map ->
+   fun (l, u) map ->
-    match (Bound.subst_lb (lb x) map, Bound.subst_ub (ub x) map) with
+    match (Bound.subst_lb l map, Bound.subst_ub u map) with
     | NonBottom l, NonBottom u ->
         NonBottom (l, u)
     | _ ->
@@ -938,7 +947,7 @@ module ItvPure = struct
         `RightSubsumesLeft
 
 
-  let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.ub u1 u2)
+  let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb ~default:MInf l1 l2, Bound.ub u1 u2)
 
   let widen : prev:t -> next:t -> num_iters:int -> t =
    fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> (Bound.widen_l l1 l2, Bound.widen_u u1 u2)
@@ -1151,7 +1160,7 @@ module ItvPure = struct
     else Boolean.Top
 
 
-  let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2)
+  let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.min_l l1 l2, Bound.min_u u1 u2)
 
   let is_invalid : t -> bool = function
     | Bound.PInf, _ | _, Bound.MInf ->

infer/src/bufferoverrun/itv.mli

@@ -70,7 +70,7 @@ module Bound : sig
 
   val join : t -> t -> t
 
-  val min : t -> t -> t
+  val min_u : t -> t -> t
 
   val mult : t -> t -> t
 

infer/src/checkers/cost.ml

@@ -338,7 +338,7 @@ return the addends of the sum x_j1+x_j2+..+x_j_n*)
     | Leaf (_, c) ->
         c
     | Min l ->
-        evaluate_operator Itv.Bound.min l
+        evaluate_operator Itv.Bound.min_u l
     | Plus l ->
         evaluate_operator Itv.Bound.plus_u l
 

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

@@ -81,7 +81,7 @@ int loop1_bad() {
   return 0;
 }
 
-int FN_loop2(int k) {
+int loop2_bad(int k) {
 
   for (int i = 0; i < k; i++) {
     alias2_OK();
@@ -89,8 +89,7 @@ int FN_loop2(int k) {
   return 0;
 }
 
-// This is currently evaluated to Top as the analysis is not powerful enough
+int loop3_bad(int k) {
-int FN_loop3(int k) {
 
   for (int i = k; i < k + 15; i++) {
     alias2_OK();

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

@@ -1,13 +1,16 @@
-codetoanalyze/c/performance/cost_test.c, FN_loop2, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
-codetoanalyze/c/performance/cost_test.c, FN_loop2, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3]
-codetoanalyze/c/performance/cost_test.c, FN_loop2, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3]
-codetoanalyze/c/performance/cost_test.c, FN_loop3, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1004]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1104]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1104]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1106]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-1)xs$0 + s$1 + 16]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-13)xs$0 + 13xs$1 + 199]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-13)xs$0 + 13xs$1 + 199]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-15)xs$0 + 15xs$1 + 231]
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 211]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 12, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 201]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1204]