diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a473013bd..5c5ffa2a1 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -16,6 +16,7 @@ open! AbstractDomain.Types module F = Format module L = Logging module Dom = BufferOverrunDomain +module PO = BufferOverrunProofObligations module Trace = BufferOverrunTrace module TraceSet = Trace.Set @@ -404,8 +405,8 @@ module Report = struct type extras = Typ.Procname.t -> Procdesc.t option let add_condition - : Typ.Procname.t -> CFG.node -> Exp.t -> Location.t -> Dom.Mem.astate -> Dom.ConditionSet.t - -> Dom.ConditionSet.t = + : Typ.Procname.t -> CFG.node -> Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t + -> PO.ConditionSet.t = fun pname node exp loc mem cond_set -> let array_access = match exp with @@ -449,7 +450,7 @@ module Report = struct match (size, idx) with | NonBottom size, NonBottom idx -> let traces = TraceSet.merge ~traces_arr ~traces_idx loc in - Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx traces cond_set + PO.ConditionSet.add_bo_safety pname loc site ~size ~idx traces cond_set | _ -> cond_set ) | None @@ -457,7 +458,7 @@ module Report = struct let instantiate_cond : Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list -> Dom.Mem.astate - -> Summary.payload -> Location.t -> Dom.ConditionSet.t = + -> Summary.payload -> Location.t -> PO.ConditionSet.t = fun tenv caller_pname callee_pdesc params caller_mem summary loc -> let callee_entry_mem = Dom.Summary.get_input summary in let callee_cond = Dom.Summary.get_cond_set summary in @@ -468,16 +469,16 @@ module Report = struct loc in let pname = Procdesc.get_proc_name pdesc in - Dom.ConditionSet.subst callee_cond subst_map caller_pname pname loc + PO.ConditionSet.subst callee_cond subst_map caller_pname pname loc | _ -> callee_cond - let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.ConditionSet.t -> unit = + let print_debug_info : Sil.instr -> Dom.Mem.astate -> PO.ConditionSet.t -> unit = fun instr pre cond_set -> L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ; L.(debug BufferOverrun Verbose) "@[Pre-state : @,%a" Dom.Mem.pp pre ; L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr ; - L.(debug BufferOverrun Verbose) "@[@\n@\n%a" Dom.ConditionSet.pp cond_set ; + L.(debug BufferOverrun Verbose) "@[@\n@\n%a" PO.ConditionSet.pp cond_set ; L.(debug BufferOverrun Verbose) "@]@\n" ; L.(debug BufferOverrun Verbose) "================================@\n@." @@ -521,8 +522,8 @@ module Report = struct end let rec collect_instrs - : extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.astate -> Dom.ConditionSet.t - -> Dom.ConditionSet.t = + : extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.astate -> PO.ConditionSet.t + -> PO.ConditionSet.t = fun ({pdesc; tenv; extras} as pdata) node instrs mem cond_set -> match instrs with | [] @@ -538,7 +539,7 @@ module Report = struct | Some summary -> let callee = extras callee_pname in instantiate_cond tenv pname callee params mem summary loc - |> Dom.ConditionSet.rm_invalid |> Dom.ConditionSet.join cond_set + |> PO.ConditionSet.join cond_set | _ -> cond_set ) | _ @@ -579,8 +580,8 @@ module Report = struct print_debug_info instr mem' cond_set ; collect_instrs pdata node rem_instrs mem' cond_set let collect_node - : extras ProcData.t -> Analyzer.invariant_map -> Dom.ConditionSet.t -> CFG.node - -> Dom.ConditionSet.t = + : extras ProcData.t -> Analyzer.invariant_map -> PO.ConditionSet.t -> CFG.node + -> PO.ConditionSet.t = fun pdata inv_map cond_set node -> match Analyzer.extract_pre (CFG.id node) inv_map with | Some mem @@ -589,10 +590,10 @@ module Report = struct | _ -> cond_set - let collect : extras ProcData.t -> Analyzer.invariant_map -> Dom.ConditionSet.t = + let collect : extras ProcData.t -> Analyzer.invariant_map -> PO.ConditionSet.t = fun ({pdesc} as pdata) inv_map -> let add_node1 acc node = collect_node pdata inv_map acc node in - Procdesc.fold_nodes add_node1 Dom.ConditionSet.empty pdesc + Procdesc.fold_nodes add_node1 PO.ConditionSet.empty pdesc let make_err_trace : Trace.t -> string -> Errlog.loc_trace = fun trace desc -> @@ -613,37 +614,36 @@ module Report = struct in List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev - let report_error : Procdesc.t -> Dom.ConditionSet.t -> unit = + let report_error : Procdesc.t -> PO.ConditionSet.t -> unit = fun pdesc conds -> let pname = Procdesc.get_proc_name pdesc in - let report1 cond = - let alarm = Dom.Condition.check cond in - let caller_pname, loc = - match Dom.Condition.get_cond_trace cond with - | Dom.Condition.Inter (caller_pname, _, loc) - -> (caller_pname, loc) - | Dom.Condition.Intra pname - -> (pname, Dom.Condition.get_location cond) - in + let report1 cond trace = + let alarm = PO.Condition.check cond in match alarm with | None -> () - | Some bucket when Typ.Procname.equal pname caller_pname - -> let description = Dom.Condition.description cond in - let error_desc = Localise.desc_buffer_overrun bucket description in - let exn = Exceptions.Checkers (IssueType.buffer_overrun.unique_id, error_desc) in - let trace = - match TraceSet.choose_shortest cond.Dom.Condition.traces with - | trace - -> make_err_trace trace description - | exception _ - -> [Errlog.make_trace_element 0 loc description []] + | Some bucket + -> let caller_pname, loc = + match PO.ConditionTrace.get_cond_trace trace with + | PO.ConditionTrace.Inter (caller_pname, _, loc) + -> (caller_pname, loc) + | PO.ConditionTrace.Intra pname + -> (pname, PO.ConditionTrace.get_location trace) in - Reporting.log_error_deprecated pname ~loc ~ltr:trace exn - | _ - -> () + if Typ.Procname.equal pname caller_pname then + let description = PO.description cond trace in + let error_desc = Localise.desc_buffer_overrun bucket description in + let exn = Exceptions.Checkers (IssueType.buffer_overrun.unique_id, 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 loc description []] + in + Reporting.log_error_deprecated pname ~loc ~ltr:trace exn in - Dom.ConditionSet.iter report1 conds + PO.ConditionSet.iter conds ~f:report1 end let compute_post : Analyzer.TransferFunctions.extras ProcData.t -> Summary.payload option = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index d74a00b15..1d9bd699e 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -17,220 +17,13 @@ module F = Format module L = Logging module ItvPure = Itv.ItvPure module MF = MarkupFormatter +module PO = BufferOverrunProofObligations module Trace = BufferOverrunTrace module TraceSet = Trace.Set +(** unsound but ok for bug catching *) let always_strong_update = true -(* unsound but ok for bug catching *) - -module Condition = struct - type cond_trace = - | Intra of Typ.Procname.t - | Inter of Typ.Procname.t * Typ.Procname.t * Location.t - [@@deriving compare] - - type t = - { proc_name: Typ.Procname.t - ; loc: Location.t - ; id: string - ; cond_trace: cond_trace - ; idx: ItvPure.astate - ; size: ItvPure.astate - ; traces: TraceSet.t } - [@@deriving compare] - - type astate = t - - let set_size_pos : t -> t = - fun c -> - let size' = ItvPure.make_positive c.size in - if phys_equal size' c.size then c else {c with size= size'} - - let pp_location : F.formatter -> t -> unit = fun fmt c -> Location.pp_file_pos fmt c.loc - - let pp : F.formatter -> t -> unit = - fun fmt c -> - let c = set_size_pos c in - if Config.bo_debug <= 1 then - F.fprintf fmt "%a < %a at %a" ItvPure.pp c.idx ItvPure.pp c.size pp_location c - else - match c.cond_trace with - | Inter (_, pname, loc) - -> let pname = Typ.Procname.to_string pname in - F.fprintf fmt "%a < %a at %a by call %s() at %a (%a)" ItvPure.pp c.idx ItvPure.pp - c.size pp_location c pname Location.pp_file_pos loc TraceSet.pp c.traces - | Intra _ - -> F.fprintf fmt "%a < %a at %a (%a)" ItvPure.pp c.idx ItvPure.pp c.size pp_location c - TraceSet.pp c.traces - - let get_location : t -> Location.t = fun c -> c.loc - - let get_cond_trace : t -> cond_trace = fun c -> c.cond_trace - - let get_proc_name : t -> Typ.Procname.t = fun c -> c.proc_name - - let make - : Typ.Procname.t -> Location.t -> string -> idx:ItvPure.t -> size:ItvPure.t -> TraceSet.t - -> t = - fun proc_name loc id ~idx ~size traces -> - {proc_name; idx; size; loc; id; cond_trace= Intra proc_name; traces} - - let filter1 : t -> bool = - fun c -> - ItvPure.is_top c.idx || ItvPure.is_top c.size - || Itv.Bound.eq (ItvPure.lb c.idx) Itv.Bound.MInf - || Itv.Bound.eq (ItvPure.lb c.size) Itv.Bound.MInf - || ItvPure.is_nat c.idx && ItvPure.is_nat c.size - - let filter2 : t -> bool = - fun c -> - (* basically, alarms involving infinity are filtered *) - (not (ItvPure.is_finite c.idx) || not (ItvPure.is_finite c.size)) - && (* except the following cases *) - not - ( Itv.Bound.is_not_infty (ItvPure.lb c.idx) - && (* idx non-infty lb < 0 *) - Itv.Bound.lt (ItvPure.lb c.idx) Itv.Bound.zero - || Itv.Bound.is_not_infty (ItvPure.lb c.idx) - && (* idx non-infty lb > size lb *) - Itv.Bound.gt (ItvPure.lb c.idx) (ItvPure.lb c.size) - || Itv.Bound.is_not_infty (ItvPure.lb c.idx) - && (* idx non-infty lb > size ub *) - Itv.Bound.gt (ItvPure.lb c.idx) (ItvPure.ub c.size) - || Itv.Bound.is_not_infty (ItvPure.ub c.idx) - && (* idx non-infty ub > size lb *) - Itv.Bound.gt (ItvPure.ub c.idx) (ItvPure.lb c.size) - || Itv.Bound.is_not_infty (ItvPure.ub c.idx) - && (* idx non-infty ub > size ub *) - Itv.Bound.gt (ItvPure.ub c.idx) (ItvPure.ub c.size) ) - - (* check buffer overrun and return its confidence *) - let check : t -> string option = - fun c -> - (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *) - let c' = set_size_pos c in - (* if sl < 0, use sl' = 0 *) - let not_overrun = ItvPure.lt_sem c'.idx c'.size in - let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in - (* il >= 0 and iu < sl, definitely not an error *) - if ItvPure.is_one not_overrun && ItvPure.is_one not_underrun then None - (* iu < 0 or il >= su, definitely an error *) - else if ItvPure.is_zero not_overrun || ItvPure.is_zero not_underrun then - Some Localise.BucketLevel.b1 (* su <= iu < +oo, most probably an error *) - else if Itv.Bound.is_not_infty (ItvPure.ub c.idx) - && Itv.Bound.le (ItvPure.ub c.size) (ItvPure.ub c.idx) - then Some Localise.BucketLevel.b2 (* symbolic il >= sl, probably an error *) - else if Itv.Bound.is_symbolic (ItvPure.lb c.idx) - && Itv.Bound.le (ItvPure.lb c'.size) (ItvPure.lb c.idx) - then Some Localise.BucketLevel.b3 (* other symbolic bounds are probably too noisy *) - else if Config.bo_debug <= 3 && (ItvPure.is_symbolic c.idx || ItvPure.is_symbolic c.size) - then None - else if filter1 c then Some Localise.BucketLevel.b5 - else if filter2 c then Some Localise.BucketLevel.b3 - else Some Localise.BucketLevel.b2 - - let invalid : t -> bool = fun x -> ItvPure.invalid x.idx || ItvPure.invalid x.size - - let pp_trace : F.formatter -> t -> unit = - fun fmt c -> - match c.cond_trace with - | Inter (_, pname, _) - when Config.bo_debug >= 1 || not (SourceFile.is_cpp_model c.loc.Location.file) - -> F.fprintf fmt " %@ %a by call %a " pp_location c MF.pp_monospaced - (Typ.Procname.to_string pname ^ "()") - | _ - -> () - - let pp_description : F.formatter -> t -> unit = - fun fmt c -> - let c = set_size_pos c in - F.fprintf fmt "Offset: %a Size: %a%a" ItvPure.pp c.idx ItvPure.pp c.size pp_trace c - - let description : t -> string = fun c -> Format.asprintf "%a" pp_description c - - let subst - : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Typ.Procname.t - -> Typ.Procname.t -> Location.t -> t option = - fun c (bound_map, trace_map) caller_pname callee_pname loc -> - match ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size with - | [] - -> Some c - | symbols -> - match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with - | NonBottom idx, NonBottom size - -> let traces_caller = - List.fold symbols ~init:TraceSet.empty ~f:(fun traces symbol -> - match Itv.SubstMap.find symbol trace_map with - | symbol_trace - -> TraceSet.join symbol_trace traces - | exception Not_found - -> traces ) - in - let traces = TraceSet.instantiate ~traces_caller ~traces_callee:c.traces loc in - let cond_trace = Inter (caller_pname, callee_pname, loc) in - Some {c with idx; size; cond_trace; traces} - | _ - -> None -end - -module ConditionSet = struct - include AbstractDomain.FiniteSet (Condition) - module Map = Caml.Map.Make (Location) - - let add_bo_safety - : Typ.Procname.t -> Location.t -> string -> idx:ItvPure.t -> size:ItvPure.t -> TraceSet.t - -> t -> t = - fun pname loc id ~idx ~size traces cond -> - add (Condition.make pname loc id ~idx ~size traces) cond - - let subst - : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Typ.Procname.t - -> Typ.Procname.t -> Location.t -> t = - fun x subst_map caller_pname callee_pname loc -> - fold - (fun e x -> - match Condition.subst e subst_map caller_pname callee_pname loc with - | Some c - -> add c x - | None - -> x) - x empty - - let group : t -> t Map.t = - fun x -> - fold - (fun cond map -> - let old_set = - try Map.find cond.loc map - with Not_found -> empty - in - Map.add cond.loc (add cond old_set) map) - x Map.empty - - let pp_summary : F.formatter -> t -> unit = - fun fmt x -> - let pp_sep fmt () = F.fprintf fmt ", @," in - let pp_element fmt v = Condition.pp fmt v in - F.fprintf fmt "@[Safety conditions:@," ; - F.fprintf fmt "@[{ " ; - F.pp_print_list ~pp_sep pp_element fmt (elements x) ; - F.fprintf fmt " }@]" ; - F.fprintf fmt "@]" - - let pp : Format.formatter -> t -> unit = - fun fmt x -> - let pp_sep fmt () = F.fprintf fmt ", @," in - let pp_element fmt v = Condition.pp fmt v in - F.fprintf fmt "@[Safety conditions :@," ; - F.fprintf fmt "@[{" ; - F.pp_print_list ~pp_sep pp_element fmt (elements x) ; - F.fprintf fmt " }@]" ; - F.fprintf fmt "@]" - - let rm_invalid : t -> t = fun x -> filter (fun c -> not (Condition.invalid c)) x -end - module Val = struct type astate = {itv: Itv.astate; powloc: PowLoc.astate; arrayblk: ArrayBlk.astate; traces: TraceSet.t} @@ -831,13 +624,13 @@ module Mem = struct end module Summary = struct - type t = Mem.t * Mem.t * ConditionSet.t + type t = Mem.t * Mem.t * PO.ConditionSet.t let get_input : t -> Mem.t = fst3 let get_output : t -> Mem.t = snd3 - let get_cond_set : t -> ConditionSet.t = trd3 + let get_cond_set : t -> PO.ConditionSet.t = trd3 let get_symbols : t -> Itv.Symbol.t list = fun s -> Mem.get_heap_symbols (get_input s) @@ -857,10 +650,11 @@ module Summary = struct let pp_summary : F.formatter -> t -> unit = fun fmt s -> - F.fprintf fmt "%a@,%a@,%a" pp_symbol_map s pp_return s ConditionSet.pp_summary + F.fprintf fmt "%a@,%a@,%a" pp_symbol_map s pp_return s PO.ConditionSet.pp_summary (get_cond_set s) let pp : F.formatter -> t -> unit = fun fmt (entry_mem, exit_mem, condition_set) -> - F.fprintf fmt "%a@,%a@,%a@," Mem.pp entry_mem Mem.pp exit_mem ConditionSet.pp condition_set + F.fprintf fmt "%a@,%a@,%a@," Mem.pp entry_mem Mem.pp exit_mem PO.ConditionSet.pp + condition_set end diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml new file mode 100644 index 000000000..a026b42d6 --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -0,0 +1,229 @@ +(* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd +open! AbstractDomain.Types +module F = Format +module L = Logging +module ItvPure = Itv.ItvPure +module MF = MarkupFormatter +module ValTraceSet = BufferOverrunTrace.Set + +module Condition = struct + type t = {idx: ItvPure.astate; size: ItvPure.astate} [@@deriving compare] + + let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size + + let set_size_pos : t -> t = + fun c -> + let size' = ItvPure.make_positive c.size in + if phys_equal size' c.size then c else {c with size= size'} + + let pp : F.formatter -> t -> unit = + fun fmt c -> + let c = set_size_pos c in + F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size + + let pp_description : F.formatter -> t -> unit = + fun fmt c -> + let c = set_size_pos c in + F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp c.idx ItvPure.pp c.size + + let make : idx:ItvPure.t -> size:ItvPure.t -> t option = + fun ~idx ~size -> + if ItvPure.is_invalid idx || ItvPure.is_invalid size then None else Some {idx; size} + + let filter1 : t -> bool = + fun c -> + ItvPure.is_top c.idx || ItvPure.is_top c.size + || Itv.Bound.eq (ItvPure.lb c.idx) Itv.Bound.MInf + || Itv.Bound.eq (ItvPure.lb c.size) Itv.Bound.MInf + || ItvPure.is_nat c.idx && ItvPure.is_nat c.size + + let filter2 : t -> bool = + fun c -> + (* basically, alarms involving infinity are filtered *) + (not (ItvPure.is_finite c.idx) || not (ItvPure.is_finite c.size)) + && (* except the following cases *) + not + ( Itv.Bound.is_not_infty (ItvPure.lb c.idx) + && (* idx non-infty lb < 0 *) + Itv.Bound.lt (ItvPure.lb c.idx) Itv.Bound.zero + || Itv.Bound.is_not_infty (ItvPure.lb c.idx) + && (* idx non-infty lb > size lb *) + Itv.Bound.gt (ItvPure.lb c.idx) (ItvPure.lb c.size) + || Itv.Bound.is_not_infty (ItvPure.lb c.idx) + && (* idx non-infty lb > size ub *) + Itv.Bound.gt (ItvPure.lb c.idx) (ItvPure.ub c.size) + || Itv.Bound.is_not_infty (ItvPure.ub c.idx) + && (* idx non-infty ub > size lb *) + Itv.Bound.gt (ItvPure.ub c.idx) (ItvPure.lb c.size) + || Itv.Bound.is_not_infty (ItvPure.ub c.idx) + && (* idx non-infty ub > size ub *) + Itv.Bound.gt (ItvPure.ub c.idx) (ItvPure.ub c.size) ) + + (* check buffer overrun and return its confidence *) + let check : t -> string option = + fun c -> + (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *) + let c' = set_size_pos c in + (* if sl < 0, use sl' = 0 *) + let not_overrun = ItvPure.lt_sem c'.idx c'.size in + let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in + (* il >= 0 and iu < sl, definitely not an error *) + if ItvPure.is_one not_overrun && ItvPure.is_one not_underrun then None + (* iu < 0 or il >= su, definitely an error *) + else if ItvPure.is_zero not_overrun || ItvPure.is_zero not_underrun then + Some Localise.BucketLevel.b1 (* su <= iu < +oo, most probably an error *) + else if Itv.Bound.is_not_infty (ItvPure.ub c.idx) + && Itv.Bound.le (ItvPure.ub c.size) (ItvPure.ub c.idx) + then Some Localise.BucketLevel.b2 (* symbolic il >= sl, probably an error *) + else if Itv.Bound.is_symbolic (ItvPure.lb c.idx) + && Itv.Bound.le (ItvPure.lb c'.size) (ItvPure.lb c.idx) + then Some Localise.BucketLevel.b3 (* other symbolic bounds are probably too noisy *) + else if Config.bo_debug <= 3 && (ItvPure.is_symbolic c.idx || ItvPure.is_symbolic c.size) + then None + else if filter1 c then Some Localise.BucketLevel.b5 + else if filter2 c then Some Localise.BucketLevel.b3 + else Some Localise.BucketLevel.b2 + + let subst : t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t -> t option = + fun c bound_map -> + match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with + | NonBottom idx, NonBottom size + -> Some {idx; size} + | _ + -> None +end + +module ConditionTrace = struct + type cond_trace = + | Intra of Typ.Procname.t + | Inter of Typ.Procname.t * Typ.Procname.t * Location.t + [@@deriving compare] + + type t = + { proc_name: Typ.Procname.t + ; loc: Location.t + ; id: string + ; cond_trace: cond_trace + ; val_traces: ValTraceSet.t } + [@@deriving compare] + + let pp_location : F.formatter -> t -> unit = fun fmt ct -> Location.pp_file_pos fmt ct.loc + + 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, loc) + -> let pname = Typ.Procname.to_string pname in + F.fprintf fmt "at %a by call %s() at %a (%a)" pp_location ct pname Location.pp_file_pos + loc 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.loc.Location.file) + -> F.fprintf fmt " %@ %a by call %a " pp_location ct MF.pp_monospaced + (Typ.Procname.to_string pname ^ "()") + | _ + -> () + + let get_location : t -> Location.t = fun ct -> ct.loc + + let get_cond_trace : t -> cond_trace = fun ct -> ct.cond_trace + + let get_proc_name : t -> Typ.Procname.t = fun ct -> ct.proc_name + + let get_caller_proc_name ct = + match ct.cond_trace with Intra pname -> pname | Inter (caller_pname, _, _) -> caller_pname + + let make : Typ.Procname.t -> Location.t -> string -> ValTraceSet.t -> t = + fun proc_name loc id val_traces -> {proc_name; loc; id; cond_trace= Intra proc_name; val_traces} + + let make_call_and_subst ~traces_caller ~caller_pname ~callee_pname loc ct = + let val_traces = ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces loc in + {ct with cond_trace= Inter (caller_pname, callee_pname, loc); val_traces} +end + +module ConditionSet = struct + type condition_with_trace = {cond: Condition.t; trace: ConditionTrace.t} + + type t = condition_with_trace list + + let empty = [] + + let join condset1 condset2 = condset1 @ condset2 + + let add_bo_safety pname loc id ~idx ~size val_traces condset = + match Condition.make ~idx ~size with + | None + -> condset + | Some cond + -> let trace = ConditionTrace.make pname loc id val_traces in + let cwt = {cond; trace} in + join [cwt] condset + + let subst condset (bound_map, trace_map) caller_pname callee_pname loc = + let subst_cwt cwt = + match Condition.get_symbols cwt.cond with + | [] + -> Some cwt + | symbols -> + match Condition.subst cwt.cond bound_map with + | None + -> None + | Some cond + -> let traces_caller = + List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol -> + match Itv.SubstMap.find symbol trace_map with + | symbol_trace + -> ValTraceSet.join symbol_trace val_traces + | exception Not_found + -> val_traces ) + in + let make_call_and_subst trace = + ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname loc + trace + in + let trace = make_call_and_subst cwt.trace in + Some {cond; trace} + in + List.filter_map condset ~f:subst_cwt + + let iter ~f condset = List.iter condset ~f:(fun cwt -> f cwt.cond cwt.trace) + + let pp_cwt fmt cwt = F.fprintf fmt "%a %a" Condition.pp cwt.cond ConditionTrace.pp cwt.trace + + let pp_summary : F.formatter -> t -> unit = + fun fmt condset -> + let pp_sep fmt () = F.fprintf fmt ", @," in + F.fprintf fmt "@[Safety conditions:@," ; + F.fprintf fmt "@[{ " ; + F.pp_print_list ~pp_sep pp_cwt fmt condset ; + F.fprintf fmt " }@]" ; + F.fprintf fmt "@]" + + let pp : Format.formatter -> t -> unit = + fun fmt condset -> + let pp_sep fmt () = F.fprintf fmt ", @," in + F.fprintf fmt "@[Safety conditions :@," ; + F.fprintf fmt "@[{" ; + F.pp_print_list ~pp_sep pp_cwt fmt condset ; + F.fprintf fmt " }@]" ; + F.fprintf fmt "@]" +end + +let description cond trace = + F.asprintf "%a%a" Condition.pp_description cond ConditionTrace.pp_description trace diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 1bd3acf47..bee8ddba6 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -854,7 +854,11 @@ module ItvPure = struct let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2) - let invalid : t -> bool = function Bound.PInf, _ | _, Bound.MInf -> true | l, u -> Bound.lt u l + let is_invalid : t -> bool = function + | Bound.PInf, _ | _, Bound.MInf + -> true + | l, u + -> Bound.lt u l let prune_le : t -> t -> t = fun x y -> @@ -922,7 +926,7 @@ module ItvPure = struct let prune_comp : Binop.t -> t -> t -> t option = fun c x y -> - if invalid y then Some x + if is_invalid y then Some x else let x = match c with @@ -937,7 +941,7 @@ module ItvPure = struct | _ -> assert false in - if invalid x then None else Some x + if is_invalid x then None else Some x let prune_eq : t -> t -> t option = fun x y -> @@ -945,10 +949,10 @@ module ItvPure = struct let prune_ne : t -> t -> t option = fun x (l, u) -> - if invalid (l, u) then Some x + if is_invalid (l, u) then Some x else let x = if Bound.eq l u then diff x l else x in - if invalid x then None else Some x + if is_invalid x then None else Some x let get_symbols : t -> Symbol.t list = fun (l, u) -> List.append (Bound.get_symbols l) (Bound.get_symbols u) @@ -956,7 +960,7 @@ module ItvPure = struct let make_positive : t -> t = fun (l, u as x) -> if Bound.lt l Bound.zero then (Bound.zero, u) else x - let normalize : t -> t option = fun (l, u) -> if invalid (l, u) then None else Some (l, u) + let normalize : t -> t option = fun (l, u) -> if is_invalid (l, u) then None else Some (l, u) end include AbstractDomain.BottomLifted (ItvPure) @@ -1024,8 +1028,6 @@ let zero = NonBottom ItvPure.zero let make : Bound.t -> Bound.t -> t = fun l u -> if Bound.lt u l then Bottom else NonBottom (ItvPure.make l u) -let invalid : t -> bool = function NonBottom x -> ItvPure.invalid x | Bottom -> false - let is_symbolic : t -> bool = function NonBottom x -> ItvPure.is_symbolic x | Bottom -> false let le : lhs:t -> rhs:t -> bool = ( <= ) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/duplicates.c b/infer/tests/codetoanalyze/c/bufferoverrun/duplicates.c new file mode 100644 index 000000000..fbfcc95bb --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/duplicates.c @@ -0,0 +1,19 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +void two_accesses(int* arr) { + if (arr[1] < 0) { + arr[1] = 0; + } +} + +void one_alarm_is_enough() { + int arr[1]; + two_accesses(arr); +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index aea7bb4b8..1fb5af523 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -7,6 +7,8 @@ codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16 codetoanalyze/c/bufferoverrun/cast.c, cast2_Good_FP, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [4, 4] Size: [4, 4]] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,Call,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,Call,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] +codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN, [ArrayDeclaration,Call,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:11:7 by call `two_accesses()` ] +codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN, [ArrayDeclaration,Call,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:12:5 by call `two_accesses()` ] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 7, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [20, 20] Size: [10, 10]]