From f55f382a78cc15dbe2566ac6dfc0e46d674e8444 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 23 Feb 2018 20:03:42 -0800 Subject: [PATCH] [inferbo] Support flexible array member Summary: It supports flexible array member using the following heuristic: - a memory for a class is allocated by `malloc(sizeof(C) + n * sizeof(T))` format - the last field of the class is an array - the static size of the last field is one, i.e., `T field_name[1]` When allocating and initializing members of classes, it sets the size of flexible array to `n+1` if the above conditions are met. Reviewed By: mbouaziz Differential Revision: D7056291 fbshipit-source-id: 31c5868 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 36 +++++--- .../src/bufferoverrun/bufferOverrunModels.ml | 22 +++-- infer/src/bufferoverrun/bufferOverrunUtils.ml | 21 +++-- infer/src/istd/IList.ml | 11 +++ infer/src/istd/IList.mli | 3 + .../codetoanalyze/cpp/bufferoverrun/class.cpp | 83 +++++++++++++++++++ .../cpp/bufferoverrun/issues.exp | 4 + 7 files changed, 153 insertions(+), 27 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 68d086e5e..22a9d2507 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -44,7 +44,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct fun pname tenv node location loc typ ~inst_num ~new_sym_num mem -> let max_depth = 2 in let new_alloc_num = BoUtils.counter_gen 1 in - let rec decl_sym_val pname tenv node location ~depth loc typ mem = + let rec decl_sym_val pname tenv node location ~depth ~is_last_field loc typ mem = if depth > max_depth then mem else let depth = depth + 1 in @@ -63,25 +63,37 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in Dom.Mem.add_heap loc v mem | Typ.Tptr (typ, _) -> - BoUtils.Exec.decl_sym_arr ~decl_sym_val pname tenv node location ~depth loc typ - ~inst_num ~new_sym_num ~new_alloc_num mem + BoUtils.Exec.decl_sym_arr + ~decl_sym_val:(decl_sym_val ~is_last_field:false) + pname tenv node location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tarray (typ, opt_int_lit, _) -> - let size = Option.map ~f:Itv.of_int_lit opt_int_lit in + let size = + match opt_int_lit with + | Some int_lit when is_last_field && (IntLit.iszero int_lit || IntLit.isone int_lit) -> + Some (Itv.make_sym pname new_sym_num) + | _ -> + Option.map ~f:Itv.of_int_lit opt_int_lit + in let offset = Itv.zero 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 + BoUtils.Exec.decl_sym_arr + ~decl_sym_val:(decl_sym_val ~is_last_field:false) + pname tenv node location ~depth loc typ ~offset ?size ~inst_num ~new_sym_num + ~new_alloc_num mem | Typ.Tstruct typename -> ( match Models.TypName.dispatch typename with | Some {Models.declare_symbolic} -> let model_env = Models.mk_model_env pname node location tenv in - declare_symbolic ~decl_sym_val model_env ~depth loc ~inst_num ~new_sym_num - ~new_alloc_num mem + declare_symbolic ~decl_sym_val:(decl_sym_val ~is_last_field) model_env ~depth loc + ~inst_num ~new_sym_num ~new_alloc_num mem | None -> - let decl_fld mem (fn, typ, _) = + let decl_fld ~is_last_field mem (fn, typ, _) = let loc_fld = Loc.append_field loc ~fn in - decl_sym_val pname tenv node location ~depth loc_fld typ mem + decl_sym_val pname tenv node location ~depth loc_fld typ ~is_last_field mem + in + let decl_flds str = + IList.fold_last ~f:(decl_fld ~is_last_field:false) + ~f_last:(decl_fld ~is_last_field) ~init:mem str.Typ.Struct.fields 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 ) | _ -> @@ -91,7 +103,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (CFG.loc node) ; mem in - decl_sym_val pname tenv node location ~depth:0 loc typ mem + decl_sym_val pname tenv node location ~depth:0 ~is_last_field:false loc typ mem let declare_symbolic_parameters diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 31d488ac6..99f8e1076 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -48,19 +48,23 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct let no_check _model_env _mem cond_set = cond_set - (* NOTE: heuristic *) - let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t = function + (* It returns a tuple of: + - type of array element + - stride of the type + - array size + - flexible array size *) + let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = function | Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length) | Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) -> - (typ, nbytes, length) - | Exp.Sizeof {typ; nbytes} -> - (typ, nbytes, Exp.one) + (typ, nbytes, length, None) + | Exp.Sizeof {typ; nbytes; dynamic_length} -> + (typ, nbytes, Exp.one, dynamic_length) | x -> - (Typ.mk (Typ.Tint Typ.IChar), Some 1, x) + (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None) let check_alloc_size size_exp {pname; location} mem cond_set = - let _, _, length0 = get_malloc_info size_exp in + let _, _, length0, _ = get_malloc_info size_exp in let v_length = Sem.eval length0 mem in match Dom.Val.get_itv v_length with | Bottom -> @@ -85,7 +89,8 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct let exec {pname; ret; node; location; tenv} mem = match ret with | Some (id, _) -> - let typ, stride, length0 = get_malloc_info size_exp in + let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in + let typ, stride, length0, dyn_length = get_malloc_info size_exp in let length = Sem.eval length0 mem in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in let v = @@ -95,6 +100,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct 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) + ?dyn_length | _ -> 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 063b89a2f..3bfafc37a 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -45,7 +45,8 @@ module type S = sig -> 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 + Tenv.t -> Typ.Procname.t -> CFG.node -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t + -> Dom.Mem.astate -> Dom.Mem.astate end module Check : sig @@ -130,35 +131,41 @@ module Make (CFG : ProcCfg.S) = struct 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 init_array_fields tenv pname node typ locs ?dyn_length mem = + let rec init_field locs dimension ?dyn_length (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 length = + Option.value_map dyn_length ~default:length ~f:(fun dyn_length -> + let i = Dom.Val.get_itv (Sem.eval dyn_length mem) in + Itv.plus i 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 + init_fields field_typ field_loc dimension ?dyn_length mem in (mem, inst_num + 1) - and init_fields typ locs dimension mem = + and init_fields typ locs dimension ?dyn_length 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 + let f = init_field locs (dimension + 1) in + IList.fold_last ~f ~f_last:(f ?dyn_length) ~init:(mem, 1) str.Typ.Struct.fields |> fst | None -> mem ) | _ -> mem in - init_fields typ locs 1 mem + init_fields typ locs 1 ?dyn_length mem end module Check = struct diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml index f036863fc..5f5d0dd5b 100644 --- a/infer/src/istd/IList.ml +++ b/infer/src/istd/IList.ml @@ -96,6 +96,17 @@ let inter compare xs ys = inter_ [] rev_xs rev_ys +(** like fold, but apply f_last to the last element *) +let rec fold_last l ~init ~f ~f_last = + match l with + | [] -> + init + | [last] -> + f_last init last + | hd :: tl -> + fold_last tl ~init:(f init hd) ~f ~f_last + + let to_string f l = let rec aux l = match l with [] -> "" | [s] -> f s | s :: rest -> f s ^ ", " ^ aux rest in "[" ^ aux l ^ "]" diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli index 540cbc95a..0f421d564 100644 --- a/infer/src/istd/IList.mli +++ b/infer/src/istd/IList.mli @@ -26,6 +26,9 @@ val intersect : ('a -> 'a -> int) -> 'a list -> 'a list -> bool val inter : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list (** [inter cmp xs ys] are the elements in both [xs] and [ys], sorted according to [cmp]. *) +val fold_last : 'a list -> init:'b -> f:('b -> 'a -> 'b) -> f_last:('b -> 'a -> 'b) -> 'b +(** like fold, but apply f_last to the last element *) + val to_string : ('a -> string) -> 'a list -> string val uncons_exn : 'a list -> 'a * 'a list diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp index 8ababc705..b77ddf589 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp @@ -78,3 +78,86 @@ void placement_new_Bad() { my_class2* x = new (mem) my_class2(); x->a[10] = 0; } + +class my_class4 { + public: + int a[3]; + int c[3]; + int b[1]; +}; + +void flexible_array1_Good() { + char* mem = (char*)malloc(sizeof(my_class4) + 4 * sizeof(int)); + my_class4* x = new (mem) my_class4(); + x->b[4] = 0; +} + +void flexible_array1_Bad() { + char* mem = (char*)malloc(sizeof(my_class4) + 4 * sizeof(int)); + my_class4* x = new (mem) my_class4(); + x->b[5] = 0; +} + +void flexible_array2_Bad_FN() { + char* mem = (char*)malloc(4 * sizeof(int) + sizeof(my_class4)); + my_class4* x = new (mem) my_class4(); + x->b[5] = 0; +} + +void flexible_array3_Bad_FN() { + char* mem = (char*)malloc(sizeof(my_class4) + sizeof(int) * 4); + my_class4* x = new (mem) my_class4(); + x->b[5] = 0; +} + +class my_class5 { + public: + int d[3]; + int f[3]; + my_class4 e; +}; + +void flexible_array4_Good() { + char* mem = (char*)malloc(sizeof(my_class5) + 4 * sizeof(int)); + my_class5* x = new (mem) my_class5(); + x->e.b[4] = 0; +} + +void flexible_array4_Bad() { + char* mem = (char*)malloc(sizeof(my_class5) + 4 * sizeof(int)); + my_class5* x = new (mem) my_class5(); + x->e.b[5] = 0; +} + +class Tree { + private: + unsigned int children_num; + + Tree(unsigned int children_num) : children_num(children_num) {} + + public: + void set_child(Tree* child, unsigned int nth) { children[nth] = child; } + + static Tree* NewNode(unsigned int children_num) { + char* mem = + (char*)malloc(sizeof(Tree) + (children_num - 1) * sizeof(Tree*)); + return new (mem) Tree(children_num); + } + + static Tree* NewLeaf() { return new Tree(0); } + + private: + Tree* children[1]; +}; + +void flexible_array5_Good_FP() { + Tree* t = Tree::NewNode(3); + t->set_child(Tree::NewLeaf(), 0); + t->set_child(Tree::NewLeaf(), 1); + t->set_child(Tree::NewLeaf(), 2); +} + +void flexible_array5_Bad() { + Tree* t = Tree::NewNode(3); + t->set_child(Tree::NewLeaf(), 5); +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 4e36b8848..e344b3605 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,6 +1,10 @@ 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, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [5, 5] Size: [1, 1] @ codetoanalyze/cpp/bufferoverrun/class.cpp:139:51 by call `Tree_set_child()` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Good_FP, 4, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [2, 2] Size: [1, 1] @ codetoanalyze/cpp/bufferoverrun/class.cpp:139:51 by call `Tree_set_child()` ] 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/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]]