From fb184a6a1d376ddf28662f77cf5c016b73334811 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 10 Oct 2019 06:17:24 -0700
Subject: [PATCH] [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 |  2 +-
 sledge/src/llair/typ.ml  | 10 ++++++++++
 sledge/src/llair/typ.mli |  4 ++++
 3 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index dbcbec9cb..07c6014ac 100644
--- a/sledge/src/llair/term.ml
+++ b/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} ->
diff --git a/sledge/src/llair/typ.ml b/sledge/src/llair/typ.ml
index c425749d7..beb333f6d 100644
--- a/sledge/src/llair/typ.ml
+++ b/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 _) -> (
diff --git a/sledge/src/llair/typ.mli b/sledge/src/llair/typ.mli
index 37fbf6f80..e1fbaaef2 100644
--- a/sledge/src/llair/typ.mli
+++ b/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. *)