[inferbo] Simplify condition trace

Reviewed By: skcho

Differential Revision: D9372262

fbshipit-source-id: 5338d5437

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -393,38 +393,36 @@ module Report = struct
 
 
   let check_binop_array_access
-      : Typ.Procname.t -> is_plus:bool -> e1:Exp.t -> e2:Exp.t -> Location.t -> Dom.Mem.astate
-        -> PO.ConditionSet.t -> PO.ConditionSet.t =
-   fun pname ~is_plus ~e1 ~e2 location mem cond_set ->
+      : is_plus:bool -> e1:Exp.t -> e2:Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t
+        -> PO.ConditionSet.t =
+   fun ~is_plus ~e1 ~e2 location mem cond_set ->
     let arr = Sem.eval e1 mem in
     let idx = Sem.eval e2 mem in
     let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) e2 in
     let relation = Dom.Mem.get_relation mem in
-    BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus pname location cond_set
+    BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus location cond_set
 
 
   let check_binop
-      : Typ.Procname.t -> bop:Binop.t -> e1:Exp.t -> e2:Exp.t -> Location.t -> Dom.Mem.astate
-        -> PO.ConditionSet.t -> PO.ConditionSet.t =
-   fun pname ~bop ~e1 ~e2 location mem cond_set ->
+      : bop:Binop.t -> e1:Exp.t -> e2:Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t
+        -> PO.ConditionSet.t =
+   fun ~bop ~e1 ~e2 location mem cond_set ->
     match bop with
     | Binop.PlusPI ->
-        check_binop_array_access pname ~is_plus:true ~e1 ~e2 location mem cond_set
+        check_binop_array_access ~is_plus:true ~e1 ~e2 location mem cond_set
     | Binop.MinusPI ->
-        check_binop_array_access pname ~is_plus:false ~e1 ~e2 location mem cond_set
+        check_binop_array_access ~is_plus:false ~e1 ~e2 location mem cond_set
     | _ ->
         cond_set
 
 
-  let check_expr
-      : Typ.Procname.t -> Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t
-        -> PO.ConditionSet.t =
-   fun pname exp location mem cond_set ->
+  let check_expr : Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t =
+   fun exp location mem cond_set ->
     let rec check_sub_expr exp cond_set =
       match exp with
       | Exp.Lindex (array_exp, index_exp) ->
           cond_set |> check_sub_expr array_exp |> check_sub_expr index_exp
-          |> BoUtils.Check.lindex ~array_exp ~index_exp mem pname location
+          |> BoUtils.Check.lindex ~array_exp ~index_exp mem location
       | Exp.BinOp (_, e1, e2) ->
           cond_set |> check_sub_expr e1 |> check_sub_expr e2
       | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e | Exp.Cast (_, e) ->
@@ -441,18 +439,17 @@ module Report = struct
         let arr = Sem.eval exp mem in
         let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in
         let relation = Dom.Mem.get_relation mem in
-        BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true pname location
-          cond_set
+        BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set
     | Exp.BinOp (bop, e1, e2) ->
-        check_binop pname ~bop ~e1 ~e2 location mem cond_set
+        check_binop ~bop ~e1 ~e2 location mem cond_set
     | _ ->
         cond_set
 
 
   let instantiate_cond
-      : Tenv.t -> Typ.Procname.t -> Procdesc.t -> (Exp.t * Typ.t) list -> Dom.Mem.astate
-        -> Payload.t -> Location.t -> PO.ConditionSet.t =
-   fun tenv caller_pname callee_pdesc params caller_mem summary location ->
+      : Tenv.t -> Procdesc.t -> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Payload.t -> Location.t
+        -> PO.ConditionSet.t =
+   fun tenv callee_pdesc params caller_mem summary location ->
     let callee_symbol_table = Dom.Summary.get_symbol_table summary in
     let callee_exit_mem = Dom.Summary.get_output summary in
     let callee_cond = Dom.Summary.get_cond_set summary in
@@ -461,22 +458,21 @@ module Report = struct
     in
     let pname = Procdesc.get_proc_name callee_pdesc in
     let caller_rel = Dom.Mem.get_relation caller_mem in
-    PO.ConditionSet.subst callee_cond bound_subst_map rel_subst_map caller_rel caller_pname pname
-      location
+    PO.ConditionSet.subst callee_cond bound_subst_map rel_subst_map caller_rel pname location
 
 
   let check_instr
       : Procdesc.t -> Tenv.t -> Itv.SymbolTable.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate
         -> PO.ConditionSet.t -> PO.ConditionSet.t =
    fun pdesc tenv symbol_table node instr mem cond_set ->
-    let pname = Procdesc.get_proc_name pdesc in
     match instr with
     | Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) ->
-        check_expr pname exp location mem cond_set
+        check_expr exp location mem cond_set
     | Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> (
       match Models.Call.dispatch tenv callee_pname params with
       | Some {Models.check} ->
           let node_hash = CFG.Node.hash node in
+          let pname = Procdesc.get_proc_name pdesc in
           check (Models.mk_model_env pname node_hash location tenv symbol_table) mem cond_set
       | None ->
         match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with
@@ -484,7 +480,7 @@ module Report = struct
           match Payload.of_summary callee_summary with
           | Some callee_payload ->
               let callee_pdesc = Summary.get_proc_desc callee_summary in
-              instantiate_cond tenv pname callee_pdesc params mem callee_payload location
+              instantiate_cond tenv callee_pdesc params mem callee_payload location
               |> PO.ConditionSet.join cond_set
           | None ->
               (* no inferbo payload *) cond_set )
@@ -582,29 +578,21 @@ module Report = struct
     List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev
 
 
-  let report_errors : Summary.t -> Procdesc.t -> PO.ConditionSet.t -> PO.ConditionSet.t =
-   fun summary pdesc cond_set ->
-    let pname = Procdesc.get_proc_name pdesc in
+  let report_errors : Summary.t -> PO.ConditionSet.t -> PO.ConditionSet.t =
+   fun summary cond_set ->
     let report cond trace issue_type =
-      let caller_pname, location =
-        match PO.ConditionTrace.get_cond_trace trace with
-        | PO.ConditionTrace.Inter (caller_pname, _, location) ->
-            (caller_pname, location)
-        | PO.ConditionTrace.Intra pname ->
-            (pname, PO.ConditionTrace.get_location trace)
+      let location = PO.ConditionTrace.get_report_location trace in
+      let description = PO.description cond trace in
+      let error_desc = Localise.desc_buffer_overrun description in
+      let exn = Exceptions.Checkers (issue_type, error_desc) in
+      let trace =
+        match TraceSet.choose_shortest trace.PO.ConditionTrace.val_traces with
+        | trace ->
+            make_err_trace trace description
+        | exception _ ->
+            [Errlog.make_trace_element 0 location description []]
       in
-      if Typ.Procname.equal pname caller_pname then
-        let description = PO.description cond trace in
-        let error_desc = Localise.desc_buffer_overrun description in
-        let exn = Exceptions.Checkers (issue_type, error_desc) in
-        let trace =
-          match TraceSet.choose_shortest trace.PO.ConditionTrace.val_traces with
-          | trace ->
-              make_err_trace trace description
-          | exception _ ->
-              [Errlog.make_trace_element 0 location description []]
-        in
-        Reporting.log_error summary ~loc:location ~ltr:trace exn
+      Reporting.log_error summary ~loc:location ~ltr:trace exn
     in
     PO.ConditionSet.check_all ~report cond_set
 
@@ -647,7 +635,7 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
   in
   let cond_set =
     Report.check_proc summary proc_desc tenv symbol_table cfg inv_map
-    |> Report.report_errors summary proc_desc |> Report.forget_locs locals
+    |> Report.report_errors summary |> Report.forget_locs locals
   in
   let summary =
     match exit_mem with

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -66,7 +66,7 @@ let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = fun
       (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None)
 
 
-let check_alloc_size size_exp {pname; location} mem cond_set =
+let check_alloc_size size_exp {location} mem cond_set =
   let _, _, length0, _ = get_malloc_info size_exp in
   let v_length = Sem.eval length0 mem in
   match Dom.Val.get_itv v_length with
@@ -77,7 +77,7 @@ let check_alloc_size size_exp {pname; location} mem cond_set =
       let traces =
         Dom.Val.get_traces v_length |> BufferOverrunTrace.Set.add_elem alloc_trace_elem
       in
-      PO.ConditionSet.add_alloc_size pname location ~length traces cond_set
+      PO.ConditionSet.add_alloc_size location ~length traces cond_set
 
 
 let set_uninitialized location (typ: Typ.t) ploc mem =
@@ -275,8 +275,8 @@ module StdArray = struct
     let exec _ ~ret:(id, _) mem =
       L.(debug BufferOverrun Verbose) "Using model std::array<_, %Ld>::at" _size ;
       BoUtils.Exec.load_val id (Sem.eval_lindex array_exp index_exp mem) mem
-    and check {pname; location} mem cond_set =
-      BoUtils.Check.lindex ~array_exp ~index_exp mem pname location cond_set
+    and check {location} mem cond_set =
+      BoUtils.Check.lindex ~array_exp ~index_exp mem location cond_set
     in
     {exec; check}
 
@@ -384,18 +384,18 @@ module Collection = struct
 
 
   let add_at_index (alist_id: Ident.t) index_exp =
-    let check {pname; location} mem cond_set =
+    let check {location} mem cond_set =
       let array_exp = Exp.Var alist_id in
-      BoUtils.Check.collection_access ~array_exp ~index_exp ~is_collection_add:true mem pname
-        location cond_set
+      BoUtils.Check.collection_access ~array_exp ~index_exp ~is_collection_add:true mem location
+        cond_set
     in
     {exec= change_size_by ~size_f:incr_size alist_id; check}
 
 
   let remove_at_index alist_id index_exp =
-    let check {pname; location} mem cond_set =
+    let check {location} mem cond_set =
       let array_exp = Exp.Var alist_id in
-      BoUtils.Check.collection_access ~array_exp ~index_exp mem pname location cond_set
+      BoUtils.Check.collection_access ~array_exp ~index_exp mem location cond_set
     in
     {exec= change_size_by ~size_f:decr_size alist_id; check}
 
@@ -405,19 +405,19 @@ module Collection = struct
       let to_add_length = get_size alist_to_add mem in
       change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id _model_env ~ret mem
     in
-    let check {pname; location} mem cond_set =
+    let check {location} mem cond_set =
       let array_exp = Exp.Var alist_id in
-      BoUtils.Check.collection_access ~index_exp ~array_exp ~is_collection_add:true mem pname
-        location cond_set
+      BoUtils.Check.collection_access ~index_exp ~array_exp ~is_collection_add:true mem location
+        cond_set
     in
     {exec; check}
 
 
   let get_or_set_at_index alist_id index_exp =
     let exec _model_env ~ret:_ mem = mem in
-    let check {pname; location} mem cond_set =
+    let check {location} mem cond_set =
       let array_exp = Exp.Var alist_id in
-      BoUtils.Check.collection_access ~index_exp ~array_exp mem pname location cond_set
+      BoUtils.Check.collection_access ~index_exp ~array_exp mem location cond_set
     in
     {exec; check}
 end

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -357,57 +357,52 @@ module Condition = struct
 end
 
 module ConditionTrace = struct
-  type cond_trace =
-    | Intra of Typ.Procname.t
-    | Inter of Typ.Procname.t * Typ.Procname.t * Location.t
+  type cond_trace = Intra | Inter of {call_site: Location.t; callee_pname: Typ.Procname.t}
   [@@deriving compare]
 
-  type t =
-    { proc_name: Typ.Procname.t
-    ; cond_trace: cond_trace
-    ; location: Location.t
-    ; val_traces: ValTraceSet.t }
+  type t = {cond_trace: cond_trace; issue_location: Location.t; val_traces: ValTraceSet.t}
   [@@deriving compare]
 
-  let pp_location : F.formatter -> t -> unit = fun fmt ct -> Location.pp_file_pos fmt ct.location
+  let pp_location : F.formatter -> t -> unit =
+   fun fmt ct -> Location.pp_file_pos fmt ct.issue_location
+
 
   let pp : F.formatter -> t -> unit =
    fun fmt ct ->
     if Config.bo_debug <= 1 then F.fprintf fmt "at %a" pp_location ct
     else
       match ct.cond_trace with
-      | Inter (_, pname, location) ->
-          let pname = Typ.Procname.to_string pname in
+      | Inter {callee_pname; call_site} ->
+          let pname = Typ.Procname.to_string callee_pname in
           F.fprintf fmt "at %a by call to %s at %a (%a)" pp_location ct pname Location.pp_file_pos
-            location ValTraceSet.pp ct.val_traces
-      | Intra _ ->
+            call_site ValTraceSet.pp ct.val_traces
+      | Intra ->
           F.fprintf fmt "%a (%a)" pp_location ct ValTraceSet.pp ct.val_traces
 
 
   let pp_description : F.formatter -> t -> unit =
    fun fmt ct ->
     match ct.cond_trace with
-    | Inter (_, pname, _)
-      when Config.bo_debug >= 1 || not (SourceFile.is_cpp_model ct.location.Location.file) ->
-        F.fprintf fmt " by call to %a " MF.pp_monospaced (Typ.Procname.to_string pname)
+    | 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_location : t -> Location.t = fun ct -> ct.location
+  let get_report_location : t -> Location.t =
+   fun ct -> match ct.cond_trace with Intra -> ct.issue_location | Inter {call_site} -> call_site
 
-  let get_cond_trace : t -> cond_trace = fun ct -> ct.cond_trace
 
-  let make : Typ.Procname.t -> Location.t -> ValTraceSet.t -> t =
-   fun proc_name location val_traces ->
-    {proc_name; location; cond_trace= Intra proc_name; val_traces}
+  let make : Location.t -> ValTraceSet.t -> t =
+   fun issue_location val_traces -> {issue_location; cond_trace= Intra; val_traces}
 
 
-  let make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location ct =
+  let make_call_and_subst ~traces_caller ~callee_pname call_site ct =
     let val_traces =
-      ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces location
+      ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces call_site
     in
-    {ct with cond_trace= Inter (caller_pname, callee_pname, location); val_traces}
+    {ct with cond_trace= Inter {callee_pname; call_site}; val_traces}
 
 
   let has_unknown ct = ValTraceSet.has_unknown ct.val_traces
@@ -442,13 +437,13 @@ module ConditionWithTrace = struct
         cmp
 
 
-  let subst (bound_map, trace_map) rel_map caller_relation caller_pname callee_pname location cwt =
+  let subst (bound_map, trace_map) rel_map caller_relation callee_pname call_site cwt =
     let symbols = Condition.get_symbols cwt.cond in
     if List.is_empty symbols then
       L.(die InternalError)
         "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \
          the first place?"
-        pp cwt Typ.Procname.pp callee_pname Location.pp location ;
+        pp cwt Typ.Procname.pp callee_pname Location.pp call_site ;
     match Condition.subst bound_map rel_map caller_relation cwt.cond with
     | None ->
         None
@@ -462,8 +457,7 @@ module ConditionWithTrace = struct
                   val_traces )
         in
         let trace =
-          ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location
-            cwt.trace
+          ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace
         in
         Some {cond; trace; reported= cwt.reported}
 
@@ -561,32 +555,31 @@ module ConditionSet = struct
 
   let join condset1 condset2 = List.fold_left ~f:join_one condset1 ~init:condset2
 
-  let add_opt pname location val_traces condset = function
+  let add_opt location val_traces condset = function
     | None ->
         condset
     | Some cond ->
-        let trace = ConditionTrace.make pname location val_traces in
+        let trace = ConditionTrace.make location val_traces in
         let cwt = ConditionWithTrace.make cond trace in
         join [cwt] condset
 
 
-  let add_array_access pname location ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp
-      ~relation val_traces condset =
+  let add_array_access location ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp ~relation
+      val_traces condset =
     ArrayAccessCondition.make ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation
-    |> Condition.make_array_access ~is_collection_add |> add_opt pname location val_traces condset
+    |> Condition.make_array_access ~is_collection_add |> add_opt location val_traces condset
 
 
-  let add_alloc_size pname location ~length val_traces condset =
+  let add_alloc_size location ~length val_traces condset =
     AllocSizeCondition.make ~length |> Condition.make_alloc_size
-    |> add_opt pname location val_traces condset
+    |> add_opt location val_traces condset
 
 
-  let subst condset bound_map_trace_map rel_subst_map caller_relation caller_pname callee_pname
-      location =
+  let subst condset bound_map_trace_map rel_subst_map caller_relation callee_pname call_site =
     let subst_add_cwt condset cwt =
       match
-        ConditionWithTrace.subst bound_map_trace_map rel_subst_map caller_relation caller_pname
-          callee_pname location cwt
+        ConditionWithTrace.subst bound_map_trace_map rel_subst_map caller_relation callee_pname
+          call_site cwt
       with
       | None ->
           condset

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -199,18 +199,18 @@ end
 
 module Check = struct
   let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces
-      ?(is_collection_add= false) pname location cond_set =
+      ?(is_collection_add= false) location cond_set =
     let arr_traces = Dom.Val.get_traces arr in
     match (size, idx) with
     | NonBottom length, NonBottom idx ->
         let traces = TraceSet.merge ~arr_traces ~idx_traces location in
-        PO.ConditionSet.add_array_access pname location ~size:length ~idx ~size_sym_exp
-          ~idx_sym_exp ~relation ~is_collection_add traces cond_set
+        PO.ConditionSet.add_array_access location ~size:length ~idx ~size_sym_exp ~idx_sym_exp
+          ~relation ~is_collection_add traces cond_set
     | _ ->
         cond_set
 
 
-  let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus pname location cond_set =
+  let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus location cond_set =
     let arr_blk = Dom.Val.get_array_blk arr in
     let size = ArrayBlk.sizeof arr_blk in
     let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in
@@ -226,12 +226,11 @@ module Check = struct
     in
     L.(debug BufferOverrun Verbose)
       "@[<v 2>Add condition :@,array: %a@,  idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ;
-    check_access ~size ~idx:idx_in_blk ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces pname
+    check_access ~size ~idx:idx_in_blk ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces
       location cond_set
 
 
-  let collection_access ~array_exp ~index_exp ?(is_collection_add= false) mem pname location
-      cond_set =
+  let collection_access ~array_exp ~index_exp ?(is_collection_add= false) mem location cond_set =
     let idx = Sem.eval index_exp mem in
     let arr = Sem.eval array_exp mem in
     let idx_traces = Dom.Val.get_traces idx in
@@ -239,13 +238,13 @@ module Check = struct
     let idx = Dom.Val.get_itv idx in
     let relation = Dom.Mem.get_relation mem in
     check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces
-      ~is_collection_add pname location cond_set
+      ~is_collection_add location cond_set
 
 
-  let lindex ~array_exp ~index_exp mem pname location cond_set =
+  let lindex ~array_exp ~index_exp mem location cond_set =
     let idx = Sem.eval index_exp mem in
     let arr = Sem.eval_arr array_exp mem in
     let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) index_exp in
     let relation = Dom.Mem.get_relation mem in
-    array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true pname location cond_set
+    array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set
 end

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -58,14 +58,14 @@ end
 module Check : sig
   val array_access :
     arr:Dom.Val.t -> idx:Dom.Val.t -> idx_sym_exp:Relation.SymExp.t option
-    -> relation:Relation.astate -> is_plus:bool -> Typ.Procname.t -> Location.t
-    -> PO.ConditionSet.t -> PO.ConditionSet.t
+    -> relation:Relation.astate -> is_plus:bool -> Location.t -> PO.ConditionSet.t
+    -> PO.ConditionSet.t
 
   val lindex :
-    array_exp:Exp.t -> index_exp:Exp.t -> Dom.Mem.astate -> Typ.Procname.t -> Location.t
-    -> PO.ConditionSet.t -> PO.ConditionSet.t
+    array_exp:Exp.t -> index_exp:Exp.t -> Dom.Mem.astate -> Location.t -> PO.ConditionSet.t
+    -> PO.ConditionSet.t
 
   val collection_access :
-    array_exp:Exp.t -> index_exp:Exp.t -> ?is_collection_add:bool -> Dom.Mem.astate
-    -> Typ.Procname.t -> Location.t -> PO.ConditionSet.t -> PO.ConditionSet.t
+    array_exp:Exp.t -> index_exp:Exp.t -> ?is_collection_add:bool -> Dom.Mem.astate -> Location.t
+    -> PO.ConditionSet.t -> PO.ConditionSet.t
 end