[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

@@ -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

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"

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, [<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]
 codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 8 Size: 4]
+codetoanalyze/c/bufferoverrun/models.c, strncpy_contents_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_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,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, [<Offset trace>,Array declaration,<Length trace>,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, [<Offset trace>,Array declaration,<Length trace>,Array declaration,Array access: Offset: 14 Size: 10]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]

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