[inferbo] Extend Simple alias domain

Summary:
This diff extends the `Simple` alias domain to address Java's
temporary variables better.  It now has an additional field to denote
an alias temporary variable.

Reviewed By: jvillard

Differential Revision: D17421907

fbshipit-source-id: 8b8b47461

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -713,7 +713,8 @@ module AliasTarget = struct
      pruning values of program variables.  For example, a C statement "if(x){...}" is translated to
      "%r=load(x); if(%r){...}" in Sil.  At the load statement, we record the alias between the
      values of %r and x, then we can prune not only the value of %r, but also that of x inside the
-     if branch.  The i field is to express "%r=load(x)+i".
+     if branch.  The java_tmp field is an additional slot for keeping one more alias of temporary
+     variable in Java.  The i field is to express "%r=load(x)+i".
 
    "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
@@ -726,7 +727,7 @@ module AliasTarget = struct
      field is to express "%r=x.size()+i", which is required to follow the semantics of `Array.add`
      inside loops precisely. *)
   type t =
-    | Simple of {l: Loc.t; i: IntLit.t}
+    | Simple of {l: Loc.t; i: IntLit.t; java_tmp: Loc.t option}
     | Empty of Loc.t
     | Size of {l: Loc.t; i: IntLit.t; java_tmp: Loc.t option}
     | Fgets of Loc.t
@@ -740,16 +741,18 @@ module AliasTarget = struct
       if IntLit.isnegative i then F.fprintf fmt "-%a" IntLit.pp (IntLit.neg i)
       else F.fprintf fmt "+%a" IntLit.pp i
     in
+    let java_tmp_pp fmt java_tmp = Option.iter java_tmp ~f:(F.fprintf fmt "=%a" Loc.pp) in
     fun fmt -> function
-      | Simple {l; i} ->
+      | Simple {l; i; java_tmp} ->
           Loc.pp fmt l ;
-          if not (IntLit.iszero i) then intlit_pp fmt i
+          if not (IntLit.iszero i) then intlit_pp fmt i ;
+          java_tmp_pp fmt java_tmp
       | Empty l ->
           F.fprintf fmt "empty(%a)" Loc.pp l
       | Size {l; i; java_tmp} ->
           F.fprintf fmt "size(%a)" Loc.pp l ;
           if not (IntLit.iszero i) then intlit_pp fmt i ;
-          Option.iter java_tmp ~f:(F.fprintf fmt "=%a" Loc.pp)
+          java_tmp_pp fmt java_tmp
       | Fgets l ->
           F.fprintf fmt "fgets(%a)" Loc.pp l
       | Top ->
@@ -759,9 +762,9 @@ module AliasTarget = struct
   let fgets l = Fgets l
 
   let get_locs = function
-    | Size {l; java_tmp= Some tmp} ->
+    | Simple {l; java_tmp= Some tmp} | Size {l; java_tmp= Some tmp} ->
         PowLoc.singleton l |> PowLoc.add tmp
-    | Simple {l} | Size {l; java_tmp= None} | Empty l | Fgets l ->
+    | Simple {l; java_tmp= None} | Size {l; java_tmp= None} | Empty l | Fgets l ->
         PowLoc.singleton l
     | Top ->
         PowLoc.empty
@@ -771,12 +774,13 @@ module AliasTarget = struct
 
   let loc_map x ~f =
     match x with
-    | Simple {l; i} ->
+    | Simple {l; i; java_tmp} ->
-        Option.map (f l) ~f:(fun l -> Simple {l; i})
+        let java_tmp = Option.bind java_tmp ~f in
+        Option.map (f l) ~f:(fun l -> Simple {l; i; java_tmp})
     | Empty l ->
         Option.map (f l) ~f:(fun l -> Empty l)
     | Size {l; i; java_tmp} ->
-        let java_tmp = Option.value_map java_tmp ~default:None ~f in
+        let java_tmp = Option.bind java_tmp ~f in
         Option.map (f l) ~f:(fun l -> Size {l; i; java_tmp})
     | Fgets l ->
         Option.map (f l) ~f:(fun l -> Fgets l)
@@ -873,8 +877,17 @@ module AliasMap = struct
 
   let store : Loc.t -> Ident.t -> t -> t =
    fun l id x ->
-    if Language.curr_language_is Java && Loc.is_frontend_tmp l then
+    if Language.curr_language_is Java then
+      if Loc.is_frontend_tmp l then
         Option.value_map (find_id id x) ~default:x ~f:(fun tgt -> add (Key.of_loc l) tgt x)
+      else
+        match find_id id x with
+        | Some (AliasTarget.Simple {i; l= java_tmp})
+          when IntLit.iszero i && Loc.is_frontend_tmp java_tmp ->
+            add (Key.of_id id) (AliasTarget.Simple {l; i; java_tmp= Some java_tmp}) x
+            |> add (Key.of_loc java_tmp) (AliasTarget.Simple {l; i; java_tmp= None})
+        | _ ->
+            x
     else x
 
 
@@ -947,10 +960,12 @@ module Alias = struct
         else a
     | Exp.BinOp (Binop.PlusA _, Exp.Var id, Exp.Const (Const.Cint i))
     | Exp.BinOp (Binop.PlusA _, Exp.Const (Const.Cint i), Exp.Var id) ->
-        lift_map (AliasMap.load id (AliasTarget.Simple {l= loc; i= IntLit.neg i})) a
+        lift_map
+          (AliasMap.load id (AliasTarget.Simple {l= loc; i= IntLit.neg i; java_tmp= None}))
+          a
         |> lift_map (AliasMap.store_n ~prev:prev.map loc id i)
     | Exp.BinOp (Binop.MinusA _, Exp.Var id, Exp.Const (Const.Cint i)) ->
-        lift_map (AliasMap.load id (AliasTarget.Simple {l= loc; i})) a
+        lift_map (AliasMap.load id (AliasTarget.Simple {l= loc; i; java_tmp= None})) a
         |> lift_map (AliasMap.store_n ~prev:prev.map loc id (IntLit.neg i))
     | _ ->
         a
@@ -1822,7 +1837,7 @@ module Mem = struct
 
 
   let load_simple_alias : Ident.t -> Loc.t -> t -> t =
-   fun id loc -> load_alias id (AliasTarget.Simple {l= loc; i= IntLit.zero})
+   fun id loc -> load_alias id (AliasTarget.Simple {l= loc; i= IntLit.zero; java_tmp= None})
 
 
   let load_empty_alias : Ident.t -> Loc.t -> t -> t =

infer/tests/codetoanalyze/java/bufferoverrun/Array.java

@@ -100,4 +100,26 @@ class Array {
     x.add(0);
     this.iterate_collection_Bad(x);
   }
+
+  boolean b;
+
+  int zero_to_five() {
+    return b ? 0 : 5;
+  }
+
+  void prune_assign_exp_Good() {
+    int idx;
+    int[] arr = new int[5];
+    if ((idx = zero_to_five()) != 5) {
+      arr[idx] = 0;
+    }
+  }
+
+  void prune_assign_exp_Bad() {
+    int idx;
+    int[] arr = new int[3];
+    if ((idx = zero_to_five()) != 5) {
+      arr[idx] = 0;
+    }
+  }
 }

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

@@ -6,6 +6,7 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Good():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.prune_assign_exp_Bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 4] Size: 3]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 6 Size: 5]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Array declaration,Assignment,<Length trace>,Parameter `b.elements[*]`,Assignment,Array declaration,Array access: Offset: b.length + 1 Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 2, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1]