[inferbo] fix the semantics of unknown library calls

Summary: Unknown library returns the unknown pointer as well as the top interval.

Reviewed By: mbouaziz, jvillard

Differential Revision: D5282669

fbshipit-source-id: 34c7e18

infer/src/bufferoverrun/absLoc.ml

@@ -19,6 +19,7 @@ struct
   include String
   let pp fmt s = Format.fprintf fmt "%s" s
   let make x = x
+  let unknown = "Unknown"
 end
 
 module Loc =
@@ -27,10 +28,9 @@ struct
     | Var of Var.t
     | Allocsite of Allocsite.t
     | Field of t * Fieldname.t
-    | Unknown
   [@@deriving compare]
 
-  let unknown = Unknown
+  let unknown = Allocsite Allocsite.unknown
   let rec pp fmt = function
     | Var v ->
         Var.pp F.str_formatter v;
@@ -40,7 +40,6 @@ struct
         else F.fprintf fmt "%s" s
     | Allocsite a -> Allocsite.pp fmt a
     | Field (l, f) -> F.fprintf fmt "%a.%a" pp l Fieldname.pp f
-    | Unknown -> F.fprintf fmt "Unknown"
   let is_var = function Var _ -> true | _ -> false
   let is_logical_var = function
     | Var (Var.LogicalVar _) -> true

infer/src/bufferoverrun/arrayBlk.ml

@@ -119,6 +119,9 @@ include AbstractDomain.Map (Allocsite) (ArrInfo)
 let bot : astate
   = empty
 
+let unknown : astate
+  = add Allocsite.unknown (ArrInfo.top) bot
+
 let is_bot : astate -> bool
   = is_empty
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -128,7 +128,8 @@ struct
           L.(debug BufferOverrun Verbose) "/!\\ Unknown call to %s at %a@\n"
             proc_name
             Location.pp loc;
-          model_by_value Dom.Val.Itv.top ret mem
+          model_by_value Dom.Val.unknown ret mem
+          |> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown
 
   let rec declare_array
     : Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> length:IntLit.t option -> ?stride:int

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -212,6 +212,9 @@ struct
   let bot : t
     = { itv = Itv.bot; powloc = PowLoc.bot; arrayblk = ArrayBlk.bot }
 
+  let unknown : t
+    = { itv = Itv.top; powloc = PowLoc.unknown; arrayblk = ArrayBlk.unknown }
+
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs then true
     else

infer/tests/codetoanalyze/c/bufferoverrun/external.c

@@ -0,0 +1,23 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+extern char** lib();
+
+void extern_bad() {
+  int arr[10];
+  char** p = lib();
+  if (p != 0)
+    arr[10] = 0;
+  char* q = *p;
+  if (q != 0)
+    arr[20] = 0;
+  int r = *q;
+  if (r != 0)
+    arr[30] = 0;
+}

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

@@ -7,6 +7,11 @@ codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16
 codetoanalyze/c/bufferoverrun/cast.c, cast2_Good_FP, 2, BUFFER_OVERRUN, [Offset: [4, 4] Size: [4, 4]]
 codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ]
 codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ]
+codetoanalyze/c/bufferoverrun/external.c, extern_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/c/bufferoverrun/external.c, extern_bad, 7, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/external.c, extern_bad, 8, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN, [Offset: [30, 30] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10]]
 codetoanalyze/c/bufferoverrun/for_loop.c, safealloc, 10, UNREACHABLE_CODE, []
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]]

infer/tests/codetoanalyze/cpp/bufferoverrun/external.cpp

@@ -0,0 +1,23 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+extern char** lib();
+
+void extern_bad() {
+  int arr[10];
+  char** p = lib();
+  if (p != 0)
+    arr[10] = 0;
+  char* q = *p;
+  if (q != 0)
+    arr[20] = 0;
+  int r = *q;
+  if (r != 0)
+    arr[30] = 0;
+}

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

@@ -1,7 +1,14 @@
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 7, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 8, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN, [Offset: [30, 30] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<LMB<TFM>*,std::allocator<LMB<TFM>*>>_operator[]()` ]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `ral()` ]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]]
@@ -9,10 +16,21 @@ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok,
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Good_FP, 2, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Good_FP, 2, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<Int_no_copy,std::allocator<Int_no_copy>>_operator[]()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:17 by call `std::vector<int,std::allocator<int>>_vector()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:31 by call `std::vector<int,std::allocator<int>>_vector()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_at()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Good_FP, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Good_FP, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Good_FP, 4, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Good_FP, 4, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]