From bc6829344f1bcf9a686aef8ba3e3b499c17a2630 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 22 Jan 2019 18:08:56 -0800 Subject: [PATCH] [inferbo] Change RiskyLibCall trace to non-final Reviewed By: mbouaziz Differential Revision: D13709906 fbshipit-source-id: 146ee0e08 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 2 +- .../src/bufferoverrun/bufferOverrunModels.ml | 12 +++-- infer/src/bufferoverrun/bufferOverrunTrace.ml | 50 +++++++++++++------ 3 files changed, 43 insertions(+), 21 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index f0888a28d..b4f15db5a 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -387,7 +387,7 @@ module Val = struct fun location ~f v -> { v with arrayblk= ArrayBlk.transform_length ~f v.arrayblk - ; traces= Trace.(Set.add_elem location Through) v.traces } + ; traces= Trace.(Set.add_elem location (through ~risky_fun:None)) v.traces } let set_array_stride : Z.t -> t -> t = diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index d17ca499e..76a7dea6c 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -232,9 +232,11 @@ let by_value = fun value -> {exec= exec ~value; check= no_check} -let by_value_with_final_trace final_trace = +let by_risky_value_from lib_fun = let exec ~value {location} ~ret mem = - let traces = Trace.(Set.singleton_final location final_trace) in + let traces = + Trace.(Set.add_elem location (through ~risky_fun:(Some lib_fun))) (Dom.Val.get_traces value) + in model_by_value {value with traces} ret mem in fun value -> {exec= exec ~value; check= no_check} @@ -296,9 +298,9 @@ let set_array_length array length_exp = {exec; check} -let snprintf = by_value_with_final_trace Trace.snprintf Dom.Val.Itv.nat +let snprintf = by_risky_value_from Trace.snprintf Dom.Val.Itv.nat -let vsnprintf = by_value_with_final_trace Trace.vsnprintf Dom.Val.Itv.nat +let vsnprintf = by_risky_value_from Trace.vsnprintf Dom.Val.Itv.nat module Split = struct let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem = @@ -306,7 +308,7 @@ module Split = struct let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in let size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in let vector_size_locs = Sem.eval_locs vector_exp mem |> PowLoc.append_field ~fn:size_field in - let f_trace _ traces = Trace.(Set.add_elem location Through) traces in + let f_trace _ traces = Trace.(Set.add_elem location (through ~risky_fun:None)) traces in Dom.Mem.transform_mem ~f:(Dom.Val.plus_a ~f_trace increment) vector_size_locs mem end diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index 76dfd4c32..cffc64dbb 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -12,10 +12,13 @@ module F = Format module BoTrace = struct type lib_fun = Snprintf | Vsnprintf [@@deriving compare] - type final = UnknownFrom of Typ.Procname.t option | RiskyLibCall of lib_fun - [@@deriving compare] + type final = UnknownFrom of Typ.Procname.t option [@@deriving compare] - type elem = ArrayDeclaration | Assign of PowLoc.t | Parameter of Loc.t | Through + type elem = + | ArrayDeclaration + | Assign of PowLoc.t + | Parameter of Loc.t + | Through of {risky_fun: lib_fun option} [@@deriving compare] type t = @@ -25,9 +28,9 @@ module BoTrace = struct | Call of {location: Location.t; length: int; caller: t; callee: t} [@@deriving compare] - let snprintf = RiskyLibCall Snprintf + let snprintf = Snprintf - let vsnprintf = RiskyLibCall Vsnprintf + let vsnprintf = Vsnprintf let length = function Empty -> 0 | Final _ -> 1 | Elem {length} | Call {length} -> length @@ -39,6 +42,8 @@ module BoTrace = struct let singleton location kind = add_elem location kind Empty + let through ~risky_fun = Through {risky_fun} + let call location ~caller ~callee = Call {location; length= 1 + length caller + length callee; caller; callee} @@ -62,8 +67,6 @@ module BoTrace = struct 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,8 +76,9 @@ module BoTrace = struct F.fprintf f "Assign `%a`" PowLoc.pp locs | Parameter loc -> F.fprintf f "Parameter `%a`" Loc.pp loc - | Through -> - F.pp_print_string f "Through" + | Through {risky_fun} -> + F.pp_print_string f "Through" ; + if Option.is_some risky_fun then F.pp_print_string f " RiskyLibCall" let rec pp f = function @@ -101,9 +105,23 @@ module BoTrace = struct final_exists ~f caller || final_exists ~f callee - let has_unknown = final_exists ~f:(function UnknownFrom _ -> true | RiskyLibCall _ -> false) + let has_unknown = final_exists ~f:(function UnknownFrom _ -> true) + + let elem_has_risky = function + | ArrayDeclaration | Assign _ | Parameter _ -> + false + | Through {risky_fun} -> + Option.is_some risky_fun + + + let rec has_risky = function + | Empty | Final _ -> + false + | Elem {kind; from} -> + elem_has_risky kind || has_risky from + | Call {caller; callee} -> + has_risky caller || has_risky callee - let has_risky = final_exists ~f:(function UnknownFrom _ -> false | RiskyLibCall _ -> true) let exists_str ~f = let rec helper = function @@ -127,8 +145,6 @@ module BoTrace = struct 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 @@ -138,8 +154,12 @@ module BoTrace = struct "Assignment" | Parameter loc -> if Loc.is_pretty loc then F.asprintf "Parameter `%a`" Loc.pp loc else "" - | Through -> - "Through" + | Through {risky_fun} -> ( + match risky_fun with + | None -> + "Through" + | Some f -> + F.asprintf "Risky value from: %a" pp_lib_fun f ) let rec make_err_trace depth t tail =