[inferbo] Extend size alias domain for Java temporary variables

Summary: This diff extends size alias domain for keeping one more alias of a Java temporary variable.

Reviewed By: ezgicicek

Differential Revision: D16984082

fbshipit-source-id: 244bbd0ee

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -693,7 +693,7 @@ module AliasTarget = struct
     | Simple of Loc.t
     | SimplePlusA of Loc.t * IntLit.t
     | Empty of Loc.t
-    | Size of Loc.t
+    | Size of {l: Loc.t; java_tmp: Loc.t option}
     | Fgets of Loc.t
     | Top
   [@@deriving compare]
@@ -708,8 +708,9 @@ module AliasTarget = struct
         else F.fprintf fmt "%a+%a" Loc.pp l IntLit.pp i
     | Empty l ->
         F.fprintf fmt "empty(%a)" Loc.pp l
-    | Size l ->
+    | Size {l; java_tmp} ->
-        F.fprintf fmt "size(%a)" Loc.pp l
+        F.fprintf fmt "size(%a)" Loc.pp l ;
+        Option.iter java_tmp ~f:(F.fprintf fmt "=%a" Loc.pp)
     | Fgets l ->
         F.fprintf fmt "fgets(%a)" Loc.pp l
     | Top ->
@@ -718,14 +719,16 @@ module AliasTarget = struct
 
   let fgets l = Fgets l
 
-  let get_loc = function
+  let get_locs = function
-    | Simple l | SimplePlusA (l, _) | Empty l | Size l | Fgets l ->
+    | Size {l; java_tmp= Some tmp} ->
-        Some l
+        PowLoc.singleton l |> PowLoc.add tmp
+    | Simple l | SimplePlusA (l, _) | Size {l; java_tmp= None} | Empty l | Fgets l ->
+        PowLoc.singleton l
     | Top ->
-        None
+        PowLoc.empty
 
 
-  let use_loc l x = Option.value_map (get_loc x) ~default:false ~f:(Loc.equal l)
+  let use_loc l x = PowLoc.mem l (get_locs x)
 
   let loc_map x ~f =
     match x with
@@ -735,8 +738,9 @@ module AliasTarget = struct
         Option.map (f l) ~f:(fun l -> SimplePlusA (l, i))
     | Empty l ->
         Option.map (f l) ~f:(fun l -> Empty l)
-    | Size l ->
+    | Size {l; java_tmp} ->
-        Option.map (f l) ~f:(fun l -> Size l)
+        let java_tmp = Option.value_map java_tmp ~default:None ~f in
+        Option.map (f l) ~f:(fun l -> Size {l; java_tmp})
     | Fgets l ->
         Option.map (f l) ~f:(fun l -> Fgets l)
     | Top ->
@@ -749,7 +753,7 @@ module AliasTarget = struct
 
   let widen ~prev ~next ~num_iters:_ = join prev next
 
-  let is_unknown x = Option.value_map (get_loc x) ~default:false ~f:Loc.is_unknown
+  let is_unknown x = PowLoc.exists Loc.is_unknown (get_locs x)
 end
 
 (* Relations between values of logical variables(registers) and program variables
@@ -763,7 +767,11 @@ end
    "AliasTarget.Empty relation": For pruning vector.length with vector::empty() results, we adopt a
    specific relation between %r and v->elements, where %r=v.empty().  So, if %r!=0, v's array length
    ([v->elements->length]) is pruned by 0.  On the other hand, if %r==0, v's array length is pruned
-   by >=1. *)
+   by >=1.
+
+   "AliasTarget.Size relation": This is for pruning vector's length.  When there is a function call,
+   %r=x.size(), the alias target for %r becomes AliasTarget.size {l=x.elements}.  The java_tmp field
+   is an additional slot for keeping one more alias of temporary variable in Java.  *)
 module AliasMap = struct
   module Key = struct
     type t = IdentKey of Ident.t | JavaTmp of Loc.t [@@deriving compare]
@@ -809,7 +817,12 @@ module AliasMap = struct
   let find_id : Ident.t -> t -> AliasTarget.t option = fun id x -> find_opt (Key.of_id id) x
 
   let find_java_tmp : Loc.t -> t -> AliasTarget.t option =
-   fun id x -> find_opt (Key.of_java_tmp id) x
+   fun loc x ->
+    match find_opt (Key.of_java_tmp loc) x with
+    | Some (AliasTarget.Size {l}) ->
+        Some (AliasTarget.Size {l; java_tmp= Some loc})
+    | _ as alias ->
+        alias
 
 
   let load : Ident.t -> AliasTarget.t -> t -> t =
@@ -1408,8 +1421,13 @@ module MemReach = struct
         None
 
 
-  let find_size_alias : Ident.t -> _ t0 -> Loc.t option =
+  let find_size_alias : Ident.t -> _ t0 -> (Loc.t * Loc.t option) option =
-   fun k m -> match Alias.find_id k m.alias with Some (AliasTarget.Size l) -> Some l | _ -> None
+   fun k m ->
+    match Alias.find_id k m.alias with
+    | Some (AliasTarget.Size {l; java_tmp}) ->
+        Some (l, java_tmp)
+    | _ ->
+        None
 
 
   let find_ret_alias : _ t0 -> AliasTarget.t option = fun m -> Alias.find_ret m.alias
@@ -1714,7 +1732,7 @@ module Mem = struct
    fun k -> f_lift_default ~default:None (MemReach.find_simple_alias k)
 
 
-  let find_size_alias : Ident.t -> _ t0 -> Loc.t option =
+  let find_size_alias : Ident.t -> _ t0 -> (Loc.t * Loc.t option) option =
    fun k -> f_lift_default ~default:None (MemReach.find_size_alias k)
 
 
@@ -1735,7 +1753,7 @@ module Mem = struct
 
 
   let load_size_alias : Ident.t -> Loc.t -> t -> t =
-   fun id loc -> load_alias id (AliasTarget.Size loc)
+   fun id loc -> load_alias id (AliasTarget.Size {l= loc; java_tmp= None})
 
 
   let store_simple_alias : Loc.t -> Exp.t -> t -> t =

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -31,8 +31,7 @@ let rec must_alias : Exp.t -> Exp.t -> Mem.t -> bool =
     match (Mem.find_alias x1 m, Mem.find_alias x2 m) with
     | Some x1', Some x2' ->
         AliasTarget.equal x1' x2'
-        && Option.value_map (AliasTarget.get_loc x1') ~default:false ~f:(fun l ->
+        && PowLoc.for_all (fun l -> not (Mem.is_rep_multi_loc l m)) (AliasTarget.get_locs x1')
-               not (Mem.is_rep_multi_loc l m) )
     | _, _ ->
         false )
   | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) ->
@@ -562,14 +561,16 @@ module Prune = struct
 
   let prune_size_alias =
     let prune_alias_core ~val_prune ~make_pruning_exp integer_type_widths x e ({mem} as astate) =
-      Option.value_map (Mem.find_size_alias x mem) ~default:astate ~f:(fun lv ->
+      Option.value_map (Mem.find_size_alias x mem) ~default:astate ~f:(fun (lv, java_tmp) ->
           let array_v = Mem.find lv mem in
           let size = Val.get_array_blk array_v |> ArrayBlk.sizeof |> Val.of_itv in
           let rhs = eval integer_type_widths e mem in
           let size' = val_prune size rhs in
           let array_v' = Val.set_array_length Location.dummy ~length:size' array_v in
           let pruning_exp = make_pruning_exp ~lhs:size' ~rhs in
-          update_mem_in_prune lv array_v' ~pruning_exp astate )
+          let astate = update_mem_in_prune lv array_v' ~pruning_exp astate in
+          Option.value_map java_tmp ~default:astate ~f:(fun java_tmp ->
+              update_mem_in_prune java_tmp size' ~pruning_exp astate ) )
     in
     gen_prune_alias_functions ~prune_alias_core
 

infer/tests/codetoanalyze/java/performance/ArrayListTest.java

@@ -274,6 +274,12 @@ public class ArrayListTest {
 
     }
   }
+
+  void linear(int i, ArrayList<Integer> a) {
+    while (a.size() >= i) {
+      a.remove(0);
+    }
+  }
 }
 
 class LexicographicComparator implements java.util.Comparator<Person> {

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -44,6 +44,7 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_lo
 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 272,{arr.length},Loop at line 272]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.linear(int,java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 9 ⋅ (-i + a.length + 1), O((-i + a.length)), degree = 1,{-i + a.length + 1},Loop at line 279]
 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 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]