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

[cost] Revise Java's cast model

Browse Source 
Summary:
It revises Java's cast model to keep type in the location when it has a field.

The type information is useful especially when generating ondemand values of Collection elements.

Depends on D16807299

Reviewed By: ezgicicek

Differential Revision: D16807378

fbshipit-source-id: 636e54429
master
Sungkeun Cho 5 years ago committed by Facebook Github Bot
parent e45526ea02
commit 28d617b345
8 changed files with 42 additions and 28 deletions
Show Stats Download Patch File Download Diff File

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

@ -132,7 +132,7 @@ module Loc = struct
type t =
| Var of Var.t
| Allocsite of Allocsite.t
| Field of {prefix: t; fn: Typ.Fieldname.t}
| Field of {prefix: t; fn: Typ.Fieldname.t; typ: Typ.t option}
| StarField of {prefix: t; last_field: Typ.Fieldname.t}
[@@deriving compare]
@ -140,10 +140,10 @@ module Loc = struct
let of_allocsite a = Allocsite a
let append_field l0 ~fn =
let append_field ?typ l0 ~fn =
let rec aux = function
| Var _ | Allocsite _ ->
Field {prefix= l0; fn}
Field {prefix= l0; fn; typ}
| StarField {last_field} as l when Typ.Fieldname.equal fn last_field ->
l
| StarField {prefix} ->
@ -173,7 +173,7 @@ module Loc = struct
type t = private
| Var of Var.t
| Allocsite of Allocsite.t
| Field of {prefix: t; fn: Typ.Fieldname.t}
| Field of {prefix: t; fn: Typ.Fieldname.t; typ: Typ.t option}
| StarField of {prefix: t; last_field: Typ.Fieldname.t}
[@@deriving compare]
@ -181,7 +181,7 @@ module Loc = struct
val of_allocsite : Allocsite.t -> t
val append_field : t -> fn:Typ.Fieldname.t -> t
val append_field : ?typ:Typ.t -> t -> fn:Typ.Fieldname.t -> t
val append_star_field : t -> fn:Typ.Fieldname.t -> t
end )
@ -320,8 +320,8 @@ module Loc = struct
Some (Symb.SymbolPath.of_pvar pvar)
| Allocsite allocsite ->
Allocsite.get_path allocsite
| Field {prefix= l; fn} ->
Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
| Field {prefix= l; fn; typ} ->
Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field ?typ p fn)
| StarField {prefix; last_field} ->
get_path prefix |> Option.map ~f:(fun p -> Symb.SymbolPath.star_field p last_field)
@ -363,6 +363,14 @@ module Loc = struct
let exists_str ~f l =
Option.exists (get_path l) ~f:(fun path -> Symb.SymbolPath.exists_str_partial ~f path)
let cast typ x =
match x with
| Field {prefix= l; fn} ->
append_field l ~fn ~typ
| StarField _ | Var _ | Allocsite _ ->
x
end
module PowLoc = struct
@ -405,6 +413,8 @@ module PowLoc = struct
let exists_str ~f x = exists (fun l -> Loc.exists_str ~f l) x
let of_c_strlen x = map Loc.of_c_strlen x
let cast typ x = map (Loc.cast typ) x
end
let always_strong_update = false

2
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -419,6 +419,8 @@ module Val = struct
let is_mone x = Itv.is_mone (get_itv x)
let cast typ v = {v with powloc= PowLoc.cast typ v.powloc}
let of_path tenv ~may_last_field integer_type_widths location typ path =
let traces_of_loc l =
let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in

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

@ -371,10 +371,11 @@ let indexOf exp =
{exec; check= no_check}
let cast exp =
let cast exp size_exp =
let exec {integer_type_widths} ~ret:(ret_id, _) mem =
let itv = Sem.eval integer_type_widths exp mem in
model_by_value itv ret_id mem
let v = Sem.eval integer_type_widths exp mem in
let v = match size_exp with Exp.Sizeof {typ} -> Dom.Val.cast typ v | _ -> v in
model_by_value v ret_id mem
in
{exec; check= no_check}
@ -1031,7 +1032,7 @@ module Call = struct
; -"CFArrayGetCount" <>$ capt_exp $!--> StdBasicString.length
; -"CFArrayGetValueAtIndex" <>$ capt_arg $+ capt_arg $!--> CFArray.at
; -"exit" <>--> bottom
; -"__cast" <>$ capt_exp $+...$--> cast
; -"__cast" <>$ capt_exp $+ capt_exp $+...$--> cast
; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255
; -"fgets" <>$ capt_exp $+ capt_exp $+...$--> fgets
; -"infer_print" <>$ capt_exp $!--> infer_print

2
infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml
Unescape View File

@ -51,6 +51,8 @@ let mk pdesc =
L.(die InternalError) "Deref of unmodeled type `%a`" Typ.Name.pp typename )
| _ ->
L.(die InternalError) "Untyped expression is given." ) )
| SPath.Field {typ= Some _ as some_typ} ->
some_typ
| SPath.Field {fn; prefix= x} -> (
match BufferOverrunField.get_type fn with
| None ->

10
infer/src/bufferoverrun/symb.ml
Unescape View File

@ -32,7 +32,7 @@ module SymbolPath = struct
type partial =
| Pvar of Pvar.t
| Deref of deref_kind * partial
| Field of {fn: Typ.Fieldname.t; prefix: partial}
| Field of {fn: Typ.Fieldname.t; prefix: partial; typ: Typ.t option}
| Callsite of {ret_typ: Typ.t; cs: CallSite.t}
| StarField of {last_field: Typ.Fieldname.t; prefix: partial}
[@@deriving compare]
@ -57,10 +57,10 @@ module SymbolPath = struct
aux p0
let field p0 fn =
let field ?typ p0 fn =
let rec aux = function
| Pvar _ | Callsite _ ->
Field {fn; prefix= p0}
Field {fn; prefix= p0; typ}
| Field {fn= fn'} when Typ.Fieldname.equal fn fn' ->
StarField {last_field= fn; prefix= p0}
| Field {prefix= p} | Deref (_, p) ->
@ -76,7 +76,7 @@ module SymbolPath = struct
type partial = private
| Pvar of Pvar.t
| Deref of deref_kind * partial
| Field of {fn: Typ.Fieldname.t; prefix: partial}
| Field of {fn: Typ.Fieldname.t; prefix: partial; typ: Typ.t option}
| Callsite of {ret_typ: Typ.t; cs: CallSite.t}
| StarField of {last_field: Typ.Fieldname.t; prefix: partial}
[@@deriving compare]
@ -87,7 +87,7 @@ module SymbolPath = struct
val deref : deref_kind:deref_kind -> partial -> partial
val field : partial -> Typ.Fieldname.t -> partial
val field : ?typ:Typ.t -> partial -> Typ.Fieldname.t -> partial
val star_field : partial -> Typ.Fieldname.t -> partial
end )

4
infer/src/bufferoverrun/symb.mli
Unescape View File

@ -25,7 +25,7 @@ module SymbolPath : sig
type partial = private
| Pvar of Pvar.t
| Deref of deref_kind * partial
| Field of {fn: Typ.Fieldname.t; prefix: partial}
| Field of {fn: Typ.Fieldname.t; prefix: partial; typ: Typ.t option}
| Callsite of {ret_typ: Typ.t; cs: CallSite.t}
| StarField of {last_field: Typ.Fieldname.t; prefix: partial}
(**
@ -60,7 +60,7 @@ module SymbolPath : sig
val deref : deref_kind:deref_kind -> partial -> partial
val field : partial -> Typ.Fieldname.t -> partial
val field : ?typ:Typ.t -> partial -> Typ.Fieldname.t -> partial
val star_field : partial -> Typ.Fieldname.t -> partial

5
infer/tests/codetoanalyze/java/performance/ArrayListTest.java
Unescape View File

@ -186,9 +186,8 @@ public class ArrayListTest {
}
}
// Control vars include element which is some intValue and list
// length. The result of intValue depends on the list element which
// is not modeled. Hence we get bottom for its value ans 0 cost.
// Control vars include element which is some intValue and list length. The result of intValue
// depends on the list element. O(list.length x (-list.elements + 11))
// Simplified version of real code https://fburl.com/a3gge1b7
public boolean iterate_over_arraylist_shortcut_FP(ArrayList<Integer> list) {
for (Integer element : list) {

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

@ -32,20 +32,20 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remov
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), O(list.length × log(list.length)), degree = 1 + 1⋅log,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 246,{l.length + list.length},Loop at line 246]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 253,{l.length + list.length},Loop at line 253]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 228,{list.length},Loop at line 228]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), O(list.length), degree = 1,{list.length + 5},Loop at line 239,{list.length + 4},Loop at line 239]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 245,{l.length + list.length},Loop at line 245]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 252,{l.length + list.length},Loop at line 252]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 227,{list.length},Loop at line 227]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), O(list.length), degree = 1,{list.length + 5},Loop at line 238,{list.length + 4},Loop at line 238]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.empty_list_constant(int):void, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 14]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, []
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 2 ⋅ list.length × (11-max(10, list.elements)) + 3 ⋅ (list.length + 1) × (11-max(10, list.elements)), O(list.length × (-list.elements + 11)), degree = 2,{11-max(10, list.elements)},Loop at line 193,{list.length + 1},Loop at line 193,{11-max(10, list.elements)},Loop at line 193,{list.length},Loop at line 193]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 11 ⋅ list1.length + 3 ⋅ (list1.length + 1), O(list1.length), degree = 1,{list1.length + 1},Loop at line 184,{list1.length},Loop at line 184]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 19]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 10 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 176,{list.length},Loop at line 176]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 170,{list.length},Loop at line 170]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.json_array_constructor_linear(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ arr.length + 3 ⋅ (arr.length + 1), O(arr.length), degree = 1,{arr.length + 1},Loop at line 273,{arr.length},Loop at line 273]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.json_array_constructor_linear(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ arr.length + 3 ⋅ (arr.length + 1), O(arr.length), degree = 1,{arr.length + 1},Loop at line 272,{arr.length},Loop at line 272]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.max_linear(java.util.ArrayList):Person, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length, O(people.length), degree = 1,{people.length},Modeled call to Collections.max]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ this.list.length + 3 ⋅ (this.list.length + 1), O(this.list.length), degree = 1,{this.list.length + 1},Loop at line 217,{this.list.length},Loop at line 217]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ this.list.length + 3 ⋅ (this.list.length + 1), O(this.list.length), degree = 1,{this.list.length + 1},Loop at line 216,{this.list.length},Loop at line 216]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), O(list.length × log(list.length)), degree = 1 + 1⋅log,{list.length},Modeled call to Collections.sort,{list.length},Modeled call to Collections.sort]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sort_comparator_nlogn(java.util.ArrayList):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 Collections.sort,{people.length},Modeled call to Collections.sort]
codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, O(p), degree = 1,{p},call to int Break.break_loop(int,int),Loop at line 12]

Write Preview
Loading…
Cancel
Save