From f0ab545594909e6b066f5fe9f39066ac846a2b01 Mon Sep 17 00:00:00 2001
From: Matthew Jin <38902361+matjin@users.noreply.github.com>
Date: Thu, 8 Jul 2021 05:27:59 -0700
Subject: [PATCH] Add Infer# Support for Inference Between Type Expressions
 (#1455)

Summary:
This PR enables implications to be drawn between .NET types.

Pull Request resolved: https://github.com/facebook/infer/pull/1455

Reviewed By: ngorogiannis

Differential Revision: D29612722

Pulled By: jvillard

fbshipit-source-id: 2e29b51a9
---
 infer/src/IR/StdTyp.ml          |  2 ++
 infer/src/IR/StdTyp.mli         |  2 ++
 infer/src/IR/Subtype.ml         |  2 ++
 infer/src/IR/Typ.ml             |  2 ++
 infer/src/IR/Typ.mli            |  2 ++
 infer/src/biabduction/Prover.ml | 12 +++++++++++-
 6 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/infer/src/IR/StdTyp.ml b/infer/src/IR/StdTyp.ml
index 04cff2f19..cca8cba19 100644
--- a/infer/src/IR/StdTyp.ml
+++ b/infer/src/IR/StdTyp.ml
@@ -48,6 +48,8 @@ module Name = struct
     open Typ.Name.CSharp
 
     let system_string = from_string "System.String"
+
+    let system_object = from_string "System.Object"
   end
 
   module Objc = struct
diff --git a/infer/src/IR/StdTyp.mli b/infer/src/IR/StdTyp.mli
index 635f433b8..69079858b 100644
--- a/infer/src/IR/StdTyp.mli
+++ b/infer/src/IR/StdTyp.mli
@@ -45,6 +45,8 @@ module Name : sig
 
   module CSharp : sig
     val system_string : t
+
+    val system_object : t
   end
 
   module Objc : sig
diff --git a/infer/src/IR/Subtype.ml b/infer/src/IR/Subtype.ml
index e8abe9a4f..afa9b73f5 100644
--- a/infer/src/IR/Subtype.ml
+++ b/infer/src/IR/Subtype.ml
@@ -46,6 +46,8 @@ let is_root_class class_name =
   match class_name with
   | Typ.JavaClass _ ->
       Typ.Name.equal class_name StdTyp.Name.Java.java_lang_object
+  | Typ.CSharpClass _ ->
+      Typ.Name.equal class_name StdTyp.Name.CSharp.system_object
   | _ ->
       false
 
diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index 35f8c4270..42676ed53 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -512,6 +512,8 @@ module Name = struct
 
   module CSharp = struct
     let from_string name_str = CSharpClass (CSharpClassName.from_string name_str)
+
+    let is_class = function CSharpClass _ -> true | _ -> false
   end
 
   module Java = struct
diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index 36d1e9ee3..bfe62dc67 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -200,6 +200,8 @@ module Name : sig
 
   module CSharp : sig
     val from_string : string -> t
+
+    val is_class : t -> bool
   end
 
   module Java : sig
diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml
index 4fb087534..076a5a016 100644
--- a/infer/src/biabduction/Prover.ml
+++ b/infer/src/biabduction/Prover.ml
@@ -45,6 +45,16 @@ let rec is_java_class tenv (typ : Typ.t) =
       false
 
 
+let rec is_csharp_class tenv (typ : Typ.t) =
+  match typ.desc with
+  | Tstruct name ->
+      Typ.Name.CSharp.is_class name
+  | Tarray {elt= inner_typ} | Tptr (inner_typ, _) ->
+      is_csharp_class tenv inner_typ
+  | _ ->
+      false
+
+
 (** Negate an atom *)
 let atom_negate tenv (atom : Predicates.atom) : Predicates.atom =
   match atom with
@@ -1845,7 +1855,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
     | Exp.Sizeof {typ= typ1}, Exp.Sizeof {typ= typ2} -> (
       match (typ1.desc, typ2.desc) with
       | (Tstruct _ | Tarray _), (Tstruct _ | Tarray _) ->
-          is_java_class tenv typ1
+          (is_java_class tenv typ1 || is_csharp_class tenv typ1)
           || (Typ.is_cpp_class typ1 && Typ.is_cpp_class typ2)
           || (Typ.is_objc_class typ1 && Typ.is_objc_class typ2)
       | _ ->