[hil] don't move reads/writes outside of a critical section

Summary:
If you write

```
boolean readUnderLockOk() {
  synchronized (mLock) {
    return mField;
  }
}
```

it will be turned into

```
lock()
irvar0 = mField
unlock()
return irvar0
```

in the bytecode. Since HIL eliminates reads/writes to temporaries, it will make the above code appear to perform a read of `mField` outside of the lock.

This diff fixes the problem by forcing HIL to perform all pending reads/writes before you exit a critical section.

Reviewed By: jberdine

Differential Revision: D6138749

fbshipit-source-id: e8ad9a0

infer/src/IR/Pvar.ml

@@ -270,4 +270,3 @@ let get_initializer_pname {pv_name; pv_kind} =
            (Config.clang_initializer_prefix ^ Mangled.to_string_full pv_name))
   | _ ->
       None
-

infer/src/absint/LowerHil.ml

@@ -29,6 +29,16 @@ struct
 
   type extras = TransferFunctions.extras
 
+  let pp_pre_post pre post hil_instr node =
+    if Config.write_html then
+      let underyling_node = CFG.underlying_node node in
+      NodePrinter.start_session underyling_node ;
+      L.d_strln
+        (Format.asprintf "PRE: %a@.INSTR: %a@.POST: %a@." TransferFunctions.Domain.pp pre
+           HilInstr.pp hil_instr TransferFunctions.Domain.pp post) ;
+      NodePrinter.finish_session underyling_node
+
+
   let exec_instr ((actual_state, id_map) as astate) extras node instr =
     let f_resolve_id id =
       try Some (IdAccessPathMapDomain.find id id_map)
@@ -45,15 +55,26 @@ struct
           List.fold ~f:(fun acc id -> IdAccessPathMapDomain.remove id acc) ~init:id_map ids
         in
         if phys_equal id_map id_map' then astate else (actual_state, id_map')
+    | Instr (Call (_, Direct callee_pname, _, _, loc) as hil_instr)
+      when Typ.Procname.equal callee_pname BuiltinDecl.__delete_locked_attribute ->
+        (* need to be careful not to move reads/writes out of a critical section. to ensure this,
+           "dump" all of the temporaries out of the id map, then execute the unlock instruction. *)
+        let actual_state' =
+          IdAccessPathMapDomain.fold
+            (fun id access_path astate_acc ->
+              let lhs_access_path = ((id, Typ.mk Typ.Tvoid), []) in
+              let dummy_assign =
+                HilInstr.Assign (lhs_access_path, HilExp.AccessPath access_path, loc)
+              in
+              TransferFunctions.exec_instr astate_acc extras node dummy_assign)
+            id_map actual_state
+        in
+        let actual_state'' = TransferFunctions.exec_instr actual_state' extras node hil_instr in
+        pp_pre_post actual_state actual_state'' hil_instr node ;
+        (actual_state'', IdAccessPathMapDomain.empty)
     | Instr hil_instr ->
         let actual_state' = TransferFunctions.exec_instr actual_state extras node hil_instr in
-        ( if Config.write_html then
-            let underyling_node = CFG.underlying_node node in
-            NodePrinter.start_session underyling_node ;
-            L.d_strln
-              (Format.asprintf "PRE: %a@.INSTR: %a@.POST: %a@." TransferFunctions.Domain.pp
-                 (fst astate) HilInstr.pp hil_instr TransferFunctions.Domain.pp actual_state') ;
-            NodePrinter.finish_session underyling_node ) ;
+        pp_pre_post actual_state actual_state' hil_instr node ;
         if phys_equal actual_state actual_state' then astate else (actual_state', id_map)
     | Ignore ->
         astate

infer/tests/codetoanalyze/java/racerd/Locks.java

@@ -188,4 +188,31 @@ public class Locks {
     mReentrantReadWriteLock.readLock().unlock();
   }
 
+  boolean mField;
+
+  boolean readUnderLockOk() {
+    synchronized (this) {
+      return mField;
+    }
+  }
+
+  void writeUnderLockOk() {
+    synchronized (this) {
+      mField = true;
+    }
+  }
+
+  boolean readOutsideLock1Bad() {
+    synchronized (this) {
+    }
+    return mField;
+  }
+
+  boolean readOutsideLock2Bad() {
+    boolean tmp = mField;
+    synchronized (this) {
+    }
+    return tmp;
+  }
+
 }

infer/tests/codetoanalyze/java/racerd/Ownership.java

@@ -390,14 +390,17 @@ public class Ownership {
 
   static MyObj global;
 
-  void storeInGlobalAndWriteBad() {
+  // would need escape analysis to detect this
+  void FN_storeInGlobalAndWriteBad() {
     MyObj x = new MyObj();
-    synchronized(this) { global = x; }
+    synchronized (Ownership.class) {
+      global = x;
+    }
     x.data = 5;
   }
 
   int readGlobalBad() {
-    synchronized(this) { return global.data; }
+    return global.data;
   }
 
   public void writeOwnedWithExceptionOk() {

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

@@ -49,6 +49,8 @@ codetoanalyze/java/racerd/Dispatch.java, void Dispatch.callUnannotatedInterfaceI
 codetoanalyze/java/racerd/Inference.java, int Inference.read4OutsideSyncBad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`]
 codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead1Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField1`]
 codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField2`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField2`]
+codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock1Bad(), 3, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`]
+codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`]
 codetoanalyze/java/racerd/Locks.java, void Locks.FP_unlockOneLock(), 4, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`]
 codetoanalyze/java/racerd/Locks.java, void Locks.afterReentrantLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`]
 codetoanalyze/java/racerd/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`]