[inferbo] Add strcpy model

Reviewed By: mbouaziz

Differential Revision: D13800678

fbshipit-source-id: 7816ecc4b

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

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, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
 codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 18446744073709551615 Size: 40]
 codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset added: 8 Size: 4]
+codetoanalyze/c/bufferoverrun/models.c, strcpy_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 4 Size: 4]
+codetoanalyze/c/bufferoverrun/models.c, strcpy_contents_Bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
+codetoanalyze/c/bufferoverrun/models.c, strcpy_no_null_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
+codetoanalyze/c/bufferoverrun/models.c, strcpy_strlen_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 4 Size: 4]
 codetoanalyze/c/bufferoverrun/models.c, strncpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
 codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 44 Size: 40]
 codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 18446744073709551615 Size: 40]

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);
+}