From 287eee78f54b48524bf7ad5dd3ad43ebf773285a Mon Sep 17 00:00:00 2001 From: Xiaoyu Liu Date: Wed, 19 May 2021 08:29:01 -0700 Subject: [PATCH] CIL race condition detection support (#1443) Summary: This PR adds race condition detection support on CIL backed languages, such as .NET platform languages. We will add unit tests later since we are still fine tunning Infer# translation module. Pull Request resolved: https://github.com/facebook/infer/pull/1443 Reviewed By: jvillard Differential Revision: D28505195 Pulled By: ngorogiannis fbshipit-source-id: f263f6ba6 --- infer/src/IR/ProcAttributes.ml | 5 ++ infer/src/IR/ProcAttributes.mli | 1 + infer/src/IR/Procdesc.ml | 2 + infer/src/IR/Procdesc.mli | 3 + infer/src/backend/InferAnalyzeJson.ml | 12 ++++ infer/src/backend/registerCheckers.ml | 7 ++- infer/src/base/Checker.ml | 3 +- infer/src/concurrency/RacerDDomain.ml | 4 +- infer/src/concurrency/RacerDFileAnalysis.ml | 10 ++-- infer/src/concurrency/RacerDModels.ml | 63 +++++++++++++++++++++ infer/src/concurrency/RacerDProcAnalysis.ml | 7 ++- infer/src/concurrency/starvation.ml | 2 +- 12 files changed, 109 insertions(+), 10 deletions(-) diff --git a/infer/src/IR/ProcAttributes.ml b/infer/src/IR/ProcAttributes.ml index 6dfc87319..5acc2cd93 100644 --- a/infer/src/IR/ProcAttributes.ml +++ b/infer/src/IR/ProcAttributes.ml @@ -70,6 +70,7 @@ type t = ; is_bridge_method: bool (** the procedure is a bridge method *) ; is_defined: bool (** true if the procedure is defined, and not just declared *) ; is_java_synchronized_method: bool (** the procedure is a Java synchronized method *) + ; is_csharp_synchronized_method: bool (** the procedure is a C# synchronized method *) ; passed_as_noescape_block_to: Procname.t option (** Present if the procedure is an Objective-C block that has been passed to the given method in a position annotated with the NS_NOESCAPE attribute. *) @@ -135,6 +136,7 @@ let default translation_unit proc_name = ; is_bridge_method= false ; is_defined= false ; is_java_synchronized_method= false + ; is_csharp_synchronized_method= false ; passed_as_noescape_block_to= None ; is_no_return= false ; is_objc_arc_on= false @@ -183,6 +185,7 @@ let pp f ; is_bridge_method ; is_defined ; is_java_synchronized_method + ; is_csharp_synchronized_method ; passed_as_noescape_block_to ; is_no_return ; is_objc_arc_on @@ -228,6 +231,8 @@ let pp f pp_bool_default ~default:default.is_defined "is_defined" is_defined f () ; pp_bool_default ~default:default.is_java_synchronized_method "is_java_synchronized_method" is_java_synchronized_method f () ; + pp_bool_default ~default:default.is_csharp_synchronized_method "is_csharp_synchronized_method" + is_csharp_synchronized_method f () ; if not ([%compare.equal: Procname.t option] default.passed_as_noescape_block_to diff --git a/infer/src/IR/ProcAttributes.mli b/infer/src/IR/ProcAttributes.mli index dc16d2251..659e8c213 100644 --- a/infer/src/IR/ProcAttributes.mli +++ b/infer/src/IR/ProcAttributes.mli @@ -42,6 +42,7 @@ type t = ; is_bridge_method: bool (** the procedure is a bridge method *) ; is_defined: bool (** true if the procedure is defined, and not just declared *) ; is_java_synchronized_method: bool (** the procedure is a Java synchronized method *) + ; is_csharp_synchronized_method: bool (** the procedure is a C# synchronized method *) ; passed_as_noescape_block_to: Procname.t option (** Present if the procedure is an Objective-C block that has been passed to the given method in a position annotated with the NS_NOESCAPE attribute. *) diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index e2d67482b..37986b0aa 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -552,6 +552,8 @@ let is_defined pdesc = pdesc.attributes.is_defined let is_java_synchronized pdesc = pdesc.attributes.is_java_synchronized_method +let is_csharp_synchronized pdesc = pdesc.attributes.is_csharp_synchronized_method + let is_objc_arc_on pdesc = pdesc.attributes.is_objc_arc_on let iter_nodes f pdesc = List.iter ~f (get_nodes pdesc) diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 79c225dd0..6e2c00cf4 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -282,6 +282,9 @@ val is_defined : t -> bool val is_java_synchronized : t -> bool (** Return [true] if the procedure signature has the Java synchronized keyword *) +val is_csharp_synchronized : t -> bool +(** Return [true] if the procedure is synchronized via a C# lock *) + val is_objc_arc_on : t -> bool (** Return [true] iff the ObjC procedure is compiled with ARC *) diff --git a/infer/src/backend/InferAnalyzeJson.ml b/infer/src/backend/InferAnalyzeJson.ml index f80a67b0e..98b881267 100644 --- a/infer/src/backend/InferAnalyzeJson.ml +++ b/infer/src/backend/InferAnalyzeJson.ml @@ -56,6 +56,18 @@ let parse_cil_procname (json : Safe.t) : Procname.t = match method_name with | "__new" -> BuiltinDecl.__new + | "__new_array" -> + BuiltinDecl.__new_array + | "__set_locked_attribute" -> + BuiltinDecl.__set_locked_attribute + | "__delete_locked_attribute" -> + BuiltinDecl.__delete_locked_attribute + | "__instanceof" -> + BuiltinDecl.__instanceof + (* We exclude this for now as it would require significant effort unrelated to our support of + null deref/resource leak/thread safety violation detection. *) + (*| "__unwrap_exception" -> + BuiltinDecl.__unwrap_exception*) | _ -> let return_type = if String.equal Procname.CSharp.constructor_method_name method_name then None diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index 25140f7fa..167853467 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -142,7 +142,12 @@ let all_checkers = ; callbacks= (let racerd_proc = interprocedural Payloads.Fields.racerd RacerDProcAnalysis.analyze in let racerd_file = file RacerDIssues Payloads.Fields.racerd RacerDFileAnalysis.analyze in - [(racerd_proc, Clang); (racerd_proc, Java); (racerd_file, Clang); (racerd_file, Java)] ) } + [ (racerd_proc, Clang) + ; (racerd_proc, Java) + ; (racerd_proc, CIL) + ; (racerd_file, Clang) + ; (racerd_file, Java) + ; (racerd_file, CIL) ] ) } ; { checker= Quandary ; callbacks= [ (interprocedural Payloads.Fields.quandary JavaTaintAnalysis.checker, Java) diff --git a/infer/src/base/Checker.ml b/infer/src/base/Checker.ml index fa12404ed..7d52710ea 100644 --- a/infer/src/base/Checker.ml +++ b/infer/src/base/Checker.ml @@ -364,7 +364,8 @@ let config_unsafe checker = ; kind= UserFacing {title= "RacerD"; markdown_body= [%blob "../../documentation/checkers/RacerD.md"]} - ; support= supports_clang_and_java + ; support= + (function Clang -> Support | Java -> Support | CIL -> Support | Erlang -> NoSupport) ; short_documentation= "Thread safety analysis." ; cli_flags= Some {deprecated= ["-threadsafety"]; show_in_help= true} ; enabled_by_default= true diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index a749f5996..b4d6a5c6f 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -623,7 +623,9 @@ let astate_to_summary proc_desc formals {threads; locks; accesses; ownership; at let return_attribute = AttributeMapDomain.get return_var_exp attribute_map in let locks = (* if method is [synchronized] released the lock once. *) - if Procdesc.is_java_synchronized proc_desc then LockDomain.release_lock locks else locks + if Procdesc.is_java_synchronized proc_desc || Procdesc.is_csharp_synchronized proc_desc then + LockDomain.release_lock locks + else locks in let attributes = (* store only the [Synchronized] attribute for class initializers/constructors *) diff --git a/infer/src/concurrency/RacerDFileAnalysis.ml b/infer/src/concurrency/RacerDFileAnalysis.ml index 9705313f7..707301675 100644 --- a/infer/src/concurrency/RacerDFileAnalysis.ml +++ b/infer/src/concurrency/RacerDFileAnalysis.ml @@ -100,7 +100,7 @@ let get_reporting_explanation_cpp = (IssueType.lock_consistency_violation, "") (** Explain why we are reporting this access *) let get_reporting_explanation ~nullsafe report_kind tenv pname thread = - if Procname.is_java pname then + if Procname.is_java pname || Procname.is_csharp pname then get_reporting_explanation_java ~nullsafe report_kind tenv pname thread else get_reporting_explanation_cpp @@ -357,6 +357,8 @@ end let should_report_on_proc tenv procdesc = let proc_name = Procdesc.get_proc_name procdesc in match proc_name with + | CSharp _ -> + not (ProcAttributes.equal_access (Procdesc.get_access procdesc) Private) | Java java_pname -> (* return true if procedure is at an abstraction boundary or reporting has been explicitly requested via @ThreadSafe in java *) @@ -490,7 +492,7 @@ let report_unsafe_accesses ~issue_log file_tenv classname (aggregated_access_map report_unannotated_interface_violation ~acc reported_pname reported_access | InterfaceCall _ -> acc - | (Write _ | ContainerWrite _) when Procname.is_java pname -> + | (Write _ | ContainerWrite _) when Procname.is_java pname || Procname.is_csharp pname -> let conflict = if ThreadsDomain.is_any threads then (* unprotected write in method that may run in parallel with itself. warn *) @@ -520,7 +522,7 @@ let report_unsafe_accesses ~issue_log file_tenv classname (aggregated_access_map let is_conflict {snapshot; threads= other_threads} = AccessSnapshot.is_write snapshot && - if Procname.is_java pname then + if Procname.is_java pname || Procname.is_csharp pname then ThreadsDomain.is_any threads || ThreadsDomain.is_any other_threads else not (AccessSnapshot.is_unprotected snapshot) in @@ -532,7 +534,7 @@ let report_unsafe_accesses ~issue_log file_tenv classname (aggregated_access_map let report_kind = ReadWriteRace conflict.snapshot in report_thread_safety_violation ~acc ~make_description ~report_kind ~nullsafe reported_access ) - | (Read _ | ContainerRead _) when Procname.is_java pname -> + | (Read _ | ContainerRead _) when Procname.is_java pname || Procname.is_csharp pname -> (* protected read. report unprotected writes and opposite protected writes as conflicts *) let can_conflict (snapshot1 : AccessSnapshot.t) (snapshot2 : AccessSnapshot.t) = if snapshot1.elem.lock && snapshot2.elem.lock then false diff --git a/infer/src/concurrency/RacerDModels.ml b/infer/src/concurrency/RacerDModels.ml index a43ea6a57..4f5a0bb89 100644 --- a/infer/src/concurrency/RacerDModels.ml +++ b/infer/src/concurrency/RacerDModels.ml @@ -24,6 +24,65 @@ let make_android_support_template suffix methods = ; {default with classname= "androidx.core.util." ^ suffix; methods} ] +let is_csharp_container_write = + let open MethodMatcher in + [ { default with + classname= "System.Collections.Generic.List`1" + ; methods= + [ "Add" + ; "AddRange" + ; "Clear" + ; "Insert" + ; "InsertRange" + ; "Remove" + ; "RemoveAll" + ; "RemoveAt" + ; "RemoveRange" + ; "set_Item" ] } + ; { default with + classname= "System.Collections.Generic.Dictionary`2" + ; methods= ["Add"; "Clear"; "Remove"; "TryAdd"; "set_Item"] } ] + |> of_records + + +let is_csharp_container_read = + let open MethodMatcher in + [ { default with + classname= "System.Collections.Generic.List`1" + ; methods= + [ "BinarySearch" + ; "Contains" + ; "CopyTo" + ; "Equals" + ; "Exists" + ; "Find" + ; "FindAll" + ; "FindIndex" + ; "FindLast" + ; "FindLastIndex" + ; "GetEnumerator" + ; "GetHashCode" + ; "GetRange" + ; "IndexOf" + ; "LastIndexOf" + ; "MemberwiseClone" + ; "ToArray" + ; "TrueForAll" + ; "get_Item" + ; "get_Count" ] } + ; { default with + classname= "System.Collections.Generic.Dictionary`2" + ; methods= + [ "ContainsKey" + ; "ContainsValue" + ; "Equals" + ; "GetHashCode" + ; "TryGetValue" + ; "get_Item" + ; "get_Count" ] } ] + |> of_records + + let is_java_container_write = let open MethodMatcher in let array_methods = @@ -139,6 +198,8 @@ let is_cpp_container_write = let is_container_write tenv pn = match pn with + | Procname.CSharp _ when is_csharp_container_write tenv pn [] -> + true | Procname.Java _ when is_java_container_write tenv pn [] -> true | (Procname.ObjC_Cpp _ | C _) when is_cpp_container_write pn -> @@ -149,6 +210,8 @@ let is_container_write tenv pn = let is_container_read tenv pn = match pn with + | Procname.CSharp _ -> + is_csharp_container_read tenv pn [] | Procname.Java _ -> is_java_container_read tenv pn [] (* The following order matters: we want to check if pname is a container write diff --git a/infer/src/concurrency/RacerDProcAnalysis.ml b/infer/src/concurrency/RacerDProcAnalysis.ml index f2a572a2d..805ad051c 100644 --- a/infer/src/concurrency/RacerDProcAnalysis.ml +++ b/infer/src/concurrency/RacerDProcAnalysis.ml @@ -306,14 +306,17 @@ let analyze ({InterproceduralAnalysis.proc_desc; tenv} as interproc) = in if RacerDModels.should_analyze_proc tenv proc_name then let locks = - if Procdesc.is_java_synchronized proc_desc then LockDomain.(acquire_lock bottom) + if Procdesc.is_java_synchronized proc_desc || Procdesc.is_csharp_synchronized proc_desc then + LockDomain.(acquire_lock bottom) else LockDomain.bottom in let threads = if runs_on_ui_thread tenv proc_name || RacerDModels.is_thread_confined_method tenv proc_name then ThreadsDomain.AnyThreadButSelf else if - Procdesc.is_java_synchronized proc_desc || RacerDModels.is_marked_thread_safe proc_name tenv + Procdesc.is_java_synchronized proc_desc + || Procdesc.is_csharp_synchronized proc_desc + || RacerDModels.is_marked_thread_safe proc_name tenv then ThreadsDomain.AnyThread else ThreadsDomain.NoThread in diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 1e0c37294..c09b8b56c 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -417,7 +417,7 @@ let analyze_procedure ({InterproceduralAnalysis.proc_desc; tenv} as interproc) = let proc_data = {interproc; formals} in let loc = Procdesc.get_loc proc_desc in let set_lock_state_for_synchronized_proc astate = - if Procdesc.is_java_synchronized proc_desc then + if Procdesc.is_java_synchronized proc_desc || Procdesc.is_csharp_synchronized proc_desc then Domain.Lock.make_java_synchronized formals procname |> Option.to_list |> Domain.acquire ~tenv astate ~procname ~loc