[frontend] don't treat Sawja-generated ternary operator vars as SSA tmps

Summary: Sawja assigns them on multiple control-flow paths, so they're not SSA.

Reviewed By: peterogithub

Differential Revision: D4896745

fbshipit-source-id: c805216

infer/src/IR/Pvar.re

@@ -260,7 +260,9 @@ let tmp_prefix = "0$?%__sil_tmp";
 let is_frontend_tmp pvar => {
   /* Check whether the program variable is a temporary one generated by Sawja, javac, or some other
      bytecode/name generation pass. valid java identifiers cannot contain `$` */
-  let is_bytecode_tmp name => String.contains name '$' || String.is_prefix prefix::"CatchVar" name;
+  let is_bytecode_tmp name =>
+    String.contains name '$' && not (String.contains name '_') ||
+    String.is_prefix prefix::"CatchVar" name;
   /* Check whether the program variable is generated by [mk_tmp] */
   let is_sil_tmp name => String.is_prefix prefix::tmp_prefix name;
   let name = to_string pvar;
@@ -272,6 +274,13 @@ let is_frontend_tmp pvar => {
   )
 };
 
+/* in Sawja, variables like $T0_18 are temporaries, but not SSA vars. */
+let is_ssa_frontend_tmp pvar =>
+  is_frontend_tmp pvar && {
+    let name = to_string pvar;
+    not (String.contains name '_' && String.contains name '$')
+  };
+
 
 /** Turn an ordinary program variable into a callee program variable */
 let to_callee pname pvar =>

infer/src/IR/Pvar.rei

@@ -92,6 +92,11 @@ let is_this: t => bool;
 let is_frontend_tmp: t => bool;
 
 
+/** return true if [pvar] is a temporary variable generated by the frontend and is only assigned
+    once on a non-looping control-flow path */
+let is_ssa_frontend_tmp: t => bool;
+
+
 /** [mk name proc_name suffix] creates a program var with the given function name and suffix */
 let mk: Mangled.t => Typ.Procname.t => t;
 

infer/src/checkers/IdAccessPathMapDomain.ml

@@ -19,9 +19,8 @@ let pp fmt astate =
   IdMap.pp ~pp_value:AccessPath.Raw.pp fmt astate
 
 let check_invariant ap1 ap2 = function
-  | Var.ProgramVar pvar when Pvar.is_frontend_tmp pvar ->
+  | Var.ProgramVar pvar when Pvar.is_ssa_frontend_tmp pvar ->
       (* Sawja reuses temporary variables which sometimes breaks this invariant *)
-      (* TODO: fix (13370224) *)
       ()
   | id ->
       if not (AccessPath.Raw.equal ap1 ap2)

infer/src/checkers/ThreadSafety.ml

@@ -596,7 +596,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         end
 
     | Sil.Store (Exp.Lvar lhs_pvar, lhs_typ, rhs_exp, _)
-      when Pvar.is_frontend_tmp lhs_pvar && not (is_constant rhs_exp) ->
+      when Pvar.is_ssa_frontend_tmp lhs_pvar && not (is_constant rhs_exp) ->
         let id_map' = analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ astate in
         { astate with id_map = id_map'; }
 

infer/src/checkers/accessPath.ml

@@ -99,7 +99,7 @@ let of_exp exp0 typ0 ~(f_resolve_id : Var.t -> Raw.t option) =
           | Some (base, base_accesses) -> (base, base_accesses @ accesses) :: acc
           | None -> (base_of_id id typ, accesses) :: acc
         end
-    | Exp.Lvar pvar when Pvar.is_frontend_tmp pvar ->
+    | Exp.Lvar pvar when Pvar.is_ssa_frontend_tmp pvar ->
         begin
           match f_resolve_id (Var.of_pvar pvar) with
           | Some (base, base_accesses) -> (base, base_accesses @ accesses) :: acc

infer/src/quandary/TaintAnalysis.ml

@@ -320,7 +320,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       match instr with
       | Sil.Load (lhs_id, rhs_exp, rhs_typ, _) ->
           analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate
-      | Sil.Store (Exp.Lvar lhs_pvar, lhs_typ, rhs_exp, _) when Pvar.is_frontend_tmp lhs_pvar ->
+      | Sil.Store (Exp.Lvar lhs_pvar, lhs_typ, rhs_exp, _) when Pvar.is_ssa_frontend_tmp lhs_pvar ->
           analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ astate
       | Sil.Store (Exp.Lvar lhs_pvar, _, Exp.Exn _, _) when Pvar.is_return lhs_pvar ->
           (* the Java frontend translates `throw Exception` as `return Exception`, which is a bit

infer/tests/codetoanalyze/java/threadsafety/Containers.java

@@ -169,6 +169,22 @@ class Containers {
     obj.f = new Object();
   }
 
+  static boolean sUsePooling;
+
+  private Obj poolWrapper() {
+    Obj obj = sUsePooling ? sPool.acquire() : null;
+    if (obj == null) {
+      obj = new Obj();
+    }
+
+    return obj;
+  }
+
+  void poolWrapperOk() {
+    Obj obj = poolWrapper();
+    obj.f = new Object();
+  }
+
   // need to understand semantics of release to get this one
   void FN_poolReleaseThenWriteBad() {
     Obj obj = sPool.acquire();