[sledge] Relax Exp type-checking to be modulo-casting

Summary:
Also weaken definition of Typ.castable to permit casting between
floats and ints of the same size.

Reviewed By: bennostein

Differential Revision: D17725611

fbshipit-source-id: 5e8114e26

sledge/src/llair/exp.ml

@@ -210,20 +210,20 @@ let rec invariant exp =
   | Label _ -> assert true
   | Ap1 (Convert {dst}, src, arg) ->
       assert (Typ.convertible dst src) ;
-      assert (Typ.equal src (typ_of arg))
+      assert (Typ.castable src (typ_of arg))
   | Ap1 (Select idx, typ, rcd) -> (
-      assert (Typ.equal typ (typ_of rcd)) ;
+      assert (Typ.castable typ (typ_of rcd)) ;
       match typ with
       | Array _ -> assert true
       | Tuple {elts} | Struct {elts} -> assert (valid_idx idx elts)
       | _ -> assert false )
   | Ap2 (Update idx, typ, rcd, elt) -> (
-      assert (Typ.equal typ (typ_of rcd)) ;
+      assert (Typ.castable typ (typ_of rcd)) ;
       match typ with
       | Tuple {elts} | Struct {elts} ->
           assert (valid_idx idx elts) ;
-          assert (Typ.equal (Vector.get elts idx) (typ_of elt))
-      | Array {elt= typ_elt} -> assert (Typ.equal typ_elt (typ_of elt))
+          assert (Typ.castable (Vector.get elts idx) (typ_of elt))
+      | Array {elt= typ_elt} -> assert (Typ.castable typ_elt (typ_of elt))
       | _ -> assert false )
   | Ap2 (op, typ, x, y) -> (
     match (op, typ) with
@@ -234,24 +234,25 @@ let rec invariant exp =
      |(Mul | Div | Rem), (Integer _ | Float _)
      |(Udiv | Urem | And | Or | Xor | Shl | Lshr | Ashr), Integer _ ->
         let typ_x = typ_of x and typ_y = typ_of y in
-        assert (Typ.equal typ typ_x) ;
-        assert (Typ.equal typ_x typ_y)
+        assert (Typ.castable typ typ_x) ;
+        assert (Typ.castable typ_x typ_y)
     | _ -> assert false )
   | Ap3 (Conditional, typ, cnd, thn, els) ->
       assert (Typ.is_sized typ) ;
-      assert (Typ.equal Typ.bool (typ_of cnd)) ;
-      assert (Typ.equal typ (typ_of thn)) ;
-      assert (Typ.equal typ (typ_of els))
+      assert (Typ.castable Typ.bool (typ_of cnd)) ;
+      assert (Typ.castable typ (typ_of thn)) ;
+      assert (Typ.castable typ (typ_of els))
   | ApN ((Record | Struct_rec), typ, args) -> (
     match typ with
     | Array {elt} ->
         assert (
-          Vector.for_all args ~f:(fun arg -> Typ.equal elt (typ_of arg)) )
+          Vector.for_all args ~f:(fun arg -> Typ.castable elt (typ_of arg))
+        )
     | Tuple {elts} | Struct {elts} ->
         assert (Vector.length elts = Vector.length args) ;
         assert (
           Vector.for_all2_exn elts args ~f:(fun typ arg ->
-              Typ.equal typ (typ_of arg) ) )
+              Typ.castable typ (typ_of arg) ) )
     | _ -> assert false )
   [@@warning "-9"]
 

sledge/src/llair/typ.ml

@@ -131,13 +131,13 @@ let rec equivalent t0 t1 =
       m = n && equivalent t u
   | _ -> equal t0 t1
 
-let rec castable t0 t1 =
+let castable t0 t1 =
   match (t0, t1) with
-  | (Pointer _ | Integer _), (Pointer _ | Integer _) -> (
+  | ( (Pointer _ | Integer _ | Float _ | Array _)
+    , (Pointer _ | Integer _ | Float _ | Array _) ) -> (
     match (prim_bit_size_of t0, prim_bit_size_of t1) with
     | Some n0, Some n1 -> n0 = n1
     | _ -> false )
-  | Array {elt= t; len= m}, Array {elt= u; len= n} -> m = n && castable t u
   | _ -> equal t0 t1
 
 let rec convertible t0 t1 =