From d55f5c02d58aa4806d4bf36616d96b6afcf130ce Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 23 Sep 2019 04:38:18 -0700 Subject: [PATCH] [cost] Add modeled range Summary: `ModeledRange` represents how many times the interval value can be updated by modeled functions. This domain is to support the case where there are mismatches between value of a control variable and actual number of loop iterations. For example, ``` while((c = file_channel.read(buf)) != -1) { ... } ``` the loop will iterates as the file size, but the control variable `c` does not have that value. In these cases, it assigns a symbolic value of the file size to the modeled range of `c`, then which is used when calculating the overall cost. Reviewed By: jvillard Differential Revision: D17476621 fbshipit-source-id: 9a81376e8 --- infer/src/absint/PatternMatch.ml | 2 + infer/src/absint/PatternMatch.mli | 3 ++ infer/src/bufferoverrun/bounds.ml | 12 +++++ infer/src/bufferoverrun/bounds.mli | 6 +++ .../src/bufferoverrun/bufferOverrunDomain.ml | 53 +++++++++++++++++-- .../src/bufferoverrun/bufferOverrunModels.ml | 40 +++++++++++++- .../codetoanalyze/java/performance/Loops.java | 17 ++++++ .../codetoanalyze/java/performance/issues.exp | 20 +++---- 8 files changed, 138 insertions(+), 15 deletions(-) diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index 5b13b6567..6a6aabd67 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -76,6 +76,8 @@ let implements_inject class_name = implements ("javax.inject." ^ class_name) let implements_io class_name = implements ("java.io." ^ class_name) +let implements_nio class_name = implements ("java.nio." ^ class_name) + let implements_map = implements "java.util.Map" let implements_set = implements "java.util.Set" diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli index c8165ad96..7aa274a09 100644 --- a/infer/src/absint/PatternMatch.mli +++ b/infer/src/absint/PatternMatch.mli @@ -61,6 +61,9 @@ val implements_inject : string -> Tenv.t -> string -> bool val implements_io : string -> Tenv.t -> string -> bool (** Check whether class implements a Java IO *) +val implements_nio : string -> Tenv.t -> string -> bool +(** Check whether class implements a Java nio *) + val implements_map : Tenv.t -> string -> bool (** Check whether class implements a Java's Map *) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index eae1e0ef8..68104a9c9 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -1132,6 +1132,8 @@ module BoundTrace = struct let compare t1 t2 = [%compare: int * t] (length t1, t1) (length t2, t2) + let join x y = if length x <= length y then x else y + let rec pp f = function | Loop loc -> F.fprintf f "Loop (%a)" Location.pp loc @@ -1162,6 +1164,16 @@ end module NonNegativeBound = struct type t = Bound.t * BoundTrace.t [@@deriving compare] + let ( <= ) ~lhs:(bound_lhs, _) ~rhs:(bound_rhs, _) = Bound.le bound_lhs bound_rhs + + let join (bound_x, trace_x) (bound_y, trace_y) = + (Bound.overapprox_max bound_x bound_y, BoundTrace.join trace_x trace_y) + + + let widen ~prev:(bound_prev, trace_prev) ~next:(bound_next, trace_next) ~num_iters:_ = + (Bound.widen_u bound_prev bound_next, BoundTrace.join trace_prev trace_next) + + let make_err_trace (b, t) = let b = F.asprintf "{%a}" Bound.pp b in (b, BoundTrace.make_err_trace ~depth:0 t) diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 73cca2a45..1b30fc464 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -132,6 +132,12 @@ type ('c, 's, 't) valclass = Constant of 'c | Symbolic of 's | ValTop of 't module NonNegativeBound : sig type t [@@deriving compare] + val ( <= ) : lhs:t -> rhs:t -> bool + + val join : t -> t -> t + + val widen : prev:t -> next:t -> num_iters:int -> t + val of_loop_bound : Location.t -> Bound.t -> t val of_modeled_function : string -> Location.t -> Bound.t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 60f0d5316..181a8ba03 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -30,10 +30,32 @@ module ItvThresholds = AbstractDomain.FiniteSet (struct let pp = pp_print end) +(* ModeledRange represents how many times the interval value can be updated by modeled functions. + This domain is to support the case where there are mismatches between value of a control variable + and actual number of loop iterations. For example, + + [while((c = file_channel.read(buf)) != -1) { ... }] + + the loop will iterates as the file size, but the control variable [c] does not have that value. + In these cases, it assigns a symbolic value of the file size to the modeled range of [c], then + which it is used when calculating the overall cost. *) +module ModeledRange = struct + include AbstractDomain.BottomLifted (struct + include Bounds.NonNegativeBound + + let pp = pp ~hum:true + end) + + let of_modeled_function pname location bound = + let pname = Typ.Procname.to_simplified_string pname in + NonBottom (Bounds.NonNegativeBound.of_modeled_function pname location bound) +end + module Val = struct type t = { itv: Itv.t ; itv_thresholds: ItvThresholds.t + ; modeled_range: ModeledRange.t ; sym: Relation.Sym.t ; powloc: PowLoc.t ; arrayblk: ArrayBlk.t @@ -44,6 +66,7 @@ module Val = struct let bot : t = { itv= Itv.bot ; itv_thresholds= ItvThresholds.empty + ; modeled_range= ModeledRange.bottom ; sym= Relation.Sym.bot ; powloc= PowLoc.bot ; arrayblk= ArrayBlk.bot @@ -60,12 +83,16 @@ module Val = struct let relation_sym_pp fmt sym = if Option.is_some Config.bo_relational_domain then F.fprintf fmt ", %a" Relation.Sym.pp sym in + let modeled_range_pp fmt range = + if not (ModeledRange.is_bottom range) then + F.fprintf fmt " (modeled_range:%a)" ModeledRange.pp range + in let trace_pp fmt traces = if Config.bo_debug >= 1 then F.fprintf fmt ", %a" TraceSet.pp traces in - F.fprintf fmt "(%a%a%a, %a, %a%a%a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds - relation_sym_pp x.sym PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym - relation_sym_pp x.size_sym trace_pp x.traces + F.fprintf fmt "(%a%a%a%a, %a, %a%a%a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds + relation_sym_pp x.sym modeled_range_pp x.modeled_range PowLoc.pp x.powloc ArrayBlk.pp + x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp x.size_sym trace_pp x.traces let unknown_from : callee_pname:_ -> location:_ -> t = @@ -73,6 +100,7 @@ module Val = struct let traces = Trace.(Set.singleton_final location (UnknownFrom callee_pname)) in { itv= Itv.top ; itv_thresholds= ItvThresholds.empty + ; modeled_range= ModeledRange.bottom ; sym= Relation.Sym.top ; powloc= PowLoc.unknown ; arrayblk= ArrayBlk.unknown @@ -86,6 +114,7 @@ module Val = struct else Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv && ItvThresholds.( <= ) ~lhs:lhs.itv_thresholds ~rhs:rhs.itv_thresholds + && ModeledRange.( <= ) ~lhs:lhs.modeled_range ~rhs:rhs.modeled_range && Relation.Sym.( <= ) ~lhs:lhs.sym ~rhs:rhs.sym && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk @@ -102,6 +131,8 @@ module Val = struct ~thresholds:(ItvThresholds.elements itv_thresholds) ~prev:prev.itv ~next:next.itv ~num_iters ; itv_thresholds + ; modeled_range= + ModeledRange.widen ~prev:prev.modeled_range ~next:next.modeled_range ~num_iters ; sym= Relation.Sym.widen ~prev:prev.sym ~next:next.sym ~num_iters ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters @@ -116,6 +147,7 @@ module Val = struct else { itv= Itv.join x.itv y.itv ; itv_thresholds= ItvThresholds.join x.itv_thresholds y.itv_thresholds + ; modeled_range= ModeledRange.join x.modeled_range y.modeled_range ; sym= Relation.Sym.join x.sym y.sym ; powloc= PowLoc.join x.powloc y.powloc ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk @@ -126,6 +158,8 @@ module Val = struct let get_itv : t -> Itv.t = fun x -> x.itv + let get_modeled_range : t -> ModeledRange.t = fun x -> x.modeled_range + let get_sym : t -> Relation.Sym.t = fun x -> x.sym let get_sym_var : t -> Relation.Var.t option = fun x -> Relation.Sym.get_var x.sym @@ -189,6 +223,8 @@ module Val = struct of_itv (Itv.set_lb_zero (Itv.of_int max_char)) + let set_modeled_range range x = {x with modeled_range= range} + let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top} let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv; sym= Relation.Sym.top} @@ -199,6 +235,7 @@ module Val = struct fun f ?f_trace x y -> let itv = f x.itv y.itv in let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in + let modeled_range = ModeledRange.join x.modeled_range y.modeled_range in let traces = match f_trace with | Some f_trace -> @@ -212,7 +249,7 @@ module Val = struct | true, true | false, false -> TraceSet.join x.traces y.traces ) in - {bot with itv; itv_thresholds; traces} + {bot with itv; itv_thresholds; modeled_range; traces} let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t = @@ -632,7 +669,13 @@ module MemPure = struct let itv = Val.get_itv v in if Itv.has_only_non_int_symbols itv then acc else - let range1 = Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial in + let range1 = + match Val.get_modeled_range v with + | NonBottom range -> + Polynomials.NonNegativePolynomial.of_non_negative_bound range + | Bottom -> + Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial + in if Polynomials.NonNegativePolynomial.is_top range1 then L.d_printfln_escaped "Range of %a (loc:%a) became top at %a." Itv.pp itv Loc.pp loc ProcCfg.Normal.Node.pp_id node_id ; diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 682021326..0af4680d6 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1119,6 +1119,36 @@ module InputStream = struct {exec; check= no_check} end +module FileChannel = struct + (* https://docs.oracle.com/javase/7/docs/api/java/io/InputStream.html#read(byte[],%20int,%20int) *) + let read buf_exp = + let exec {pname; location} ~ret:(ret_id, ret_typ) mem = + let buf_locs = Sem.eval_locs buf_exp mem in + let buf_v = Dom.Mem.find_set buf_locs mem in + let range = + Symb.SymbolPath.of_callsite ~ret_typ (CallSite.make pname location) + |> Bounds.Bound.of_modeled_path Symb.Symbol.make_onevalue + |> Dom.ModeledRange.of_modeled_function pname location + in + let mem = Dom.Mem.add_heap_set buf_locs (Dom.Val.set_modeled_range range buf_v) mem in + let v = + Dom.Val.of_itv (Itv.set_lb Itv.Bound.mone Itv.nat) |> Dom.Val.set_modeled_range range + in + model_by_value v ret_id mem + in + {exec; check= no_check} +end + +module ByteBuffer = struct + let get_int buf_exp = + let exec _ ~ret:(ret_id, _) mem = + let range = Dom.Mem.find_set (Sem.eval_locs buf_exp mem) mem |> Dom.Val.get_modeled_range in + let v = Dom.Val.of_itv Itv.nat |> Dom.Val.set_modeled_range range in + model_by_value v ret_id mem + in + {exec; check= no_check} +end + module Call = struct let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in @@ -1350,5 +1380,13 @@ module Call = struct &:: "intValue" <>$ capt_exp $--> JavaInteger.intValue ; +PatternMatch.implements_lang "Integer" &:: "valueOf" <>$ capt_exp $--> JavaInteger.valueOf ; +PatternMatch.implements_io "InputStream" - &:: "read" <>$ any_arg $+ any_arg $+ any_arg $+ capt_exp $--> InputStream.read ] + &:: "read" <>$ any_arg $+ any_arg $+ any_arg $+ capt_exp $--> InputStream.read + ; +PatternMatch.implements_nio "channels.FileChannel" + &:: "read" <>$ any_arg $+ capt_exp $+ any_arg $--> FileChannel.read + ; +PatternMatch.implements_nio "ByteBuffer" &:: "get" <>$ capt_exp $--> ByteBuffer.get_int + ; +PatternMatch.implements_nio "ByteBuffer" + &:: "getShort" <>$ capt_exp $--> ByteBuffer.get_int + ; +PatternMatch.implements_nio "ByteBuffer" &:: "getInt" <>$ capt_exp $--> ByteBuffer.get_int + ; +PatternMatch.implements_nio "ByteBuffer" + &:: "getLong" <>$ capt_exp $--> ByteBuffer.get_int ] end diff --git a/infer/tests/codetoanalyze/java/performance/Loops.java b/infer/tests/codetoanalyze/java/performance/Loops.java index ad1d7efbc..f97eb5355 100644 --- a/infer/tests/codetoanalyze/java/performance/Loops.java +++ b/infer/tests/codetoanalyze/java/performance/Loops.java @@ -6,6 +6,10 @@ */ package codetoanalyze.java.performance; +import java.io.IOException; +import java.nio.ByteBuffer; +import java.nio.channels.FileChannel; + public class Loops { static int do_while_independent_of_p(int p) { @@ -110,4 +114,17 @@ public class Loops { void charsequence_length_linear(CharSequence seq) { for (int i = 0; i < seq.length(); i++) {} } + + void modeled_range_linear(FileChannel fc, ByteBuffer bb) throws IOException { + int i; + int offset = 0; + do { + int numBytesRead = fc.read(bb, offset); + if (numBytesRead == -1) { + break; + } + i = bb.getInt(); + offset += 8; + } while (i != 0); + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 53767dc4b..cdd8f17a4 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -150,18 +150,20 @@ codetoanalyze/java/performance/ListTest.java, ListTest.asList_linear(java.lang.S codetoanalyze/java/performance/ListTest.java, ListTest.indexOfImpl_linear(java.util.List,java.lang.Object):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 16,{list.length},Loop at line 16] codetoanalyze/java/performance/ListTest.java, ListTest.sort_comparator_nlogn(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length × log(people.length), O(people.length × log(people.length)), degree = 1 + 1⋅log,{people.length},Modeled call to List.sort,{people.length},Modeled call to List.sort] codetoanalyze/java/performance/ListTest.java, ListTest.sublist(java.util.List):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 8 ⋅ (filesList.length - 1) + 3 ⋅ filesList.length, O(filesList.length), degree = 1,{filesList.length},Loop at line 30,{filesList.length - 1},Loop at line 30] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.charsequence_length_linear(java.lang.CharSequence):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ seq.length + 3 ⋅ (seq.length + 1), O(seq.length), degree = 1,{seq.length + 1},Loop at line 111,{seq.length},Loop at line 111] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.charsequence_length_linear(java.lang.CharSequence):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ seq.length + 3 ⋅ (seq.length + 1), O(seq.length), degree = 1,{seq.length + 1},Loop at line 115,{seq.length},Loop at line 115] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 250, O(1), degree = 0] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 25 ⋅ (length - 1), O(length), degree = 1,{length - 1},Loop at line 40] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length, O(length × length), degree = 2,{length},Loop at line 50,{length - 1},Loop at line 51,{length - 1},Loop at line 50] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 25 ⋅ (length - 1), O(length), degree = 1,{length - 1},Loop at line 44] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length, O(length × length), degree = 2,{length},Loop at line 54,{length - 1},Loop at line 55,{length - 1},Loop at line 54] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `a[*]`,,Parameter `b[*]`,Binary operation: (a[*] × b[*]):signed64] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 82] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 30] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 86] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 14 ⋅ FileChannel.read(...).modeled, O(FileChannel.read(...).modeled), degree = 1,{FileChannel.read(...).modeled},Modeled call to read(...)] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 8):signed32] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 34] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 16 + 26 ⋅ x.length, O(x.length), degree = 1,{x.length},Loop at line 73] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_concat_linear(java.lang.String,java.lang.String):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ (p.length + s.length) + 3 ⋅ (p.length + s.length + 1), O((p.length + s.length)), degree = 1,{p.length + s.length + 1},Loop at line 99,{p.length + s.length},Loop at line 99] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_length_linear(java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ s.length + 3 ⋅ (s.length + 1), O(s.length), degree = 1,{s.length + 1},Loop at line 94,{s.length},Loop at line 94] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.linear(int),Loop at line 82] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 16 + 26 ⋅ x.length, O(x.length), degree = 1,{x.length},Loop at line 77] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_concat_linear(java.lang.String,java.lang.String):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ (p.length + s.length) + 3 ⋅ (p.length + s.length + 1), O((p.length + s.length)), degree = 1,{p.length + s.length + 1},Loop at line 103,{p.length + s.length},Loop at line 103] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_length_linear(java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ s.length + 3 ⋅ (s.length + 1), O(s.length), degree = 1,{s.length + 1},Loop at line 98,{s.length},Loop at line 98] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.linear(int),Loop at line 86] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6996, O(1), degree = 0] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([-oo, +oo] × [-oo, +oo]):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32 by call to `void Loops.linear(int)` ]