pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo,cost] Add models for Java Strings

Browse Source 
Reviewed By: mbouaziz, skcho

Differential Revision: D14522624

fbshipit-source-id: 1ec2e0389
master
Ezgi Çiçek 6 years ago committed by Facebook Github Bot
parent f78dfbaeda
commit ce0ccc10ec
5 changed files with 37 additions and 4 deletions
Show Stats Download Patch File Download Diff File

6
infer/src/bufferoverrun/absLoc.ml
Unescape View File

@ -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

3
infer/src/bufferoverrun/bufferOverrunField.ml
Unescape View File

@ -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

13
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -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")

17
infer/tests/codetoanalyze/java/performance/Loops.java
Unescape View File

@ -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");
}
}
}

2
infer/tests/codetoanalyze/java/performance/issues.exp
Unescape View File

@ -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, [<LHS trace>,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, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] × [-oo, +oo]):signed32]

Write Preview
Loading…
Cancel
Save