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`]