From 4b700b37b588706b78f777fac72c9fecfe48c723 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 9 Apr 2021 08:13:41 -0700 Subject: [PATCH] [sledge] Translate casts between Typ.equivalent types to no-op Summary: `Typ.equivalent` relates types that denote the same sets of values in the semantic model, such as pointers and integers of the appropriate size. This diff strengthens the treatment of casts between such types in the first-order solver by translating `(s)(t)e` to `e` for equivalent types `s` and `t`. These casts are usually simplified out of the bitcode produced by clang. However, code using `_Atomic(...)` leads to `load atomic` llvm instructions that, for some reason, cast pointers to i64 and back. Reviewed By: ngorogiannis Differential Revision: D27564881 fbshipit-source-id: 6138eb4f1 --- sledge/src/llair_to_Fol.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml index 20486ec9c..3ec36a25b 100644 --- a/sledge/src/llair_to_Fol.ml +++ b/sledge/src/llair_to_Fol.ml @@ -90,7 +90,7 @@ and term : Llair.Exp.t -> T.t = | Some fml -> F.inject fml | _ -> uap1 (Unsigned bits) a else uap1 (Unsigned bits) a - | Ap1 (Convert {src= Pointer _}, Pointer _, e) -> term e + | Ap1 (Convert {src}, dst, e) when Llair.Typ.equivalent src dst -> term e | Ap1 (Convert {src= Float _}, Float _, e) -> term e | Ap1 (Convert {src}, dst, e) -> let s =