[inferbo] Add strndup model

Reviewed By: mbouaziz

Differential Revision: D13668557

fbshipit-source-id: e6d3d4161

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -204,6 +204,34 @@ let placement_new size_exp (src_exp1, t1) src_arg2_opt =
       {exec; check= no_check}
 
 
+let strndup src_exp length_exp =
+  let exec ({pname; node_hash; location; integer_type_widths} as model_env) ~ret:((id, _) as ret)
+      mem =
+    let v =
+      let src_strlen = Dom.Mem.get_c_strlen (Sem.eval_locs src_exp mem) mem in
+      let length = Sem.eval integer_type_widths length_exp mem in
+      let size = Itv.incr (Itv.min_sem (Dom.Val.get_itv src_strlen) (Dom.Val.get_itv length)) in
+      let allocsite =
+        let represents_multiple_values = not (Itv.is_one size) in
+        Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None
+          ~represents_multiple_values
+      in
+      let traces =
+        Trace.Set.join (Dom.Val.get_traces src_strlen) (Dom.Val.get_traces length)
+        |> Trace.Set.add_elem location (Trace.through ~risky_fun:(Some Trace.strndup))
+        |> Trace.Set.add_elem location ArrayDeclaration
+      in
+      Dom.Val.of_c_array_alloc allocsite
+        ~stride:(Some (integer_type_widths.char_width / 8))
+        ~offset:Itv.zero ~size ~traces
+    in
+    mem
+    |> Dom.Mem.add_stack (Loc.of_id id) v
+    |> (strncpy (Exp.Var id) src_exp length_exp).exec model_env ~ret
+  in
+  {exec; check= no_check}
+
+
 let inferbo_min e1 e2 =
   let exec {integer_type_widths} ~ret:(id, _) mem =
     let i1 = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_itv in
@@ -604,6 +632,7 @@ module Call = struct
       ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy
       ; -"snprintf" <>--> snprintf
       ; -"vsnprintf" <>--> vsnprintf
+      ; -"strndup" <>$ capt_exp $+ capt_exp $+...$--> strndup
       ; -"boost" &:: "split"
         $ capt_arg_of_typ (-"std" &:: "vector")
         $+ any_arg $+ any_arg $+? any_arg $--> Boost.Split.std_vector

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -10,7 +10,7 @@ open AbsLoc
 module F = Format
 
 module BoTrace = struct
-  type lib_fun = Snprintf | Vsnprintf [@@deriving compare]
+  type lib_fun = Snprintf | Strndup | Vsnprintf [@@deriving compare]
 
   type final = UnknownFrom of Typ.Procname.t option [@@deriving compare]
 
@@ -30,6 +30,8 @@ module BoTrace = struct
 
   let snprintf = Snprintf
 
+  let strndup = Strndup
+
   let vsnprintf = Vsnprintf
 
   let length = function Empty -> 0 | Final _ -> 1 | Elem {length} | Call {length} -> length
@@ -60,6 +62,8 @@ module BoTrace = struct
   let pp_lib_fun f = function
     | Snprintf ->
         F.fprintf f "snprintf"
+    | Strndup ->
+        F.fprintf f "strndup"
     | Vsnprintf ->
         F.fprintf f "vsnprintf"
 

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

@@ -204,6 +204,10 @@ codetoanalyze/c/bufferoverrun/models.c, strncpy_contents_Bad, 5, BUFFER_OVERRUN_
 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/models.c, strndup_1_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Risky value from: strndup,Array declaration,Assignment,Array access: Offset: [0, 99] Size: 13]
+codetoanalyze/c/bufferoverrun/models.c, strndup_2_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Risky value from: strndup,Array declaration,Assignment,Array access: Offset: [0, 11] Size: 6]
+codetoanalyze/c/bufferoverrun/models.c, strndup_3_Bad, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/c/bufferoverrun/models.c, strndup_3_Bad, 7, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Assignment,Risky value from: strndup,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: 6]
 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

@@ -333,3 +333,65 @@ void strncpy_no_null_4_Bad() {
   int a[10];
   a[strlen(dst)] = 0;
 }
+
+void strndup_1_Good() {
+  char s1[] = "Hello Infer!";
+  int len = strlen(s1);
+  char* s2 = strndup(s1, len);
+  for (int i = 0; i < len; i++) {
+    s2[i] = 'a';
+  }
+}
+
+void strndup_1_Bad() {
+  char s1[] = "Hello Infer!";
+  int len = 100;
+  char* s2 = strndup(s1, len);
+  for (int i = 0; i < len; i++) {
+    s2[i] = 'a';
+  }
+}
+
+void strndup_2_Good() {
+  char s1[] = "Hello Infer!";
+  int len = strlen(s1);
+  s1[5] = '\0';
+  char* s2 = strndup(s1, len);
+  for (int i = 0; i < strlen(s2); i++) {
+    s2[i] = 'a';
+  }
+}
+
+void strndup_2_Bad() {
+  char s1[] = "Hello Infer!";
+  int len = strlen(s1);
+  s1[5] = '\0';
+  char* s2 = strndup(s1, len);
+  for (int i = 0; i < len; i++) {
+    s2[i] = 'a';
+  }
+}
+
+void strndup_3_Good() {
+  int size = unknown();
+  if (size >= 10) {
+    char* s1 = (char*)malloc(sizeof(char) * size);
+    s1[5] = '\0';
+    char* s2 = strndup(s1, size - 1);
+    for (int i = 0; i < strlen(s2); i++) {
+      s2[i] = 'a';
+    }
+  }
+}
+
+void strndup_3_Bad() {
+  int size = unknown();
+  if (size >= 10) {
+    char* s1 = (char*)malloc(sizeof(char) * size);
+    s1[5] = '\0';
+    char* s2 = strndup(s1, size - 1);
+    for (int i = 0; i < size - 1; i++) {
+      s2[i] = 'a';
+    }
+  }
+}