From b0216035f4e91b40e480c0bd0c77ccce59c367c5 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 17 Apr 2017 09:07:43 -0700 Subject: [PATCH] [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 | 11 ++++++++++- infer/src/IR/Pvar.rei | 5 +++++ infer/src/checkers/IdAccessPathMapDomain.ml | 3 +-- infer/src/checkers/ThreadSafety.ml | 2 +- infer/src/checkers/accessPath.ml | 2 +- infer/src/quandary/TaintAnalysis.ml | 2 +- .../java/threadsafety/Containers.java | 16 ++++++++++++++++ 7 files changed, 35 insertions(+), 6 deletions(-) diff --git a/infer/src/IR/Pvar.re b/infer/src/IR/Pvar.re index 662f0525b..b11e9423f 100644 --- a/infer/src/IR/Pvar.re +++ b/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 => diff --git a/infer/src/IR/Pvar.rei b/infer/src/IR/Pvar.rei index bc630e4fd..7d0a2d292 100644 --- a/infer/src/IR/Pvar.rei +++ b/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; diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index 133513c65..b4563a6fe 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/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) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index e32fc463c..ace1e5435 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/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'; } diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 34144152f..b3db1771a 100644 --- a/infer/src/checkers/accessPath.ml +++ b/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 diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 768512830..964d82057 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/java/threadsafety/Containers.java b/infer/tests/codetoanalyze/java/threadsafety/Containers.java index 87ec63cdb..0b791a9e2 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Containers.java +++ b/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();