From 4ed3be9f0011c404c9eadb14f8cec1421ed4b5a7 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 16 Jan 2018 13:02:42 -0800 Subject: [PATCH] [inferbo] First models for std::array Reviewed By: jberdine Differential Revision: D6408415 fbshipit-source-id: 114776c --- .../src/bufferoverrun/bufferOverrunModels.ml | 49 ++++++++++++++++++- infer/src/bufferoverrun/bufferOverrunUtils.ml | 18 +++++++ infer/src/bufferoverrun/itv.ml | 4 ++ .../cpp/bufferoverrun/issues.exp | 2 + .../cpp/bufferoverrun/std_array.cpp | 19 +++++++ 5 files changed, 90 insertions(+), 2 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 6a46ca6c5..cb8fbbf36 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -206,9 +206,50 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct end end + module StdArray = struct + let typ typ length = + let declare_local ~decl_local pname node location loc ~inst_num ~dimension mem = + (* should this be deferred to the constructor? *) + let length = Some (IntLit.of_int64 length) in + BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length ~inst_num + ~dimension mem + in + let declare_symbolic ~decl_sym_val pname tenv node location ~depth loc ~inst_num ~new_sym_num + ~new_alloc_num mem = + let offset = Itv.zero in + let size = Itv.of_int64 length in + BoUtils.Exec.decl_sym_arr ~decl_sym_val pname tenv node location ~depth loc typ ~offset + ~size ~inst_num ~new_sym_num ~new_alloc_num mem + in + {declare_local; declare_symbolic} + + + let constructor _size = + let exec _pname _ret _node _location mem = mem (* initialize? *) in + {exec; check= no_check} + + + let at _size (array_exp, _) (index_exp, _) = + (* TODO? use size *) + let exec _pname ret _node _location mem = + L.(debug BufferOverrun Verbose) "Using model std::array<_, %Ld>::at" _size ; + match ret with + | Some (id, _) -> + BoUtils.Exec.load_val id (Sem.eval_lindex array_exp index_exp mem) mem + | None -> + mem + and check pname _node location mem cond_set = + BoUtils.Check.lindex ~array_exp ~index_exp mem pname location cond_set + in + {exec; check} + end + module Procname = struct let dispatch : model ProcnameDispatcher.dispatcher = let open ProcnameDispatcher.Procname in + let mk_std_array () = -"std" &:: "array" < any_typ &+ capt_int in + let std_array0 = mk_std_array () in + let std_array2 = mk_std_array () in make_dispatcher [ -"__inferbo_min" <>$ capt_exp $+ capt_exp $!--> inferbo_min ; -"__inferbo_set_size" <>$ capt_exp $+ capt_exp $!--> inferbo_set_size @@ -224,11 +265,15 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg $+? any_arg $--> Boost.Split.std_vector ; -"folly" &:: "split" $ any_arg $+ any_arg $+ capt_arg_of_typ (-"std" &:: "vector") - $+? capt_exp $--> Folly.Split.std_vector ] + $+? capt_exp $--> Folly.Split.std_vector + ; std_array0 >:: "array" &--> StdArray.constructor + ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at + ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at ] end module TypName = struct let dispatch : typ_model ProcnameDispatcher.typ_dispatcher = - ProcnameDispatcher.TypName.make_dispatcher [] + let open ProcnameDispatcher.TypName in + make_dispatcher [-"std" &:: "array" < capt_typ `T &+ capt_int >--> StdArray.typ] end end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index e94166f23..2787278eb 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -24,13 +24,31 @@ module type S = sig type counter = unit -> int module Exec : sig + val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate + type decl_local = Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int + val decl_local_array : + decl_local:decl_local -> Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t + -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate + -> Dom.Mem.astate * int + type decl_sym_val = Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate + + val decl_sym_arr : + decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int + -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int -> new_sym_num:counter + -> new_alloc_num:counter -> Dom.Mem.astate -> Dom.Mem.astate + end + + module Check : sig + val lindex : + array_exp:Exp.t -> index_exp:Exp.t -> Dom.Mem.astate -> Typ.Procname.t -> Location.t + -> PO.ConditionSet.t -> PO.ConditionSet.t end end diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 3e7b74777..725eadbde 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -1145,6 +1145,10 @@ let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n) let of_int_lit n = try of_int (IntLit.to_int n) with _ -> top +let of_int64 : Int64.t -> astate = + fun n -> Int64.to_int n |> Option.value_map ~f:of_int ~default:top + + let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false let false_sem = NonBottom ItvPure.false_sem diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 599ff3b43..e049974db 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -13,6 +13,8 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_u_FP, 5, BUFFER_OVERRUN_S2, codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, [Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, [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_L2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp new file mode 100644 index 000000000..cbf89e3b3 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp @@ -0,0 +1,19 @@ +/* + * 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. + */ +#include + +int std_array_bo_Bad() { + std::array a; + return a[42]; +} + +int normal_array_bo() { + int b[42]; + return b[42]; +}