[inferbo][trace] Trace element for Unknown values

Summary:
Helps understand the origin of L5 issues.

Depends on D7194479

Reviewed By: skcho

Differential Revision: D7194493

fbshipit-source-id: 901c40d

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -262,8 +262,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                 L.(debug BufferOverrun Verbose)
                   "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp
                   location ;
-                Models.model_by_value Dom.Val.unknown model_env mem
+                let val_unknown = Dom.Val.unknown_from ~callee_pname ~location in
-                |> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown )
+                Models.model_by_value val_unknown model_env mem
+                |> Dom.Mem.add_heap Loc.unknown val_unknown )
       | Declare_locals (locals, location) ->
           (* array allocation in stack e.g., int arr[10] *)
           let rec decl_local pname node location loc typ ~inst_num ~dimension mem =
@@ -508,6 +509,9 @@ module Report = struct
           else
             let desc = Format.asprintf "Parameter: %a" Loc.pp loc in
             (Errlog.make_trace_element depth location desc [] :: trace, depth)
+      | Trace.UnknownFrom (pname, location) ->
+          let desc = Format.asprintf "Unknown value from: %a" Typ.Procname.pp pname in
+          (Errlog.make_trace_element depth location desc [] :: trace, depth)
     in
     List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev
 

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -40,7 +40,17 @@ module Val = struct
         TraceSet.pp x.traces
 
 
-  let unknown : t = {bot with itv= Itv.top; powloc= PowLoc.unknown; arrayblk= ArrayBlk.unknown}
+  let unknown : traces:TraceSet.t -> t =
+   fun ~traces -> {itv= Itv.top; powloc= PowLoc.unknown; arrayblk= ArrayBlk.unknown; traces}
+
+
+  let unknown_from : callee_pname:_ -> location:_ -> t =
+   fun ~callee_pname ~location ->
+    let traces =
+      Trace.UnknownFrom (callee_pname, location) |> Trace.singleton |> TraceSet.singleton
+    in
+    unknown ~traces
+
 
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -19,6 +19,7 @@ module BoTrace = struct
     | Call of Location.t
     | Return of Location.t
     | SymAssign of Loc.t * Location.t
+    | UnknownFrom of Typ.Procname.t * Location.t
     [@@deriving compare]
 
   type t = {length: int; trace: elem list} [@@deriving compare]
@@ -46,6 +47,8 @@ module BoTrace = struct
         F.fprintf fmt "Return (%a)" Location.pp_file_pos location
     | SymAssign (loc, location) ->
         F.fprintf fmt "SymAssign (%a, %a)" Loc.pp loc Location.pp_file_pos location
+    | UnknownFrom (pname, location) ->
+        F.fprintf fmt "UnknownFrom (%a, %a)" Typ.Procname.pp pname Location.pp_file_pos location
 
 
   let pp : F.formatter -> t -> unit =

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

@@ -12,7 +12,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, [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, [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, [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, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_L5, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, [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, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
@@ -44,8 +44,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, [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, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_L5, [Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_L5, [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_L5, [ArrayDeclaration,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_L5, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, [Offset: [s$0, +oo] Size: [s$0, s$1]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, [Offset: [s$0, +oo] Size: [s$0, s$1]]
 codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, []

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, [Call,Call,Parameter: n,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, [Return,ArrayAccess: Offset: [5, 5] Size: [5, 5]]
-codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, [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, [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, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
@@ -33,8 +33,8 @@ codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [Arr
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, [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, [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, [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, [Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [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, [Call,Call,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_L3, [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, [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, [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, [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()` ]