diff --git a/infer/src/bufferoverrun/ints.ml b/infer/src/bufferoverrun/ints.ml index 887618079..ae95bdbeb 100644 --- a/infer/src/bufferoverrun/ints.ml +++ b/infer/src/bufferoverrun/ints.ml @@ -91,5 +91,13 @@ module PositiveInt = struct let succ = Z.succ - let pp = Z.pp_print + let ten = Z.of_int 10 + + let exponent_chars = [|"⁰"; "¹"; "²"; "³"; "⁴"; "⁵"; "⁶"; "⁷"; "⁸"; "⁹"|] + + let rec pp_exponent f i = + if not Z.(i <= zero) then ( + let d, r = Z.ediv_rem i ten in + pp_exponent f d ; + F.pp_print_string f exponent_chars.(Z.to_int r) ) end diff --git a/infer/src/bufferoverrun/ints.mli b/infer/src/bufferoverrun/ints.mli index b54a11868..baea58cf7 100644 --- a/infer/src/bufferoverrun/ints.mli +++ b/infer/src/bufferoverrun/ints.mli @@ -81,5 +81,5 @@ module PositiveInt : sig val succ : t -> t - val pp : F.formatter -> t -> unit + val pp_exponent : F.formatter -> t -> unit end diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 1e3183cfb..b4120bd11 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -336,7 +336,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct if Z.((c :> Z.t) > one) then F.fprintf fmt "%a ⋅ " NonNegativeInt.pp c in let pp_exp fmt (e : PositiveInt.t) = - if Z.((e :> Z.t) > one) then F.fprintf fmt "^%a" PositiveInt.pp e + if Z.((e :> Z.t) > one) then PositiveInt.pp_exponent fmt e in let pp_magic_parentheses pp fmt x = let s = F.asprintf "%a" pp x in diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 6787e5d54..f8c0bcb58 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -117,8 +117,8 @@ codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16007, degree = 0] codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ (m.ub - 1) × m.ub + 8 ⋅ m.ub + 2 ⋅ m.ub × (max(1, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2] codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ (m.ub - 1) × m.ub + 8 ⋅ m.ub + 2 ⋅ m.ub × (max(1, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2] -codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m.ub + 6 ⋅ m.ub^2 + 2 ⋅ m.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2] -codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m.ub + 6 ⋅ m.ub^2 + 2 ⋅ m.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2] +codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m.ub + 6 ⋅ m.ub² + 2 ⋅ m.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2] +codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m.ub + 6 ⋅ m.ub² + 2 ⋅ m.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2] codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1] codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1] codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 6d23855c7..e8f8836f0 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -138,14 +138,14 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. 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] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 ⋅ (length.ub - 1), degree = 1] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 ⋅ (length.ub - 1), degree = 1] -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 3 + 71 ⋅ (length.ub - 1)^2 + 8 ⋅ length.ub, degree = 2] -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 + 71 ⋅ (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 + 71 ⋅ (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 + 71 ⋅ (length.ub - 1)^2 + 8 ⋅ length.ub, degree = 2] +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 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] +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 3 + 71 ⋅ (length.ub - 1)² + 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 + 71 ⋅ (length.ub - 1)² + 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 + 71 ⋅ (length.ub - 1)² + 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[*]):signed64] -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 + 71 ⋅ (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 + 71 ⋅ (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 + 71 ⋅ (length.ub - 1)^2 + 8 ⋅ length.ub, degree = 2] +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 + 71 ⋅ (length.ub - 1)² + 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 + 71 ⋅ (length.ub - 1)² + 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 + 71 ⋅ (length.ub - 1)² + 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):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []