From ce0ccc10ec26fb1d614f52731641bd22ed7f25f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 26 Mar 2019 03:54:40 -0700 Subject: [PATCH] [inferbo,cost] Add models for Java Strings Reviewed By: mbouaziz, skcho Differential Revision: D14522624 fbshipit-source-id: 1ec2e0389 --- infer/src/bufferoverrun/absLoc.ml | 6 +++--- infer/src/bufferoverrun/bufferOverrunField.ml | 3 ++- infer/src/bufferoverrun/bufferOverrunModels.ml | 13 +++++++++++++ .../codetoanalyze/java/performance/Loops.java | 17 +++++++++++++++++ .../codetoanalyze/java/performance/issues.exp | 2 ++ 5 files changed, 37 insertions(+), 4 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 684fde390..96dc44e96 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -175,7 +175,7 @@ module Loc = struct let is_c_strlen = function | Field (_, fn) -> - Typ.Fieldname.equal fn BufferOverrunField.c_strlen + Typ.Fieldname.equal fn (BufferOverrunField.c_strlen ()) | _ -> false @@ -193,7 +193,7 @@ module Loc = struct let of_allocsite a = Allocsite a - let of_c_strlen loc = Field (loc, BufferOverrunField.c_strlen) + let of_c_strlen loc = Field (loc, BufferOverrunField.c_strlen ()) let of_pvar pvar = Var (Var.of_pvar pvar) @@ -223,7 +223,7 @@ module Loc = struct let is_literal_string = function Allocsite a -> Allocsite.is_literal_string a | _ -> None let is_literal_string_strlen = function - | Field (l, fn) when Typ.Fieldname.equal BufferOverrunField.c_strlen fn -> + | Field (l, fn) when Typ.Fieldname.equal (BufferOverrunField.c_strlen ()) fn -> is_literal_string l | _ -> None diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml index ab2523e8c..576a560ad 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.ml +++ b/infer/src/bufferoverrun/bufferOverrunField.ml @@ -42,4 +42,5 @@ let mk, get_type = let java_collection_internal_array = mk "java.collection.$elements." Typ.(mk_array void) -let c_strlen = mk "c.strlen" Typ.uint +let c_strlen () = + if Language.curr_language_is Java then mk "length" Typ.uint else mk "c.strlen" Typ.uint diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index ac93d6135..4d27e0eff 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -741,11 +741,14 @@ module Call = struct ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc ; -"__get_array_length" <>$ capt_exp $!--> get_array_length ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length + ; +PatternMatch.implements_lang "String" &:: "length" <>$ capt_exp $!--> strlen ; -"strlen" <>$ capt_exp $!--> strlen ; -"memcpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy ; -"memmove" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy ; -"memset" <>$ capt_exp $+ any_arg $+ capt_exp $!--> memset ; -"strcat" <>$ capt_exp $+ capt_exp $+...$--> strcat + ; +PatternMatch.implements_lang "String" + &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> strcat ; -"strcpy" <>$ capt_exp $+ capt_exp $+...$--> strcpy ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy ; -"snprintf" <>--> snprintf @@ -779,6 +782,16 @@ module Call = struct ; -"std" &:: "basic_string" &:: "length" $ capt_exp $--> StdBasicString.length ; -"std" &:: "basic_string" &:: "size" $ capt_exp $--> StdBasicString.length ; -"std" &:: "basic_string" &:: "compare" &--> by_value Dom.Val.Itv.top + ; +PatternMatch.implements_lang "String" + &:: "equals" + $ any_arg_of_typ (+PatternMatch.implements_lang "String") + $+ any_arg_of_typ (+PatternMatch.implements_lang "String") + $--> by_value Dom.Val.Itv.unknown_bool + ; +PatternMatch.implements_lang "String" + &:: "startsWith" + $ any_arg_of_typ (+PatternMatch.implements_lang "String") + $+ any_arg_of_typ (+PatternMatch.implements_lang "String") + $--> by_value Dom.Val.Itv.unknown_bool ; -"std" &:: "operator==" $ any_arg_of_typ (-"std" &:: "basic_string") $+ any_arg_of_typ (-"std" &:: "basic_string") diff --git a/infer/tests/codetoanalyze/java/performance/Loops.java b/infer/tests/codetoanalyze/java/performance/Loops.java index 64e09fae7..99b629c7e 100644 --- a/infer/tests/codetoanalyze/java/performance/Loops.java +++ b/infer/tests/codetoanalyze/java/performance/Loops.java @@ -89,4 +89,21 @@ public class Loops { } linear(infinite); } + + void string_length_linear(String s) { + for (int i = 0; i < s.length(); i++) {} + } + + void string_concat_linear(String s, String p) { + p = p.concat(s); + for (int i = 0; i < p.length(); i++) {} + } + + void zeropad_linear_FN(String s, String p) { + // control variable for the loop is the result of equals which is + // in [0,1]. It should be p instead. + while (s.equals(p)) { + p = p.concat("0"); + } + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index dda486c41..e52435a60 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -123,6 +123,8 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 30] 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_CALL, no_bucket, ERROR, [with estimated cost 16 + 26 ⋅ 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_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ (p.length + s.length) + 3 ⋅ (p.length + s.length + 1), 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_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ s.length + 3 ⋅ (s.length + 1), 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_CALL, 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.unboundedSymbol():void, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 6996, 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]