diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 267f71a71..0b4d2e1fa 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -204,6 +204,34 @@ let placement_new size_exp (src_exp1, t1) src_arg2_opt = {exec; check= no_check} +let strndup src_exp length_exp = + let exec ({pname; node_hash; location; integer_type_widths} as model_env) ~ret:((id, _) as ret) + mem = + let v = + let src_strlen = Dom.Mem.get_c_strlen (Sem.eval_locs src_exp mem) mem in + let length = Sem.eval integer_type_widths length_exp mem in + let size = Itv.incr (Itv.min_sem (Dom.Val.get_itv src_strlen) (Dom.Val.get_itv length)) in + let allocsite = + let represents_multiple_values = not (Itv.is_one size) in + Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None + ~represents_multiple_values + in + let traces = + Trace.Set.join (Dom.Val.get_traces src_strlen) (Dom.Val.get_traces length) + |> Trace.Set.add_elem location (Trace.through ~risky_fun:(Some Trace.strndup)) + |> Trace.Set.add_elem location ArrayDeclaration + in + Dom.Val.of_c_array_alloc allocsite + ~stride:(Some (integer_type_widths.char_width / 8)) + ~offset:Itv.zero ~size ~traces + in + mem + |> Dom.Mem.add_stack (Loc.of_id id) v + |> (strncpy (Exp.Var id) src_exp length_exp).exec model_env ~ret + in + {exec; check= no_check} + + let inferbo_min e1 e2 = let exec {integer_type_widths} ~ret:(id, _) mem = let i1 = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_itv in @@ -604,6 +632,7 @@ module Call = struct ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy ; -"snprintf" <>--> snprintf ; -"vsnprintf" <>--> vsnprintf + ; -"strndup" <>$ capt_exp $+ capt_exp $+...$--> strndup ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg $+? any_arg $--> Boost.Split.std_vector diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index cffc64dbb..d7691fc55 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -10,7 +10,7 @@ open AbsLoc module F = Format module BoTrace = struct - type lib_fun = Snprintf | Vsnprintf [@@deriving compare] + type lib_fun = Snprintf | Strndup | Vsnprintf [@@deriving compare] type final = UnknownFrom of Typ.Procname.t option [@@deriving compare] @@ -30,6 +30,8 @@ module BoTrace = struct let snprintf = Snprintf + let strndup = Strndup + let vsnprintf = Vsnprintf let length = function Empty -> 0 | Final _ -> 1 | Elem {length} | Call {length} -> length @@ -60,6 +62,8 @@ module BoTrace = struct let pp_lib_fun f = function | Snprintf -> F.fprintf f "snprintf" + | Strndup -> + F.fprintf f "strndup" | Vsnprintf -> F.fprintf f "vsnprintf" diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index dd1e8b925..86fd48e93 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -204,6 +204,10 @@ codetoanalyze/c/bufferoverrun/models.c, strncpy_contents_Bad, 5, BUFFER_OVERRUN_ codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 10 Size: 5] codetoanalyze/c/bufferoverrun/models.c, strncpy_no_null_2_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 5 Size: 5] codetoanalyze/c/bufferoverrun/models.c, strncpy_no_null_4_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 14 Size: 10] +codetoanalyze/c/bufferoverrun/models.c, strndup_1_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Risky value from: strndup,Array declaration,Assignment,Array access: Offset: [0, 99] Size: 13] +codetoanalyze/c/bufferoverrun/models.c, strndup_2_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Risky value from: strndup,Array declaration,Assignment,Array access: Offset: [0, 11] Size: 6] +codetoanalyze/c/bufferoverrun/models.c, strndup_3_Bad, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/c/bufferoverrun/models.c, strndup_3_Bad, 7, BUFFER_OVERRUN_R2, no_bucket, ERROR, [,Assignment,,Assignment,Risky value from: strndup,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: 6] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop3_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop4_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/models.c b/infer/tests/codetoanalyze/c/bufferoverrun/models.c index f6a5b794d..59800f720 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/models.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c @@ -333,3 +333,65 @@ void strncpy_no_null_4_Bad() { int a[10]; a[strlen(dst)] = 0; } + +void strndup_1_Good() { + char s1[] = "Hello Infer!"; + int len = strlen(s1); + char* s2 = strndup(s1, len); + for (int i = 0; i < len; i++) { + s2[i] = 'a'; + } +} + +void strndup_1_Bad() { + char s1[] = "Hello Infer!"; + int len = 100; + char* s2 = strndup(s1, len); + for (int i = 0; i < len; i++) { + s2[i] = 'a'; + } +} + +void strndup_2_Good() { + char s1[] = "Hello Infer!"; + int len = strlen(s1); + s1[5] = '\0'; + char* s2 = strndup(s1, len); + for (int i = 0; i < strlen(s2); i++) { + s2[i] = 'a'; + } +} + +void strndup_2_Bad() { + char s1[] = "Hello Infer!"; + int len = strlen(s1); + s1[5] = '\0'; + char* s2 = strndup(s1, len); + for (int i = 0; i < len; i++) { + s2[i] = 'a'; + } +} + +void strndup_3_Good() { + int size = unknown(); + if (size >= 10) { + char* s1 = (char*)malloc(sizeof(char) * size); + s1[5] = '\0'; + char* s2 = strndup(s1, size - 1); + for (int i = 0; i < strlen(s2); i++) { + s2[i] = 'a'; + } + } +} + +void strndup_3_Bad() { + int size = unknown(); + if (size >= 10) { + char* s1 = (char*)malloc(sizeof(char) * size); + s1[5] = '\0'; + char* s2 = strndup(s1, size - 1); + for (int i = 0; i < size - 1; i++) { + s2[i] = 'a'; + } + } +}