[cost] Set the minimum basic cost of node

Summary:
The zero cost of node does not make sense especially when the abstract memory is non-bottom.  This
resulted in unreasonable zero cost results sometimes, e.g. when the checker could not find
appropriate control varaibles having interval values of iteration.  This diff fixes this, so sets
the minimum basic cost as 1, if the abstract memory at the node is non-bottom.

Reviewed By: ezgicicek

Differential Revision: D18199291

fbshipit-source-id: b215d10e5

infer/src/checkers/cost.ml

@@ -84,8 +84,13 @@ module BoundMap = struct
                 | ExcRaised ->
                     BasicCost.one
                 | NonBottom mem ->
-                    BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map)
-                      ~node_id mem
+                    let cost =
+                      BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map)
+                        ~node_id mem
+                    in
+                    (* The zero cost of node does not make sense especially when the abstract memory
+                       is non-bottom.  *)
+                    if BasicCost.is_zero cost then BasicCost.one else cost
               in
               L.(debug Analysis Medium)
                 "@\n>>>Setting bound for node = %a  to %a@\n\n" Node.pp_id node_id BasicCost.pp

infer/tests/codetoanalyze/java/performance/Loops.java

@@ -127,4 +127,21 @@ public class Loops {
       offset += 8;
     } while (i != 0);
   }
+
+  class MyLinkedList {
+    MyLinkedList next;
+
+    MyLinkedList getNext() {
+      return next;
+    }
+  }
+
+  void length_of_linked_list_linear_FP(MyLinkedList p) {
+    int n = 0;
+    while (p != null) {
+      n++;
+      p = p.getNext();
+    }
+    linear(n);
+  }
 }

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

@@ -162,6 +162,8 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 25 ⋅ (length - 1), O(length), degree = 1,{length - 1},Loop at line 44]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length, O(length × length), degree = 2,{length},Loop at line 54,{length - 1},Loop at line 55,{length - 1},Loop at line 54]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `a[*]`,<RHS trace>,Parameter `b[*]`,Binary operation: (a[*] × b[*]):signed64]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.linear(int),Loop at line 86]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 86]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 14 ⋅ FileChannel.read(...).modeled, O(FileChannel.read(...).modeled), degree = 1,{FileChannel.read(...).modeled},Modeled call to read(...)]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 8):signed32]