diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 7fbf8ef0b..f2ffc79f8 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -16,6 +16,8 @@ open AbsLoc module F = Format module L = Logging module Dom = BufferOverrunDomain +module Trace = BufferOverrunTrace +module TraceSet = Trace.Set module Summary = Summary.Make (struct type payload = Dom.Summary.t @@ -53,13 +55,15 @@ struct let model_malloc : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node - -> Dom.Mem.astate -> Dom.Mem.astate - = fun pname ret params node mem -> + -> Location.t -> Dom.Mem.astate -> Dom.Mem.astate + = fun pname ret params node location mem -> match ret with | Some (id, _) -> let (typ, stride, length0) = get_malloc_info (List.hd_exn params |> fst) in - let length = Sem.eval length0 mem (CFG.loc node) |> Dom.Val.get_itv in - let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in + let length = Sem.eval length0 mem (CFG.loc node) in + let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in + let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1 + |> Dom.Val.set_traces traces in mem |> Dom.Mem.add_stack (Loc.of_id id) v |> set_uninitialized node typ (Dom.Val.get_array_locs v) @@ -70,9 +74,9 @@ struct let model_realloc : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node - -> Dom.Mem.astate -> Dom.Mem.astate - = fun pname ret params node mem -> - model_malloc pname ret (List.tl_exn params) node mem + -> Location.t -> Dom.Mem.astate -> Dom.Mem.astate + = fun pname ret params node location mem -> + model_malloc pname ret (List.tl_exn params) node location mem let model_by_value value ret mem = match ret with @@ -120,8 +124,8 @@ struct | "fgetc" -> model_by_value Dom.Val.Itv.m1_255 ret mem | "infer_print" -> model_infer_print params mem loc | "malloc" - | "__new_array" -> model_malloc pname ret params node mem - | "realloc" -> model_realloc pname ret params node mem + | "__new_array" -> model_malloc pname ret params node loc mem + | "realloc" -> model_realloc pname ret params node loc mem | "__set_array_length" -> model_infer_set_array_length pname node params mem loc | "strlen" -> model_by_value Dom.Val.Itv.nat ret mem | proc_name -> @@ -132,12 +136,13 @@ struct |> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown let rec declare_array - : Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> length:IntLit.t option -> ?stride:int - -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate - = fun pname node loc typ ~length ?stride ~inst_num ~dimension mem -> + : Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t -> length:IntLit.t option + -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate + = fun pname node location loc typ ~length ?stride ~inst_num ~dimension mem -> let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in let arr = Sem.eval_array_alloc pname node typ Itv.zero size ?stride inst_num dimension + |> Dom.Val.add_trace_elem (Trace.ArrDecl location) in let mem = if Int.equal dimension 1 @@ -149,8 +154,8 @@ struct in match typ.Typ.desc with | Typ.Tarray (typ, length, stride) -> - declare_array pname node loc typ ~length ?stride:(Option.map ~f:IntLit.to_int stride) - ~inst_num ~dimension:(dimension + 1) mem + declare_array pname node location loc typ ~length + ?stride:(Option.map ~f:IntLit.to_int stride) ~inst_num ~dimension:(dimension + 1) mem | _ -> mem let counter_gen init = @@ -163,9 +168,9 @@ struct get_num let declare_symbolic_val - : Typ.Procname.t -> Tenv.t -> CFG.node -> Loc.t -> Typ.typ + : Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> Loc.t -> Typ.typ -> inst_num:int -> new_sym_num: (unit -> int) -> Domain.t -> Domain.t - = fun pname tenv node loc typ ~inst_num ~new_sym_num mem -> + = fun pname tenv node location loc typ ~inst_num ~new_sym_num mem -> let max_depth = 2 in let new_alloc_num = counter_gen 1 in let rec decl_sym_val ~depth loc typ mem = @@ -174,17 +179,21 @@ struct match typ.Typ.desc with | Typ.Tint ikind -> let unsigned = Typ.ikind_is_unsigned ikind in - let v = Dom.Val.make_sym ~unsigned pname new_sym_num in + let v = Dom.Val.make_sym ~unsigned pname new_sym_num + |> Dom.Val.add_trace_elem (Trace.SymAssign location) + in Dom.Mem.add_heap loc v mem | Typ.Tfloat _ -> - let v = Dom.Val.make_sym pname new_sym_num in + let v = Dom.Val.make_sym pname new_sym_num + |> Dom.Val.add_trace_elem (Trace.SymAssign location) + in Dom.Mem.add_heap loc v mem | Typ.Tptr (typ, _) -> - decl_sym_arr ~depth loc typ mem + decl_sym_arr ~depth loc location typ mem | Typ.Tarray (typ, opt_int_lit, _) -> let opt_size = Option.map ~f:Itv.of_int_lit opt_int_lit in let opt_offset = Some Itv.zero in - decl_sym_arr ~depth loc typ ~opt_offset ~opt_size mem + decl_sym_arr ~depth loc location typ ~opt_offset ~opt_size mem | Typ.Tstruct typename -> let decl_fld mem (fn, typ, _) = let loc_fld = Loc.append_field loc fn in @@ -202,7 +211,7 @@ struct Location.pp (CFG.loc node); mem - and decl_sym_arr ~depth loc typ ?(opt_offset=None) ?(opt_size=None) mem = + and decl_sym_arr ~depth loc location typ ?(opt_offset=None) ?(opt_size=None) mem = let option_value opt_x default_f = match opt_x with | Some x -> x @@ -212,8 +221,10 @@ struct let offset = option_value opt_offset itv_make_sym in let size = option_value opt_size itv_make_sym in let alloc_num = new_alloc_num () in + let elem = Trace.SymAssign location in let arr = Sem.eval_array_alloc pname node typ offset size inst_num alloc_num + |> Dom.Val.add_trace_elem elem in let mem = Dom.Mem.add_heap loc arr mem in let deref_loc = @@ -224,27 +235,28 @@ struct decl_sym_val ~depth:0 loc typ mem let declare_symbolic_parameter - : Procdesc.t -> Tenv.t -> CFG.node -> int -> Dom.Mem.astate -> Dom.Mem.astate - = fun pdesc tenv node inst_num mem -> + : Procdesc.t -> Tenv.t -> CFG.node -> Location.t -> int -> Dom.Mem.astate -> Dom.Mem.astate + = fun pdesc tenv node location inst_num mem -> let pname = Procdesc.get_proc_name pdesc in let new_sym_num = counter_gen 0 in let add_formal (mem, inst_num) (pvar, typ) = let loc = Loc.of_pvar pvar in let mem = - declare_symbolic_val pname tenv node loc typ ~inst_num ~new_sym_num mem + declare_symbolic_val pname tenv node location loc typ ~inst_num ~new_sym_num mem in (mem, inst_num + 1) in List.fold ~f:add_formal ~init:(mem, inst_num) (Sem.get_formals pdesc) |> fst - let instantiate_ret ret callee_pname callee_exit_mem subst_map mem = + let instantiate_ret ret callee_pname callee_exit_mem subst_map mem loc = match ret with | Some (id, _) -> let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in let ret_var = Loc.of_var (Var.of_id id) in - Dom.Val.subst ret_val subst_map + Dom.Val.subst ret_val subst_map loc + |> Dom.Val.add_trace_elem (Trace.Return loc) |> Fn.flip (Dom.Mem.add_stack ret_var) mem | None -> mem @@ -264,7 +276,7 @@ struct let formal_fields = PowLoc.append_field formal_locs fn in let v = Dom.Mem.find_heap_set formal_fields callee_exit_mem in let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) fn in - Dom.Val.subst v subst_map + Dom.Val.subst v subst_map location |> Fn.flip (Dom.Mem.strong_update_heap actual_fields) mem in List.fold ~f:instantiate_fld ~init:mem str.Typ.Struct.fields @@ -274,7 +286,7 @@ struct |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in let v = Dom.Mem.find_heap_set formal_locs callee_exit_mem in let actual_locs = Dom.Val.get_all_locs actual in - Dom.Val.subst v subst_map + Dom.Val.subst v subst_map location |> Fn.flip (Dom.Mem.strong_update_heap actual_locs) mem) | _ -> mem in @@ -291,7 +303,7 @@ struct let subst_map = Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc in - instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem + instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem loc |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map loc | None -> caller_mem @@ -321,7 +333,8 @@ struct |> Dom.Mem.load_alias id exp | Store (exp1, _, exp2, loc) -> let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in - Dom.Mem.update_mem locs (Sem.eval exp2 mem loc) mem + let v = Sem.eval exp2 mem loc |> Dom.Val.add_trace_elem (Trace.Assign loc) in + Dom.Mem.update_mem locs v mem |> Dom.Mem.store_alias exp1 exp2 | Prune (exp, loc, _, _) -> Sem.prune exp loc mem | Call (ret, Const (Cfun callee_pname), params, loc, _) -> @@ -331,21 +344,22 @@ struct instantiate_mem tenv ret callee callee_pname params mem summary loc | None -> handle_unknown_call pname ret callee_pname params node mem loc) - | Declare_locals (locals, _) -> + | Declare_locals (locals, location) -> (* array allocation in stack e.g., int arr[10] *) - let try_decl_arr (mem, inst_num) (pvar, typ) = + let try_decl_arr location (mem, inst_num) (pvar, typ) = match typ.Typ.desc with | Typ.Tarray (typ, length, stride0) -> let loc = Loc.of_pvar pvar in let stride = Option.map ~f:IntLit.to_int stride0 in let mem = - declare_array pname node loc typ ~length ?stride ~inst_num ~dimension:1 mem + declare_array pname node location loc typ ~length ?stride ~inst_num + ~dimension:1 mem in (mem, inst_num + 1) | _ -> (mem, inst_num) in - let (mem, inst_num) = List.fold ~f:try_decl_arr ~init:(mem, 1) locals in - declare_symbolic_parameter pdesc tenv node inst_num mem + let (mem, inst_num) = List.fold ~f:(try_decl_arr location) ~init:(mem, 1) locals in + declare_symbolic_parameter pdesc tenv node location inst_num mem | Call (_, fun_exp, _, loc, _) -> let () = L.(debug BufferOverrun Verbose) "/!\\ Call to non-const function %a at %a" @@ -377,23 +391,33 @@ struct let array_access = match exp with | Exp.Var _ -> - let arr = Sem.eval exp mem loc |> Dom.Val.get_array_blk in - Some (arr, Itv.zero, true) + let v = Sem.eval exp mem loc in + let arr = Dom.Val.get_array_blk v in + let arr_traces = Dom.Val.get_traces v in + Some (arr, arr_traces, Itv.zero, TraceSet.empty, true) | Exp.Lindex (e1, e2) -> let locs = Sem.eval_locs e1 mem loc |> Dom.Val.get_all_locs in - let arr = Dom.Mem.find_set locs mem |> Dom.Val.get_array_blk in - let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in - Some (arr, idx, true) + let v_arr = Dom.Mem.find_set locs mem in + let arr = Dom.Val.get_array_blk v_arr in + let arr_traces = Dom.Val.get_traces v_arr in + let v_idx = Sem.eval e2 mem loc in + let idx = Dom.Val.get_itv v_idx in + let idx_traces = Dom.Val.get_traces v_idx in + Some (arr, arr_traces, idx, idx_traces, true) | Exp.BinOp (Binop.PlusA as bop, e1, e2) | Exp.BinOp (Binop.MinusA as bop, e1, e2) -> - let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in - let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in + let v_arr = Sem.eval e1 mem loc in + let arr = Dom.Val.get_array_blk v_arr in + let arr_traces = Dom.Val.get_traces v_arr in + let v_idx = Sem.eval e2 mem loc in + let idx = Dom.Val.get_itv v_idx in + let idx_traces = Dom.Val.get_traces v_idx in let is_plus = Binop.equal bop Binop.PlusA in - Some (arr, idx, is_plus) + Some (arr, arr_traces, idx, idx_traces, is_plus) | _ -> None in match array_access with - | Some (arr, idx, is_plus) -> + | Some (arr, traces_arr, idx, traces_idx, is_plus) -> let site = Sem.get_allocsite pname node 0 0 in let size = ArrayBlk.sizeof arr in let offset = ArrayBlk.offsetof arr in @@ -403,7 +427,8 @@ struct L.(debug BufferOverrun Verbose) " idx: %a@," Itv.pp idx; L.(debug BufferOverrun Verbose) "@]@."; if size <> Itv.bot && idx <> Itv.bot then - Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx cond_set + let traces = TraceSet.merge ~traces_arr ~traces_idx loc in + Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx traces cond_set else cond_set | None -> cond_set @@ -506,13 +531,31 @@ struct let add_node1 acc node = collect_node pdata inv_map acc node in Procdesc.fold_nodes add_node1 Dom.ConditionSet.empty pdesc + let make_err_trace : Trace.t -> string -> Errlog.loc_trace + = fun trace desc -> + let f elem (trace,depth) = + match elem with + | Trace.Assign loc -> + ((Errlog.make_trace_element depth loc "Assignment" []) :: trace, depth) + | Trace.ArrDecl loc -> + ((Errlog.make_trace_element depth loc "ArrayDeclaration" []) :: trace, depth) + | Trace.Call loc -> + ((Errlog.make_trace_element depth loc "Call" []) :: trace, depth + 1) + | Trace.Return loc -> + ((Errlog.make_trace_element (depth - 1) loc "Return" []) :: trace, depth - 1) + | Trace.SymAssign _ -> (trace,depth) + | Trace.ArrAccess loc -> + ((Errlog.make_trace_element depth loc ("ArrayAccess: " ^ desc) []) :: trace, depth) + in + List.fold_right ~f ~init:([],0) trace.trace |> fst |> List.rev + let report_error : Procdesc.t -> Dom.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_trace cond with + 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 @@ -523,7 +566,9 @@ struct let error_desc = Localise.desc_buffer_overrun bucket description in let exn = Exceptions.Checkers (Localise.to_issue_id Localise.buffer_overrun, error_desc) in - let trace = [Errlog.make_trace_element 0 loc description []] 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 []] in Reporting.log_error_deprecated pname ~loc ~ltr:trace exn | _ -> () in diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index d6b0ba9db..dec293b16 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -16,22 +16,25 @@ open AbsLoc module F = Format module L = Logging module MF = MarkupFormatter +module Trace = BufferOverrunTrace +module TraceSet = Trace.Set let always_strong_update = true (* unsound but ok for bug catching *) module Condition = struct - type trace = Intra of Typ.Procname.t - | Inter of Typ.Procname.t * Typ.Procname.t * Location.t + 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; - trace : trace; + cond_trace : cond_trace; idx : Itv.astate; size : Itv.astate; + traces : TraceSet.t; } [@@deriving compare] @@ -53,25 +56,27 @@ struct if Config.bo_debug <= 1 then F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c else - match c.trace with + 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" + F.fprintf fmt "%a < %a at %a by call %s() at %a (%a)" Itv.pp c.idx Itv.pp c.size pp_location c pname Location.pp_file_pos loc - | Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c + TraceSet.pp c.traces + | Intra _ -> F.fprintf fmt "%a < %a at %a (%a)" Itv.pp c.idx Itv.pp c.size pp_location c + TraceSet.pp c.traces let get_location : t -> Location.t = fun c -> c.loc - let get_trace : t -> trace - = fun c -> c.trace + 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:Itv.t -> size:Itv.t -> t - = fun proc_name loc id ~idx ~size -> - { proc_name; idx; size; loc; id ; trace = Intra proc_name } + let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.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 -> @@ -138,19 +143,28 @@ struct = fun c -> let c = set_size_pos c in "Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size - ^ (match c.trace with + ^ (match c.cond_trace with | Inter (_, pname, _) -> let loc = pp_location F.str_formatter c; F.flush_str_formatter () in " @ " ^ loc ^ " by call " ^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " " | Intra _ -> "") - let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t - = fun c subst_map caller_pname callee_pname loc -> + let subst : t -> (Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) -> Typ.Procname.t -> + Typ.Procname.t -> Location.t -> t + = fun c (bound_map, trace_map) caller_pname callee_pname loc -> if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then - { c with idx = Itv.subst c.idx subst_map; - size = Itv.subst c.size subst_map; - trace = Inter (caller_pname, callee_pname, loc) } + let symbols = Itv.get_symbols c.idx @ Itv.get_symbols c.size in + 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 + { c with idx = Itv.subst c.idx bound_map; + size = Itv.subst c.size bound_map; + cond_trace = Inter (caller_pname, callee_pname, loc); + traces } else c end @@ -161,11 +175,12 @@ struct module Map = Caml.Map.Make (Location) let add_bo_safety - : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t -> t - = fun pname loc id ~idx ~size cond -> - add (Condition.make pname loc id ~idx ~size) cond + : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.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 Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t + let subst : t -> (Itv.Bound.t 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 -> add (Condition.subst e subst_map caller_pname callee_pname loc)) x empty @@ -205,15 +220,23 @@ struct itv : Itv.astate; powloc : PowLoc.astate; arrayblk : ArrayBlk.astate; + traces : TraceSet.t; } type t = astate let bot : t - = { itv = Itv.bot; powloc = PowLoc.bot; arrayblk = ArrayBlk.bot } + = { itv = Itv.bot; powloc = PowLoc.bot; arrayblk = ArrayBlk.bot; traces = TraceSet.empty } + + let pp fmt x = + if Config.bo_debug <= 1 then + F.fprintf fmt "(%a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk + else + F.fprintf fmt "(%a, %a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk + TraceSet.pp x.traces let unknown : t - = { itv = Itv.top; powloc = PowLoc.unknown; arrayblk = ArrayBlk.unknown } + = { bot with itv = Itv.top; powloc = PowLoc.unknown; arrayblk = ArrayBlk.unknown } let (<=) ~lhs ~rhs = if phys_equal lhs rhs then true @@ -227,10 +250,8 @@ struct else { itv = Itv.widen ~prev:(prev.itv) ~next:(next.itv) ~num_iters; powloc = PowLoc.widen ~prev:(prev.powloc) ~next:(next.powloc) ~num_iters; - arrayblk = ArrayBlk.widen ~prev:(prev.arrayblk) ~next:(next.arrayblk) ~num_iters; } - - let pp fmt x = - F.fprintf fmt "(%a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk + arrayblk = ArrayBlk.widen ~prev:(prev.arrayblk) ~next:(next.arrayblk) ~num_iters; + traces = TraceSet.join prev.traces next.traces; } let join : t -> t -> t = fun x y -> @@ -238,7 +259,8 @@ struct else { itv = Itv.join x.itv y.itv; powloc = PowLoc.join x.powloc y.powloc; - arrayblk = ArrayBlk.join x.arrayblk y.arrayblk } + arrayblk = ArrayBlk.join x.arrayblk y.arrayblk; + traces = TraceSet.join x.traces y.traces; } let rec joins : t list -> t = function @@ -261,6 +283,12 @@ struct let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x) + let get_traces : t -> TraceSet.t + = fun x -> x.traces + + let set_traces : TraceSet.t -> t -> t + = fun traces x -> { x with traces } + let of_itv itv = { bot with itv } let of_int n = of_itv (Itv.of_int n) @@ -305,19 +333,20 @@ struct let plus : t -> t -> t = fun x y -> - { x with itv = Itv.plus x.itv y.itv; arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv } + { x with itv = Itv.plus x.itv y.itv; arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv; + traces = TraceSet.join x.traces y.traces } let minus : t -> t -> t = fun x y -> let n = Itv.join (Itv.minus x.itv y.itv) (ArrayBlk.diff x.arrayblk y.arrayblk) in let a = ArrayBlk.minus_offset x.arrayblk y.itv in - { bot with itv = n; arrayblk = a} + { bot with itv = n; arrayblk = a; traces = TraceSet.join x.traces y.traces } let mult : t -> t -> t - = lift_itv Itv.mult + = fun x y -> { (lift_itv Itv.mult x y) with traces = TraceSet.join x.traces y.traces } let div : t -> t -> t - = lift_itv Itv.div + = fun x y -> { (lift_itv Itv.div x y) with traces = TraceSet.join x.traces y.traces } let mod_sem : t -> t -> t = lift_itv Itv.mod_sem @@ -359,7 +388,8 @@ struct : (Itv.t -> Itv.t -> Itv.t) -> (ArrayBlk.astate -> ArrayBlk.astate -> ArrayBlk.astate) -> t -> t -> t = fun f g x y -> - { x with itv = f x.itv y.itv; arrayblk = g x.arrayblk y.arrayblk } + { x with itv = f x.itv y.itv; arrayblk = g x.arrayblk y.arrayblk; + traces = TraceSet.join x.traces y.traces } let prune_zero : t -> t = lift_prune1 Itv.prune_zero @@ -373,13 +403,15 @@ struct let prune_ne : t -> t -> t = lift_prune2 Itv.prune_ne ArrayBlk.prune_eq + let lift_pi : (ArrayBlk.astate -> Itv.t -> ArrayBlk.astate) -> t -> t -> t + = fun f x y -> + { bot with arrayblk = f x.arrayblk y.itv; traces = TraceSet.join x.traces y.traces } + let plus_pi : t -> t -> t - = fun x y -> - { bot with powloc = x.powloc; arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv } + = fun x y -> lift_pi ArrayBlk.plus_offset x y let minus_pi : t -> t -> t - = fun x y -> - { bot with powloc = x.powloc; arrayblk = ArrayBlk.minus_offset x.arrayblk y.itv } + = fun x y -> lift_pi ArrayBlk.minus_offset x y let minus_pp : t -> t -> t = fun x y -> @@ -387,7 +419,8 @@ struct if (not (PowLoc.is_bot x.powloc) && ArrayBlk.is_bot x.arrayblk) || (not (PowLoc.is_bot y.powloc) && ArrayBlk.is_bot y.arrayblk) then { bot with itv = Itv.top } - else { bot with itv = ArrayBlk.diff x.arrayblk y.arrayblk } + else { bot with itv = ArrayBlk.diff x.arrayblk y.arrayblk; + traces = TraceSet.join x.traces y.traces } let get_symbols : t -> Itv.Symbol.t list = fun x -> @@ -397,12 +430,28 @@ struct = fun x -> { x with itv = Itv.normalize x.itv; arrayblk = ArrayBlk.normalize x.arrayblk } - let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t - = fun x subst_map -> - { x with itv = Itv.subst x.itv subst_map; - arrayblk = ArrayBlk.subst x.arrayblk subst_map } + let subst : t -> (Itv.Bound.t Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) -> Location.t -> t + = fun x (bound_map, trace_map) loc -> + let symbols = get_symbols x in + let traces_caller = List.fold ~f:(fun traces symbol -> + try + TraceSet.join (Itv.SubstMap.find symbol trace_map) traces + with _ -> traces) ~init:TraceSet.empty symbols in + let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces loc in + { x with itv = Itv.subst x.itv bound_map; arrayblk = ArrayBlk.subst x.arrayblk bound_map; + traces } |> normalize (* normalize bottom *) + let add_trace_elem : Trace.elem -> t -> t + = fun elem x -> + let traces = TraceSet.add_elem elem x.traces in + { x with traces } + + let add_trace_elem_last : Trace.elem -> t -> t + = fun elem x -> + let traces = TraceSet.add_elem_last elem x.traces in + { x with traces } + let pp_summary : F.formatter -> t -> unit = fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index fd32820a3..9bd874ca3 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -16,6 +16,8 @@ open AbsLoc module F = Format module L = Logging module Domain = BufferOverrunDomain +module Trace = BufferOverrunTrace +module TraceSet = Trace.Set open Domain module Make (CFG : ProcCfg.S) = @@ -376,7 +378,7 @@ struct let get_matching_pairs : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate - -> (Itv.Bound.t * Itv.Bound.t) list + -> (Itv.Bound.t * Itv.Bound.t * TraceSet.t) list = fun tenv formal actual typ caller_mem callee_mem -> let get_itv v = Val.get_itv v in let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in @@ -386,20 +388,20 @@ struct Mem.find_heap_set (PowLoc.append_field (Val.get_all_locs v) fn) mem in let deref_ptr v mem = Mem.find_heap_set (Val.get_array_locs v) mem in - let add_pair_itv itv1 itv2 l = + let add_pair_itv itv1 itv2 traces l = let open Itv in if itv1 <> bot && itv1 <> top && itv2 <> bot then - (lb itv1, lb itv2) :: (ub itv1, ub itv2) :: l + (lb itv1, lb itv2, traces) :: (ub itv1, ub itv2, traces) :: l else if itv1 <> bot && itv1 <> top && Itv.eq itv2 bot then - (lb itv1, Bound.Bot) :: (ub itv1, Bound.Bot) :: l + (lb itv1, Bound.Bot, TraceSet.empty) :: (ub itv1, Bound.Bot, TraceSet.empty) :: l else l in let add_pair_val v1 v2 pairs = pairs - |> add_pair_itv (get_itv v1) (get_itv v2) - |> add_pair_itv (get_offset v1) (get_offset v2) - |> add_pair_itv (get_size v1) (get_size v2) + |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) + |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) + |> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) in let add_pair_field v1 v2 pairs fn = let v1' = deref_field v1 fn callee_mem in @@ -422,22 +424,23 @@ struct in [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual - let subst_map_of_pairs - : (Itv.Bound.t * Itv.Bound.t) list -> Itv.Bound.t Itv.SubstMap.t + let subst_map_of_pairs : (Itv.Bound.t * Itv.Bound.t * TraceSet.t) list + -> (Itv.Bound.t Itv.SubstMap.t) * (TraceSet.t Itv.SubstMap.t) = fun pairs -> - let add_pair map (formal, actual) = + let add_pair (bound_map, trace_map) (formal, actual, traces) = match formal with - | Itv.Bound.Linear (_, se1) when Itv.SymLinear.is_zero se1 -> map + | Itv.Bound.Linear (_, se1) when Itv.SymLinear.is_zero se1 -> (bound_map, trace_map) | Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 -> let (symbol, coeff) = Itv.SymLinear.choose se1 in if Int.equal coeff 1 - then Itv.SubstMap.add symbol actual map + then + (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map) else assert false | Itv.Bound.MinMax (Itv.Bound.Max, 0, symbol) -> - Itv.SubstMap.add symbol actual map + (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map) | _ -> assert false in - List.fold ~f:add_pair ~init:Itv.SubstMap.empty pairs + List.fold ~f:add_pair ~init:(Itv.SubstMap.empty, Itv.SubstMap.empty) pairs let rec list_fold2_def : default:Val.t -> f:('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> init:'b -> 'b @@ -450,7 +453,7 @@ struct let get_subst_map : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate - -> Location.t -> Itv.Bound.t Itv.SubstMap.t + -> Location.t -> (Itv.Bound.t Itv.SubstMap.t) * (TraceSet.t Itv.SubstMap.t) = fun tenv callee_pdesc params caller_mem callee_entry_mem loc -> let add_pair (formal, typ) actual l = let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml new file mode 100644 index 000000000..3f6f62dcb --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -0,0 +1,85 @@ +(* + * 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 + +module F = Format + +module BoTrace = +struct + type elem = ArrAccess of Location.t | ArrDecl of Location.t | Assign of Location.t + | Call of Location.t | Return of Location.t | SymAssign of Location.t + [@@deriving compare] + type t = { length : int; trace : elem list } [@@deriving compare] + let empty = { length = 0; trace = [] } + let singleton elem = { length = 1; trace = [elem] } + let add_elem elem t = { length = t.length + 1; trace = elem :: t.trace } + let add_elem_last elem t = { length = t.length + 1; trace = t.trace @ [elem] } + let append x y = { length = x.length + y.length; trace = x.trace @ y.trace } + + let pp_elem : F.formatter -> elem -> unit + = fun fmt elem -> + match elem with + | Assign loc -> F.fprintf fmt "Assign (%a)" Location.pp_file_pos loc + | ArrDecl loc -> F.fprintf fmt "ArrDecl (%a)" Location.pp_file_pos loc + | Call loc -> F.fprintf fmt "Call (%a)" Location.pp_file_pos loc + | Return loc -> F.fprintf fmt "Return (%a)" Location.pp_file_pos loc + | SymAssign loc -> F.fprintf fmt "SymAssign (%a)" Location.pp_file_pos loc + | ArrAccess loc -> F.fprintf fmt "ArrAccess (%a)" Location.pp_file_pos loc + + let pp : F.formatter -> t -> unit + = fun fmt t -> + let pp_sep fmt () = F.fprintf fmt " :: " in + F.pp_print_list ~pp_sep pp_elem fmt t.trace +end + +module Set = +struct + include AbstractDomain.FiniteSet(BoTrace) + (* currently, we keep only one trace for efficiency *) + let join x y = + if is_empty x then y + else if is_empty y then x + else + let (tx, ty) = (min_elt x, min_elt y) in + if Pervasives.(<=) tx.length ty.length then x + else y + + let choose_shortest set = min_elt set + + let add_elem elem t = + if is_empty t then singleton (BoTrace.singleton elem) + else map (BoTrace.add_elem elem) t + + let add_elem_last elem t = + if is_empty t then singleton (BoTrace.singleton elem) + else map (BoTrace.add_elem_last elem) t + + let instantiate ~traces_caller ~traces_callee loc = + if is_empty traces_caller then + map (fun trace_callee -> BoTrace.add_elem_last (BoTrace.Call loc) trace_callee) traces_callee + else + fold (fun trace_callee traces -> + fold (fun trace_caller traces -> + let new_trace_caller = BoTrace.add_elem (BoTrace.Call loc) trace_caller in + let new_trace = BoTrace.append trace_callee new_trace_caller in + add new_trace traces) traces_caller traces) traces_callee empty + + let merge ~traces_arr ~traces_idx loc = + if is_empty traces_idx then + map (fun trace_arr -> BoTrace.add_elem (BoTrace.ArrAccess loc) trace_arr) traces_arr + else + fold (fun trace_idx traces -> + fold (fun trace_arr traces -> + let new_trace_idx = BoTrace.add_elem (BoTrace.ArrAccess loc) trace_idx in + let new_trace = BoTrace.append new_trace_idx trace_arr in + add new_trace traces) traces_arr traces) traces_idx empty +end + +include BoTrace diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index a367931ba..e6629e615 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,34 +1,34 @@ -codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]] -codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]] +codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]] +codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]] codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, [] -codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/cast.c, cast2_Good_FP, 2, BUFFER_OVERRUN, [Offset: [4, 4] Size: [4, 4]] -codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [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, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] -codetoanalyze/c/bufferoverrun/external.c, extern_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/c/bufferoverrun/external.c, extern_bad, 7, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/external.c, extern_bad, 8, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN, [Offset: [30, 30] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10]] +codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]] +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/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]] +codetoanalyze/c/bufferoverrun/external.c, extern_bad, 8, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]] codetoanalyze/c/bufferoverrun/for_loop.c, safealloc, 10, UNREACHABLE_CODE, [] -codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:21:3 by call `arr_access()` ] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:22:3 by call `arr_access()` ] -codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:21:3 by call `arr_access()` ] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,Call,ArrayAccess: Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:22:3 by call `arr_access()` ] +codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, [] -codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN, [Offset: [0, 255] Size: [255, 255]] -codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN, [Offset: [-1, 255] Size: [10000, 10000]] -codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1]] +codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: [255, 255]] +codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, 255] Size: [10000, 10000]] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1]] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, [] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, [] @@ -50,10 +50,10 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, COND codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, [] -codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0]] -codetoanalyze/c/bufferoverrun/sizeof.c, sizeof_char_good_FP, 2, BUFFER_OVERRUN, [Offset: [79, 79] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0]] -codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]] +codetoanalyze/c/bufferoverrun/sizeof.c, sizeof_char_good_FP, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [79, 79] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]] +codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/unreachable.c, FP_exit_at_end_of_proc_good, 2, UNREACHABLE_CODE, [] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, [] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_break_good, 1, CONDITION_ALWAYS_TRUE, [] @@ -66,4 +66,4 @@ codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_with_else_bad codetoanalyze/c/bufferoverrun/unreachable.c, infinite_loop_bad, 1, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/unreachable.c, never_loops_bad, 1, CONDITION_ALWAYS_FALSE, [] codetoanalyze/c/bufferoverrun/unreachable.c, unreachable_statement_exit_bad, 1, UNREACHABLE_CODE, [] -codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 9c81cc90e..caf27d4da 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,23 +1,23 @@ -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 4, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 7, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 8, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN, [Offset: [30, 30] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector*,std::allocator*>>_operator[]()` ] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `ral()` ] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]] -codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] -codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] -codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:17 by call `std::vector>_vector()` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:31 by call `std::vector>_vector()` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_at()` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, 0] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN, [Call,Assignment,Call,Assignment,Return,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN, [Call,Call,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 7, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [20, 20] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 8, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN, [Call,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector*,std::allocator*>>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `ral()` ] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [ArrayAccess: Offset: [-oo, +oo] Size: [16, 16]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [ArrayAccess: Offset: [-oo, +oo] Size: [16, 16]] +codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] +codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] +codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:17 by call `std::vector>_vector()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:31 by call `std::vector>_vector()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_at()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector>_operator[]()` ]