From 7176fc936a26959495a21b75d88b5fd70c45e81e Mon Sep 17 00:00:00 2001 From: Kihong Heo Date: Mon, 26 Jun 2017 10:35:02 -0700 Subject: [PATCH] [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 | 5 ++-- infer/src/bufferoverrun/arrayBlk.ml | 3 +++ .../src/bufferoverrun/bufferOverrunChecker.ml | 3 ++- .../src/bufferoverrun/bufferOverrunDomain.ml | 3 +++ .../codetoanalyze/c/bufferoverrun/external.c | 23 +++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 5 ++++ .../cpp/bufferoverrun/external.cpp | 23 +++++++++++++++++++ .../cpp/bufferoverrun/issues.exp | 18 +++++++++++++++ 8 files changed, 79 insertions(+), 4 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/external.c create mode 100644 infer/tests/codetoanalyze/cpp/bufferoverrun/external.cpp diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 08e65d224..34147117c 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/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 diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index ca7096137..6768cd416 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index cb87eecbf..7fbf8ef0b 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index fd5e63519..d6b0ba9db 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/external.c b/infer/tests/codetoanalyze/c/bufferoverrun/external.c new file mode 100644 index 000000000..c18689878 --- /dev/null +++ b/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; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index a5aca49c7..a367931ba 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/external.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/external.cpp new file mode 100644 index 000000000..c18689878 --- /dev/null +++ b/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; +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 1386f601f..637e08cbb 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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_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*,std::allocator*>>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_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>_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>_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>_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>_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>_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>_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>_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>_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>_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>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Good_FP, 4, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]