From 7fda4f1cc2bb580d78d57015db6b2f5cfb889b9d Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 23 Jan 2019 06:46:16 -0800 Subject: [PATCH] [inferbo] Revise strncpy model Summary: `strncpy` should update the `c_strlen` value. Depends on D13668505 Reviewed By: mbouaziz Differential Revision: D13668536 fbshipit-source-id: 64e09c734 --- infer/src/bufferoverrun/absLoc.ml | 2 + .../src/bufferoverrun/bufferOverrunModels.ml | 12 ++++- .../codetoanalyze/c/bufferoverrun/issues.exp | 3 ++ .../codetoanalyze/c/bufferoverrun/models.c | 50 +++++++++++++++++++ 4 files changed, 66 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 78f5e3ba9..3b3168f1d 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -290,6 +290,8 @@ module PowLoc = struct let exists_str ~f x = exists (fun l -> Loc.exists_str ~f l) x + + let of_c_strlen x = map Loc.of_c_strlen x end let always_strong_update = false diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 76a7dea6c..267f71a71 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -151,6 +151,16 @@ let strlen arr_exp = {exec; check= no_check} +let strncpy dest_exp src_exp size_exp = + let {exec= memcpy_exec; check= memcpy_check} = memcpy dest_exp src_exp size_exp in + let exec model_env ~ret mem = + let dest_strlen_loc = PowLoc.of_c_strlen (Sem.eval_locs dest_exp mem) in + let strlen = Dom.Mem.find_set (PowLoc.of_c_strlen (Sem.eval_locs src_exp mem)) mem in + mem |> memcpy_exec model_env ~ret |> Dom.Mem.update_mem dest_strlen_loc strlen + in + {exec; check= memcpy_check} + + let realloc src_exp size_exp = let exec ({location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in @@ -591,7 +601,7 @@ module Call = struct ; -"memcpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy ; -"memmove" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy ; -"memset" <>$ capt_exp $+ any_arg $+ capt_exp $!--> memset - ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy + ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy ; -"snprintf" <>--> snprintf ; -"vsnprintf" <>--> vsnprintf ; -"boost" &:: "split" diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 695fff658..dd1e8b925 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -200,7 +200,10 @@ codetoanalyze/c/bufferoverrun/models.c, strncpy_bad1, 3, BUFFER_OVERRUN_L1, no_b codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 18446744073709551615 Size: 40] codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, strncpy_contents_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 4 Size: 4] 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/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 fd92a82b7..f6a5b794d 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/models.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c @@ -283,3 +283,53 @@ void memcpy_integer_Bad() { int a[5]; a[dst] = 0; } + +void strncpy_contents_Good() { + char src[5] = "test"; + char dst[10]; + strncpy(dst, src, 5); + int a[5]; + a[strlen(dst)] = 0; +} + +void strncpy_contents_Bad() { + char src[5] = "test"; + char dst[10]; + strncpy(dst, src, 5); + int a[4]; + a[strlen(dst)] = 0; +} + +void strncpy_no_null_1_Bad_FN() { + char src[5] = "test"; + src[4] = 'a'; + char dst[10]; + strncpy(dst, src, 5); // [dst] may not have null character. + int a[10]; + a[strlen(dst)] = 0; +} + +void strncpy_no_null_2_Bad() { + char src[5] = "test"; + src[4] = 'a'; + char dst[10]; + strncpy(dst, src, 5); // [dst] may not have null character. + int a[5]; + a[strlen(dst)] = 0; +} + +void strncpy_no_null_3_Bad_FN() { + char src[15] = "test.test.test"; + char dst[10]; + strncpy(dst, src, 10); // [dst] does not have null character. + int a[20]; + a[strlen(dst)] = 0; +} + +void strncpy_no_null_4_Bad() { + char src[15] = "test.test.test"; + char dst[10]; + strncpy(dst, src, 10); // [dst] does not have null character. + int a[10]; + a[strlen(dst)] = 0; +}