diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 48650078a..eff41355f 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -152,80 +152,98 @@ struct ~inst_num ~dimension:(dimension + 1) mem | _ -> mem - let declare_symbolic_array + let counter_gen init = + let num_ref = ref init in + let get_num () = + let v = !num_ref in + num_ref := v + 1; + v + in + get_num + + let declare_symbolic_val : Typ.Procname.t -> Tenv.t -> CFG.node -> Loc.t -> Typ.t -> inst_num:int - -> sym_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int - = fun pname tenv node loc typ ~inst_num ~sym_num ~dimension mem -> - let offset = Itv.make_sym pname sym_num in - let size = Itv.make_sym pname (sym_num + 2) in - let arr = - Sem.eval_array_alloc pname node typ offset size inst_num dimension - in - let elem_val = Dom.Val.make_sym pname (sym_num + 4) in - let arr_loc = arr |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in - let mem = - mem - |> Dom.Mem.add_heap loc arr - |> Dom.Mem.strong_update_heap arr_loc elem_val - in - let decl_fld (mem, sym_num) (fn, typ, _) = - let loc = - mem |> Dom.Mem.find_heap loc |> Dom.Val.get_array_locs |> PowLoc.choose + -> new_sym_num: (unit -> int) -> Domain.t -> Domain.t + = fun pname tenv node loc typ ~inst_num ~new_sym_num mem -> + let max_depth = 2 in + let new_alloc_num = counter_gen 1 in + let rec decl_sym_fld ~depth loc typ mem = + if depth > max_depth then mem else + let depth = depth + 1 in + match typ.Typ.desc with + | Typ.Tint ikind -> + let unsigned = Typ.ikind_is_unsigned ikind in + let sym_num = new_sym_num () in + let _ = new_sym_num () in + let v = Dom.Val.make_sym ~unsigned pname sym_num in + Dom.Mem.add_heap loc v mem + | Typ.Tfloat _ -> + let sym_num = new_sym_num () in + let _ = new_sym_num () in + let v = Dom.Val.make_sym pname sym_num in + Dom.Mem.add_heap loc v mem + | Typ.Tptr (typ, _) -> + decl_sym_arr ~depth loc typ mem + | Typ.Tarray (typ, opt_int_lit, _) -> + let opt_size = Option.map ~f:Itv.of_int_lit opt_int_lit in + let opt_offset = Some Itv.zero in + decl_sym_arr ~depth loc typ ~opt_offset ~opt_size mem + | Typ.Tstruct typename -> + let decl_fld mem (fn, typ, _) = + let loc_fld = Loc.append_field loc fn in + decl_sym_fld ~depth loc_fld typ mem + in + let decl_flds str = + List.fold ~f:decl_fld ~init:mem str.Typ.Struct.fields + in + let opt_struct = Tenv.lookup tenv typename in + Option.value_map opt_struct ~default:mem ~f:decl_flds + | _ -> + if Config.bo_debug >= 3 then + L.(debug BufferOverrun Verbose) "/!\\ decl_fld of unhandled type: %a at %a@." + (Typ.pp Pp.text) typ + Location.pp (CFG.loc node); + mem + + and decl_sym_arr ~depth loc typ ?(opt_offset=None) ?(opt_size=None) mem = + let option_value opt_x default_f = + match opt_x with + | Some x -> x + | None -> default_f () in - let field = Loc.append_field loc fn in - match typ.Typ.desc with - | Typ.Tint ikind -> - let unsigned = Typ.ikind_is_unsigned ikind in - let v = Dom.Val.make_sym ~unsigned pname sym_num in - (Dom.Mem.add_heap field v mem, sym_num + 2) - | Typ.Tfloat _ -> - let v = Dom.Val.make_sym pname sym_num in - (Dom.Mem.add_heap field v mem, sym_num + 2) - | Typ.Tptr (typ, _) -> - let offset = Itv.make_sym pname sym_num in - let size = Itv.make_sym pname (sym_num + 2) in - let v = - Sem.eval_array_alloc pname node typ offset size inst_num dimension - in - (Dom.Mem.add_heap field v mem, sym_num + 4) - | _ -> - L.(debug BufferOverrun Verbose) "/!\\ decl_fld of unhandled type: %a at %a@." - (Typ.pp Pp.text) typ - Location.pp (CFG.loc node); - (mem, sym_num) + let itv_make_sym () = + let sym_num = new_sym_num () in + let _ = new_sym_num () in + Itv.make_sym pname sym_num + in + let offset = option_value opt_offset itv_make_sym in + let size = option_value opt_size itv_make_sym in + let alloc_num = new_alloc_num () in + let arr = + Sem.eval_array_alloc pname node typ offset size inst_num alloc_num + in + let mem = Dom.Mem.add_heap loc arr mem in + let deref_loc = + Loc.of_allocsite (Sem.get_allocsite pname node inst_num alloc_num) + in + decl_sym_fld ~depth deref_loc typ mem in - match typ.Typ.desc with - | Typ.Tstruct typename -> - (match Tenv.lookup tenv typename with - | Some str -> - List.fold ~f:decl_fld ~init:(mem, sym_num + 6) str.Typ.Struct.fields - | _ -> (mem, sym_num + 6)) - | _ -> (mem, sym_num + 6) + decl_sym_fld ~depth:0 loc typ mem let declare_symbolic_parameter : Procdesc.t -> Tenv.t -> CFG.node -> int -> Dom.Mem.astate -> Dom.Mem.astate = fun pdesc tenv node inst_num mem -> let pname = Procdesc.get_proc_name pdesc in - let add_formal (mem, inst_num, sym_num) (pvar, typ) = - match typ.Typ.desc with - | Typ.Tint ikind -> - let unsigned = Typ.ikind_is_unsigned ikind in - let v = Dom.Val.make_sym ~unsigned pname sym_num in - let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in - (mem, inst_num + 1, sym_num + 2) - | Typ.Tptr (typ, _) -> - let (mem, sym_num) = - declare_symbolic_array pname tenv node (Loc.of_pvar pvar) typ - ~inst_num ~sym_num ~dimension:1 mem - in - (mem, inst_num + 1, sym_num) - | _ -> - L.(debug BufferOverrun Verbose) "declare_symbolic_parameter of unhandled type: %a@." - (Typ.pp Pp.text) typ; - (mem, inst_num, sym_num) (* TODO: add other cases if necessary *) + let new_sym_num = counter_gen 0 in + let add_formal (mem, inst_num) (pvar, typ) = + let loc = Loc.of_pvar pvar in + let mem = + declare_symbolic_val pname tenv node loc typ ~inst_num ~new_sym_num mem + in + (mem, inst_num + 1) in - List.fold ~f:add_formal ~init:(mem, inst_num, 0) (Sem.get_formals pdesc) - |> fst3 + List.fold ~f:add_formal ~init:(mem, inst_num) (Sem.get_formals pdesc) + |> fst let instantiate_ret ret callee_pname callee_exit_mem subst_map mem = match ret with @@ -365,15 +383,17 @@ struct | Exp.Var _ -> let arr = Sem.eval exp mem loc |> Dom.Val.get_array_blk in Some (arr, Itv.zero, true) - | Exp.Lindex (e1, e2) - | Exp.BinOp (Binop.PlusA, e1, e2) -> - let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in + | Exp.Lindex (e1, e2) -> + let locs = Sem.eval_locs e1 mem loc |> Dom.Val.get_all_locs in + let arr = Dom.Mem.find_set locs mem |> Dom.Val.get_array_blk in let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in Some (arr, idx, true) - | Exp.BinOp (Binop.MinusA, e1, e2) -> + | Exp.BinOp (Binop.PlusA as bop, e1, e2) + | Exp.BinOp (Binop.MinusA as bop, e1, e2) -> let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in - Some (arr, idx, false) + let is_plus = Binop.equal bop Binop.PlusA in + Some (arr, idx, is_plus) | _ -> None in match array_access with diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 9ed813e80..098113c86 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -621,6 +621,10 @@ struct let find_heap_set : PowLoc.t -> t -> Val.t = fun k m -> Heap.find_set k m.heap + let find_set : PowLoc.t -> t -> Val.t + = fun k m -> + Val.join (find_stack_set k m) (find_heap_set k m) + let find_alias : Ident.t -> t -> Pvar.t option = fun k m -> Alias.find k m.alias @@ -711,6 +715,10 @@ module Mem = struct = fun k -> f_lift_default Val.bot (MemReach.find_heap_set k) + let find_set : PowLoc.t -> t -> Val.t + = fun k -> + f_lift_default Val.bot (MemReach.find_set k) + let find_alias : Ident.t -> t -> Pvar.t option = fun k -> f_lift_default None (MemReach.find_alias k) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 075448a3a..f6c9dac16 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -214,6 +214,33 @@ struct | Binop.LOr -> Val.lor_sem v1 v2 | Binop.PtrFld -> raise Not_implemented + let rec eval_locs : Exp.t -> Mem.astate -> Location.t -> Val.t + = fun exp mem loc -> + match exp with + | Exp.Var id -> + (match Mem.find_alias id mem with + | Some pvar -> + Var.of_pvar pvar |> Loc.of_var |> PowLoc.singleton |> Val.of_pow_loc + | None -> Val.bot) + | Exp.Lvar pvar -> + pvar |> Loc.of_pvar |> PowLoc.singleton |> Val.of_pow_loc + | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc + | Exp.Cast (_, e) -> eval_locs e mem loc + | Exp.Lfield (e, fn, _) -> + eval e mem loc + |> Val.get_all_locs + |> Fn.flip PowLoc.append_field fn + |> Val.of_pow_loc + | Exp.Lindex (e1, e2) -> + let arr = eval e1 mem loc in + let idx = eval e2 mem loc in + Val.plus_pi arr idx + | Exp.Const _ + | Exp.UnOp _ + | Exp.Sizeof _ + | Exp.Exn _ + | Exp.Closure _ -> Val.bot + let get_allocsite : Typ.Procname.t -> CFG.node -> int -> int -> string = fun proc_name node inst_num dimension -> let proc_name = Typ.Procname.to_string proc_name in @@ -400,6 +427,7 @@ struct = fun pairs -> let add_pair map (formal, actual) = match formal with + | Itv.Bound.Linear (_, se1) when Itv.SymLinear.is_zero se1 -> map | Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 -> let (symbol, coeff) = Itv.SymLinear.choose se1 in if Int.equal coeff 1 diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 2754383ae..f82a3d529 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -879,7 +879,9 @@ let ub : t -> Bound.t let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n) -let of_int_lit n = of_int (IntLit.to_int n) +let of_int_lit n = + try of_int (IntLit.to_int n) with + | _ -> top let is_bot : t -> bool = fun x -> equal x Bottom diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp new file mode 100644 index 000000000..86cb34ca7 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp @@ -0,0 +1,27 @@ +/* + * 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. + */ +class my_class { + int idx; + int arr[10]; + + void set_a(int n) { idx = n; } + + int id(int n) { return n; } + + public: + int access_Bad() { + set_a(10); + return arr[idx]; + } + + int access2_Bad() { + int n = 10; + return arr[id(n)]; + } +}; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index b1df493ee..1386f601f 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,13 +1,17 @@ +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/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, 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]] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, +oo] @ 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$6), s$7] Size: [max(0, s$6), s$7] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] +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, 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, 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$14), s$15] Size: [max(0, s$14), s$15] @ 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: [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, 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_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, 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[]()` ]