[inferbo] Alloc site in the trace for INFERBO_ALLOC_xx issues

Reviewed By: skcho

Differential Revision: D9398353

fbshipit-source-id: 0d2e5c961

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -555,6 +555,9 @@ module Report = struct
    fun trace issue_desc ->
     let f elem (trace, depth) =
       match elem with
+      | Trace.Alloc location ->
+          let desc = "Alloc: " ^ issue_desc in
+          (Errlog.make_trace_element depth location desc [] :: trace, depth)
       | Trace.ArrAccess location ->
           let desc = "ArrayAccess: " ^ issue_desc in
           (Errlog.make_trace_element depth location desc [] :: trace, depth)

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -73,7 +73,10 @@ let check_alloc_size size_exp {pname; location} mem cond_set =
   | Bottom ->
       cond_set
   | NonBottom length ->
-      let traces = Dom.Val.get_traces v_length in
+      let alloc_trace_elem = BufferOverrunTrace.Alloc location in
+      let traces =
+        Dom.Val.get_traces v_length |> BufferOverrunTrace.Set.add_elem alloc_trace_elem
+      in
       PO.ConditionSet.add_alloc_size pname location ~length traces cond_set
 
 
@@ -303,7 +306,7 @@ module StdArray = struct
     {declare_local; declare_symbolic}
 end
 
-(* Java's Collections are represented by their size. We don't care about the elements. 
+(* Java's Collections are represented by their size. We don't care about the elements.
 - when they are constructed, we set the size to 0
 - each time we add an element, we increase the length of the array
 - each time we delete an element, we decrease the length of the array *)

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -24,7 +24,7 @@ module AllocSizeCondition = struct
 
   let pp fmt length = F.fprintf fmt "alloc(%a)" ItvPure.pp length
 
-  let pp_description fmt length = F.fprintf fmt "Alloc: %a" ItvPure.pp length
+  let pp_description fmt length = F.fprintf fmt "Length: %a" ItvPure.pp length
 
   let make ~length = if ItvPure.is_invalid length then None else Some length
 

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -11,6 +11,7 @@ module F = Format
 
 module BoTrace = struct
   type elem =
+    | Alloc of Location.t
     | ArrAccess of Location.t
     | ArrDecl of Location.t
     | Assign of Location.t
@@ -33,6 +34,8 @@ module BoTrace = struct
   let pp_elem : F.formatter -> elem -> unit =
    fun fmt elem ->
     match elem with
+    | Alloc location ->
+        F.fprintf fmt "Alloc (%a)" Location.pp_file_pos location
     | ArrAccess location ->
         F.fprintf fmt "ArrAccess (%a)" Location.pp_file_pos location
     | ArrDecl location ->

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

@@ -27,13 +27,13 @@ codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_O
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,ArrayDeclaration,Assignment,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: 10 Size: [5, +oo]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Alloc: 2000000000]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Alloc: -2]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: 0]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Bad, 0, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Alloc: Length: 2000000000]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Alloc: Length: -2]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: Length: 0]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Bad, 0, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [1, 1000000001]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [1, 1000000001]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, i.lb), i.ub] Size: 10]

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

@@ -50,5 +50,5 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN
 codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: 1]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: 0]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Alloc: Length: 0]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []