From ca463d17c1b790877a76227cf78e2291e940ef52 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 24 Jan 2019 03:30:35 -0800 Subject: [PATCH] [inferbo] Add strcpy model Reviewed By: mbouaziz Differential Revision: D13800678 fbshipit-source-id: 7816ecc4b --- .../src/bufferoverrun/bufferOverrunModels.ml | 25 ++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 4 ++ .../codetoanalyze/c/bufferoverrun/models.c | 57 +++++++++++++++++++ 3 files changed, 86 insertions(+) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 0b4d2e1fa..2774ed4cd 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -151,6 +151,30 @@ let strlen arr_exp = {exec; check= no_check} +let strcpy dest_exp src_exp = + let exec {integer_type_widths} ~ret:(id, _) mem = + let src_loc = Sem.eval_locs src_exp mem in + let dest_loc = Sem.eval_locs dest_exp mem in + mem + |> Dom.Mem.update_mem dest_loc (Dom.Mem.find_set src_loc mem) + |> Dom.Mem.update_mem (PowLoc.of_c_strlen dest_loc) (Dom.Mem.get_c_strlen src_loc mem) + |> Dom.Mem.add_stack (Loc.of_id id) (Sem.eval integer_type_widths dest_exp mem) + and check {integer_type_widths; location} mem cond_set = + let access_last_char = + let idx = Dom.Mem.get_c_strlen (Sem.eval_locs src_exp mem) mem in + let relation = Dom.Mem.get_relation mem in + let latest_prune = Dom.Mem.get_latest_prune mem in + fun arr cond_set -> + BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true + ~last_included:false ~latest_prune location cond_set + in + cond_set + |> access_last_char (Sem.eval integer_type_widths dest_exp mem) + |> access_last_char (Sem.eval integer_type_widths src_exp mem) + in + {exec; 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 = @@ -629,6 +653,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 + ; -"strcpy" <>$ capt_exp $+ capt_exp $+...$--> strcpy ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy ; -"snprintf" <>--> snprintf ; -"vsnprintf" <>--> vsnprintf diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index ba810a9ee..01750da4a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -196,6 +196,10 @@ codetoanalyze/c/bufferoverrun/models.c, memmove_bad4, 4, BUFFER_OVERRUN_L1, no_b codetoanalyze/c/bufferoverrun/models.c, memset_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 18446744073709551615 Size: 40] codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: 8 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, strcpy_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 4 Size: 4] +codetoanalyze/c/bufferoverrun/models.c, strcpy_contents_Bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 5 Size: 5] +codetoanalyze/c/bufferoverrun/models.c, strcpy_no_null_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 5 Size: 5] +codetoanalyze/c/bufferoverrun/models.c, strcpy_strlen_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 4 Size: 4] codetoanalyze/c/bufferoverrun/models.c, strncpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 44 Size: 40] 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] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/models.c b/infer/tests/codetoanalyze/c/bufferoverrun/models.c index 59800f720..f7da53c6b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/models.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c @@ -395,3 +395,60 @@ void strndup_3_Bad() { } } } + +void strcpy_Good() { + char src[5] = "test"; + char dst[10]; + strcpy(dst, src); +} + +void strcpy_Bad() { + char src[5] = "test"; + char dst[4]; + strcpy(dst, src); +} + +void strcpy_strlen_Good() { + char src[5] = "test"; + char dst[10]; + strcpy(dst, src); + int a[5]; + a[strlen(dst)] = 0; +} + +void strcpy_strlen_Bad() { + char src[5] = "test"; + char dst[10]; + strcpy(dst, src); + int a[4]; + a[strlen(dst)] = 0; +} + +void strcpy_contents_Good() { + char src[5] = "aaaa"; + char dst[5]; + strcpy(dst, src); + char c = dst[0]; + if (c >= 'a') { + int a[5]; + a[c - 'a' + 4] = 0; + } +} + +void strcpy_contents_Bad() { + char src[5] = "aaaa"; + char dst[5]; + strcpy(dst, src); + char c = dst[0]; + if (c >= 'a') { + int a[5]; + a[c - 'a' + 5] = 0; + } +} + +void strcpy_no_null_Bad() { + char src[5] = "test"; + src[4] = 'a'; + char dst[10]; + strcpy(dst, src); +}