From d6494f725b8c267dd4f5b52df65edc5d65d4c02a Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 8 Jan 2019 18:49:11 -0800 Subject: [PATCH] [inferbo] Prepare supressing intended integer overflow Reviewed By: mbouaziz Differential Revision: D13595958 fbshipit-source-id: 39aef1d1b --- .../src/bufferoverrun/bufferOverrunChecker.ml | 4 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 4 +- .../bufferOverrunProofObligations.ml | 160 +++++++++--------- infer/src/bufferoverrun/bufferOverrunTrace.ml | 9 +- 4 files changed, 90 insertions(+), 87 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 5b5c52f82..daf493d68 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -191,7 +191,9 @@ module TransferFunctions = struct BoUtils.Exec.decl_string pname ~node_hash integer_type_widths location locs s mem | Store (exp1, _, exp2, location) -> let locs = Sem.eval_locs exp1 mem in - let v = Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location in + let v = + Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location locs + in let mem = let sym_exps = Dom.Relation.SymExp.of_exps diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 005744555..aa687473a 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -357,8 +357,8 @@ module Val = struct |> normalize - let add_assign_trace_elem location x = - let traces = Trace.(Set.add_elem location Assign) x.traces in + let add_assign_trace_elem location locs x = + let traces = Trace.(Set.add_elem location (Assign locs)) x.traces in {x with traces} diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 80411165a..161e0ba30 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -16,6 +16,86 @@ module MF = MarkupFormatter module Relation = BufferOverrunDomainRelation module ValTrace = BufferOverrunTrace +module ConditionTrace = struct + type intra_cond_trace = Intra | Inter of {call_site: Location.t; callee_pname: Typ.Procname.t} + [@@deriving compare] + + type 'cond_trace t0 = + {cond_trace: 'cond_trace; issue_location: Location.t; val_traces: ValTrace.Issue.t} + [@@deriving compare] + + type t = intra_cond_trace t0 [@@deriving compare] + + type summary_t = unit t0 + + let pp_summary : F.formatter -> _ t0 -> unit = + fun fmt ct -> F.fprintf fmt "at %a" Location.pp_file_pos ct.issue_location + + + let pp : F.formatter -> t -> unit = + fun fmt ct -> + pp_summary fmt ct ; + if Config.bo_debug > 1 then + match ct.cond_trace with + | Inter {callee_pname; call_site} -> + let pname = Typ.Procname.to_string callee_pname in + F.fprintf fmt " by call to %s at %a (%a)" pname Location.pp_file_pos call_site + ValTrace.Issue.pp ct.val_traces + | Intra -> + F.fprintf fmt " (%a)" ValTrace.Issue.pp ct.val_traces + + + let pp_description : F.formatter -> t -> unit = + fun fmt ct -> + match ct.cond_trace with + | Inter {callee_pname} + when Config.bo_debug >= 1 || not (SourceFile.is_cpp_model ct.issue_location.Location.file) -> + F.fprintf fmt " by call to %a " MF.pp_monospaced (Typ.Procname.to_string callee_pname) + | _ -> + () + + + let get_val_traces {val_traces} = val_traces + + let get_report_location : t -> Location.t = + fun ct -> match ct.cond_trace with Intra -> ct.issue_location | Inter {call_site} -> call_site + + + let make : Location.t -> ValTrace.Issue.t -> t = + fun issue_location val_traces -> {issue_location; cond_trace= Intra; val_traces} + + + let make_call_and_subst ~traces_caller ~callee_pname call_site ct = + let val_traces = ValTrace.Issue.call call_site traces_caller ct.val_traces in + {ct with cond_trace= Inter {callee_pname; call_site}; val_traces} + + + let has_unknown ct = ValTrace.Issue.has_unknown ct.val_traces + + 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 = + 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 + type report_issue_type = NotIssue | Issue of IssueType.t | SymbolicIssue type checked_condition = {report_issue_type: report_issue_type; propagate: bool} @@ -595,86 +675,6 @@ module Condition = struct x end -module ConditionTrace = struct - type intra_cond_trace = Intra | Inter of {call_site: Location.t; callee_pname: Typ.Procname.t} - [@@deriving compare] - - type 'cond_trace t0 = - {cond_trace: 'cond_trace; issue_location: Location.t; val_traces: ValTrace.Issue.t} - [@@deriving compare] - - type t = intra_cond_trace t0 [@@deriving compare] - - type summary_t = unit t0 - - let pp_summary : F.formatter -> _ t0 -> unit = - fun fmt ct -> F.fprintf fmt "at %a" Location.pp_file_pos ct.issue_location - - - let pp : F.formatter -> t -> unit = - fun fmt ct -> - pp_summary fmt ct ; - if Config.bo_debug > 1 then - match ct.cond_trace with - | Inter {callee_pname; call_site} -> - let pname = Typ.Procname.to_string callee_pname in - F.fprintf fmt " by call to %s at %a (%a)" pname Location.pp_file_pos call_site - ValTrace.Issue.pp ct.val_traces - | Intra -> - F.fprintf fmt " (%a)" ValTrace.Issue.pp ct.val_traces - - - let pp_description : F.formatter -> t -> unit = - fun fmt ct -> - match ct.cond_trace with - | Inter {callee_pname} - when Config.bo_debug >= 1 || not (SourceFile.is_cpp_model ct.issue_location.Location.file) -> - F.fprintf fmt " by call to %a " MF.pp_monospaced (Typ.Procname.to_string callee_pname) - | _ -> - () - - - let get_val_traces {val_traces} = val_traces - - let get_report_location : t -> Location.t = - fun ct -> match ct.cond_trace with Intra -> ct.issue_location | Inter {call_site} -> call_site - - - let make : Location.t -> ValTrace.Issue.t -> t = - fun issue_location val_traces -> {issue_location; cond_trace= Intra; val_traces} - - - let make_call_and_subst ~traces_caller ~callee_pname call_site ct = - let val_traces = ValTrace.Issue.call call_site traces_caller ct.val_traces in - {ct with cond_trace= Inter {callee_pname; call_site}; val_traces} - - - let has_unknown ct = ValTrace.Issue.has_unknown ct.val_traces - - 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 = - 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 - module Reported = struct type t = IssueType.t [@@deriving compare] diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index 2ba015c79..a57e19f29 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -15,7 +15,8 @@ module BoTrace = struct 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] + type elem = ArrayDeclaration | Assign of PowLoc.t | Parameter of Loc.t | Through + [@@deriving compare] type t = | Empty @@ -68,8 +69,8 @@ module BoTrace = struct let pp_elem f = function | ArrayDeclaration -> F.pp_print_string f "ArrayDeclaration" - | Assign -> - F.pp_print_string f "Assign" + | Assign locs -> + F.fprintf f "Assign `%a`" PowLoc.pp locs | Parameter loc -> F.fprintf f "Parameter `%a`" Loc.pp loc | Through -> @@ -114,7 +115,7 @@ module BoTrace = struct let elem_err_desc = function | ArrayDeclaration -> "Array declaration" - | Assign -> + | Assign _ -> "Assignment" | Parameter loc -> if Loc.is_pretty loc then F.asprintf "Parameter `%a`" Loc.pp loc else ""