diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 319b4f642..039eaca53 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index b15b29dd0..713a1660d 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 391fe2e4e..a671ba107 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 49423a700..a44efae87 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/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) "@[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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 4b19d647b..09c31cada 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/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