From 5a5f83a492933d856133696594dbdaf5d00fdcc0 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Sat, 2 Feb 2019 22:50:44 -0800 Subject: [PATCH] [inferbo] Add strcat model Reviewed By: mbouaziz Differential Revision: D13915381 fbshipit-source-id: e385130f3 --- .../src/bufferoverrun/bufferOverrunModels.ml | 44 +++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 2 + .../codetoanalyze/c/bufferoverrun/models.c | 28 ++++++++++++ 3 files changed, 74 insertions(+) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 6fe643a9d..fb01dd1c5 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -185,6 +185,49 @@ let strncpy dest_exp src_exp size_exp = {exec; check= memcpy_check} +let strcat 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 + let new_contents = + let src_contents = Dom.Mem.find_set src_loc mem in + let dest_contents = Dom.Mem.find_set dest_loc mem in + Dom.Val.join dest_contents src_contents + in + let src_strlen = Dom.Mem.get_c_strlen src_loc mem in + let new_strlen = + let dest_strlen = Dom.Mem.get_c_strlen dest_loc mem in + Dom.Val.plus_a dest_strlen src_strlen + in + mem + |> Dom.Mem.update_mem dest_loc new_contents + |> Dom.Mem.update_mem (PowLoc.of_c_strlen dest_loc) new_strlen + |> 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 arr idx cond_set = + let relation = Dom.Mem.get_relation mem in + let latest_prune = Dom.Mem.get_latest_prune mem in + BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true + ~last_included:false ~latest_prune location cond_set + in + let src_strlen = + let str_loc = Sem.eval_locs src_exp mem in + Dom.Mem.get_c_strlen str_loc mem + in + let new_strlen = + let dest_strlen = + let dest_loc = Sem.eval_locs dest_exp mem in + Dom.Mem.get_c_strlen dest_loc mem + in + Dom.Val.plus_a dest_strlen src_strlen + in + cond_set + |> access_last_char (Sem.eval integer_type_widths dest_exp mem) new_strlen + |> access_last_char (Sem.eval integer_type_widths src_exp mem) src_strlen + in + {exec; 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 @@ -688,6 +731,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 + ; -"strcat" <>$ capt_exp $+ capt_exp $+...$--> strcat ; -"strcpy" <>$ capt_exp $+ capt_exp $+...$--> strcpy ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy ; -"snprintf" <>--> snprintf diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 2875db447..6311bf755 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -196,6 +196,8 @@ 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, strcat_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 8 Size: 8] +codetoanalyze/c/bufferoverrun/models.c, strcat_strlen_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 8 Size: 8] 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_literal_string_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 4 Size: 4] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/models.c b/infer/tests/codetoanalyze/c/bufferoverrun/models.c index ec80321e0..fa9a59ca0 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/models.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c @@ -462,3 +462,31 @@ void strcpy_no_null_Bad() { char dst[10]; strcpy(dst, src); } + +void strcat_Good() { + char str[8]; + strcpy(str, "abc"); + strcat(str, "defg"); +} + +void strcat_Bad() { + char str[8]; + strcpy(str, "abc"); + strcat(str, "defgh"); +} + +void strcat_strlen_Good() { + char str[8]; + strcpy(str, "abc"); + strcat(str, "defg"); + int a[8]; + a[strlen(str)] = 0; +} + +void strcat_strlen_Bad() { + char str[20]; + strcpy(str, "abc"); + strcat(str, "defgh"); + int a[8]; + a[strlen(str)] = 0; +}