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

@@ -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

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. *)

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)

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 *)
 

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

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)

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

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 *)

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

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

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

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