pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'f41575411c'
${ noResults }
infer_clone/sledge/src/exp_test.ml

51 lines
1.5 KiB
Raw Normal View History Unescape

[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
[sledge] Rearrange into CLI binary and LLVM-independent library Summary: Move files, adjust build system, etc. This also separates out the ppx_trace conditional compilation debug tracing machinery into an independent package and library. Reviewed By: jvillard Differential Revision: D20322876 fbshipit-source-id: a50522462
5 years ago
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
[sledge] Improve tracing in unit tests Summary: It is more convenient, and harder to misunderstand, if the verbose tracing setting comes commented-out after the default non-verbose setting. Reviewed By: jvillard Differential Revision: D20583755 fbshipit-source-id: 06ecb0e9a
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 )