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
master
Josh Berdine
5 years ago
committed by
Facebook Github Bot
parent
e6d93dcf94
commit
1f64634093
@ -0,0 +1,49 @@
|
|||||||
|
(*
|
||||||
|
* 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 ~config:all () *)
|
||||||
|
let () = Trace.init ~margin:68 ~config:none ()
|
||||||
|
|
||||||
|
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 )
|
||||||
@ -0,0 +1,6 @@
|
|||||||
|
(*
|
||||||
|
* 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.
|
||||||
|
*)
|
||||||
Loading…
Reference in new issue