From 28d617b345bd3edcb212f6424bfc65a0bde08001 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 22 Aug 2019 01:11:42 -0700 Subject: [PATCH] [cost] Revise Java's cast model 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 --- infer/src/bufferoverrun/absLoc.ml | 24 +++++++++++++------ .../src/bufferoverrun/bufferOverrunDomain.ml | 2 ++ .../src/bufferoverrun/bufferOverrunModels.ml | 9 +++---- .../bufferoverrun/bufferOverrunOndemandEnv.ml | 2 ++ infer/src/bufferoverrun/symb.ml | 10 ++++---- infer/src/bufferoverrun/symb.mli | 4 ++-- .../java/performance/ArrayListTest.java | 5 ++-- .../codetoanalyze/java/performance/issues.exp | 14 +++++------ 8 files changed, 42 insertions(+), 28 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index c0818a288..f6c8fbcf1 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -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 diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index e31ca4a3b..b9685efb4 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -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 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 3a2eb3ad1..236a58b83 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -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 diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml index 50edfa198..14ecebf7f 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -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 -> diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 852277a07..e686b5491 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -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 ) diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 5ab80f21a..9586602d0 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -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 diff --git a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index dc5f0653d..e40fac181 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -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 list) { for (Integer element : list) { diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index ec85b79eb..fa5d8af6f 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -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, [,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, [,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]