Added inferBO model for the C memset function.

Reviewed By: mbouaziz

Differential Revision: D9833430

fbshipit-source-id: 9ed377789

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -136,6 +136,14 @@ let memcpy dest_exp src_exp size_exp =
   {exec; check}
 
 
+let memset arr_exp size_exp =
+  let exec _ ~ret:_ mem = mem
+  and check {location} mem cond_set =
+    BoUtils.Check.lindex_byte ~array_exp:arr_exp ~byte_index_exp:size_exp mem location cond_set
+  in
+  {exec; check}
+
+
 let realloc src_exp size_exp =
   let exec {location; tenv} ~ret:(id, _) mem =
     let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in
@@ -477,6 +485,7 @@ module Call = struct
       ; -"strlen" <>--> by_value Dom.Val.Itv.nat
       ; -"memcpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy
       ; -"memmove" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy
+      ; -"memset" <>$ capt_exp $+ any_arg $+ capt_exp $!--> memset
       ; -"boost" &:: "split"
         $ capt_arg_of_typ (-"std" &:: "vector")
         $+ any_arg $+ any_arg $+? any_arg $--> Boost.Split.std_vector

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -74,6 +74,9 @@ codetoanalyze/c/bufferoverrun/models.c, memmove_bad1, 3, BUFFER_OVERRUN_L1, no_b
 codetoanalyze/c/bufferoverrun/models.c, memmove_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40]
 codetoanalyze/c/bufferoverrun/models.c, memmove_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40]
 codetoanalyze/c/bufferoverrun/models.c, memmove_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4]
+codetoanalyze/c/bufferoverrun/models.c, memset_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40]
+codetoanalyze/c/bufferoverrun/models.c, memset_bad2, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40]
+codetoanalyze/c/bufferoverrun/models.c, memset_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 8 Size: 4]
 codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] Size: 1024]

infer/tests/codetoanalyze/c/bufferoverrun/models.c

@@ -145,3 +145,39 @@ void memmove_good4() {
   int dst[3];
   memmove(dst, src, sizeof(dst));
 }
+
+void memset_bad1() {
+  int arr[10];
+  memset(arr, 0, 44);
+}
+
+void memset_bad2() {
+  int arr[10];
+  memset(arr, 0, -1);
+}
+
+void memset_bad3() {
+  int arr[1];
+  int* dst = &arr[0];
+  memset(dst, 0, sizeof(dst));
+}
+
+void memset_good1() {
+  int arr[10];
+  memset(arr, 0, 40);
+}
+
+void memset_good2() {
+  int arr[10];
+  memset(arr, 0, 0);
+}
+
+void memset_good3() {
+  int arr[10];
+  memset(arr, 0, 20);
+}
+
+void memset_good4() {
+  int arr[10];
+  memset(arr, 0, sizeof(arr));
+}