From b48534c6407e67e2870bf0d2b5258ead7e064309 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 26 Jun 2020 07:54:48 -0700 Subject: [PATCH] [cost] Support a specific form of linked list iteration Summary: This diff tries to support a specific form of linked list iteration in Java. ``` while (p != null) { p = p.getNext(); } ``` This example was a constant cost before because the cost checker could not detect that it is an iteration on a linked list. The heuristic this diff implemented is: (1) `p = p.getNext()`: It tries to find this specific form of assignment. Then, it increments `p.linked_list_index` by 1. Note that `linked_list_index` is a virtual field for keeping an index in the linked list. Its initial value is always 0. (2) At `p != null`, it tries to prune the value of `p.linked_list_index`: the upper-bound of `p.linked_list_index` is pruned by `<= p.linked_list_length`. Here again, `p.linked_list_length` is also a virtual field to denote the length of the linked list. Reviewed By: ezgicicek Differential Revision: D22234892 fbshipit-source-id: 2fee176bb --- infer/src/bufferoverrun/absLoc.ml | 21 +++++++++ infer/src/bufferoverrun/absLoc.mli | 5 ++ .../bufferoverrun/bufferOverrunAnalysis.ml | 9 ++++ .../src/bufferoverrun/bufferOverrunDomain.ml | 47 ++++++++++++------- .../src/bufferoverrun/bufferOverrunDomain.mli | 3 ++ infer/src/bufferoverrun/bufferOverrunField.ml | 4 ++ .../src/bufferoverrun/bufferOverrunField.mli | 6 +++ .../bufferoverrun/bufferOverrunSemantics.ml | 24 ++++++++-- infer/src/bufferoverrun/itv.mli | 3 ++ .../codetoanalyze/java/performance/Loops.java | 6 +++ .../java/performance/cost-issues.exp | 1 + .../codetoanalyze/java/performance/issues.exp | 1 + 12 files changed, 108 insertions(+), 22 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 015798c42..c2e40b481 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -379,6 +379,19 @@ module Loc = struct append_field l fn ~typ | BoField.(StarField _ | Prim (Var _ | Allocsite _)) -> x + + + let get_linked_list_next ~lhs ~rhs = + match (get_path lhs, get_path rhs) with + | ( Some lhs_path + , Some + (Prim + (Deref (Deref_JavaPointer, Field {prefix= Prim (Deref (Deref_JavaPointer, rhs_path))}))) + ) + when Symb.SymbolPath.equal_partial lhs_path rhs_path -> + Some lhs + | _, _ -> + None end module LocSet = PrettyPrintable.MakePPSet (Loc) @@ -582,6 +595,14 @@ module PowLoc = struct LocSet.singleton Loc.unknown | Known ploc -> ploc + + + let get_linked_list_next ~lhs ~rhs = + match (is_singleton_or_more lhs, is_singleton_or_more rhs) with + | Singleton lhs, Singleton rhs -> + Loc.get_linked_list_next ~lhs ~rhs + | _, _ -> + None end let always_strong_update = false diff --git a/infer/src/bufferoverrun/absLoc.mli b/infer/src/bufferoverrun/absLoc.mli index bfdf76c99..9a0fd120c 100644 --- a/infer/src/bufferoverrun/absLoc.mli +++ b/infer/src/bufferoverrun/absLoc.mli @@ -153,6 +153,11 @@ module PowLoc : sig [Boolean.EqualOrder.ne], etc. *) val to_set : t -> LocSet.t + + val get_linked_list_next : lhs:t -> rhs:t -> Loc.t option + (** It checks whether [rhs] is of [lhs.any_field], which is a heuristic for detecting a linked + list, e.g. [x = x.next()]. It returns [Some lhs] if the condition is satisfied, [None] + otherwise. *) end val can_strong_update : PowLoc.t -> bool diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index af7d02d7c..a1ca26e60 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -243,6 +243,14 @@ module TransferFunctions = struct mem ) + let java_store_linked_list_next locs v mem = + PowLoc.get_linked_list_next ~lhs:locs ~rhs:(Dom.Val.get_all_locs v) + |> Option.value_map ~default:mem ~f:(fun loc -> + let linked_list_index = Loc.append_field loc BufferOverrunField.java_linked_list_index in + let v = Dom.Mem.find linked_list_index mem |> Dom.Val.plus_a Dom.Val.Itv.one in + Dom.Mem.add_heap linked_list_index v mem ) + + let modeled_load_of_empty_collection_opt = let known_empty_collections = String.Set.of_list ["EMPTY_LIST"; "EMPTY_SET"; "EMPTY_MAP"] in fun exp model_env ret mem -> @@ -355,6 +363,7 @@ module TransferFunctions = struct Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location locs in let mem = Dom.Mem.update_mem locs v mem in + let mem = java_store_linked_list_next locs v mem in let mem = if Language.curr_language_is Clang && Typ.is_char typ then BoUtils.Exec.set_c_strlen ~tgt:(Sem.eval integer_type_widths exp1 mem) ~src:v mem diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index e1a657425..b7b6b14dd 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -634,23 +634,28 @@ module Val = struct | Some s -> of_itv (Itv.of_int (String.length s)) | None -> ( - match Loc.get_path l with - | None -> - L.d_printfln_escaped "Val.on_demand for %a -> no path" Loc.pp l ; - default - | Some path -> ( - match typ_of_param_path path with - | None -> ( - match typ with - | Some typ when Loc.is_global l -> - L.d_printfln_escaped "Val.on_demand for %a -> global" Loc.pp l ; - do_on_demand path typ - | _ -> - L.d_printfln_escaped "Val.on_demand for %a -> no type" Loc.pp l ; - default ) - | Some typ -> - L.d_printfln_escaped "Val.on_demand for %a" Loc.pp l ; - do_on_demand path typ ) ) ) + match l with + | Field {fn} when Fieldname.equal fn BufferOverrunField.java_linked_list_index -> + L.d_printfln_escaped "Val.on_demand for %a as zero" Loc.pp l ; + of_itv Itv.zero + | _ -> ( + match Loc.get_path l with + | None -> + L.d_printfln_escaped "Val.on_demand for %a -> no path" Loc.pp l ; + default + | Some path -> ( + match typ_of_param_path path with + | None -> ( + match typ with + | Some typ when Loc.is_global l -> + L.d_printfln_escaped "Val.on_demand for %a -> global" Loc.pp l ; + do_on_demand path typ + | _ -> + L.d_printfln_escaped "Val.on_demand for %a -> no type" Loc.pp l ; + default ) + | Some typ -> + L.d_printfln_escaped "Val.on_demand for %a" Loc.pp l ; + do_on_demand path typ ) ) ) ) module Itv = struct @@ -667,6 +672,8 @@ module Val = struct let unknown_bool = of_itv Itv.unknown_bool let zero = of_itv Itv.zero + + let one = of_itv Itv.one end end @@ -705,6 +712,11 @@ module MemPure = struct let bot = empty + let get_linked_list_index loc mem = + let linked_list_index = Loc.append_field loc BufferOverrunField.java_linked_list_index in + Option.map (find_opt linked_list_index mem) ~f:(fun (_, v) -> (linked_list_index, v)) + + let range : filter_loc:(Loc.t -> LoopHeadLoc.t option) -> node_id:ProcCfg.Normal.Node.id @@ -715,6 +727,7 @@ module MemPure = struct (fun loc (_, v) acc -> match filter_loc loc with | Some loop_head_loc -> ( + let loc, v = Option.value (get_linked_list_index loc mem) ~default:(loc, v) in let itv_updated_by = Val.get_itv_updated_by v in match itv_updated_by with | Addition | Multiplication -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index 7ec271387..d75534855 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -274,6 +274,9 @@ module Val : sig val zero : t (** [\[0,0\]] *) + val one : t + (** [\[1,1\]] *) + val zero_255 : t (** [\[0,255\]] *) diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml index 807820dc8..168e49e50 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.ml +++ b/infer/src/bufferoverrun/bufferOverrunField.ml @@ -31,6 +31,10 @@ let mk, get_type = let java_collection_internal_array = mk "java.collection.elements" Typ.(mk_array void) +let java_linked_list_index = mk "java.linked_list_index" Typ.(int) + +let java_linked_list_length = mk "java.linked_list_length" Typ.(int) + let is_java_collection_internal_array fn = Fieldname.equal fn java_collection_internal_array let c_strlen () = diff --git a/infer/src/bufferoverrun/bufferOverrunField.mli b/infer/src/bufferoverrun/bufferOverrunField.mli index 3bdd0c8b5..891fc7795 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.mli +++ b/infer/src/bufferoverrun/bufferOverrunField.mli @@ -29,6 +29,12 @@ val cpp_vector_elem : vec_typ:Typ.t -> elt_typ:Typ.t -> Fieldname.t val java_collection_internal_array : Fieldname.t (** Field for Java collection's elements *) +val java_linked_list_index : Fieldname.t +(** Virtual field for index of Java's linked list *) + +val java_linked_list_length : Fieldname.t +(** Virtual field for length of Java's linked list *) + val is_cpp_vector_elem : Fieldname.t -> bool (** Check if the field is for C++ vector's elements *) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index bc48a315b..0ab34c048 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -564,6 +564,19 @@ module Prune = struct AliasTargets.fold accum_pruned (Mem.find_alias_loc iterator mem) astate + let prune_linked_list_index loc mem acc = + let lv_linked_list_index = Loc.append_field loc BufferOverrunField.java_linked_list_index in + Option.value_map (Mem.find_opt lv_linked_list_index mem) ~default:acc ~f:(fun index_v -> + let linked_list_length = Loc.append_field loc BufferOverrunField.java_linked_list_length in + Option.value_map (Loc.get_path linked_list_length) ~default:acc + ~f:(fun linked_list_length -> + let pruned_v = + Val.of_itv (Itv.of_normal_path ~unsigned:true linked_list_length) + |> Val.prune_binop Le index_v + in + update_mem_in_prune lv_linked_list_index pruned_v acc ) ) + + let prune_unop : Exp.t -> t -> t = fun e ({mem} as astate) -> match e with @@ -571,11 +584,12 @@ module Prune = struct let accum_prune_var rhs tgt acc = match tgt with | AliasTarget.Simple {i} when IntLit.iszero i -> - let v = Mem.find rhs mem in - if Val.is_bot v then acc - else - let v' = Val.prune_ne_zero v in - update_mem_in_prune rhs v' acc + (let v = Mem.find rhs mem in + if Val.is_bot v then acc + else + let v' = Val.prune_ne_zero v in + update_mem_in_prune rhs v' acc ) + |> prune_linked_list_index rhs mem | AliasTarget.Empty -> let v = Mem.find rhs mem in if Val.is_bot v then acc diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 213aac9ae..0b4d241ce 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -148,6 +148,9 @@ val top : t val zero : t (** 0 *) +val one : t +(** 1 *) + val zero_one : t (** [0, 1] *) diff --git a/infer/tests/codetoanalyze/java/performance/Loops.java b/infer/tests/codetoanalyze/java/performance/Loops.java index 801d20a2a..3e1d4bdf8 100644 --- a/infer/tests/codetoanalyze/java/performance/Loops.java +++ b/infer/tests/codetoanalyze/java/performance/Loops.java @@ -136,6 +136,12 @@ public class Loops { } } + void length_of_linked_list_simple_linear(MyLinkedList p) { + while (p != null) { + p = p.getNext(); + } + } + void length_of_linked_list_linear_FP(MyLinkedList p) { int n = 0; while (p != null) { diff --git a/infer/tests/codetoanalyze/java/performance/cost-issues.exp b/infer/tests/codetoanalyze/java/performance/cost-issues.exp index c3df7ab0b..9d5766af1 100644 --- a/infer/tests/codetoanalyze/java/performance/cost-issues.exp +++ b/infer/tests/codetoanalyze/java/performance/cost-issues.exp @@ -269,6 +269,7 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort_quadratic(long[],long[],int):void, 5 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length, OnUIThread:false, [{length},Loop at line 54,{length - 1},Loop at line 55,{length - 1},Loop at line 54] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb_linear(long[],int):void, 5 + 25 ⋅ (length - 1), OnUIThread:false, [{length - 1},Loop at line 44] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, ⊤, OnUIThread:false, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 86] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_simple_linear(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3 + 10 ⋅ (p.linked_list_length + 1), OnUIThread:false, [{p.linked_list_length + 1},Loop at line 140] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.loop_linear(int):void, 5 + 5 ⋅ x, OnUIThread:false, [{x},Loop at line 86] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 6 + 14 ⋅ FileChannel.read(...).modeled, OnUIThread:false, [{FileChannel.read(...).modeled},Modeled call to read(...)] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, ⊤, OnUIThread:false, [Unbounded loop,Loop at line 34] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index fce36b7fb..e13c33ab6 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -64,6 +64,7 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Call to void JsonUtils.escape(StringBuilder,String),Unbounded loop,Loop at line 13] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 86] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32 by call to `void Loops.loop_linear(int)` ] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 8):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 34] 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]