[sledge] Revise and fix unsigned conversions

Summary:
Be more explicit about semantics of unsigned vs. signed conversions,
and fix a few related corner cases.

Reviewed By: bennostein

Differential Revision: D17665268

fbshipit-source-id: 67fecdf34

sledge/src/llair/exp.ml

@@ -11,7 +11,7 @@ module T = struct
   module T0 = struct
     type op1 =
       (* conversion *)
-      | Convert of {dst: Typ.t; signed: bool}
+      | Convert of {unsigned: bool; dst: Typ.t}
       (* array/struct operations *)
       | Select of int
     [@@deriving compare, equal, hash, sexp]
@@ -140,10 +140,12 @@ 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; signed}, src, arg) ->
-        pf "((%a)(%s%a)@ %a)" Typ.pp dst
-          (if signed then "u" else "")
-          Typ.pp src pp arg
+    | Ap1 (Convert {dst; unsigned= true}, Integer {bits}, 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) ->
+        pf "((%a)(%a)@ %a)" Typ.pp dst Typ.pp src pp arg
     | Ap1 (Select idx, _, rcd) -> pf "%a[%i]" pp rcd idx
     | Ap2 (Update idx, _, rcd, elt) ->
         pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
@@ -375,9 +377,9 @@ let null = integer Typ.ptr Z.zero
 let bool b = integer Typ.bool (Z.of_bool b)
 let float typ data = Float {data; typ} |> check invariant
 
-let convert ~dst ?(signed = false) ~src exp =
-  ( if Typ.castable dst src then exp
-  else Ap1 (Convert {dst; signed}, src, exp) )
+let convert ?(unsigned = false) ~dst ~src exp =
+  ( if (not unsigned) && Typ.equal dst src then exp
+  else Ap1 (Convert {unsigned; dst}, src, exp) )
   |> check invariant
 
 let select typ rcd idx = Ap1 (Select idx, typ, rcd) |> check invariant

sledge/src/llair/exp.mli

@@ -11,8 +11,14 @@
     bitwise-logical, etc. operations over literal values and registers. *)
 
 type op1 =
-  | Convert of {dst: Typ.t; signed: bool}
-      (** Convert between specified types, possibly with loss of information *)
+  | 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. *)
   | Select of int  (** Select an index from a record *)
 [@@deriving compare, equal, hash, sexp]
 
@@ -164,7 +170,7 @@ val struct_rec :
     one point on each cycle. Failure to obey these requirements will lead to
     stack overflow. *)
 
-val convert : dst:Typ.t -> ?signed:bool -> src:Typ.t -> t -> t
+val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t
 
 (** Access *)
 

sledge/src/llair/frontend.ml

@@ -450,12 +450,12 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
         todo "vector operations: %a" pp_llvalue llv () )
   in
   let cast () = xlate_rand 0 in
-  let convert signed =
+  let convert ?unsigned () =
     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 ~dst ~signed ~src arg
+    Exp.convert ?unsigned ~dst ~src arg
   in
   let binary mk =
     Lazy.force check_vector ;
@@ -467,10 +467,9 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
   in
   ( match opcode with
   | AddrSpaceCast | BitCast -> cast ()
-  | Trunc | ZExt | FPToUI | UIToFP | FPTrunc | FPExt | PtrToInt | IntToPtr
-    ->
-      convert false
-  | SExt | FPToSI | SIToFP -> convert true
+  | Trunc | ZExt | FPToUI | UIToFP | PtrToInt | IntToPtr ->
+      convert ~unsigned:true ()
+  | SExt | FPTrunc | FPExt | FPToSI | SIToFP -> convert ()
   | ICmp -> (
     match Option.value_exn (Llvm.icmp_predicate llv) with
     | Eq -> binary Exp.eq
@@ -891,8 +890,8 @@ let xlate_instr :
             let num_operand = Llvm.operand instr 0 in
             let num =
               Exp.convert ~dst:Typ.siz
-                (xlate_value x num_operand)
                 ~src:(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
             emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)

sledge/src/llair/typ.ml

@@ -121,13 +121,14 @@ let rec prim_bit_size_of = function
       Option.map (prim_bit_size_of elt) ~f:(fun n -> n * len)
   | Function _ | Tuple _ | Struct _ | Opaque _ -> None
 
-let castable t0 t1 =
+let rec castable t0 t1 =
   match (t0, t1) with
-  | Pointer _, Pointer _ -> true
-  | _ -> (
+  | (Pointer _ | Integer _), (Pointer _ | Integer _) -> (
     match (prim_bit_size_of t0, prim_bit_size_of t1) with
     | Some n0, Some n1 -> n0 = n1
     | _ -> false )
+  | Array {elt= t; len= m}, Array {elt= u; len= n} -> m = n && castable t u
+  | _ -> equal t0 t1
 
 let rec convertible t0 t1 =
   castable t0 t1

sledge/src/symbheap/equality_test.ml

@@ -321,14 +321,17 @@ let%test_module _ =
     let%test _ = entails_eq r14 a (Term.bool true)
     let%test _ = entails_eq r14 b (Term.bool true)
 
-    let b = Term.convert ~dst:i64 ~src:i8 (Term.dq x !0)
+    let b = Term.dq x !0
     let r15 = of_eqs [(b, b); (x, !1)]
 
     let%expect_test _ =
-      pp r15 ;
-      [%expect
-        {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [((i64)(i8) (%x_5 ≠ 0)) ↦ ]]} |}]
+      pp r15 ; [%expect {|
+          {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
-    let%test _ = entails_eq r15 b !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
   end )

sledge/src/symbheap/term.ml

@@ -79,7 +79,7 @@ module rec T : sig
     | Update
     | Struct_rec of {elts: t vector}  (** NOTE: may be cyclic *)
     (* unary: conversion *)
-    | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
+    | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
     (* numeric constants *)
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
@@ -137,7 +137,7 @@ and T0 : sig
     | Select
     | Update
     | Struct_rec of {elts: t vector}
-    | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
+    | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
   [@@deriving compare, equal, hash, sexp]
@@ -181,7 +181,7 @@ end = struct
     | Select
     | Update
     | Struct_rec of {elts: t vector}
-    | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
+    | Convert of {unsigned: bool; dst: Typ.t; src: Typ.t}
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
   [@@deriving compare, equal, hash, sexp]
@@ -309,6 +309,10 @@ let rec pp ?is_x fs term =
       | op, [x; y] -> pf "(%a@ %a %a)" pp x pp op pp y
       | _ -> pf "(%a@ %a)" pp op pp arg )
     | Struct_rec {elts} -> pf "{|%a|}" (Vector.pp ",@ " pp) elts
+    | Convert {unsigned= true; dst; src= Integer {bits}} ->
+        pf "(%a)(u%i)" Typ.pp dst bits
+    | Convert {unsigned= true; dst= Integer {bits}; src} ->
+        pf "(u%i)(%a)" bits Typ.pp src
     | Convert {dst; src} -> pf "(%a)(%a)" Typ.pp dst Typ.pp src
   in
   fix_flip pp_ (fun _ _ -> ()) fs term
@@ -629,12 +633,13 @@ let one (typ : Typ.t) =
 let minus_one (typ : Typ.t) =
   match typ with Float _ -> float "-1" | _ -> integer Z.minus_one typ
 
-let simp_convert signed (dst : Typ.t) src arg =
-  match (dst, arg) with
-  | _ when Typ.castable dst src -> arg
-  | Integer {bits= m}, Integer {data; typ= Integer {bits= n}} ->
-      integer (Z.clamp ~signed (min m n) data) dst
-  | _ -> App {op= Convert {signed; dst; src}; arg}
+let simp_convert ~unsigned dst src arg =
+  if (not unsigned) && Typ.castable dst src then arg
+  else
+    match (dst, src, arg) with
+    | Integer {bits= m}, Integer {bits= n}, Integer {data} ->
+        integer (Z.clamp ~signed:(not unsigned) (min m n) data) dst
+    | _ -> App {op= Convert {unsigned; dst; src}; arg}
 
 let simp_gt x y =
   match (x, y) with
@@ -1064,7 +1069,7 @@ let app1 ?(partial = false) op arg =
   | App {op= Lshr; arg= x}, y -> simp_lshr x y
   | App {op= Ashr; arg= x}, y -> simp_ashr x y
   | App {op= App {op= Conditional; arg= x}; arg= y}, z -> simp_cond x y z
-  | Convert {signed; dst; src}, x -> simp_convert signed dst src x
+  | Convert {unsigned; dst; src}, x -> simp_convert ~unsigned dst src x
   | _ -> App {op; arg} )
   |> check (invariant ~partial)
   |> check (fun e ->
@@ -1187,8 +1192,8 @@ let struct_rec key =
          forcing the recursive thunks also updates this value. *)
       Struct_rec {elts}
 
-let convert ?(signed = false) ~dst ~src term =
-  app1 (Convert {signed; dst; src}) term
+let convert ?(unsigned = false) ~dst ~src term =
+  app1 (Convert {unsigned; dst; src}) term
 
 let rec of_exp (e : Exp.t) =
   match e with
@@ -1199,8 +1204,8 @@ let rec of_exp (e : Exp.t) =
       integer (Z.signed_extract data 0 bits) typ
   | Integer {data; typ} -> integer data typ
   | Float {data} -> float data
-  | Ap1 (Convert {dst; signed}, src, arg) ->
-      convert ~signed ~dst ~src (of_exp arg)
+  | Ap1 (Convert {unsigned; dst}, src, arg) ->
+      convert ~unsigned ~dst ~src (of_exp arg)
   | Ap1 (Select idx, _, arg) ->
       select ~rcd:(of_exp arg) ~idx:(integer (Z.of_int idx) Typ.siz)
   | Ap2 (Eq, _, x, y) -> eq (of_exp x) (of_exp y)

sledge/src/symbheap/term.mli

@@ -64,8 +64,13 @@ and t = private
   | Struct_rec of {elts: t vector}
       (** Struct constant that may recursively refer to itself
           (transitively) from [elts]. NOTE: represented by cyclic values. *)
-  | Convert of {signed: bool; dst: Typ.t; src: Typ.t}
-      (** Convert between specified types, possibly with loss of information *)
+  | 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. *)
   | Integer of {data: Z.t; typ: Typ.t}
       (** Integer constant, or if [typ] is a [Pointer], null pointer value
           that never refers to an object *)
@@ -169,7 +174,7 @@ val conditional : cnd:t -> thn:t -> els:t -> t
 val record : t list -> t
 val select : rcd:t -> idx:t -> t
 val update : rcd:t -> elt:t -> idx:t -> t
-val convert : ?signed:bool -> dst:Typ.t -> src:Typ.t -> t -> t
+val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t
 val size_of : Typ.t -> t option
 
 (** Access *)