[inferbo] Prepare supressing intended integer overflow

Reviewed By: mbouaziz

Differential Revision: D13595958

fbshipit-source-id: 39aef1d1b

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

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -357,8 +357,8 @@ module Val = struct
     |> normalize
 
 
-  let add_assign_trace_elem location x =
+  let add_assign_trace_elem location locs x =
-    let traces = Trace.(Set.add_elem location Assign) x.traces in
+    let traces = Trace.(Set.add_elem location (Assign locs)) x.traces in
     {x with traces}
 
 

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]
 

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 ->
+    | Assign locs ->
-        F.pp_print_string f "Assign"
+        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 ""