[thread-safety] add OwnedIf attribute to all formals at the beginning

Reviewed By: jberdine

Differential Revision: D5580114

fbshipit-source-id: 137e9ca

infer/src/absint/FormalMap.ml

@@ -38,3 +38,5 @@ let get_formal_index base t =
 let get_formal_base index t =
   List.find ~f:(fun (_, i) -> Int.equal i index) (AccessPath.BaseMap.bindings t)
   |> Option.map ~f:fst
+
+let get_formals_indexes = AccessPath.BaseMap.bindings

infer/src/absint/FormalMap.mli

@@ -29,3 +29,5 @@ val get_formal_index : AccessPath.base -> t -> int option
 val get_formal_base : int -> t -> AccessPath.base option
 (** return the base var for the given index if it exists, or None if it does not. Note: this is
     linear in the size of the formal map *)
+
+val get_formals_indexes : t -> (AccessPath.base * int) list

infer/src/checkers/ThreadSafety.ml

@@ -36,7 +36,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = ThreadSafetyDomain
 
-  type extras = FormalMap.t
+  type extras = ProcData.no_extras
 
   type lock_model = Lock | Unlock | LockedIfTrue | NoEffect
 
@@ -179,8 +179,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | _
      -> None
 
-  let add_conditional_ownership_attribute access_path formal_map attribute_map attributes =
+  let add_conditional_ownership_attribute access_path attribute_map attributes =
-    match FormalMap.get_formal_index (fst access_path) formal_map with
+    match
+      Domain.AttributeMapDomain.get_conditional_ownership_index (fst access_path, []) attribute_map
+    with
     | Some formal_index when not (is_owned access_path attribute_map)
      -> Domain.AttributeSetDomain.add (Domain.Attribute.OwnedIf (Some formal_index)) attributes
     | _
@@ -193,7 +195,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   (* propagate attributes from the leaves to the root of an RHS Hil expression.
      Special casing on ownership. *)
-  let rec attributes_of_expr formal_map attribute_map e =
+  let rec attributes_of_expr attribute_map e =
     let open HilExp in
     let open Domain in
     match e with
@@ -202,14 +204,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | AccessPath ap
      -> ( try AttributeMapDomain.find ap attribute_map
           with Not_found -> AttributeSetDomain.empty )
-        |> add_conditional_ownership_attribute ap formal_map attribute_map
+        |> add_conditional_ownership_attribute ap attribute_map
     | Exception expr (* treat exceptions as transparent wrt attributes *) | Cast (_, expr)
-     -> attributes_of_expr formal_map attribute_map expr
+     -> attributes_of_expr attribute_map expr
     | UnaryOperator (_, expr, _)
-     -> attributes_of_expr formal_map attribute_map expr |> remove_ownership_attributes
+     -> attributes_of_expr attribute_map expr |> remove_ownership_attributes
     | BinaryOperator (_, expr1, expr2)
-     -> let attributes1 = attributes_of_expr formal_map attribute_map expr1 in
+     -> let attributes1 = attributes_of_expr attribute_map expr1 in
-        let attributes2 = attributes_of_expr formal_map attribute_map expr2 in
+        let attributes2 = attributes_of_expr attribute_map expr2 in
         AttributeSetDomain.join attributes1 attributes2 |> remove_ownership_attributes
     | Closure _ | Sizeof _
      -> AttributeSetDomain.empty
@@ -222,8 +224,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let prefixes = aux [] but_last_rev in
     List.for_all ~f:(fun ap -> is_owned (base, ap) attribute_map) prefixes
 
-  let propagate_attributes lhs_access_path rhs_exp attribute_map formal_map =
+  let propagate_attributes lhs_access_path rhs_exp attribute_map =
-    let rhs_attributes = attributes_of_expr formal_map attribute_map rhs_exp in
+    let rhs_attributes = attributes_of_expr attribute_map rhs_exp in
     let lhs_root = fst lhs_access_path in
     let filter_on_globals =
       (* do not assign ownership to access paths rooted at globals *)
@@ -236,7 +238,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       match snd lhs_access_path with
       | []
        -> Fn.id
-      | [_] when FormalMap.is_formal lhs_root formal_map
+      | [_]
+        when Option.is_some
+               (Domain.AttributeMapDomain.get_conditional_ownership_index (lhs_root, [])
+                  attribute_map)
        -> Fn.id
       | _ when all_prefixes_owned lhs_access_path attribute_map
        -> Fn.id
@@ -246,7 +251,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let final_attributes = filter_on_globals rhs_attributes |> filter_on_lhs in
     Domain.AttributeMapDomain.add lhs_access_path final_attributes attribute_map
 
-  let propagate_return_attributes ret_opt ret_attributes actuals attribute_map formal_map =
+  let propagate_return_attributes ret_opt ret_attributes actuals attribute_map =
     let open Domain in
     match ret_opt with
     | None
@@ -266,9 +271,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             | Some HilExp.AccessPath actual_ap
              -> if is_owned actual_ap attribute_map then
                   AttributeSetDomain.add Attribute.unconditionally_owned other_attributes
-                else
+                else add_conditional_ownership_attribute actual_ap attribute_map other_attributes
-                  add_conditional_ownership_attribute actual_ap formal_map attribute_map
-                    other_attributes
             | Some HilExp.Constant _
              -> AttributeSetDomain.add Attribute.unconditionally_owned other_attributes
             | _
@@ -305,7 +308,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     Annotations.pname_has_return_annot pn ~attrs_of_pname:Specs.proc_resolve_attributes predicate
 
   let add_unannotated_call_access pname (call_flags: CallFlags.t) loc tenv ~locks ~threads
-      attribute_map (proc_data: FormalMap.t ProcData.t) =
+      attribute_map (proc_data: ProcData.no_extras ProcData.t) =
     if call_flags.cf_interface && Typ.Procname.is_java pname
        && not (is_java_library pname || is_builder_function pname)
        (* can't ask anyone to annotate interfaces in library code, and Builder's should always be
@@ -324,7 +327,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     else attribute_map
 
   let add_access exp loc ~is_write_access accesses locks threads attribute_map
-      (proc_data: FormalMap.t ProcData.t) =
+      (proc_data: ProcData.no_extras ProcData.t) =
     let open Domain in
     (* we don't want to warn on accesses to the field if it is (a) thread-confined, or
        (b) volatile *)
@@ -358,11 +361,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           add_field_accesses pre access_path access_acc' access_list'
     in
     let add_access_ acc (base, accesses) =
+      let base_access_path = (base, []) in
       if List.is_empty accesses then acc
       else
         let pre =
           if is_unprotected locks threads proc_data.pdesc then
-            match FormalMap.get_formal_index base proc_data.extras with
+            match
+              AttributeMapDomain.get_conditional_ownership_index base_access_path attribute_map
+            with
             | Some formal_index
              -> AccessPrecondition.Unprotected (Some formal_index)
             | None
@@ -371,7 +377,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             AccessPrecondition.Protected
               (make_excluder (locks || Procdesc.is_java_synchronized proc_data.pdesc) threads)
         in
-        add_field_accesses pre (base, []) acc accesses
+        add_field_accesses pre base_access_path acc accesses
     in
     List.fold ~f:add_access_ ~init:accesses (HilExp.get_access_paths exp)
 
@@ -539,8 +545,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         add_access exp loc ~is_write_access:false acc locks threads attribute_map proc_data)
       exps ~init:accesses
 
-  let add_escapees_from_exp rhs_exp extras escapees =
+  let add_escapees_from_exp rhs_exp attribute_map escapees =
-    HilExp.get_access_paths rhs_exp |> List.rev_map ~f:(Domain.Escapee.of_access_path extras)
+    HilExp.get_access_paths rhs_exp
+    |> List.rev_map ~f:(Domain.Escapee.of_access_path attribute_map)
     |> Domain.EscapeeDomain.add_from_list escapees
 
   let add_escapees_from_exp_list exp_list extras escapees =
@@ -552,7 +559,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     in
     add_escapees_from_exp_list escapee_actuals extras escapees
 
-  let exec_instr (astate: Domain.astate) ({ProcData.extras; tenv; pdesc} as proc_data) _
+  let exec_instr (astate: Domain.astate) ({ProcData.tenv; pdesc} as proc_data) _
       (instr: HilInstr.t) =
     let open Domain in
     match instr with
@@ -566,7 +573,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             astate.attribute_map
         in
         (* TODO: we need to model escaping formals, now just assume all escape *)
-        let escapees = add_escapees_from_exp_list actuals extras astate.escapees in
+        let escapees = add_escapees_from_exp_list actuals astate.attribute_map astate.escapees in
         {astate with accesses; attribute_map; escapees}
     | Call (ret_opt, Direct callee_pname, actuals, call_flags, loc)
      -> (
@@ -653,7 +660,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                           let pre =
                             if unprotected then
                               let base = fst actual_access_path in
-                              match FormalMap.get_formal_index base extras with
+                              match
+                                AttributeMapDomain.get_conditional_ownership_index (base, [])
+                                  astate.attribute_map
+                              with
                               | Some formal_index
                                -> (* the actual passed to the current callee is rooted in a
                                          formal *)
@@ -700,15 +710,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                   in
                   let attribute_map =
                     propagate_return_attributes ret_opt return_attributes actuals
-                      astate.attribute_map extras
+                      astate.attribute_map
                   in
                   let escapees =
-                    add_escapees_from_call actuals escapee_formals extras astate.escapees
+                    add_escapees_from_call actuals escapee_formals astate.attribute_map
+                      astate.escapees
                   in
                   {thumbs_up; locks; threads; accesses; attribute_map; escapees}
               | None
                -> (* TODO: assume actuals escape, should we? *)
-                  let new_escapees = add_escapees_from_exp_list actuals extras astate.escapees in
+                  let new_escapees =
+                    add_escapees_from_exp_list actuals astate.attribute_map astate.escapees
+                  in
                   let astate = {astate with escapees= new_escapees} in
                   let should_assume_returns_ownership (call_flags: CallFlags.t) actuals =
                     (* assume non-interface methods with no summary and no parameters return
@@ -786,13 +799,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             add_access (AccessPath lhs_access_path) loc ~is_write_access:true rhs_accesses
               astate.locks astate.threads astate.attribute_map proc_data
         in
-        let attribute_map =
+        let attribute_map = propagate_attributes lhs_access_path rhs_exp astate.attribute_map in
-          propagate_attributes lhs_access_path rhs_exp astate.attribute_map extras
-        in
         (* assigning to the return variable leads to no new escapees *)
         let escapees =
           if fst lhs_access_path |> fst |> Var.is_return then astate.escapees
-          else add_escapees_from_exp rhs_exp extras astate.escapees
+          else add_escapees_from_exp rhs_exp astate.attribute_map astate.escapees
         in
         {astate with accesses; attribute_map; escapees}
     | Assume (assume_exp, _, _, loc)
@@ -968,13 +979,13 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
   (* convert the abstract state to a summary by dropping the id map *)
   if should_analyze_proc proc_desc tenv then (
     if not (Procdesc.did_preanalysis proc_desc) then Preanal.do_liveness proc_desc tenv ;
-    let extras = FormalMap.make proc_desc in
+    let formal_map = FormalMap.make proc_desc in
-    let proc_data = ProcData.make proc_desc tenv extras in
+    let proc_data = ProcData.make_default proc_desc tenv in
     let initial =
       let threads = runs_on_ui_thread proc_desc || is_thread_confined_method tenv proc_desc in
       if is_initializer tenv (Procdesc.get_proc_name proc_desc) then
         let add_owned_formal acc formal_index =
-          match FormalMap.get_formal_base formal_index extras with
+          match FormalMap.get_formal_base formal_index formal_map with
           | Some base
            -> AttributeMapDomain.add_attribute (base, []) Attribute.unconditionally_owned acc
           | None
@@ -993,7 +1004,17 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
           List.fold ~f:add_owned_formal owned_formals ~init:ThreadSafetyDomain.empty.attribute_map
         in
         ({ThreadSafetyDomain.empty with attribute_map; threads}, IdAccessPathMapDomain.empty)
-      else ({ThreadSafetyDomain.empty with threads}, IdAccessPathMapDomain.empty)
+      else
+        (* add Owned(formal_index) predicates for each formal to indicate that each one is owned if
+           it is owned in the caller *)
+        let add_owned_formal acc (formal, formal_index) =
+          AttributeMapDomain.add_attribute (formal, []) (Attribute.OwnedIf (Some formal_index)) acc
+        in
+        let attribute_map =
+          List.fold ~f:add_owned_formal (FormalMap.get_formals_indexes formal_map)
+            ~init:ThreadSafetyDomain.empty.attribute_map
+        in
+        ({ThreadSafetyDomain.empty with attribute_map; threads}, IdAccessPathMapDomain.empty)
     in
     match Analyzer.compute_post proc_data ~initial ~debug:false with
     | Some ({thumbs_up; threads; locks; accesses; attribute_map; escapees}, _)

infer/src/checkers/ThreadSafetyDomain.ml

@@ -233,8 +233,8 @@ module Escapee = struct
     | Local loc
      -> F.fprintf fmt "Local(%a)" Var.pp loc
 
-  let of_access_path extras (base, _) =
+  let of_access_path attribute_map (base, _) =
-    match FormalMap.get_formal_index base extras with
+    match AttributeMapDomain.get_conditional_ownership_index (base, []) attribute_map with
     | Some fml
      -> Formal fml
     | None

infer/src/checkers/ThreadSafetyDomain.mli

@@ -140,7 +140,7 @@ module Escapee : sig
 
   val pp : F.formatter -> t -> unit
 
-  val of_access_path : FormalMap.t -> AccessPath.t -> t
+  val of_access_path : AttributeMapDomain.astate -> AccessPath.t -> t
 end
 
 (** set of formals or locals that may escape *)

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

@@ -240,11 +240,13 @@ class Containers {
     if (list == null) {
       list = new ArrayList<>();
     }
+    // we get list |->  ({ OwnedIf (0) } |_| { Owned }) here, which simplifies to list |-> {} due
+    // to limitations in AttributeMapDomain (join is just simple intersection)
     list.add(new Object());
     return list;
   }
 
-  public void addToNullListOk() {
+  public void FP_addToNullListOk() {
     List list = null;
     addOrCreateList(list);
   }

infer/tests/codetoanalyze/java/threadsafety/Ownership.java

@@ -33,6 +33,9 @@ public class Ownership {
 
   Obj field;
 
+  public Ownership() {
+  }
+
   public Ownership(Obj o) {
     field = o;
   }
@@ -430,6 +433,79 @@ public class Ownership {
     m.g.g.g = new Obj();
   }
 
+  private void reassignParamToOwned(Obj o) {
+    o = new Obj();
+    o.f = null; // we know the reassigned o is owned, mutating is ok
+  }
+
+  Obj unownedField1;
+  void reassignParamToOwnedOk() {
+    reassignParamToOwned(this.unownedField1); // ok even though this.unownedField1 isn't owned
+  }
+
+  Obj unownedField2;
+  private void reassignParamToUnowned(Obj o) {
+    o = this.unownedField2;
+    o.f = null; // don't know that this.unownedField2 is owned
+  }
+
+  void reassignParamToUnownedBad() {
+    reassignParamToUnowned(new Obj()); // although o is owned here, it gets reassigned in the callee
+  }
+
+  void ownedViaLocalAliasOk() {
+    Obj owned = new Obj();
+    Obj alias = owned;
+    alias.f = null;
+    owned.f = new Object();
+  }
+
+  private void ownedViaParamAlias(Obj o) {
+    Obj alias = o;
+    alias.f = null; // ok if o is owned in caller
+    o.f = new Object(); // ok if alias is owned in
+  }
+
+  public void ownedViaAliasOk() {
+    Obj owned = new Obj();
+    ownedViaParamAlias(owned);
+  }
+
+  Obj unownedField3;
+  private void ownedViaThisAlias() {
+    Ownership alias = this;
+    alias.unownedField3 = null; // ok if this owned in caller
+    this.unownedField3 = new Obj(); // also ok if this is owned in caller
+  }
+
+  public static void ownedViaThisAliasOk() {
+    Ownership owned = new Ownership();
+    owned.ownedViaThisAlias();
+  }
+
+  boolean nondet;
+
+  private void conditionalAlias(Obj o1, Obj o2) {
+    Obj alias;
+    if (nondet) {
+      alias = o1;
+    } else {
+      alias = o2;
+    }
+    alias.f = null; // ok if both o1 and o2 are owned
+  }
+
+  // we don't allow multiple owned(formal_index) predicates to be associated with a single access
+  // path. this means we can't tell that alias is owned in conditionAlias, and so we'll report a
+  // false positive
+  void FP_conditionalAliasOk() {
+    conditionalAlias(new Obj(), new Obj());
+  }
+
+  void conditionalAliasBad(Obj unowned) {
+    conditionalAlias(new Obj(), unowned);
+  }
+
 }
 
 class MyObj { int data; }

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

@@ -27,6 +27,7 @@ codetoanalyze/java/threadsafety/Constructors.java, Constructors.<init>(), 1, THR
 codetoanalyze/java/threadsafety/Constructors.java, Constructors.<init>(Constructors), 1, THREAD_SAFETY_VIOLATION, [access to `Constructors.field`]
 codetoanalyze/java/threadsafety/Containers.java, boolean Containers.listReadBad(String), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,Read of container `&this.codetoanalyze.java.checkers.Containers.mList` via call to `contains`,<Beginning of write trace>,Write to container `&this.codetoanalyze.java.checkers.Containers.mList` via call to `set`]
 codetoanalyze/java/threadsafety/Containers.java, int Containers.readSimpleArrayMap(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,Read of container `&this.codetoanalyze.java.checkers.Containers.si_map` via call to `get`,<Beginning of write trace>,Write to container `&this.codetoanalyze.java.checkers.Containers.si_map` via call to `put`]
+codetoanalyze/java/threadsafety/Containers.java, void Containers.FP_addToNullListOk(), 2, THREAD_SAFETY_VIOLATION, [call to List Containers.addOrCreateList(List),Write to container `&list` via call to `add`]
 codetoanalyze/java/threadsafety/Containers.java, void Containers.addToSimpleArrayMapBad(SimpleArrayMap), 1, THREAD_SAFETY_VIOLATION, [Write to container `&map` via call to `put`]
 codetoanalyze/java/threadsafety/Containers.java, void Containers.addToSparseArrayBad(SparseArray), 1, THREAD_SAFETY_VIOLATION, [Write to container `&sparseArray` via call to `put`]
 codetoanalyze/java/threadsafety/Containers.java, void Containers.addToSparseArrayCompatBad(SparseArrayCompat), 1, THREAD_SAFETY_VIOLATION, [Write to container `&sparseArray` via call to `put`]
@@ -63,16 +64,19 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.tryLockNoCheckBad(), 2, T
 codetoanalyze/java/threadsafety/Locks.java, void Locks.tryLockWrongBranchBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Locks.f`]
 codetoanalyze/java/threadsafety/Ownership.java, Ownership.<init>(Obj,Object), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, int Ownership.readGlobalBad(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.Ownership.global`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.Ownership.global`]
+codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_conditionalAliasOk(), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.conditionalAlias(Obj,Obj),access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_ownAndConditionalOwnOk(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_twoDifferentConditionalOwnsOk(), 4, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.cantOwnThisBad(), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.setField(Obj),access to `codetoanalyze.java.checkers.Ownership.field`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.castThenCallBad(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.castThenCall(Obj),call to void Subclass.doWrite(),access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.castThenReturnBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.f`]
+codetoanalyze/java/threadsafety/Ownership.java, void Ownership.conditionalAliasBad(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.conditionalAlias(Obj,Obj),access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.notOwnedInCalleeBad(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.mutateIfNotNull(Obj),access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.notPropagatingOwnershipToAccessPathRootedAtFormalBad(Obj), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.g`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad(), 2, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.Ownership.field`,<Beginning of write trace>,call to void Ownership.setField(Obj),access to `codetoanalyze.java.checkers.Ownership.field`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.g`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 5, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.f`]
+codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignParamToUnownedBad(), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.reassignParamToUnowned(Obj),access to `codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignToFormalBad(Obj), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Obj.g`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignToFormalBad(Obj), 3, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.Obj.g`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.Obj.g`]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad1(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to `codetoanalyze.java.checkers.Obj.f`]