diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index e35ddbe93..02e32682f 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -109,7 +109,22 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct {exec; check} - let realloc = malloc + let realloc src_exp size_exp = + let {exec= malloc_exec; check= malloc_check} = malloc size_exp in + let exec ({ret; tenv} as model_env) mem = + let mem = malloc_exec model_env mem in + match ret with + | Some (id, _) -> + let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in + let typ, _, _, _ = get_malloc_info size_exp in + let tgt_locs = Dom.Val.get_all_locs (Dom.Mem.find_stack (Loc.of_id id) mem) in + let src_locs = Dom.Val.get_all_locs (Sem.eval src_exp mem) in + BoUtils.Exec.structural_copy tenv typ ~tgt_locs ~src_locs mem + | _ -> + mem + in + {exec; check= malloc_check} + let placement_new allocated_mem_exp = let exec {ret} mem = @@ -310,7 +325,7 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct ; -"__new" <>$ capt_exp $+...$--> malloc ; -"__new_array" <>$ capt_exp $+...$--> malloc ; -"__placement_new" <>$ any_arg $+ capt_exp $!--> placement_new - ; -"realloc" <>$ any_arg $+ capt_exp $+...$--> realloc + ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length ; -"strlen" <>--> by_value Dom.Val.Itv.nat ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 197c79fd1..6dc120ff5 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -47,6 +47,9 @@ module type S = sig val init_array_fields : Tenv.t -> Typ.Procname.t -> CFG.node -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t -> Dom.Mem.astate -> Dom.Mem.astate + + val structural_copy : + Tenv.t -> Typ.t -> tgt_locs:PowLoc.t -> src_locs:PowLoc.t -> Dom.Mem.astate -> Dom.Mem.astate end module Check : sig @@ -166,6 +169,28 @@ module Make (CFG : ProcCfg.S) = struct mem in init_fields typ locs 1 ?dyn_length mem + + + let rec structural_copy tenv typ ~tgt_locs ~src_locs mem = + match typ with + | {Typ.desc= Tint _} | {Typ.desc= Tfloat _} | {Typ.desc= Tvoid} | {Typ.desc= Tptr _} -> + let v = Dom.Mem.find_heap_set src_locs mem in + Dom.Mem.strong_update_heap tgt_locs v mem + | {Typ.desc= Tarray {elt}} -> + let tgt_locs = Dom.Val.get_all_locs (Dom.Mem.find_heap_set tgt_locs mem) in + let src_locs = Dom.Val.get_all_locs (Dom.Mem.find_heap_set src_locs mem) in + structural_copy tenv elt ~tgt_locs ~src_locs mem + | {Typ.desc= Tstruct typename} -> ( + match Tenv.lookup tenv typename with + | Some str -> + List.fold str.Typ.Struct.fields ~init:mem ~f:(fun mem (fn, typ, _) -> + let tgt_locs = PowLoc.append_field tgt_locs ~fn in + let src_locs = PowLoc.append_field src_locs ~fn in + structural_copy tenv typ ~tgt_locs ~src_locs mem ) + | None -> + mem ) + | _ -> + mem end module Check = struct diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 3e92a57de..d09100cf0 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -13,6 +13,8 @@ codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, [] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, [] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp new file mode 100644 index 000000000..86bb442d4 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/realloc.cpp @@ -0,0 +1,72 @@ +/* + * Copyright (c) 2018 - 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 + +void realloc_Good() { + int* buf1 = (int*)malloc(2 * sizeof(int)); + buf1[0] = 3; + int* buf2 = (int*)realloc(buf1, 5 * sizeof(int)); + buf2[buf2[0]] = 0; +} + +void realloc_Bad() { + int* buf1 = (int*)malloc(2 * sizeof(int)); + buf1[0] = 5; + int* buf2 = (int*)realloc(buf1, 5 * sizeof(int)); + buf2[buf2[0]] = 0; +} + +void realloc_Good_FP() { + int* buf1 = (int*)malloc(2 * sizeof(int)); + for (int i = 0; i < 2; i++) { + buf1[i] = 3; + } + int* buf2 = (int*)realloc(buf1, 5 * sizeof(int)); + buf2[buf2[0]] = 0; +} + +struct S1 { + int x[2]; +}; + +void realloc_struct1_Good() { + struct S1* buf1 = (struct S1*)malloc(2 * sizeof(struct S1)); + buf1[0].x[0] = 3; + struct S1* buf2 = (struct S1*)realloc(buf1, 5 * sizeof(struct S1)); + buf2[buf2[0].x[0]].x[0] = 0; +} + +void realloc_struct1_Bad_FN() { + struct S1* buf1 = (struct S1*)malloc(2 * sizeof(struct S1)); + buf1[0].x[0] = 5; + struct S1* buf2 = (struct S1*)realloc(buf1, 5 * sizeof(struct S1)); + buf2[buf2[0].x[0]].x[0] = 0; +} + +struct S2 { + int x; +}; + +struct S3 { + struct S2 s; +}; + +void realloc_struct2_Good() { + struct S3* buf1 = (struct S3*)malloc(2 * sizeof(struct S3)); + buf1[0].s.x = 3; + struct S3* buf2 = (struct S3*)realloc(buf1, 5 * sizeof(struct S3)); + buf2[buf2[0].s.x].s.x = 0; +} + +void realloc_struct2_Bad_FN() { + struct S3* buf1 = (struct S3*)malloc(2 * sizeof(struct S3)); + buf1[0].s.x = 5; + struct S3* buf2 = (struct S3*)realloc(buf1, 5 * sizeof(struct S3)); + buf2[buf2[0].s.x].s.x = 0; +}