[inferbo] Ignore encoding error in the snprintf model

Reviewed By: mbouaziz

Differential Revision: D13588979

fbshipit-source-id: 4cd9de71d

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -262,9 +262,9 @@ let set_array_length array length_exp =
   {exec; check}
 
 
-let snprintf = by_value_with_final_trace Trace.snprintf Dom.Val.Itv.top
+let snprintf = by_value_with_final_trace Trace.snprintf Dom.Val.Itv.nat
 
-let vsnprintf = by_value_with_final_trace Trace.vsnprintf Dom.Val.Itv.top
+let vsnprintf = by_value_with_final_trace Trace.vsnprintf Dom.Val.Itv.nat
 
 module Split = struct
   let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem =

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

@@ -85,16 +85,16 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Good, 2, CONDITION_ALWAYS_
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal2_Good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
-codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, +oo] Size: 1024]
-codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, INTEGER_OVERFLOW_R2, no_bucket, ERROR, [<LHS trace>,Risky value from: snprintf,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, +oo] Size: 1024]
-codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024]
-codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, INTEGER_OVERFLOW_R2, no_bucket, ERROR, [<LHS trace>,Risky value from: vsnprintf,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, length2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, length3_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, length_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, size_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
-codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [-oo, +oo] Size: 1024]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [0, +oo] Size: 1024]
-codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [-oo, +oo] Size: 1024]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [0, +oo] Size: 1024]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Good, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]

infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp

@@ -71,6 +71,22 @@ std::string to_string2_Good(const char* fmt, ...) {
   return std::string(buf, n);
 }
 
+/* Inferbo's model ignores the encoding errors for less noise of
+   analysis results.  While [vsnprintf] returns a nagative number when
+   an encoding error, it is less likely to lead to a security
+   problem.  */
+std::string to_string3_Bad_FN(const char* fmt, ...) {
+  char buf[1024];
+  va_list args;
+  va_start(args, fmt);
+  int n = vsnprintf(buf, sizeof(buf), fmt, args);
+  va_end(args);
+  if (n > sizeof(buf)) {
+    n = sizeof(buf);
+  }
+  return std::string(buf, n);
+}
+
 void empty_Good(std::string s) {
   if (s.empty()) {
     if (!s.empty()) {