[inferbo] XML escape in L.d_printfln

Reviewed By: mbouaziz

Differential Revision: D13527168

fbshipit-source-id: 0ae420cbb

infer/src/base/IssueType.ml

@@ -112,6 +112,8 @@ let buffer_overrun_l4 = from_string ~enabled:false "BUFFER_OVERRUN_L4"
 
 let buffer_overrun_l5 = from_string ~enabled:false "BUFFER_OVERRUN_L5"
 
+let buffer_overrun_r2 = from_string "BUFFER_OVERRUN_R2"
+
 let buffer_overrun_s2 = from_string "BUFFER_OVERRUN_S2"
 
 let buffer_overrun_u5 = from_string ~enabled:false "BUFFER_OVERRUN_U5"
@@ -291,6 +293,8 @@ let integer_overflow_l2 = from_string "INTEGER_OVERFLOW_L2"
 
 let integer_overflow_l5 = from_string ~enabled:false "INTEGER_OVERFLOW_L5"
 
+let integer_overflow_r2 = from_string "INTEGER_OVERFLOW_R2"
+
 let integer_overflow_u5 = from_string ~enabled:false "INTEGER_OVERFLOW_U5"
 
 let interface_not_thread_safe = from_string "INTERFACE_NOT_THREAD_SAFE"

infer/src/base/IssueType.mli

@@ -56,6 +56,8 @@ val buffer_overrun_l4 : t
 
 val buffer_overrun_l5 : t
 
+val buffer_overrun_r2 : t
+
 val buffer_overrun_s2 : t
 
 val buffer_overrun_u5 : t
@@ -197,6 +199,8 @@ val integer_overflow_l2 : t
 
 val integer_overflow_l5 : t
 
+val integer_overflow_r2 : t
+
 val integer_overflow_u5 : t
 
 val interface_not_thread_safe : t

infer/src/base/Logging.ml

@@ -446,7 +446,7 @@ let d_printf ?color fmt = F.kasprintf (d_str ?color) fmt
 
 let d_printfln ?color fmt = F.kasprintf (d_strln ?color) fmt
 
-let d_printfln_escaped fmt = F.kasprintf (fun s -> d_strln (Escape.escape_xml s)) fmt
+let d_printfln_escaped ?color fmt = F.kasprintf (fun s -> d_strln ?color (Escape.escape_xml s)) fmt
 
 (** dump an indentation *)
 let d_indent indent =

infer/src/base/Logging.mli

@@ -112,7 +112,7 @@ val d_printf : ?color:Pp.color -> ('a, F.formatter, unit) format -> 'a
 
 val d_printfln : ?color:Pp.color -> ('a, F.formatter, unit) format -> 'a
 
-val d_printfln_escaped : ('a, F.formatter, unit) format -> 'a
+val d_printfln_escaped : ?color:Pp.color -> ('a, F.formatter, unit) format -> 'a
 
 val d_error : string -> unit
 (** dump an error string *)

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -171,14 +171,15 @@ module TransferFunctions = struct
               let v = Dom.Mem.find (Loc.of_pvar pvar) callee_mem in
               Dom.Mem.add_stack (Loc.of_id id) v mem
           | None ->
-              L.d_printfln "/!\\ Initializer of global constant %a has no inferbo payload"
+              L.d_printfln_escaped "/!\\ Initializer of global constant %a has no inferbo payload"
                 (Pvar.pp Pp.text) pvar ;
               Dom.Mem.add_unknown_from id ~callee_pname ~location mem )
         | None ->
-            L.d_printfln "/!\\ Unknown initializer of global constant %a" (Pvar.pp Pp.text) pvar ;
+            L.d_printfln_escaped "/!\\ Unknown initializer of global constant %a" (Pvar.pp Pp.text)
+              pvar ;
             Dom.Mem.add_unknown_from id ~callee_pname ~location mem )
       | None ->
-          L.d_printfln "/!\\ Failed to get initializer name of global constant %a"
+          L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a"
             (Pvar.pp Pp.text) pvar ;
           Dom.Mem.add_unknown id ~location mem )
     | Load (id, exp, _, _) ->
@@ -244,10 +245,11 @@ module TransferFunctions = struct
                   payload location
             | None ->
                 (* This may happen for procedures with a biabduction model. *)
-                L.d_printfln "/!\\ Call to %a has no inferbo payload" Typ.Procname.pp callee_pname ;
+                L.d_printfln_escaped "/!\\ Call to %a has no inferbo payload" Typ.Procname.pp
+                  callee_pname ;
                 Dom.Mem.add_unknown_from id ~callee_pname ~location mem )
           | None ->
-              L.d_printfln "/!\\ Unknown call to %a" Typ.Procname.pp callee_pname ;
+              L.d_printfln_escaped "/!\\ Unknown call to %a" Typ.Procname.pp callee_pname ;
               if is_external callee_pname then (
                 L.(debug BufferOverrun Verbose)
                   "/!\\ External call to unknown  %a \n\n" Typ.Procname.pp callee_pname ;
@@ -259,7 +261,7 @@ module TransferFunctions = struct
               else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) )
     | Call ((id, _), fun_exp, _, location, _) ->
         let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
-        let () = L.d_printfln "/!\\ Call to non-const function %a" Exp.pp fun_exp in
+        L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ;
         Dom.Mem.add_unknown id ~location mem
     | ExitScope (dead_vars, _) ->
         Dom.Mem.remove_temps (List.filter_map dead_vars ~f:Var.get_ident) mem

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -257,7 +257,7 @@ module Val = struct
   let warn_against_pruning_multiple_values : t -> t =
    fun x ->
     if x.represents_multiple_values && Config.write_html then
-      L.d_printfln ~color:Pp.Red "Pruned %a that represents multiple values" pp x ;
+      L.d_printfln_escaped ~color:Pp.Red "Pruned %a that represents multiple values" pp x ;
     x
 
 
@@ -370,7 +370,7 @@ module Val = struct
 
   let of_path tenv ~may_last_field integer_type_widths location typ path =
     let is_java = Language.curr_language_is Java in
-    L.d_printfln "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ
+    L.d_printfln_escaped "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ
       (if may_last_field then ", may_last_field" else "")
       (if is_java then ", is_java" else "") ;
     match typ.Typ.desc with
@@ -453,15 +453,15 @@ module Val = struct
    fun ~default {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} l ->
     match Loc.get_path l with
     | None ->
-        L.d_printfln "Val.on_demand for %a -> no path" Loc.pp l ;
+        L.d_printfln_escaped "Val.on_demand for %a -> no path" Loc.pp l ;
         default
     | Some path -> (
       match typ_of_param_path path with
       | None ->
-          L.d_printfln "Val.on_demand for %a -> no type" Loc.pp l ;
+          L.d_printfln_escaped "Val.on_demand for %a -> no type" Loc.pp l ;
           default
       | Some typ ->
-          L.d_printfln "Val.on_demand for %a" Loc.pp l ;
+          L.d_printfln_escaped "Val.on_demand for %a" Loc.pp l ;
           let may_last_field = may_last_field path in
           let path = OndemandEnv.canonical_path typ_of_param_path path in
           of_path tenv ~may_last_field integer_type_widths entry_location typ path )
@@ -993,9 +993,9 @@ module MemReach = struct
   let update_mem : PowLoc.t -> Val.t -> t -> t =
    fun ploc v s ->
     if can_strong_update ploc then strong_update ploc v s
-    else
-      let () = L.d_printfln "Weak update for %a <- %a" PowLoc.pp ploc Val.pp v in
-      weak_update ploc v s
+    else (
+      L.d_printfln_escaped "Weak update for %a <- %a" PowLoc.pp ploc Val.pp v ;
+      weak_update ploc v s )
 
 
   let remove_temp : Ident.t -> t -> t =

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -190,6 +190,14 @@ let by_value =
   fun value -> {exec= exec ~value; check= no_check}
 
 
+let by_value_with_final_trace final_trace =
+  let exec ~value {location} ~ret mem =
+    let traces = Trace.(Set.singleton_final location final_trace) in
+    model_by_value {value with traces} ret mem
+  in
+  fun value -> {exec= exec ~value; check= no_check}
+
+
 let bottom =
   let exec _model_env ~ret:_ _mem = Bottom in
   {exec; check= no_check}
@@ -246,6 +254,10 @@ let set_array_length array length_exp =
   {exec; check}
 
 
+let snprintf = by_value_with_final_trace Trace.snprintf Dom.Val.Itv.top
+
+let vsnprintf = by_value_with_final_trace Trace.vsnprintf Dom.Val.Itv.top
+
 module Split = struct
   let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem =
     let increment = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in
@@ -304,7 +316,7 @@ module StdArray = struct
 
   let no_model =
     let exec {pname} ~ret:_ mem =
-      L.d_printfln "No model for %a" Typ.Procname.pp pname ;
+      L.d_printfln_escaped "No model for %a" Typ.Procname.pp pname ;
       mem
     in
     {exec; check= no_check}
@@ -469,6 +481,8 @@ module Call = struct
       ; -"memmove" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy
       ; -"memset" <>$ capt_exp $+ any_arg $+ capt_exp $!--> memset
       ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy
+      ; -"snprintf" <>--> snprintf
+      ; -"vsnprintf" <>--> vsnprintf
       ; -"boost" &:: "split"
         $ capt_arg_of_typ (-"std" &:: "vector")
         $+ any_arg $+ any_arg $+? any_arg $--> Boost.Split.std_vector

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -651,13 +651,26 @@ module ConditionTrace = struct
 
   let has_unknown ct = ValTrace.Issue.has_unknown ct.val_traces
 
-  let check issue_type_u5 : _ t0 -> IssueType.t option =
-   fun ct -> if has_unknown ct then Some issue_type_u5 else None
+  let has_risky ct = ValTrace.Issue.has_risky ct.val_traces
 
+  let check ~issue_type_u5 ~issue_type_r2 : _ t0 -> IssueType.t option =
+   fun ct ->
+    if has_risky ct then Some issue_type_r2
+    else if has_unknown ct then Some issue_type_u5
+    else None
 
-  let check_buffer_overrun ct = check IssueType.buffer_overrun_u5 ct
 
-  let check_integer_overflow ct = check IssueType.integer_overflow_u5 ct
+  let check_buffer_overrun ct =
+    let issue_type_u5 = IssueType.buffer_overrun_u5 in
+    let issue_type_r2 = IssueType.buffer_overrun_r2 in
+    check ~issue_type_u5 ~issue_type_r2 ct
+
+
+  let check_integer_overflow ct =
+    let issue_type_u5 = IssueType.integer_overflow_u5 in
+    let issue_type_r2 = IssueType.integer_overflow_r2 in
+    check ~issue_type_u5 ~issue_type_r2 ct
+
 
   let for_summary : _ t0 -> summary_t = fun ct -> {ct with cond_trace= ()}
 end
@@ -813,19 +826,19 @@ module ConditionSet = struct
     let rec aux acc ~same = function
       | [] ->
           if Config.bo_debug >= 3 then
-            L.d_printfln "[InferboPO] Adding new condition %a@." pp_cond new_ ;
+            L.d_printfln_escaped "[InferboPO] Adding new condition %a@." pp_cond new_ ;
           if same then new_ :: condset else new_ :: acc
       | existing :: rest as existings -> (
         match try_merge ~existing ~new_ with
         | `DoNotAddAndStop ->
             if Config.bo_debug >= 3 then
-              L.d_printfln "[InferboPO] Not adding condition %a (because of existing %a)@." pp_cond
-                new_ pp_cond existing ;
+              L.d_printfln_escaped "[InferboPO] Not adding condition %a (because of existing %a)@."
+                pp_cond new_ pp_cond existing ;
             if same then condset else List.rev_append acc existings
         | `RemoveExistingAndContinue ->
             if Config.bo_debug >= 3 then
-              L.d_printfln "[InferboPO] Removing condition %a (because of new %a)@." pp_cond
-                existing pp_cond new_ ;
+              L.d_printfln_escaped "[InferboPO] Removing condition %a (because of new %a)@."
+                pp_cond existing pp_cond new_ ;
             aux acc ~same:false rest
         | `KeepExistingAndContinue ->
             aux (existing :: acc) ~same rest )

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -343,10 +343,10 @@ let rec eval_sympath_partial params p mem =
   match p with
   | Symb.SymbolPath.Pvar x -> (
     try ParamBindings.find x params with Caml.Not_found ->
-      L.d_printfln "Symbol %a is not found in parameters." (Pvar.pp Pp.text) x ;
+      L.d_printfln_escaped "Symbol %a is not found in parameters." (Pvar.pp Pp.text) x ;
       Val.Itv.top )
   | Symb.SymbolPath.Callsite {cs} ->
-      L.d_printfln "Symbol for %a is not expected to be in parameters." Typ.Procname.pp
+      L.d_printfln_escaped "Symbol for %a is not expected to be in parameters." Typ.Procname.pp
         (CallSite.pname cs) ;
       Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem
   | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ ->
@@ -368,7 +368,7 @@ and eval_locpath params p mem =
         PowLoc.append_field ~fn locs
   in
   if PowLoc.is_empty res then (
-    L.d_printfln "Location value for %a is not found." Symb.SymbolPath.pp_partial p ;
+    L.d_printfln_escaped "Location value for %a is not found." Symb.SymbolPath.pp_partial p ;
     PowLoc.unknown )
   else res
 

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -10,7 +10,10 @@ open AbsLoc
 module F = Format
 
 module BoTrace = struct
-  type final = UnknownFrom of Typ.Procname.t option [@@deriving compare]
+  type lib_fun = Snprintf | Vsnprintf [@@deriving compare]
+
+  type final = UnknownFrom of Typ.Procname.t option | RiskyLibCall of lib_fun
+  [@@deriving compare]
 
   type elem = ArrayDeclaration | Assign | Parameter of Loc.t | Through [@@deriving compare]
 
@@ -21,6 +24,10 @@ module BoTrace = struct
     | Call of {location: Location.t; length: int; caller: t; callee: t}
   [@@deriving compare]
 
+  let snprintf = RiskyLibCall Snprintf
+
+  let vsnprintf = RiskyLibCall Vsnprintf
+
   let length = function Empty -> 0 | Final _ -> 1 | Elem {length} | Call {length} -> length
 
   let compare t1 t2 = [%compare: int * t] (length t1, t1) (length t2, t2)
@@ -44,9 +51,18 @@ module BoTrace = struct
 
   let pp_location = Location.pp_file_pos
 
+  let pp_lib_fun f = function
+    | Snprintf ->
+        F.fprintf f "snprintf"
+    | Vsnprintf ->
+        F.fprintf f "vsnprintf"
+
+
   let pp_final f = function
     | UnknownFrom pname_opt ->
         F.fprintf f "UnknownFrom `%a`" pp_pname_opt pname_opt
+    | RiskyLibCall lib_fun ->
+        F.fprintf f "RiskyLibCall `%a`" pp_lib_fun lib_fun
 
 
   let pp_elem f = function
@@ -73,20 +89,26 @@ module BoTrace = struct
 
   and pp_arrow f = function Empty -> () | t -> F.fprintf f "%a -> " pp t
 
-  let rec has_unknown = function
+  let rec final_exists ~f = function
     | Empty ->
         false
-    | Final {kind= UnknownFrom _} ->
-        true
+    | Final {kind= final} ->
+        f final
     | Elem {from} ->
-        has_unknown from
+        final_exists ~f from
     | Call {caller; callee} ->
-        has_unknown caller || has_unknown callee
+        final_exists ~f caller || final_exists ~f callee
 
 
+  let has_unknown = final_exists ~f:(function UnknownFrom _ -> true | RiskyLibCall _ -> false)
+
+  let has_risky = final_exists ~f:(function UnknownFrom _ -> false | RiskyLibCall _ -> true)
+
   let final_err_desc = function
     | UnknownFrom pname_opt ->
         F.asprintf "Unknown value from: %a" pp_pname_opt pname_opt
+    | RiskyLibCall lib_fun ->
+        F.asprintf "Risky value from: %a" pp_lib_fun lib_fun
 
 
   let elem_err_desc = function
@@ -162,6 +184,8 @@ module Set = struct
 
   let has_unknown t = exists BoTrace.has_unknown t
 
+  let has_risky t = exists BoTrace.has_risky t
+
   let make_err_trace depth set tail =
     if is_empty set then tail else BoTrace.make_err_trace depth (choose_shortest set) tail
 
@@ -194,14 +218,18 @@ module Issue = struct
     Call {location; length= 1 + Set.length caller + length callee; caller; callee}
 
 
-  let rec has_unknown = function
+  let rec has_common ~f = function
     | Elem {from} ->
-        Set.has_unknown from
+        f from
     | Binary {left; right} ->
-        Set.has_unknown left || Set.has_unknown right
+        f left || f right
     | Call {caller; callee} ->
-        Set.has_unknown caller || has_unknown callee
+        f caller || has_common ~f callee
+
+
+  let has_unknown = has_common ~f:Set.has_unknown
 
+  let has_risky = has_common ~f:Set.has_risky
 
   let binary_labels = function ArrayAccess -> ("Offset", "Length") | Binop -> ("LHS", "RHS")
 

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

@@ -77,6 +77,10 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
+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, 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: [-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/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

@@ -0,0 +1,72 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <string>
+
+char last_char1_Bad(char* s, int i) {
+  char buf[1024];
+  int n = snprintf(buf, sizeof(buf), "%s%d", s, i);
+  return buf[n - 1];
+}
+
+char last_char1_Good(char* s, int i) {
+  char buf[1024];
+  int n = snprintf(buf, sizeof(buf), "%s%d", s, i);
+  if (n > 0 && n <= sizeof(buf)) {
+    return buf[n - 1];
+  } else {
+    return '\0';
+  }
+}
+
+char last_char2_Bad(const char* fmt, ...) {
+  char buf[1024];
+  va_list args;
+  va_start(args, fmt);
+  int n = vsnprintf(buf, sizeof(buf), fmt, args);
+  va_end(args);
+  return buf[n - 1];
+}
+
+std::string to_string1_Bad_FN(char* s, int i) {
+  char buf[1024];
+  int n = snprintf(buf, sizeof(buf), "%s%d", s, i);
+  return std::string(buf, n);
+}
+
+std::string to_string1_Good(char* s, int i) {
+  char buf[1024];
+  int n = snprintf(buf, sizeof(buf), "%s%d", s, i);
+  if (n < 0) {
+    return NULL;
+  } else if (n > sizeof(buf)) {
+    n = sizeof(buf);
+  }
+  return std::string(buf, n);
+}
+
+std::string to_string2_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);
+  return std::string(buf, n);
+}
+
+std::string to_string2_Good(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 < 0) {
+    return NULL;
+  } else if (n > sizeof(buf)) {
+    n = sizeof(buf);
+  }
+  return std::string(buf, n);
+}