[cost] Revise CostDomain.plus functionality: zero+unreachable

Summary:
We defined cost's plus as "zero+unreachable = unreachable" for the operation cost.  The meaning of
the zero cost is that no statment is analyzed yet, and the unreachable(bottom) cost means a program
point is analyzed as unreachable.  We thought "zero+unreachable" happens in very specific cases we
need to check, or due to an analyzer bug.  For debugging purpose, we defined it to return more
specific unreachable cost.

However, in allocation/autoreleasepool costs, the zero cost is not very special value. If there is
no alloc/autorelease calls, they can have the zero cost. "zero+unreachable = unreachable" doesn't
make sense there.

This diff changes the plus as "zero+unreachable = zero" for the non-operation costs.

Reviewed By: ezgicicek

Differential Revision: D23578869

fbshipit-source-id: 5392eca1c

infer/src/cost/costDomain.ml

@@ -98,9 +98,20 @@ let zero_record = VariantCostMap.empty
 (** If nb_exec is unreachable, we map to unreachable, not 0 *)
 let mult_by cost_record ~nb_exec = map cost_record ~f:(BasicCostWithReason.mult_unreachable nb_exec)
 
+(** "zero+unreachable" is defined as unreachable in the operation cost, but as zero in the other
+    costs. This is because "zero+unreachable" is a bit weird in the operation cost: it means that no
+    statment is analyzed yet, but at the same time the a program point is analyzed as unreachable.
+    For debugging purpose, we define it to return the more specific unreachable cost. *)
 let plus cost_record1 cost_record2 =
-  VariantCostMap.union
-    (fun _kind cost1 cost2 -> Some (BasicCostWithReason.plus cost1 cost2))
+  VariantCostMap.merge
+    (fun kind cost1 cost2 ->
+      match (kind, cost1, cost2) with
+      | OperationCost, Some cost, None | OperationCost, None, Some cost ->
+          Some cost
+      | (OperationCost | AllocationCost | AutoreleasepoolSize), _, _ ->
+          let cost1 = Option.value cost1 ~default:BasicCostWithReason.zero in
+          let cost2 = Option.value cost2 ~default:BasicCostWithReason.zero in
+          Some (BasicCostWithReason.plus cost1 cost2) )
     cost_record1 cost_record2
 
 

infer/tests/codetoanalyze/objc/autoreleasepool/basic.m

@@ -93,4 +93,13 @@
   }
 }
 
+- (void)autorelease_unreachable_zero:(int)n {
+  int i = 1;
+  if (i == 0) {
+    for (int j = 0; j < n; j++) {
+      [self call_autorelease_constant];
+    }
+  }
+}
+
 @end