[inferbo] Add an issue type for alarms by unknown function call

Summary: It adds an issue type, `BUFFER_OVERRUN_U5`, for alarms involving unknown values, i.e., when the trace set includes an unknown function call.

Reviewed By: mbouaziz

Differential Revision: D7178841

fbshipit-source-id: bfe857b

infer/src/base/IssueType.ml

@@ -104,6 +104,8 @@ let buffer_overrun_l5 = from_string ~enabled:false "BUFFER_OVERRUN_L5"
 
 let buffer_overrun_s2 = from_string "BUFFER_OVERRUN_S2"
 
+let buffer_overrun_u5 = from_string ~enabled:false "BUFFER_OVERRUN_U5"
+
 let cannot_star = from_string "Cannot_star"
 
 let checkers_allocates_memory = from_string "CHECKERS_ALLOCATES_MEMORY"

infer/src/base/IssueType.mli

@@ -55,6 +55,8 @@ val buffer_overrun_l5 : t
 
 val buffer_overrun_s2 : t
 
+val buffer_overrun_u5 : t
+
 val cannot_star : t
 
 val checkers_allocates_memory : t

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -117,6 +117,8 @@ module ArrayAccessCondition = struct
     ItvPure.have_similar_bounds lidx ridx && ItvPure.have_similar_bounds lsiz rsiz
 
 
+  let has_infty {idx; size} = ItvPure.has_infty idx || ItvPure.has_infty size
+
   let xcompare ~lhs:{idx= lidx; size= lsiz} ~rhs:{idx= ridx; size= rsiz} =
     let idxcmp = ItvPure.xcompare ~lhs:lidx ~rhs:ridx in
     let sizcmp = ItvPure.xcompare ~lhs:lsiz ~rhs:rsiz in
@@ -257,6 +259,8 @@ module Condition = struct
         false
 
 
+  let has_infty = function ArrayAccess c -> ArrayAccessCondition.has_infty c | _ -> false
+
   let xcompare ~lhs ~rhs =
     match (lhs, rhs) with
     | AllocSize lhs, AllocSize rhs ->
@@ -341,6 +345,12 @@ module ConditionTrace = struct
       ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces location
     in
     {ct with cond_trace= Inter (caller_pname, callee_pname, location); val_traces}
+
+
+  let has_unknown ct = ValTraceSet.has_unknown ct.val_traces
+
+  let check : t -> IssueType.t option =
+   fun ct -> if has_unknown ct then Some IssueType.buffer_overrun_u5 else None
 end
 
 module ConditionSet = struct
@@ -441,12 +451,22 @@ module ConditionSet = struct
     List.fold condset ~f:subst_add_cwt ~init:[]
 
 
+  let set_buffer_overrun_u5 cwt issue_type =
+    if ( IssueType.equal issue_type IssueType.buffer_overrun_l3
+       || IssueType.equal issue_type IssueType.buffer_overrun_l4
+       || IssueType.equal issue_type IssueType.buffer_overrun_l5 )
+       && Condition.has_infty cwt.cond
+    then Option.value (ConditionTrace.check cwt.trace) ~default:issue_type
+    else issue_type
+
+
   let check_all ~report condset =
     List.iter condset ~f:(fun cwt ->
         match Condition.check cwt.cond with
         | None ->
             ()
         | Some issue_type ->
+            let issue_type = set_buffer_overrun_u5 cwt issue_type in
             report cwt.cond cwt.trace issue_type )
 
 

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -55,6 +55,11 @@ module BoTrace = struct
    fun fmt t ->
     let pp_sep fmt () = F.fprintf fmt " :: " in
     F.pp_print_list ~pp_sep pp_elem fmt t.trace
+
+
+  let is_unknown_elem = function UnknownFrom _ -> true | _ -> false
+
+  let has_unknown x = List.exists x.trace ~f:is_unknown_elem
 end
 
 module Set = struct
@@ -105,6 +110,9 @@ module Set = struct
               add new_trace traces )
             arr_traces traces )
         idx_traces empty
+
+
+  let has_unknown t = exists BoTrace.has_unknown t
 end
 
 include BoTrace

infer/src/bufferoverrun/itv.ml

@@ -840,6 +840,8 @@ module ItvPure = struct
 
   let have_similar_bounds (l1, u1) (l2, u2) = Bound.are_similar l1 l2 && Bound.are_similar u1 u2
 
+  let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false
+
   let subst : t -> Bound.t bottom_lifted SubstMap.t -> t bottom_lifted =
    fun x map ->
     match (Bound.subst_lb (lb x) map, Bound.subst_ub (ub x) map) with

infer/src/bufferoverrun/itv.mli

@@ -82,6 +82,8 @@ module ItvPure : sig
 
   val have_similar_bounds : t -> t -> bool
 
+  val has_infty : t -> bool
+
   val make_positive : t -> t
 
   val join : t -> t -> t

infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c

@@ -158,3 +158,37 @@ void alloc_may_be_big_Bad() { malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1); }
 void alloc_may_be_big_Good_FP() {
   malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1);
 }
+
+void l1_unknown_function_Bad() {
+  int a[5];
+  int idx = unknown_function() * 10;
+  if (10 <= idx) {
+    if (idx <= 10) {
+      a[idx] = 0;
+    }
+  }
+}
+
+int zero_to_infty() {
+  int r = 0;
+  for (int i = 0; i < zero_or_ten(0); i++) {
+    r++;
+  }
+  return r;
+}
+
+/* Inferbo raises U5 alarm because
+   - the pair of offset:[10,10] and size:[5,+oo] is belong to L3
+   - the offset value is from an unknown function
+   - there is at least one infinity bound (in size).
+   However, it should ideally raise L3, because the infinity is not
+   from the unknown function. */
+void False_Issue_Type_l3_unknown_function_Bad() {
+  int* a = (int*)malloc((zero_to_infty() + 5) * sizeof(int));
+  int idx = unknown_function() * 10;
+  if (10 <= idx) {
+    if (idx <= 10) {
+      a[idx] = 0;
+    }
+  }
+}

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

@@ -15,7 +15,7 @@ codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERR
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [3, 3] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:23:3 by call to `two_symbolic_accesses()` ]
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [-1, -1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:24:3 by call to `two_symbolic_accesses()` ]
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:23:3 by call to `two_symbolic_accesses()` ]
-codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_L5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, ERROR, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
@@ -25,6 +25,7 @@ codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_
 codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, WARNING, []
+codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 5, BUFFER_OVERRUN_U5, ERROR, [Call,Assignment,Assignment,Return,ArrayDeclaration,Assignment,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, +oo]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, ERROR, [Alloc: [2000000000, 2000000000]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, ERROR, [Alloc: [-2, -2]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, ERROR, [Alloc: [0, 0]]
@@ -36,6 +37,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, s$0), s$1] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [s$0, min(-1, s$1)] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: [9, 9]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: [10, 10]]
@@ -47,8 +49,8 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_L5, ERROR, [Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_L5, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]]
 codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, ERROR, []

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -9,7 +9,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERR
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Parameter: n,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [Return,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
-codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, 0] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
@@ -33,8 +33,8 @@ codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, ERRO
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [6, 6] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [4, 4] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, -1] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ]