From fb4086c6f604657c1e687f02c158aa41fc0e5317 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 18 Oct 2018 01:31:44 -0700 Subject: [PATCH] [inferbo] Add integer overflow issue type Reviewed By: mbouaziz Differential Revision: D10253878 fbshipit-source-id: 9905d7db4 --- infer/src/IR/Typ.ml | 42 +++++ infer/src/IR/Typ.mli | 6 + infer/src/base/IssueType.ml | 8 + infer/src/base/IssueType.mli | 8 + .../src/bufferoverrun/bufferOverrunChecker.ml | 116 +++++++++--- .../bufferOverrunProofObligations.ml | 172 +++++++++++++++++- .../bufferOverrunProofObligations.mli | 10 + infer/src/bufferoverrun/bufferOverrunTrace.ml | 3 + infer/src/bufferoverrun/bufferOverrunUtils.ml | 18 ++ .../src/bufferoverrun/bufferOverrunUtils.mli | 9 + infer/src/bufferoverrun/itv.mli | 6 + .../introduced.exp | 1 + .../codetoanalyze/c/bufferoverrun/arith.c | 16 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 26 ++- .../c/bufferoverrun/prune_alias.c | 18 ++ .../codetoanalyze/c/performance/issues.exp | 23 +++ .../cpp/bufferoverrun/issues.exp | 20 ++ .../codetoanalyze/java/performance/issues.exp | 22 +++ 18 files changed, 482 insertions(+), 42 deletions(-) diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 62cbd3e46..208c715ce 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -55,6 +55,8 @@ type ikind = | IU128 (** [__uint128_t] *) [@@deriving compare] +let equal_ikind = [%compare.equal: ikind] + let ikind_to_string = function | IChar -> "char" @@ -86,6 +88,46 @@ let ikind_to_string = function "__uint128_t" +let range_of_ikind = + let range bits ~signed = + if signed then + let bound = Z.(shift_left ~$1) (bits - 1) in + Z.(~-bound, bound - ~$1) + else Z.(~$0, shift_left ~$1 bits - ~$1) + in + let u1 = range 1 ~signed:false in + let s128 = range 128 ~signed:true in + let u128 = range 128 ~signed:false in + fun {IntegerWidths.char_width; short_width; int_width; long_width; longlong_width} x -> + match x with + | IBool -> + u1 + | ISChar -> + range char_width ~signed:true + | IChar | IUChar -> + range char_width ~signed:false + | IShort -> + range short_width ~signed:true + | IUShort -> + range short_width ~signed:false + | IInt -> + range int_width ~signed:true + | IUInt -> + range int_width ~signed:false + | ILong -> + range long_width ~signed:true + | IULong -> + range long_width ~signed:false + | ILongLong -> + range longlong_width ~signed:true + | IULongLong -> + range longlong_width ~signed:false + | I128 -> + s128 + | IU128 -> + u128 + + let ikind_is_char = function IChar | ISChar | IUChar -> true | _ -> false let ikind_is_unsigned = function diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index 356280b5b..bd934f4b4 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -41,6 +41,12 @@ type ikind = | IU128 (** [__uint128_t] *) [@@deriving compare] +val equal_ikind : ikind -> ikind -> bool + +val ikind_to_string : ikind -> string + +val range_of_ikind : IntegerWidths.t -> ikind -> Z.t * Z.t + val ikind_is_char : ikind -> bool (** Check whether the integer kind is a char *) diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index df1d26c09..5483f0fad 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -277,6 +277,14 @@ let infinite_execution_time_call = from_string ~enabled:false "INFINITE_EXECUTIO let inherently_dangerous_function = from_string "INHERENTLY_DANGEROUS_FUNCTION" +let integer_overflow_l1 = from_string "INTEGER_OVERFLOW_L1" + +let integer_overflow_l2 = from_string "INTEGER_OVERFLOW_L2" + +let integer_overflow_l5 = from_string "INTEGER_OVERFLOW_L5" + +let integer_overflow_u5 = from_string "INTEGER_OVERFLOW_U5" + let interface_not_thread_safe = from_string "INTERFACE_NOT_THREAD_SAFE" let internal_error = from_string "Internal_error" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 035c616a7..f672723d8 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -185,6 +185,14 @@ val infinite_execution_time_call : t val inherently_dangerous_function : t +val integer_overflow_l1 : t + +val integer_overflow_l2 : t + +val integer_overflow_l5 : t + +val integer_overflow_u5 : t + val interface_not_thread_safe : t val internal_error : t diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 8a2cf3e62..a64bc04d6 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -500,8 +500,8 @@ module Report = struct cond_set - let check_expr : Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t - = + let check_expr_for_array_access : + 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 @@ -531,6 +531,41 @@ module Report = struct cond_set + let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set = + match bop with + | Binop.PlusA (Some _) | Binop.MinusA (Some _) | Binop.Mult (Some _) -> + let lhs_v = Sem.eval lhs mem in + let rhs_v = Sem.eval rhs mem in + BoUtils.Check.binary_operation integer_type_widths bop ~lhs:lhs_v ~rhs:rhs_v location + cond_set + | _ -> + cond_set + + + let rec check_expr_for_integer_overflow integer_type_widths exp location mem cond_set = + match exp with + | Exp.UnOp (_, e, _) + | Exp.Exn e + | Exp.Lfield (e, _, _) + | Exp.Cast (_, e) + | Exp.Sizeof {dynamic_length= Some e} -> + check_expr_for_integer_overflow integer_type_widths e location mem cond_set + | Exp.BinOp (bop, lhs, rhs) -> + cond_set + |> check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem + |> check_expr_for_integer_overflow integer_type_widths lhs location mem + |> check_expr_for_integer_overflow integer_type_widths rhs location mem + | Exp.Lindex (e1, e2) -> + cond_set + |> check_expr_for_integer_overflow integer_type_widths e1 location mem + |> check_expr_for_integer_overflow integer_type_widths e2 location mem + | Exp.Closure {captured_vars} -> + List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) -> + check_expr_for_integer_overflow integer_type_widths e location mem cond_set ) + | Exp.Var _ | Exp.Const _ | Exp.Lvar _ | Exp.Sizeof {dynamic_length= None} -> + cond_set + + let instantiate_cond : Tenv.t -> Procdesc.t @@ -552,34 +587,48 @@ module Report = struct let check_instr : Procdesc.t -> Tenv.t + -> Typ.IntegerWidths.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 -> + fun pdesc tenv integer_type_widths symbol_table node instr mem cond_set -> match instr with - | Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) -> - check_expr exp location mem cond_set + | Sil.Load (_, exp, _, location) -> + cond_set + |> check_expr_for_array_access exp location mem + |> check_expr_for_integer_overflow integer_type_widths exp location mem + | Sil.Store (lexp, _, rexp, location) -> + cond_set + |> check_expr_for_array_access lexp location mem + |> check_expr_for_integer_overflow integer_type_widths lexp location mem + |> check_expr_for_integer_overflow integer_type_widths rexp location mem | 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 - | Some callee_summary -> ( - match Payload.of_summary callee_summary with - | Some callee_payload -> - let callee_pdesc = Summary.get_proc_desc callee_summary in - instantiate_cond tenv callee_pdesc params mem callee_payload location - |> PO.ConditionSet.join cond_set + let cond_set = + List.fold params ~init:cond_set ~f:(fun cond_set (exp, _) -> + check_expr_for_integer_overflow integer_type_widths exp location mem cond_set ) + in + 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 + | Some callee_summary -> ( + match Payload.of_summary callee_summary with + | Some callee_payload -> + let callee_pdesc = Summary.get_proc_desc callee_summary in + instantiate_cond tenv callee_pdesc params mem callee_payload location + |> PO.ConditionSet.join cond_set + | None -> + (* no inferbo payload *) cond_set ) | None -> - (* no inferbo payload *) cond_set ) - | None -> - (* unknown call *) cond_set ) ) + (* unknown call *) cond_set ) ) + | Sil.Prune (exp, location, _, _) -> + check_expr_for_integer_overflow integer_type_widths exp location mem cond_set | _ -> cond_set @@ -598,6 +647,7 @@ module Report = struct Summary.t -> Procdesc.t -> Tenv.t + -> Typ.IntegerWidths.t -> Itv.SymbolTable.t -> CFG.t -> CFG.Node.t @@ -605,7 +655,7 @@ module Report = struct -> Dom.Mem.astate AbstractInterpreter.State.t -> PO.ConditionSet.t -> PO.ConditionSet.t = - fun summary pdesc tenv symbol_table cfg node instrs state cond_set -> + fun summary pdesc tenv integer_type_widths symbol_table cfg node instrs state cond_set -> match state with | _ when Instrs.is_empty instrs -> cond_set @@ -622,7 +672,9 @@ module Report = struct | NonBottom _ -> () in - let cond_set = check_instr pdesc tenv symbol_table node instr pre cond_set in + let cond_set = + check_instr pdesc tenv integer_type_widths symbol_table node instr pre cond_set + in print_debug_info instr pre cond_set ; cond_set @@ -631,17 +683,19 @@ module Report = struct Summary.t -> Procdesc.t -> Tenv.t + -> Typ.IntegerWidths.t -> Itv.SymbolTable.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t -> CFG.Node.t -> PO.ConditionSet.t = - fun summary pdesc tenv symbol_table cfg inv_map cond_set node -> + fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map cond_set node -> match Analyzer.extract_state (CFG.Node.id node) inv_map with | Some state -> let instrs = CFG.instrs node in - check_instrs summary pdesc tenv symbol_table cfg node instrs state cond_set + check_instrs summary pdesc tenv integer_type_widths symbol_table cfg node instrs state + cond_set | _ -> cond_set @@ -650,13 +704,14 @@ module Report = struct Summary.t -> Procdesc.t -> Tenv.t + -> Typ.IntegerWidths.t -> Itv.SymbolTable.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t = - fun summary pdesc tenv symbol_table cfg inv_map -> + fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map -> CFG.fold_nodes cfg - ~f:(check_node summary pdesc tenv symbol_table cfg inv_map) + ~f:(check_node summary pdesc tenv integer_type_widths symbol_table cfg inv_map) ~init:PO.ConditionSet.empty @@ -674,6 +729,9 @@ module Report = struct (Errlog.make_trace_element depth location "ArrayDeclaration" [] :: trace, depth) | Trace.Assign location -> (Errlog.make_trace_element depth location "Assignment" [] :: trace, depth) + | Trace.Binop location -> + let desc = "Binop: " ^ issue_desc in + (Errlog.make_trace_element depth location desc [] :: trace, depth) | Trace.Call location -> (Errlog.make_trace_element depth location "Call" [] :: trace, depth + 1) | Trace.Return location -> @@ -734,7 +792,7 @@ let get_local_decls proc_desc = let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t = - fun {proc_desc; tenv; summary; integer_type_widths= _} -> + fun {proc_desc; tenv; integer_type_widths; summary} -> Preanal.do_preanalysis proc_desc tenv ; let symbol_table = Itv.SymbolTable.empty () in let pdata = ProcData.make proc_desc tenv symbol_table in @@ -747,7 +805,7 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_ |> Option.map ~f:(Dom.Mem.forget_locs locals) in let cond_set = - Report.check_proc summary proc_desc tenv symbol_table cfg inv_map + Report.check_proc summary proc_desc tenv integer_type_widths symbol_table cfg inv_map |> Report.report_errors summary |> Report.forget_locs locals |> Report.for_summary in let summary = diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index fa60f400c..5b748e7c1 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -286,10 +286,133 @@ module ArrayAccessCondition = struct fun locs c -> {c with relation= Relation.forget_locs locs c.relation} end +module BinaryOperationCondition = struct + type binop_t = Plus | Minus | Mult [@@deriving compare] + + let equal_binop = [%compare.equal: binop_t] + + let binop_to_string = function Plus -> "+" | Minus -> "-" | Mult -> "*" + + type t = + { binop: binop_t + ; typ: Typ.ikind + ; integer_widths: Typ.IntegerWidths.t + ; lhs: ItvPure.astate + ; rhs: ItvPure.astate } + + let get_symbols c = ItvPure.get_symbols c.lhs @ ItvPure.get_symbols c.rhs + + let subst eval_sym c = + match (ItvPure.subst c.lhs eval_sym, ItvPure.subst c.rhs eval_sym) with + | NonBottom lhs, NonBottom rhs -> + Some {c with lhs; rhs} + | _, _ -> + None + + + let have_similar_bounds {binop= binop1; typ= typ1; lhs= lhs1; rhs= rhs1} + {binop= binop2; typ= typ2; lhs= lhs2; rhs= rhs2} = + equal_binop binop1 binop2 && Typ.equal_ikind typ1 typ2 + && ItvPure.have_similar_bounds lhs1 lhs2 + && ItvPure.have_similar_bounds rhs1 rhs2 + + + let has_infty {lhs; rhs} = ItvPure.has_infty lhs || ItvPure.has_infty rhs + + let xcompare ~lhs:{binop= binop1; typ= typ1; lhs= lhs1; rhs= rhs1} + ~rhs:{binop= binop2; typ= typ2; lhs= lhs2; rhs= rhs2} = + if not (equal_binop binop1 binop2 && Typ.equal_ikind typ1 typ2) then `NotComparable + else + let lhscmp = ItvPure.xcompare ~lhs:lhs1 ~rhs:lhs2 in + let rhscmp = ItvPure.xcompare ~lhs:rhs1 ~rhs:rhs2 in + match (lhscmp, rhscmp) with + | `Equal, `Equal -> + `Equal + | `Equal, `LeftSubsumesRight + | `LeftSubsumesRight, `Equal + | `LeftSubsumesRight, `LeftSubsumesRight -> + `LeftSubsumesRight + | `Equal, `RightSubsumesLeft + | `RightSubsumesLeft, `Equal + | `RightSubsumesLeft, `RightSubsumesLeft -> + `RightSubsumesLeft + | `NotComparable, _ + | _, `NotComparable + | `LeftSmallerThanRight, _ + | _, `LeftSmallerThanRight + | `RightSmallerThanLeft, _ + | _, `RightSmallerThanLeft + | `LeftSubsumesRight, `RightSubsumesLeft + | `RightSubsumesLeft, `LeftSubsumesRight -> + `NotComparable + + + let pp fmt {binop; typ; lhs; rhs} = + F.fprintf fmt "(%a %s %a):%s" ItvPure.pp lhs (binop_to_string binop) ItvPure.pp rhs + (Typ.ikind_to_string typ) + + + let pp_description = pp + + let check {binop; typ; integer_widths; lhs; rhs} = + let v = + match binop with + | Plus -> + ItvPure.plus lhs rhs + | Minus -> + ItvPure.minus lhs rhs + | Mult -> + ItvPure.mult lhs rhs + in + let v_lb, v_ub = (ItvPure.lb v, ItvPure.ub v) in + let typ_lb, typ_ub = + let lb, ub = Typ.range_of_ikind integer_widths typ in + (Bound.of_big_int lb, Bound.of_big_int ub) + in + if + (* typ_lb <= v_lb and v_ub <= typ_ub, not an error *) + Bound.le v_ub typ_ub && Bound.le typ_lb v_lb + then {report_issue_type= None; propagate= false} + else if + (* v_ub < typ_lb or typ_ub < v_lb, definitely an error *) + Bound.lt v_ub typ_lb || Bound.lt typ_ub v_lb + then {report_issue_type= Some IssueType.integer_overflow_l1; propagate= false} + else if + (* -oo != v_lb < typ_lb or typ_ub < v_ub != +oo, probably an error *) + (Bound.lt v_lb typ_lb && Bound.is_not_infty v_lb) + || (Bound.lt typ_ub v_ub && Bound.is_not_infty v_ub) + then {report_issue_type= Some IssueType.integer_overflow_l2; propagate= false} + else + let is_symbolic = ItvPure.is_symbolic v in + let report_issue_type = + if Config.bo_debug <= 3 && is_symbolic then None else Some IssueType.integer_overflow_l5 + in + {report_issue_type; propagate= is_symbolic} + + + let make integer_widths bop ~lhs ~rhs = + if ItvPure.is_invalid lhs || ItvPure.is_invalid rhs then None + else + let binop, typ = + match bop with + | Binop.PlusA (Some typ) -> + (Plus, typ) + | Binop.MinusA (Some typ) -> + (Minus, typ) + | Binop.Mult (Some typ) -> + (Mult, typ) + | _ -> + L.(die InternalError) + "Unexpected type %s is given to BinaryOperationCondition." (Binop.str Pp.text bop) + in + Some {binop; typ; integer_widths; lhs; rhs} +end + module Condition = struct type t = | AllocSize of AllocSizeCondition.t | ArrayAccess of {is_collection_add: bool; c: ArrayAccessCondition.t} + | BinaryOperation of BinaryOperationCondition.t let make_alloc_size = Option.map ~f:(fun c -> AllocSize c) @@ -297,11 +420,15 @@ module Condition = struct Option.map ~f:(fun c -> ArrayAccess {is_collection_add; c}) + let make_binary_operation = Option.map ~f:(fun c -> BinaryOperation c) + let get_symbols = function | AllocSize c -> AllocSizeCondition.get_symbols c | ArrayAccess {c} -> ArrayAccessCondition.get_symbols c + | BinaryOperation c -> + BinaryOperationCondition.get_symbols c let subst eval_sym rel_map caller_relation = function @@ -310,6 +437,8 @@ module Condition = struct | ArrayAccess {is_collection_add; c} -> ArrayAccessCondition.subst eval_sym rel_map caller_relation c |> make_array_access ~is_collection_add + | BinaryOperation c -> + BinaryOperationCondition.subst eval_sym c |> make_binary_operation let have_similar_bounds c1 c2 = @@ -318,11 +447,20 @@ module Condition = struct AllocSizeCondition.have_similar_bounds c1 c2 | ArrayAccess {c= c1}, ArrayAccess {c= c2} -> ArrayAccessCondition.have_similar_bounds c1 c2 + | BinaryOperation c1, BinaryOperation c2 -> + BinaryOperationCondition.have_similar_bounds c1 c2 | _ -> false - let has_infty = function ArrayAccess {c} -> ArrayAccessCondition.has_infty c | _ -> false + let has_infty = function + | ArrayAccess {c} -> + ArrayAccessCondition.has_infty c + | BinaryOperation c -> + BinaryOperationCondition.has_infty c + | _ -> + false + let xcompare ~lhs ~rhs = match (lhs, rhs) with @@ -331,6 +469,8 @@ module Condition = struct | ArrayAccess {is_collection_add= b1; c= lhs}, ArrayAccess {is_collection_add= b2; c= rhs} when Bool.equal b1 b2 -> ArrayAccessCondition.xcompare ~lhs ~rhs + | BinaryOperation lhs, BinaryOperation rhs -> + BinaryOperationCondition.xcompare ~lhs ~rhs | _ -> `NotComparable @@ -340,6 +480,8 @@ module Condition = struct AllocSizeCondition.pp fmt c | ArrayAccess {c} -> ArrayAccessCondition.pp fmt c + | BinaryOperation c -> + BinaryOperationCondition.pp fmt c let pp_description fmt = function @@ -347,6 +489,8 @@ module Condition = struct AllocSizeCondition.pp_description fmt c | ArrayAccess {c} -> ArrayAccessCondition.pp_description fmt c + | BinaryOperation c -> + BinaryOperationCondition.pp_description fmt c let check = function @@ -354,13 +498,15 @@ module Condition = struct AllocSizeCondition.check c | ArrayAccess {is_collection_add; c} -> ArrayAccessCondition.check ~is_collection_add c + | BinaryOperation c -> + BinaryOperationCondition.check c let forget_locs locs x = match x with | ArrayAccess {is_collection_add; c} -> ArrayAccess {is_collection_add; c= ArrayAccessCondition.forget_locs locs c} - | AllocSize _ -> + | AllocSize _ | BinaryOperation _ -> x end @@ -422,9 +568,13 @@ module ConditionTrace = struct let has_unknown ct = ValTraceSet.has_unknown ct.val_traces - let check : _ t0 -> IssueType.t option = - fun ct -> if has_unknown ct then Some IssueType.buffer_overrun_u5 else None + let check issue_type_u5 : _ t0 -> IssueType.t option = + fun ct -> if has_unknown ct then Some issue_type_u5 else None + + let check_buffer_overrun ct = check IssueType.buffer_overrun_u5 ct + + let check_integer_overflow ct = check IssueType.integer_overflow_u5 ct let for_summary : _ t0 -> summary_t = fun ct -> {ct with cond_trace= ()} end @@ -481,13 +631,15 @@ module ConditionWithTrace = struct Some {cond; trace; reported= cwt.reported} - let set_buffer_overrun_u5 {cond; trace} issue_type = + let set_u5 {cond; trace} issue_type = if ( IssueType.equal issue_type IssueType.buffer_overrun_l3 || IssueType.equal issue_type IssueType.buffer_overrun_l4 || IssueType.equal issue_type IssueType.buffer_overrun_l5 ) && Condition.has_infty cond - then Option.value (ConditionTrace.check trace) ~default:issue_type + then Option.value (ConditionTrace.check_buffer_overrun trace) ~default:issue_type + else if IssueType.equal issue_type IssueType.integer_overflow_l5 && Condition.has_infty cond + then Option.value (ConditionTrace.check_integer_overflow trace) ~default:issue_type else issue_type @@ -497,7 +649,7 @@ module ConditionWithTrace = struct | None -> checked | Some issue_type -> - let issue_type = set_buffer_overrun_u5 cwt issue_type in + let issue_type = set_u5 cwt issue_type in (* Only report if the precision has improved. This is approximated by: only report if the issue_type has changed. *) let report_issue_type = @@ -602,6 +754,12 @@ module ConditionSet = struct |> add_opt location val_traces condset + let add_binary_operation integer_type_widths location bop ~lhs ~rhs val_traces condset = + BinaryOperationCondition.make integer_type_widths bop ~lhs ~rhs + |> Condition.make_binary_operation + |> add_opt location val_traces condset + + let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site = let subst_add_cwt condset cwt = match diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index c95bd0e45..1cc97f799 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -48,6 +48,16 @@ module ConditionSet : sig val add_alloc_size : Location.t -> length:ItvPure.astate -> ValTraceSet.t -> t -> t + val add_binary_operation : + Typ.IntegerWidths.t + -> Location.t + -> Binop.t + -> lhs:ItvPure.astate + -> rhs:ItvPure.astate + -> ValTraceSet.t + -> t + -> t + val join : t -> t -> t val subst : diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index d49e1c451..eab083e27 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -15,6 +15,7 @@ module BoTrace = struct | ArrAccess of Location.t | ArrDecl of Location.t | Assign of Location.t + | Binop of Location.t | Call of Location.t | Return of Location.t | SymAssign of Loc.t * Location.t @@ -49,6 +50,8 @@ module BoTrace = struct F.fprintf fmt "ArrDecl (%a)" Location.pp_file_pos location | Assign location -> F.fprintf fmt "Assign (%a)" Location.pp_file_pos location + | Binop location -> + F.fprintf fmt "Binop (%a)" Location.pp_file_pos location | Call location -> F.fprintf fmt "Call (%a)" Location.pp_file_pos location | Return location -> diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 1e2d82df3..454273eab 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -364,4 +364,22 @@ module Check = struct let arr = Sem.eval_arr array_exp mem in let relation = Dom.Mem.get_relation mem in array_access_byte ~arr ~idx ~relation ~is_plus:true location cond_set + + + let binary_operation integer_type_widths bop ~lhs ~rhs location cond_set = + let lhs_itv = Dom.Val.get_itv lhs in + let rhs_itv = Dom.Val.get_itv rhs in + match (lhs_itv, rhs_itv) with + | NonBottom lhs_itv, NonBottom rhs_itv -> + let traces = + TraceSet.join (Dom.Val.get_traces lhs) (Dom.Val.get_traces rhs) + |> TraceSet.add_elem (Trace.Binop location) + in + L.(debug BufferOverrun Verbose) + "@[Add condition :@,bop:%s@, lhs: %a@, rhs: %a@,@]@." (Binop.str Pp.text bop) + Itv.ItvPure.pp lhs_itv Itv.ItvPure.pp rhs_itv ; + PO.ConditionSet.add_binary_operation integer_type_widths location bop ~lhs:lhs_itv + ~rhs:rhs_itv traces cond_set + | _, _ -> + cond_set end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 425b71fe9..a883a5062 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -167,4 +167,13 @@ module Check : sig -> Location.t -> PO.ConditionSet.t -> PO.ConditionSet.t + + val binary_operation : + Typ.IntegerWidths.t + -> Binop.t + -> lhs:Dom.Val.t + -> rhs:Dom.Val.t + -> Location.t + -> PO.ConditionSet.t + -> PO.ConditionSet.t end diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index dee9f58f7..655dbf1fd 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -127,6 +127,12 @@ module ItvPure : sig val get_symbols : t -> Symbol.t list val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted + + val plus : t -> t -> t + + val minus : t -> t -> t + + val mult : t -> t -> t end include module type of AbstractDomain.BottomLifted (ItvPure) diff --git a/infer/tests/build_systems/differential_of_costs_report/introduced.exp b/infer/tests/build_systems/differential_of_costs_report/introduced.exp index ee65a9ec8..10185c24f 100644 --- a/infer/tests/build_systems/differential_of_costs_report/introduced.exp +++ b/infer/tests/build_systems/differential_of_costs_report/introduced.exp @@ -1,2 +1,3 @@ +INTEGER_OVERFLOW_L5, no_bucket, src/DiffExample.java, DiffExample.f1(int):void, 3 PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, int DiffExample.f4(int), 39 INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, void DiffExample.f1(int), 19 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 8ef3789dd..0b162e3f2 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -111,7 +111,7 @@ void plus_linear_min3_Good_FP() { a[plus_linear_min(15)] = 1; } -void integer_overflow_by_addition_Bad_FN() { +void integer_overflow_by_addition_Bad() { char arr[10]; int32_t x = 2000000000; int32_t y = 2000000000; @@ -121,7 +121,17 @@ void integer_overflow_by_addition_Bad_FN() { } } -void integer_overflow_by_subtraction_Bad_FN() { +void integer_overflow_by_addition_l2_Bad(int x) { + int32_t y; + if (x) { + y = 0; + } else { + y = 2000000000; + } + y = y + y; +} + +void integer_overflow_by_subtraction_Bad() { char arr[10]; int32_t x = -2000000000; int32_t y = 2000000000; @@ -131,7 +141,7 @@ void integer_overflow_by_subtraction_Bad_FN() { } } -void integer_overflow_by_multiplication_Bad_FN() { +void integer_overflow_by_multiplication_Bad() { char arr[10]; int32_t x = 300000; int32_t y = 300000; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 212c4cfde..d689e4cf7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,6 +1,10 @@ -codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad_FN, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad_FN, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad_FN, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):int] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Binop: ([0, 2000000000] + [0, 2000000000]):int] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (300000 * 300000):int] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-2000000000 - 2000000000):int] +codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5] codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5] codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10] @@ -9,6 +13,7 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2 codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [1, +oo] Size: 2 by call to `array_min_index_from_one_FP` ] +codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([1, +oo] - 1):int] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] @@ -16,6 +21,7 @@ codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_ codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 20 Size: 10] codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/calloc.c, calloc_bad1, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: -1 Size: 10] @@ -28,6 +34,7 @@ codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10 by call to `do_while_sub` ] +codetoanalyze/c/bufferoverrun/do_while.c, do_while_sub, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: 1 Size: 1 by call to `two_accesses` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: -1 Size: 1 by call to `two_symbolic_accesses` ] @@ -50,6 +57,9 @@ codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CON codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: 10] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([5, +oo] * 4):unsigned long] +codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([0, +oo] + 5):int] +codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_function,Binop: ([-oo, +oo] * 10):int] codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,ArrayDeclaration,Assignment,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: 10 Size: [5, +oo]] codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Alloc: Length: 2000000000] codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Alloc: Length: -2] @@ -59,11 +69,14 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERB codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]] codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]] codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Call,Parameter: n,Alloc: Length: [100000000, +oo] by call to `alloc_may_be_big2_Silenced` ] +codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: n,Binop: (100000000 + [0, +oo]):int by call to `alloc_may_be_big2_Silenced` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: n,Assignment,Binop: ([1, +oo] + 1):int by call to `s2_symbolic_widened_Bad` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, i.lb), i.ub] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [i.lb, min(-1, i.ub)] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_function,Binop: ([-oo, +oo] * 10):int] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 9] @@ -74,11 +87,14 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2, codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Offset: [0, 10] Size: [5, 15]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: n] codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: n] +codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, [] codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: 255] codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 256] Size: 256] @@ -99,7 +115,9 @@ codetoanalyze/c/bufferoverrun/models.c, strncpy_bad2, 3, BUFFER_OVERRUN_L1, no_b codetoanalyze/c/bufferoverrun/models.c, strncpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40] codetoanalyze/c/bufferoverrun/models.c, strncpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4] codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] +codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10] codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] Size: 1024] codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10] @@ -107,6 +125,8 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFE codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 Size: 5 by call to `FN_pointer_arith4_Bad` ] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: 5 by call to `prune_arrblk_eq` ] +codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax1_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Binop: (0 - 1):unsigned int by call to `prune_minmax1_Ok` ] +codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_minmax2_Ok, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 2):unsigned int by call to `prune_minmax2_Ok` ] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index 37cfa99c6..fb8832a32 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -138,3 +138,21 @@ void FP_call_prune_arrblk_eq_Ok() { int* x = (int*)malloc(sizeof(int) * 5); prune_arrblk_eq(x); } + +void prune_minmax1_Ok(unsigned int x, unsigned int y) { + if (x > 0) { + if (y >= x + 1) { + unsigned int z = y - 1; + } + } +} + +void FP_call_prune_minmax1_Ok() { prune_minmax1_Ok(0, 0); } + +void prune_minmax2_Ok(unsigned int x, unsigned int y) { + if (x > y) { + unsigned int z = x - y; + } +} + +void FP_call_prune_minmax2_Ok() { prune_minmax2_Ok(0, 2); } diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index d64974b3d..14edf7726 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -17,12 +17,14 @@ codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDI codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] +codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 603, degree = 0] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] codetoanalyze/c/performance/compound_loop_guard.c, simplified_simulated_while_with_and, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 604, degree = 0] codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_shortcut, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] @@ -32,6 +34,8 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 7 * p.ub, degree = 1] codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] +codetoanalyze/c/performance/cost_test.c, alias_OK, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: ([-oo, +oo] + 1):int] codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 606, degree = 0] codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1103, degree = 0] codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1103, degree = 0] @@ -47,6 +51,7 @@ codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTIO codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (-m.lb + 20), degree = 1] codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 * (-m.lb + 20), degree = 1] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] +codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([-oo, +oo] + 1):int] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0] @@ -54,20 +59,29 @@ codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 5, EXPENSIVE codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1207, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 606, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 606, degree = 0] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 608, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 611, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 611, degree = 0] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 613, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/cost_test_deps.c, real_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, real_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0] +codetoanalyze/c/performance/cost_test_deps.c, real_while, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):int] codetoanalyze/c/performance/cost_test_deps.c, real_while, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 217, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_cond_in_goto, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop_more_expensive, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0] +codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):int] codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 217, degree = 0] +codetoanalyze/c/performance/cost_test_deps.c, two_loops, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([3, +oo] + 1):int] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 548, degree = 0] @@ -83,20 +97,25 @@ codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 8 * n.ub, degree = 1] codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 8 * n.ub, degree = 1] codetoanalyze/c/performance/invariant.c, do_n_m_times_nested_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/c/performance/invariant.c, do_n_m_times_nested_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/invariant.c, while_infinite_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2003, degree = 0] codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2003, degree = 0] +codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2005, degree = 0] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0] +codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 226, degree = 0] codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 227, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0] +codetoanalyze/c/performance/loops.c, if_in_loop, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/loops.c, if_in_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0] codetoanalyze/c/performance/loops.c, if_in_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 321, degree = 0] @@ -106,6 +125,7 @@ codetoanalyze/c/performance/loops.c, if_out_loop, 8, EXPENSIVE_EXECUTION_TIME_CA codetoanalyze/c/performance/loops.c, if_out_loop, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 514, degree = 0] codetoanalyze/c/performance/loops.c, larger_state_FN, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0] codetoanalyze/c/performance/loops.c, larger_state_FN, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0] +codetoanalyze/c/performance/loops.c, larger_state_FN, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/loops.c, larger_state_FN, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0] codetoanalyze/c/performance/loops.c, larger_state_FN, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1004, degree = 0] codetoanalyze/c/performance/switch_continue.c, test_switch, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] @@ -114,7 +134,10 @@ codetoanalyze/c/performance/switch_continue.c, test_switch, 11, EXPENSIVE_EXECUT codetoanalyze/c/performance/switch_continue.c, test_switch, 17, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 604, degree = 0] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Binop: (n + [-oo, +oo]):int] +codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 15, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Assignment,Binop: ([-oo, +oo] - 1):int] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * m.ub, degree = 1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 7 * m.ub, degree = 1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * m.ub, degree = 1] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 218628f9f..c9c87b296 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,3 +1,5 @@ +INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_erase, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (this[*].infer_size - [-oo, +oo]):unsigned long] +INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_insert_>, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (this[*].infer_size + [-oo, +oo]):unsigned long] codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter: n,ArrayAccess: Offset: 15 Size: 10 by call to `my_class_access_nth` ] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: 10 Size: 5] @@ -16,7 +18,10 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFE codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Return,ArrayAccess: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 30 Size: 10] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned long] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [0, +oo]):unsigned long] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Binop: (4 * [1, +oo]):unsigned long] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 5] @@ -36,18 +41,33 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_O codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Return,Binop: ([-oo, +oo] + 1):unsigned long] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned long] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Binop: ([-oo, +oo] - 1):int] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Binop: (4 * [0, +oo]):unsigned long] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Call,Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Call,Call,Call,Parameter: bi,Binop: ([-oo, +oo] - 1):int by call to `ral_FP` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ] codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42] codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42] codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayAccess: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned long] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 6 Size: 5] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned long] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Binop: ([0, +oo] + 1):unsigned long] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 4 Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Binop: (4 * [0, +oo]):unsigned long] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Binop: ([0, +oo] + 1):unsigned long] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([1, +oo] + 1):unsigned long] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([2, +oo] + 1):unsigned long] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [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,Binop: ([3, +oo] + 42):unsigned long] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [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,Binop: (4 * [45, +oo]):unsigned long] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter: __n,Assignment,Call,Call,Binop: (4 * [0, +oo]):unsigned long] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter: __n,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: v[*].infer_size Size: v[*].infer_size] codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: -1 Size: 10 by call to `access_minus_one` ] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index c9e144f0f..311857cc1 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -11,6 +11,7 @@ codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):bool codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 4 Size: 3] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 5 Size: 4] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 202, degree = 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 0] @@ -19,6 +20,7 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_o codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 0 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] @@ -39,9 +41,12 @@ codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break. codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 7 * p.ub, degree = 1] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * p.ub, degree = 1] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_FN(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_FN(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, maxJ.ub + -1]):int] +codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_FN(int,int):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * list.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * list.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __cast,Assignment,Call,Assignment,Binop: ([0, +oo] + 1):int by call to `void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection)` ] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 * (mSubscribers.length.ub + -1) + 4 * mSubscribers.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 * (mSubscribers.length.ub + -1) + 4 * mSubscribers.length.ub, degree = 1] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] @@ -53,7 +58,9 @@ codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performanc codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop_FN():int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop_FN():int, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([2, +oo] + 1):int] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 * k.ub, degree = 1] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 13 * k.ub, degree = 1] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1202, degree = 0] @@ -69,26 +76,36 @@ codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Co codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 608, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 609, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([-oo, +oo] + 1):int] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1304, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 606, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 605, degree = 0] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 611, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 610, degree = 0] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep2(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.nested_loop():int, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 215, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 29]):int] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([3, +oo] + 1):int] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0] codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: j,Assignment,Assignment,Assignment,Assignment,Binop: ([-oo, 9] + 1):int] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub, degree = 1] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * test.a.ub, degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * (k.ub + -1), degree = 1] +codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 7 * (k.ub + -1), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * (k.ub + -1), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: size,Binop: (size + [-oo, +oo]):int] +codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 9 * items.length.ub, degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 * items.length.ub, degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] @@ -108,9 +125,11 @@ codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils. codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.(java.lang.String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 251, degree = 0] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 29 * (length.ub + -1), degree = 1] @@ -120,10 +139,13 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binop: (a[*] * b[*]):long] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):int] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([10, +oo] + 1):int] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 799, degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]