[sledge] Add support for BFloat type

Reviewed By: jvillard

Differential Revision: D27280740

fbshipit-source-id: c4702727d

sledge/cli/frontend.ml

@@ -280,6 +280,7 @@ let rec xlate_type : x -> Llvm.lltype -> Typ.t =
       let bits = bit_size_of x llt in
       match Llvm.classify_type llt with
       | Half | Float | Double | Fp128 -> Typ.float ~bits ~byts ~enc:`IEEE
+      | BFloat -> Typ.float ~bits ~byts ~enc:`Brain
       | X86fp80 -> Typ.float ~bits ~byts ~enc:`Extended
       | Ppc_fp128 -> Typ.float ~bits ~byts ~enc:`Pair
       | Integer -> Typ.integer ~bits ~byts
@@ -336,8 +337,8 @@ let rec xlate_type : x -> Llvm.lltype -> Typ.t =
       | Token -> Typ.opaque ~name:"token"
       | Vector | Array | Struct ->
           todo "unsized non-opaque aggregate types: %a" pp_lltype llt ()
-      | Half | Float | Double | X86fp80 | Fp128 | Ppc_fp128 | Integer
+      | Half | BFloat | Float | Double | X86fp80 | Fp128 | Ppc_fp128
-       |X86_mmx | Pointer ->
+       |Integer | X86_mmx | Pointer ->
           fail "expected to be sized: %a" pp_lltype llt ()
       | Void | Label | Metadata -> assert false
   in

sledge/src/llair/typ.ml

@@ -10,7 +10,8 @@
 type t =
   | Function of {return: t option; args: t iarray}
   | Integer of {bits: int; byts: int}
-  | Float of {bits: int; byts: int; enc: [`IEEE | `Extended | `Pair]}
+  | Float of
+      {bits: int; byts: int; enc: [`Brain | `IEEE | `Extended | `Pair]}
   | Pointer of {elt: t}
   | Array of {elt: t; len: int; bits: int; byts: int}
   | Tuple of {elts: (int * t) iarray; bits: int; byts: int}
@@ -35,6 +36,7 @@ let rec pp fs typ =
   | Float {bits; enc} ->
       let enc_str =
         match enc with
+        | `Brain -> "brain"
         | `IEEE -> ""
         | `Extended -> "extend"
         | `Pair -> "pair"

sledge/src/llair/typ.mli

@@ -11,7 +11,8 @@ type t = private
   | Function of {return: t option; args: t iarray}
       (** (Global) function names have type Pointer to Function. *)
   | Integer of {bits: int; byts: int}  (** Integer of given bitwidth. *)
-  | Float of {bits: int; byts: int; enc: [`IEEE | `Extended | `Pair]}
+  | Float of
+      {bits: int; byts: int; enc: [`Brain | `IEEE | `Extended | `Pair]}
       (** Floating-point numbers of given bitwidth and encoding. *)
   | Pointer of {elt: t}  (** Pointer to element type. *)
   | Array of {elt: t; len: int; bits: int; byts: int}
@@ -41,7 +42,10 @@ val siz : t
 val ptr : t
 val function_ : return:t option -> args:t iarray -> t
 val integer : bits:int -> byts:int -> t
-val float : bits:int -> byts:int -> enc:[`Extended | `IEEE | `Pair] -> t
+
+val float :
+  bits:int -> byts:int -> enc:[`Brain | `Extended | `IEEE | `Pair] -> t
+
 val pointer : elt:t -> t
 val array : elt:t -> len:int -> bits:int -> byts:int -> t
 val tuple : (int * t) iarray -> bits:int -> byts:int -> t