From 1f64634093a4e6e20eb5d9463dbda459a8a08cfd Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 12 Nov 2019 16:33:22 -0800 Subject: [PATCH] [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 --- sledge/src/domain/itv.ml | 5 +- sledge/src/llair/exp.ml | 51 ++++++++++------ sledge/src/llair/exp.mli | 31 +++++++--- sledge/src/llair/exp_test.ml | 49 +++++++++++++++ sledge/src/llair/exp_test.mli | 6 ++ sledge/src/llair/frontend.ml | 48 ++++++++++----- sledge/src/llair/term.ml | 89 +++++++++++----------------- sledge/src/llair/term.mli | 27 +++++---- sledge/src/llair/term_test.ml | 45 ++------------ sledge/src/symbheap/equality_test.ml | 17 ++---- 10 files changed, 209 insertions(+), 159 deletions(-) create mode 100644 sledge/src/llair/exp_test.ml create mode 100644 sledge/src/llair/exp_test.mli diff --git a/sledge/src/domain/itv.ml b/sledge/src/domain/itv.ml index 70cb93ef0..43e3a4da5 100644 --- a/sledge/src/domain/itv.ml +++ b/sledge/src/domain/itv.ml @@ -106,7 +106,7 @@ and apron_texpr_of_llair_term tm q typ = try Float.of_string data with _ -> failwith "malformed float: %s" in Some (Texpr1.Cst (Coeff.s_of_float f)) - | Ap1 (Convert {unsigned= false; dst; src}, t) -> ( + | Ap1 (Convert {dst; src}, t) -> ( match (apron_typ_of_llair_typ dst, apron_typ_of_llair_typ src) with | None, _ | _, None -> None | Some dst, Some src -> @@ -117,8 +117,7 @@ and apron_texpr_of_llair_term tm q typ = Some (Texpr1.Unop (Texpr1.Cast, t, dst, Texpr0.Rnd)) ) (* extraction to unsigned 1-bit int is llvm encoding of C boolean; restrict to [0,1] *) - | Ap1 (Extract {unsigned= true; bits= 1}, _t) -> - Some (Texpr1.Cst (Coeff.i_of_int 0 1)) + | Ap1 (Unsigned {bits= 1}, _t) -> Some (Texpr1.Cst (Coeff.i_of_int 0 1)) (* "t xor true" and "true xor t" are negation *) | Ap2 (Xor, t, Integer {data}) when Z.is_true data -> let%map t = apron_texpr_of_llair_term t q typ in diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 5a31effdd..eff512c30 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -13,7 +13,9 @@ module T = struct module T0 = struct type op1 = (* conversion *) - | Convert of {unsigned: bool; dst: Typ.t} + | Signed of {bits: int} + | Unsigned of {bits: int} + | Convert of {src: Typ.t} (* array/struct operations *) | Select of int [@@deriving compare, equal, hash, sexp] @@ -150,11 +152,11 @@ let rec pp fs exp = | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null" | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data | Float {data} -> pf "%s" data - | Ap1 (Convert {dst; unsigned= true}, Integer {bits}, arg) -> + | Ap1 (Signed {bits}, dst, arg) -> + pf "((%a)(s%i)@ %a)" Typ.pp dst bits pp arg + | Ap1 (Unsigned {bits}, dst, arg) -> pf "((%a)(u%i)@ %a)" Typ.pp dst bits pp arg - | Ap1 (Convert {dst= Integer {bits}; unsigned= true}, src, arg) -> - pf "((u%i)(%a)@ %a)" bits Typ.pp src pp arg - | Ap1 (Convert {dst}, src, arg) -> + | Ap1 (Convert {src}, dst, arg) -> pf "((%a)(%a)@ %a)" Typ.pp dst Typ.pp src pp arg | Ap1 (Select idx, _, rcd) -> pf "%a[%i]" pp rcd idx | Ap2 (Splat, _, byt, siz) -> pf "%a^%a" pp byt pp siz @@ -211,10 +213,19 @@ let rec invariant exp = | Float {typ} -> ( match typ with Float _ -> assert true | _ -> assert false ) | Label _ -> assert true - | Ap1 (Convert {dst}, src, arg) -> - assert (not (Typ.equal dst src)) ; - assert (Typ.convertible dst src) ; - assert (Typ.castable src (typ_of arg)) + | Ap1 (Signed {bits}, dst, arg) -> ( + match (dst, typ_of arg) with + | Integer {bits= dst_bits}, Typ.Integer _ -> assert (bits <= dst_bits) + | _ -> assert false ) + | Ap1 (Unsigned {bits}, dst, arg) -> ( + match (dst, typ_of arg) with + | Integer {bits= dst_bits}, Typ.Integer _ -> assert (bits < dst_bits) + | _ -> assert false ) + | Ap1 (Convert {src= Integer _}, Integer _, _) -> assert false + | Ap1 (Convert {src}, dst, arg) -> + assert (Typ.convertible src dst) ; + assert (Typ.castable src (typ_of arg)) ; + assert (not (Typ.equal src dst) (* avoid redundant representations *)) | Ap1 (Select idx, typ, rcd) -> ( assert (Typ.castable typ (typ_of rcd)) ; match typ with @@ -273,7 +284,7 @@ and typ_of exp = match exp.desc with | Reg {typ} | Nondet {typ} | Integer {typ} | Float {typ} -> typ | Label _ -> Typ.ptr - | Ap1 (Convert {dst}, _, _) -> dst + | Ap1 ((Signed _ | Unsigned _ | Convert _), dst, _) -> dst | Ap1 (Select idx, typ, _) -> ( match typ with | Array {elt} -> elt @@ -411,11 +422,17 @@ let float typ data = (* type conversions *) -let convert ?(unsigned = false) ~dst ~src exp = - ( if (not unsigned) && Typ.equal dst src then exp - else - { desc= Ap1 (Convert {unsigned; dst}, src, exp) - ; term= Term.convert ~unsigned ~dst ~src exp.term } ) +let signed bits x ~to_:typ = + {desc= Ap1 (Signed {bits}, typ, x); term= Term.signed bits x.term} + |> check invariant + +let unsigned bits x ~to_:typ = + {desc= Ap1 (Unsigned {bits}, typ, x); term= Term.unsigned bits x.term} + |> check invariant + +let convert src ~to_:dst exp = + { desc= Ap1 (Convert {src}, dst, exp) + ; term= Term.convert src ~to_:dst exp.term } |> check invariant (* comparisons *) @@ -427,8 +444,8 @@ let binary op mk ?typ x y = let ubinary op mk ?typ x y = let typ = match typ with Some typ -> typ | None -> typ_of x in let umk x y = - let extract = Term.extract ~unsigned:true ~bits:(Typ.bit_size_of typ) in - mk (extract x) (extract y) + let unsigned = Term.unsigned (Typ.bit_size_of typ) in + mk (unsigned x) (unsigned y) in binary op umk ~typ x y diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index 160f26108..c6a05a34a 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -11,14 +11,25 @@ bitwise-logical, etc. operations over literal values and registers. *) type op1 = - | Convert of {unsigned: bool; dst: Typ.t} - (** Convert between specified types, possibly with loss of - information. In [Ap1 (Convert {unsigned; dst}, src, arg)], if - [src] is an [Integer] type, then [unsigned] indicates that [arg] - should be interpreted as an [unsigned] integer. If [src] is a - [Float] type and [dst] is an [Integer] type, then [unsigned] - indidates that the result should be the nearest non-negative - value. *) + | 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. *) | Select of int (** Select an index from a record *) [@@deriving compare, equal, hash, sexp] @@ -140,7 +151,9 @@ val integer : Typ.t -> Z.t -> t val float : Typ.t -> string -> t (* type conversions *) -val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t +val signed : int -> t -> to_:Typ.t -> t +val unsigned : int -> t -> to_:Typ.t -> t +val convert : Typ.t -> to_:Typ.t -> t -> t (* comparisons *) val eq : ?typ:Typ.t -> t -> t -> t diff --git a/sledge/src/llair/exp_test.ml b/sledge/src/llair/exp_test.ml new file mode 100644 index 000000000..07bb74028 --- /dev/null +++ b/sledge/src/llair/exp_test.ml @@ -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 ) diff --git a/sledge/src/llair/exp_test.mli b/sledge/src/llair/exp_test.mli new file mode 100644 index 000000000..81857a06f --- /dev/null +++ b/sledge/src/llair/exp_test.mli @@ -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. + *) diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index f967f9dd9..b3438d453 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -22,7 +22,7 @@ type llvaluekind = [%import: (Llvm.ValueKind.t[@with Opcode.t := llopcode])] [@@deriving sexp] let _pp_lllinkage fs l = Sexp.pp_hum fs (sexp_of_lllinkage l) -let _pp_llopcode fs l = Sexp.pp_hum fs (sexp_of_llopcode l) +let pp_llopcode fs l = Sexp.pp_hum fs (sexp_of_llopcode l) let pp_llvaluekind fs l = Sexp.pp_hum fs (sexp_of_llvaluekind l) exception Invalid_llvm of string @@ -356,8 +356,18 @@ let ptr_idx x ~ptr ~idx ~llelt = Exp.add ~typ:Typ.ptr ptr (Exp.mul ~typ:Typ.siz (Exp.integer Typ.siz (Z.of_int64 stride)) idx) +let convert_to_siz = + let siz_bits = Typ.bit_size_of Typ.siz in + fun typ arg -> + match (typ : Typ.t) with + | Integer {bits} -> + if siz_bits < bits then Exp.signed siz_bits arg ~to_:Typ.siz + else if siz_bits > bits then Exp.signed bits arg ~to_:Typ.siz + else arg + | _ -> fail "convert_to_siz: %a" Typ.pp typ () + let xlate_llvm_eh_typeid_for : x -> Typ.t -> Exp.t -> Exp.t = - fun x typ arg -> Exp.convert ~dst:(i32 x) ~src:typ arg + fun x typ arg -> Exp.convert typ ~to_:(i32 x) arg let rec xlate_intrinsic_exp : string -> (x -> Llvm.llvalue -> Exp.t) option = @@ -479,12 +489,20 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = ( if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then todo "vector operations: %a" pp_llvalue llv () ) in - let convert ?unsigned () = + let convert opcode = let dst = Lazy.force typ in let rand = Llvm.operand llv 0 in let src = xlate_type x (Llvm.type_of rand) in let arg = xlate_value x rand in - Exp.convert ?unsigned ~dst ~src arg + match opcode with + | Trunc -> Exp.signed (Typ.bit_size_of dst) arg ~to_:dst + | SExt -> Exp.signed (Typ.bit_size_of src) arg ~to_:dst + | ZExt -> Exp.unsigned (Typ.bit_size_of src) arg ~to_:dst + | (BitCast | AddrSpaceCast) when Typ.equal dst src -> arg + | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc | FPExt | PtrToInt + |IntToPtr | BitCast | AddrSpaceCast -> + Exp.convert src ~to_:dst arg + | _ -> fail "convert: %a" pp_llopcode opcode () in let binary (mk : ?typ:_ -> _) = Lazy.force check_vector ; @@ -496,10 +514,9 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = Exp.or_ ~typ:Typ.bool (Exp.uno ?typ e f) (mk ?typ e f) ) in ( match opcode with - | AddrSpaceCast | BitCast -> convert () - | Trunc | ZExt | FPToUI | UIToFP | PtrToInt | IntToPtr -> - convert ~unsigned:true () - | SExt | FPTrunc | FPExt | FPToSI | SIToFP -> convert () + | Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc + |FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast -> + convert opcode | ICmp -> ( match Option.value_exn (Llvm.icmp_predicate llv) with | Eq -> binary Exp.eq @@ -602,15 +619,16 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then todo "vector operations: %a" pp_llvalue llv () ; let len = Llvm.num_operands llv in - if len <= 1 then convert () + assert (len > 0 || invalid_llvm (Llvm.string_of_llvalue llv)) ; + if len = 1 then convert BitCast else let rec xlate_indices i = [%Trace.call fun {pf} -> pf "%i %a" i pp_llvalue (Llvm.operand llv i)] ; let idx = - Exp.convert ~dst:Typ.siz - ~src:(xlate_type x (Llvm.type_of (Llvm.operand llv i))) + convert_to_siz + (xlate_type x (Llvm.type_of (Llvm.operand llv i))) (xlate_rand i) in ( if i = 1 then @@ -891,8 +909,8 @@ let xlate_instr : let reg = xlate_name x instr in let rand = Llvm.operand instr 0 in let num = - Exp.convert ~dst:Typ.siz - ~src:(xlate_type x (Llvm.type_of rand)) + convert_to_siz + (xlate_type x (Llvm.type_of rand)) (xlate_value x rand) in assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ; @@ -936,8 +954,8 @@ let xlate_instr : let reg = xlate_name x instr in let num_operand = Llvm.operand instr 0 in let num = - Exp.convert ~dst:Typ.siz - ~src:(xlate_type x (Llvm.type_of num_operand)) + convert_to_siz + (xlate_type x (Llvm.type_of num_operand)) (xlate_value x num_operand) in let len = Exp.integer Typ.siz (Z.of_int 1) in diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index 92937b699..e9e4db10c 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -9,20 +9,13 @@ [@@@warning "+9"] -module Z = struct - include Z - - (** Interpret as a bounded integer with specified signedness and width. *) - let extract ?(unsigned = false) bits z = - if unsigned then Z.extract z 0 bits else Z.signed_extract z 0 bits -end - module rec T : sig type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] type op1 = - | Extract of {unsigned: bool; bits: int} - | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t} + | Signed of {bits: int} + | Unsigned of {bits: int} + | Convert of {src: Typ.t; dst: Typ.t} | Select of int [@@deriving compare, equal, hash, sexp] @@ -81,8 +74,9 @@ and T0 : sig type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] type op1 = - | Extract of {unsigned: bool; bits: int} - | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t} + | Signed of {bits: int} + | Unsigned of {bits: int} + | Convert of {src: Typ.t; dst: Typ.t} | Select of int [@@deriving compare, equal, hash, sexp] @@ -128,8 +122,9 @@ end = struct type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] type op1 = - | Extract of {unsigned: bool; bits: int} - | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t} + | Signed of {bits: int} + | Unsigned of {bits: int} + | Convert of {src: Typ.t; dst: Typ.t} | Select of int [@@deriving compare, equal, hash, sexp] @@ -219,13 +214,9 @@ let rec pp ?is_x fs term = | Float {data} -> pf "%s" data | Nondet {msg} -> pf "nondet \"%s\"" msg | Label {name} -> pf "%s" name - | Ap1 (Extract {unsigned; bits}, arg) -> - pf "(%s%i)@ %a" (if unsigned then "u" else "i") bits pp arg - | Ap1 (Convert {dst; unsigned= true; src= Integer {bits}}, arg) -> - pf "((%a)(u%i)@ %a)" Typ.pp dst bits pp arg - | Ap1 (Convert {unsigned= true; dst= Integer {bits}; src}, arg) -> - pf "((u%i)(%a)@ %a)" bits Typ.pp src pp arg - | Ap1 (Convert {dst; src}, arg) -> + | Ap1 (Signed {bits}, arg) -> pf "((s%i)@ %a)" bits pp arg + | Ap1 (Unsigned {bits}, arg) -> pf "((u%i)@ %a)" bits pp arg + | Ap1 (Convert {src; dst}, arg) -> pf "((%a)(%a)@ %a)" Typ.pp dst Typ.pp src pp arg | Ap2 (Eq, x, y) -> pf "(%a@ = %a)" pp x pp y | Ap2 (Dq, x, y) -> pf "(%a@ @<2>≠ %a)" pp x pp y @@ -352,9 +343,12 @@ let invariant e = | ApN (Concat, mems) -> assert (Vector.length mems <> 1) | ApN (Record, elts) | RecN (Record, elts) -> assert (not (Vector.is_empty elts)) - | Ap1 (Convert {dst; src}, _) -> - assert (not (Typ.equivalent dst src)) ; - assert (Typ.convertible dst src) + | Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false + | Ap1 (Convert {src; dst}, _) -> + assert (Typ.convertible src dst) ; + assert ( + not (Typ.equivalent src dst) (* avoid redundant representations *) + ) | _ -> () [@@warning "-9"] @@ -500,27 +494,18 @@ let label ~parent ~name = Label {parent; name} |> check invariant (* type conversions *) -let simp_extract ~unsigned bits arg = +let simp_signed bits arg = match arg with - | Integer {data} -> integer (Z.extract ~unsigned bits data) - | _ -> Ap1 (Extract {unsigned; bits}, arg) - -let simp_convert ~unsigned dst src arg = - match (dst, src) with - | Typ.Integer {bits= m; _}, Typ.Integer {bits= n; _} -> ( - if m < n then - match arg with - | Integer {data} -> integer (Z.extract m data) - | _ -> Ap1 (Convert {unsigned= false; dst; src}, arg) - else - match arg with - | Integer {data} -> integer (Z.extract ~unsigned n data) - | _ -> - if unsigned then Ap1 (Convert {unsigned; dst; src}, arg) - else arg ) - | _ -> - if Typ.equivalent dst src then arg - else Ap1 (Convert {unsigned; dst; src}, arg) + | Integer {data} -> integer (Z.signed_extract data 0 bits) + | _ -> Ap1 (Signed {bits}, arg) + +let simp_unsigned bits arg = + match arg with + | Integer {data} -> integer (Z.extract data 0 bits) + | _ -> Ap1 (Unsigned {bits}, arg) + +let simp_convert src dst arg = + if Typ.equivalent src dst then arg else Ap1 (Convert {src; dst}, arg) (* arithmetic *) @@ -685,7 +670,7 @@ let simp_cond cnd thn els = (* boolean / bitwise *) let rec is_boolean = function - | Ap1 ((Extract {bits= 1; _} | Convert {dst= Integer {bits= 1; _}; _}), _) + | Ap1 ((Unsigned {bits= 1} | Convert {dst= Integer {bits= 1; _}; _}), _) |Ap2 ((Eq | Dq | Lt | Le), _, _) -> true | Ap2 ((Div | Rem | And | Or | Xor | Shl | Lshr | Ashr), x, y) @@ -898,8 +883,9 @@ let rec_app key = let norm1 op x = ( match op with - | Extract {unsigned; bits} -> simp_extract ~unsigned bits x - | Convert {unsigned; dst; src} -> simp_convert ~unsigned dst src x + | Signed {bits} -> simp_signed bits x + | Unsigned {bits} -> simp_unsigned bits x + | Convert {src; dst} -> simp_convert src dst x | Select idx -> simp_select idx x ) |> check invariant @@ -933,12 +919,9 @@ let normN op xs = (* exposed interface *) -let extract ?(unsigned = false) ~bits term = - norm1 (Extract {unsigned; bits}) term - -let convert ?(unsigned = false) ~dst ~src term = - norm1 (Convert {unsigned; dst; src}) term - +let signed bits term = norm1 (Signed {bits}) term +let unsigned bits term = norm1 (Unsigned {bits}) term +let convert src ~to_:dst term = norm1 (Convert {src; dst}) term let eq = norm2 Eq let dq = norm2 Dq let lt = norm2 Lt diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli index 4e6b82fce..ab3804b3f 100644 --- a/sledge/src/llair/term.mli +++ b/sledge/src/llair/term.mli @@ -13,15 +13,19 @@ type comparator_witness type op1 = - | Extract of {unsigned: bool; bits: int} - (** Interpret integer argument with given signedness and bitwidth. *) - | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t} - (** Convert between specified types, possibly with loss of - information. If [src] is an [Integer] type, then [unsigned] - indicates that the argument should be interpreted as an [unsigned] - integer. If [src] is a [Float] type and [dst] is an [Integer] - type, then [unsigned] indidates that the result should be the - nearest non-negative value. *) + | Signed of {bits: int} + (** [Ap1 (Signed {bits= n}, arg)] is [arg] interpreted as an [n]-bit + signed integer. That is, it two's-complement--decodes the low [n] + bits of the infinite two's-complement encoding of [arg]. *) + | Unsigned of {bits: int} + (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an [n]-bit + unsigned integer. That is, it unsigned-binary--decodes the low [n] + bits of the infinite two's-complement encoding of [arg]. *) + | Convert of {src: Typ.t; dst: 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. *) | Select of int (** Select an index from a record *) [@@deriving compare, equal, hash, sexp] @@ -151,8 +155,9 @@ val rational : Q.t -> t val float : string -> t (* type conversions *) -val extract : ?unsigned:bool -> bits:int -> t -> t -val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t +val signed : int -> t -> t +val unsigned : int -> t -> t +val convert : Typ.t -> to_:Typ.t -> t -> t (* comparisons *) val eq : t -> t -> t diff --git a/sledge/src/llair/term_test.ml b/sledge/src/llair/term_test.ml index b2ed97866..6fde19254 100644 --- a/sledge/src/llair/term_test.ml +++ b/sledge/src/llair/term_test.ml @@ -30,51 +30,16 @@ let%test_module _ = let y = var y_ let z = var z_ - let%test "booleans distinct" = is_false (eq minus_one zero) - let%test "unsigned booleans distinct" = is_false (eq one zero) - - let%test "boolean overflow" = - is_true - (Exp.eq - (Exp.integer Typ.bool Z.minus_one) - (Exp.convert ~dst:Typ.bool ~src:Typ.siz - (Exp.integer Typ.siz Z.one))) - .term - - let%expect_test _ = - pp - (Exp.convert ~dst:Typ.byt ~unsigned:true ~src:Typ.int - (Exp.integer Typ.int (Z.of_int 255))) - .term ; - [%expect {| -1 |}] - - let%expect_test _ = - pp - (Exp.convert ~dst:Typ.byt ~unsigned:false ~src:Typ.int - (Exp.integer Typ.int (Z.of_int 255))) - .term ; - [%expect {| -1 |}] - - let%expect_test _ = - pp - (Exp.convert ~dst:Typ.int ~unsigned:true ~src:Typ.byt - (Exp.integer Typ.byt (Z.of_int (-1)))) - .term ; - [%expect {| 255 |}] - - let%expect_test _ = - pp - (Exp.convert ~dst:Typ.int ~unsigned:false ~src:Typ.byt - (Exp.integer Typ.byt (Z.of_int (-1)))) - .term ; - [%expect {| -1 |}] + let%test "booleans distinct" = is_false (true_ = false_) + let%test "u1 values distinct" = is_false (one = zero) + let%test "boolean overflow" = is_true (minus_one = signed 1 one) + let%test _ = is_true (one = unsigned 1 minus_one) let%test "unsigned boolean overflow" = is_true (Exp.uge (Exp.integer Typ.bool Z.minus_one) - (Exp.convert ~dst:Typ.bool ~src:Typ.siz - (Exp.integer Typ.siz Z.one))) + (Exp.signed 1 (Exp.integer Typ.siz Z.one) ~to_:Typ.bool)) .term let%expect_test _ = diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml index 1a9e9480d..7bfe28327 100644 --- a/sledge/src/symbheap/equality_test.ml +++ b/sledge/src/symbheap/equality_test.ml @@ -16,13 +16,11 @@ let%test_module _ = let pp = printf pp let pp_classes = printf pp_classes let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r) - let i8 = Typ.int - let i64 = Typ.siz let ( ! ) i = Term.integer (Z.of_int i) let ( + ) = Term.add let ( - ) = Term.sub let ( * ) = Term.mul - let f = Term.convert ~dst:i64 ~src:i8 + let f = Term.unsigned 8 let g = Term.rem let wrt = Var.Set.empty let t_, wrt = Var.fresh "t" ~wrt @@ -99,9 +97,10 @@ let%test_module _ = pp r2 ; [%expect {| - %x_5 = %y_6 = %z_7 + %x_5 = %y_6 = %z_7 = ((u8) %x_5) - {sat= true; rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]} |}] + {sat= true; + rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [((u8) %x_5) ↦ %x_5]]} |}] let%test _ = entails_eq r2 x z let%test _ = entails_eq (or_ r1 r2) x y @@ -326,10 +325,6 @@ let%test_module _ = pp r15 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}] - let%test _ = entails_eq r15 b (Term.convert ~dst:Typ.bool ~src:i64 !1) - - let%test _ = - entails_eq r15 - (Term.convert ~dst:i64 ~unsigned:true ~src:Typ.bool b) - !1 + let%test _ = entails_eq r15 b (Term.signed 1 !1) + let%test _ = entails_eq r15 (Term.unsigned 1 b) !1 end )