[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

@@ -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 =