From 9bafbe0e1e4ea75a0b41e5b42f3fad8acc415329 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 25 Oct 2017 11:24:10 -0700 Subject: [PATCH] [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 | 1 - infer/src/absint/LowerHil.ml | 35 +++++++++++++++---- .../codetoanalyze/java/racerd/Locks.java | 27 ++++++++++++++ .../codetoanalyze/java/racerd/Ownership.java | 9 +++-- .../codetoanalyze/java/racerd/issues.exp | 2 ++ 5 files changed, 63 insertions(+), 11 deletions(-) diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml index c5c6b6fc1..bef228962 100644 --- a/infer/src/IR/Pvar.ml +++ b/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 - diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 5723ba963..d0dbcf2b6 100644 --- a/infer/src/absint/LowerHil.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/java/racerd/Locks.java b/infer/tests/codetoanalyze/java/racerd/Locks.java index 0d1fc7940..dfa5b6960 100644 --- a/infer/tests/codetoanalyze/java/racerd/Locks.java +++ b/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; + } + } diff --git a/infer/tests/codetoanalyze/java/racerd/Ownership.java b/infer/tests/codetoanalyze/java/racerd/Ownership.java index 1f8ea2160..4971c6748 100644 --- a/infer/tests/codetoanalyze/java/racerd/Ownership.java +++ b/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() { diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index 8d6807fb2..80ad72e0b 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/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, [,access to `&this.codetoanalyze.java.checkers.Inference.mField4`,,access to `&this.codetoanalyze.java.checkers.Inference.mField4`] codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead1Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Inference.mField1`,,access to `&this.codetoanalyze.java.checkers.Inference.mField1`] codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead2Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Inference.mField2`,,access to `&this.codetoanalyze.java.checkers.Inference.mField2`] +codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock1Bad(), 3, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Locks.mField`,,access to `&this.codetoanalyze.java.checkers.Locks.mField`] +codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock2Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Locks.mField`,,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`]