[sledge] Introduce the notion of types having the same semantics

Summary:
Typ.equivalent is currently defined the same as Typ.castable, but
conceptually they are different and castable needs to be
weakened. They are different since for example it is possible to cast
from an i64 to a f64, but those types denote different sets of values
in the semantics, and the bitcast is modeled using a conversion
function.

Reviewed By: bennostein

Differential Revision: D17725615

fbshipit-source-id: 973574f2a

sledge/src/llair/term.ml

@@ -497,7 +497,7 @@ let simp_extract ~unsigned bits arg =
   | _ -> Ap1 (Extract {unsigned; bits}, arg)
 
 let simp_convert ~unsigned dst src arg =
-  if (not unsigned) && Typ.castable dst src then arg
+  if (not unsigned) && Typ.equivalent dst src then arg
   else
     match (dst, src, arg) with
     | Integer {bits= m}, Integer {bits= n}, Integer {data} ->

sledge/src/llair/typ.ml

@@ -121,6 +121,16 @@ let rec prim_bit_size_of = function
       Option.map (prim_bit_size_of elt) ~f:(fun n -> n * len)
   | Function _ | Tuple _ | Struct _ | Opaque _ -> None
 
+let rec equivalent t0 t1 =
+  match (t0, t1) with
+  | (Pointer _ | Integer _), (Pointer _ | Integer _) -> (
+    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 && equivalent t u
+  | _ -> equal t0 t1
+
 let rec castable t0 t1 =
   match (t0, t1) with
   | (Pointer _ | Integer _), (Pointer _ | Integer _) -> (

sledge/src/llair/typ.mli

@@ -54,6 +54,10 @@ val prim_bit_size_of : t -> int option
 val is_sized : t -> bool
 (** Holds of types which are first-class and have a statically-known size. *)
 
+val equivalent : t -> t -> bool
+(** Equivalent types are those that denote the same sets of values in the
+    semantic model. An equivalence relation. *)
+
 val castable : t -> t -> bool
 (** Castable types are those that can be cast between without loss of
     information. An equivalence relation. *)