From 4299848dad75ca878e911f56c7c12545c51579f7 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 23 Feb 2018 18:54:26 -0800 Subject: [PATCH] [inferbo] Initialize array member in class Reviewed By: mbouaziz Differential Revision: D7053775 fbshipit-source-id: c451d46 --- .../src/bufferoverrun/bufferOverrunModels.ml | 3 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 34 +++++++++++++++++++ .../codetoanalyze/cpp/bufferoverrun/class.cpp | 27 +++++++++++++++ .../cpp/bufferoverrun/issues.exp | 2 ++ 4 files changed, 65 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 191400cc5..283ffcdfe 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -82,7 +82,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct let malloc size_exp = - let exec {pname; ret; node; location} mem = + let exec {pname; ret; node; location; tenv} mem = match ret with | Some (id, _) -> let typ, stride, length0 = get_malloc_info size_exp in @@ -94,6 +94,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct in mem |> Dom.Mem.add_stack (Loc.of_id id) v |> set_uninitialized node typ (Dom.Val.get_array_locs v) + |> BoUtils.Exec.init_array_fields tenv pname node typ (Dom.Val.get_array_locs v) | _ -> L.(debug BufferOverrun Verbose) "/!\\ Do not know where to model malloc at %a@\n" Location.pp (CFG.loc node) ; diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 2787278eb..063b89a2f 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -43,6 +43,9 @@ module type S = sig 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 + + val init_array_fields : + Tenv.t -> Typ.Procname.t -> CFG.node -> Typ.t -> PowLoc.t -> Dom.Mem.astate -> Dom.Mem.astate end module Check : sig @@ -125,6 +128,37 @@ module Make (CFG : ProcCfg.S) = struct 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_val pname tenv node location ~depth deref_loc typ mem + + + let init_array_fields tenv pname node typ locs mem = + let rec init_field locs dimension (mem, inst_num) (field_name, field_typ, _) = + let field_loc = PowLoc.append_field locs ~fn:field_name in + let mem = + match field_typ.Typ.desc with + | Tarray (typ, Some length, stride) -> + let length = Itv.of_int_lit length in + let stride = Option.map stride ~f:IntLit.to_int in + let v = + Sem.eval_array_alloc pname node typ ?stride Itv.zero length inst_num dimension + in + Dom.Mem.strong_update_heap field_loc v mem + | _ -> + init_fields field_typ field_loc dimension mem + in + (mem, inst_num + 1) + and init_fields typ locs dimension mem = + match typ.Typ.desc with + | Tstruct typename -> ( + match Tenv.lookup tenv typename with + | Some str -> + List.fold ~f:(init_field locs (dimension + 1)) ~init:(mem, 1) str.Typ.Struct.fields + |> fst + | None -> + mem ) + | _ -> + mem + in + init_fields typ locs 1 mem end module Check = struct diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp index 64c7e0c3d..d938d5777 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp @@ -37,3 +37,30 @@ void access_after_new_Bad() { my_class* x = new my_class(); x->access_nth(15); } + +#include + +class my_class2 { + public: + int a[5]; +}; + +void array_member_malloc_Good() { + my_class2* x = (my_class2*)malloc(sizeof(my_class2)); + x->a[0] = 0; +} + +void array_member_malloc_Bad() { + my_class2* x = (my_class2*)malloc(sizeof(my_class2)); + x->a[10] = 0; +} + +class my_class3 { + public: + my_class2 b; +}; + +void array_member_malloc2_Bad() { + my_class3* x = (my_class3*)malloc(sizeof(my_class3)); + x->b.a[10] = 0; +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index e614bae12..468bccead 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,4 +1,6 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [15, 15] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/class.cpp:28:34 by call `my_class_access_nth()` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Assignment,Return,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]