Reviewed By: mbouaziz Differential Revision: D4937918 fbshipit-source-id: 3f723bamaster
Kihong Heo
8 years ago
committed by
Facebook Github Bot
parent
257e684392
commit
94d6efb83a
@ -0,0 +1,85 @@
|
||||
(*
|
||||
* 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.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
module F = Format
|
||||
|
||||
module BoTrace =
|
||||
struct
|
||||
type elem = ArrAccess of Location.t | ArrDecl of Location.t | Assign of Location.t
|
||||
| Call of Location.t | Return of Location.t | SymAssign of Location.t
|
||||
[@@deriving compare]
|
||||
type t = { length : int; trace : elem list } [@@deriving compare]
|
||||
let empty = { length = 0; trace = [] }
|
||||
let singleton elem = { length = 1; trace = [elem] }
|
||||
let add_elem elem t = { length = t.length + 1; trace = elem :: t.trace }
|
||||
let add_elem_last elem t = { length = t.length + 1; trace = t.trace @ [elem] }
|
||||
let append x y = { length = x.length + y.length; trace = x.trace @ y.trace }
|
||||
|
||||
let pp_elem : F.formatter -> elem -> unit
|
||||
= fun fmt elem ->
|
||||
match elem with
|
||||
| Assign loc -> F.fprintf fmt "Assign (%a)" Location.pp_file_pos loc
|
||||
| ArrDecl loc -> F.fprintf fmt "ArrDecl (%a)" Location.pp_file_pos loc
|
||||
| Call loc -> F.fprintf fmt "Call (%a)" Location.pp_file_pos loc
|
||||
| Return loc -> F.fprintf fmt "Return (%a)" Location.pp_file_pos loc
|
||||
| SymAssign loc -> F.fprintf fmt "SymAssign (%a)" Location.pp_file_pos loc
|
||||
| ArrAccess loc -> F.fprintf fmt "ArrAccess (%a)" Location.pp_file_pos loc
|
||||
|
||||
let pp : F.formatter -> t -> unit
|
||||
= fun fmt t ->
|
||||
let pp_sep fmt () = F.fprintf fmt " :: " in
|
||||
F.pp_print_list ~pp_sep pp_elem fmt t.trace
|
||||
end
|
||||
|
||||
module Set =
|
||||
struct
|
||||
include AbstractDomain.FiniteSet(BoTrace)
|
||||
(* currently, we keep only one trace for efficiency *)
|
||||
let join x y =
|
||||
if is_empty x then y
|
||||
else if is_empty y then x
|
||||
else
|
||||
let (tx, ty) = (min_elt x, min_elt y) in
|
||||
if Pervasives.(<=) tx.length ty.length then x
|
||||
else y
|
||||
|
||||
let choose_shortest set = min_elt set
|
||||
|
||||
let add_elem elem t =
|
||||
if is_empty t then singleton (BoTrace.singleton elem)
|
||||
else map (BoTrace.add_elem elem) t
|
||||
|
||||
let add_elem_last elem t =
|
||||
if is_empty t then singleton (BoTrace.singleton elem)
|
||||
else map (BoTrace.add_elem_last elem) t
|
||||
|
||||
let instantiate ~traces_caller ~traces_callee loc =
|
||||
if is_empty traces_caller then
|
||||
map (fun trace_callee -> BoTrace.add_elem_last (BoTrace.Call loc) trace_callee) traces_callee
|
||||
else
|
||||
fold (fun trace_callee traces ->
|
||||
fold (fun trace_caller traces ->
|
||||
let new_trace_caller = BoTrace.add_elem (BoTrace.Call loc) trace_caller in
|
||||
let new_trace = BoTrace.append trace_callee new_trace_caller in
|
||||
add new_trace traces) traces_caller traces) traces_callee empty
|
||||
|
||||
let merge ~traces_arr ~traces_idx loc =
|
||||
if is_empty traces_idx then
|
||||
map (fun trace_arr -> BoTrace.add_elem (BoTrace.ArrAccess loc) trace_arr) traces_arr
|
||||
else
|
||||
fold (fun trace_idx traces ->
|
||||
fold (fun trace_arr traces ->
|
||||
let new_trace_idx = BoTrace.add_elem (BoTrace.ArrAccess loc) trace_idx in
|
||||
let new_trace = BoTrace.append new_trace_idx trace_arr in
|
||||
add new_trace traces) traces_arr traces) traces_idx empty
|
||||
end
|
||||
|
||||
include BoTrace
|
||||
@ -1,23 +1,23 @@
|
||||
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:13 by call `std::vector<LMB<TFM>*,std::allocator<LMB<TFM>*>>_operator[]()` ]
|
||||
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:13 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]]
|
||||
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ]
|
||||
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, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<Int_no_copy,std::allocator<Int_no_copy>>_operator[]()` ]
|
||||
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: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
|
||||
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:13 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:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, 0] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN, [Call,Assignment,Call,Assignment,Return,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
|
||||
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN, [Call,Call,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
|
||||
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
|
||||
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
|
||||
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 7, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [20, 20] Size: [10, 10]]
|
||||
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 8, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
|
||||
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]]
|
||||
codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
|
||||
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Call,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<LMB<TFM>*,std::allocator<LMB<TFM>*>>_operator[]()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `ral()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [ArrayAccess: Offset: [-oo, +oo] Size: [16, 16]]
|
||||
codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [ArrayAccess: Offset: [-oo, +oo] Size: [16, 16]]
|
||||
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: 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, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
|
||||
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<Int_no_copy,std::allocator<Int_no_copy>>_operator[]()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Call,ArrayAccess: 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, [Call,ArrayAccess: 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, [Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_at()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
|
||||
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
|
||||
|
||||
Loading…
Reference in new issue