[sledge] Simplify type conversions
Summary:
The treatment of type conversions is too complicated, non-uniform,
etc. This diff attempts to simplify things by separating integer to
integer conversions, which are interpreted, from others, which are
essentially just uninterpreted functions. Integer conversions are now
handled using two expression and term forms: Signed and
Unsigned. These each interpret their argument as either a signed or
unsigned number of a given bitwidth:
```
| Signed of {bits: int}
(** [Ap1 (Signed {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit signed integer and injected into the [dst] type. That is,
it two's-complement--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth at least
[n]. *)
| Unsigned of {bits: int}
(** [Ap1 (Unsigned {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit unsigned integer and injected into the [dst] type. That
is, it unsigned-binary--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth greater than
[n]. *)
| Convert of {src: Typ.t}
(** [Ap1 (Convert {src}, dst, arg)] is [arg] converted from type [src]
to type [dst], possibly with loss of information. The [src] and
[dst] types must be [Typ.convertible] and must not both be
[Integer] types. *)
```
Reviewed By: ngorogiannis
Differential Revision: D18298140
fbshipit-source-id: 690f065b4
5 years ago
|
|
|
(*
|
|
|
|
|
* Copyright (c) Facebook, Inc. and its affiliates.
|
|
|
|
|
*
|
|
|
|
|
* This source code is licensed under the MIT license found in the
|
|
|
|
|
* LICENSE file in the root directory of this source tree.
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
let%test_module _ =
|
|
|
|
|
( module struct
|
|
|
|
|
let () = Trace.init ~margin:68 ()
|
[sledge] Simplify type conversions
Summary:
The treatment of type conversions is too complicated, non-uniform,
etc. This diff attempts to simplify things by separating integer to
integer conversions, which are interpreted, from others, which are
essentially just uninterpreted functions. Integer conversions are now
handled using two expression and term forms: Signed and
Unsigned. These each interpret their argument as either a signed or
unsigned number of a given bitwidth:
```
| Signed of {bits: int}
(** [Ap1 (Signed {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit signed integer and injected into the [dst] type. That is,
it two's-complement--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth at least
[n]. *)
| Unsigned of {bits: int}
(** [Ap1 (Unsigned {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit unsigned integer and injected into the [dst] type. That
is, it unsigned-binary--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth greater than
[n]. *)
| Convert of {src: Typ.t}
(** [Ap1 (Convert {src}, dst, arg)] is [arg] converted from type [src]
to type [dst], possibly with loss of information. The [src] and
[dst] types must be [Typ.convertible] and must not both be
[Integer] types. *)
```
Reviewed By: ngorogiannis
Differential Revision: D18298140
fbshipit-source-id: 690f065b4
5 years ago
|
|
|
|
|
|
|
|
(* let () = Trace.init ~margin:68 ~config:Trace.all () *)
|
|
|
|
|
|
[sledge] Simplify type conversions
Summary:
The treatment of type conversions is too complicated, non-uniform,
etc. This diff attempts to simplify things by separating integer to
integer conversions, which are interpreted, from others, which are
essentially just uninterpreted functions. Integer conversions are now
handled using two expression and term forms: Signed and
Unsigned. These each interpret their argument as either a signed or
unsigned number of a given bitwidth:
```
| Signed of {bits: int}
(** [Ap1 (Signed {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit signed integer and injected into the [dst] type. That is,
it two's-complement--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth at least
[n]. *)
| Unsigned of {bits: int}
(** [Ap1 (Unsigned {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit unsigned integer and injected into the [dst] type. That
is, it unsigned-binary--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth greater than
[n]. *)
| Convert of {src: Typ.t}
(** [Ap1 (Convert {src}, dst, arg)] is [arg] converted from type [src]
to type [dst], possibly with loss of information. The [src] and
[dst] types must be [Typ.convertible] and must not both be
[Integer] types. *)
```
Reviewed By: ngorogiannis
Differential Revision: D18298140
fbshipit-source-id: 690f065b4
5 years ago
|
|
|
open Exp
|
|
|
|
|
|
|
|
|
|
let pp e = Format.printf "@\n{desc= %a; term= %a}@." pp e Term.pp e.term
|
|
|
|
|
let ( ! ) i = integer Typ.siz (Z.of_int i)
|
|
|
|
|
|
|
|
|
|
let%expect_test _ =
|
|
|
|
|
pp (signed 1 !1 ~to_:Typ.bool) ;
|
|
|
|
|
[%expect {| {desc= ((i1)(s1) 1); term= -1} |}]
|
|
|
|
|
|
|
|
|
|
let%expect_test _ =
|
|
|
|
|
pp (unsigned 1 !(-1) ~to_:Typ.byt) ;
|
|
|
|
|
[%expect {| {desc= ((i8)(u1) -1); term= 1} |}]
|
|
|
|
|
|
|
|
|
|
let%expect_test _ =
|
|
|
|
|
pp (signed 8 !(-1) ~to_:Typ.int) ;
|
|
|
|
|
[%expect {| {desc= ((i32)(s8) -1); term= -1} |}]
|
|
|
|
|
|
|
|
|
|
let%expect_test _ =
|
|
|
|
|
pp (unsigned 8 !(-1) ~to_:Typ.int) ;
|
|
|
|
|
[%expect {| {desc= ((i32)(u8) -1); term= 255} |}]
|
|
|
|
|
|
|
|
|
|
let%expect_test _ =
|
|
|
|
|
pp (signed 8 !255 ~to_:Typ.byt) ;
|
|
|
|
|
[%expect {| {desc= ((i8)(s8) 255); term= -1} |}]
|
|
|
|
|
|
|
|
|
|
let%expect_test _ =
|
|
|
|
|
pp (signed 7 !255 ~to_:Typ.byt) ;
|
|
|
|
|
[%expect {| {desc= ((i8)(s7) 255); term= -1} |}]
|
|
|
|
|
|
|
|
|
|
let%expect_test _ =
|
|
|
|
|
pp (unsigned 7 !255 ~to_:Typ.byt) ;
|
|
|
|
|
[%expect {| {desc= ((i8)(u7) 255); term= 127} |}]
|
|
|
|
|
|
|
|
|
|
let%expect_test _ =
|
|
|
|
|
pp (uge (integer Typ.bool Z.minus_one) (signed 1 !1 ~to_:Typ.bool)) ;
|
|
|
|
|
[%expect {| {desc= (-1 u≥ ((i1)(s1) 1)); term= -1} |}]
|
|
|
|
|
end )
|
