[sledge] Make type argument of Exp constructors optional where computable

Reviewed By: bennostein

Differential Revision: D17665251

fbshipit-source-id: 4d8bccfe8

sledge/src/control.ml

@@ -406,15 +406,14 @@ module Make (Dom : Domain_sig.Dom) = struct
     | Switch {key; tbl; els} ->
         Vector.fold tbl
           ~f:(fun x (case, jump) ->
-            match Dom.exec_assume state (Exp.eq (Exp.typ key) key case) with
+            match Dom.exec_assume state (Exp.eq key case) with
             | Some state -> exec_jump stk state block jump |> Work.seq x
             | None -> x )
           ~init:
             ( match
                 Dom.exec_assume state
                   (Vector.fold tbl ~init:Exp.true_ ~f:(fun b (case, _) ->
-                       Exp.and_ Typ.bool (Exp.dq (Exp.typ key) key case) b
-                   ))
+                       Exp.and_ (Exp.dq key case) b ))
               with
             | Some state -> exec_jump stk state block els
             | None -> Work.skip )
@@ -422,7 +421,7 @@ module Make (Dom : Domain_sig.Dom) = struct
         Vector.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) ->
             match
               Dom.exec_assume state
-                (Exp.eq Typ.ptr ptr
+                (Exp.eq ptr
                    (Exp.label
                       ~parent:(Reg.name jump.dst.parent.name.reg)
                       ~name:jump.dst.lbl))

sledge/src/llair/exp.ml

@@ -284,8 +284,6 @@ and typ_of exp =
       typ
   [@@warning "-9"]
 
-let typ = typ_of
-
 type exp = t
 
 let pp_exp = pp
@@ -406,121 +404,59 @@ let convert ?(unsigned = false) ~dst ~src exp =
 
 (* comparisons *)
 
-let unsigned typ op x y =
-  let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
-  op
-    (Term.extract ~unsigned:true ~bits x)
-    (Term.extract ~unsigned:true ~bits y)
-
-let eq typ x y =
-  {desc= Ap2 (Eq, typ, x, y); term= Term.eq x.term y.term}
-  |> check invariant
-
-let dq typ x y =
-  {desc= Ap2 (Dq, typ, x, y); term= Term.dq x.term y.term}
-  |> check invariant
-
-let gt typ x y =
-  {desc= Ap2 (Gt, typ, x, y); term= Term.lt y.term x.term}
-  |> check invariant
-
-let ge typ x y =
-  {desc= Ap2 (Ge, typ, x, y); term= Term.le y.term x.term}
-  |> check invariant
-
-let lt typ x y =
-  {desc= Ap2 (Lt, typ, x, y); term= Term.lt x.term y.term}
-  |> check invariant
-
-let le typ x y =
-  {desc= Ap2 (Le, typ, x, y); term= Term.le x.term y.term}
-  |> check invariant
-
-let ugt typ x y =
-  {desc= Ap2 (Ugt, typ, x, y); term= unsigned typ Term.lt y.term x.term}
-  |> check invariant
-
-let uge typ x y =
-  {desc= Ap2 (Uge, typ, x, y); term= unsigned typ Term.le y.term x.term}
-  |> check invariant
-
-let ult typ x y =
-  {desc= Ap2 (Ult, typ, x, y); term= unsigned typ Term.lt x.term y.term}
-  |> check invariant
-
-let ule typ x y =
-  {desc= Ap2 (Ule, typ, x, y); term= unsigned typ Term.le x.term y.term}
-  |> check invariant
-
-let ord typ x y =
-  {desc= Ap2 (Ord, typ, x, y); term= Term.ord x.term y.term}
-  |> check invariant
-
-let uno typ x y =
-  {desc= Ap2 (Uno, typ, x, y); term= Term.uno x.term y.term}
-  |> check invariant
+let binary op mk ?typ x y =
+  let typ = match typ with Some typ -> typ | None -> typ_of x in
+  {desc= Ap2 (op, typ, x, y); term= mk x.term y.term} |> check invariant
+
+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 bits = Option.value_exn (Typ.prim_bit_size_of typ) in
+    mk
+      (Term.extract ~unsigned:true ~bits x)
+      (Term.extract ~unsigned:true ~bits y)
+  in
+  binary op umk ~typ x y
+
+let eq = binary Eq Term.eq
+let dq = binary Dq Term.dq
+let gt = binary Gt (fun x y -> Term.lt y x)
+let ge = binary Ge (fun x y -> Term.le y x)
+let lt = binary Lt Term.lt
+let le = binary Le Term.le
+let ugt = ubinary Ugt (fun x y -> Term.lt y x)
+let uge = ubinary Uge (fun x y -> Term.le y x)
+let ult = ubinary Ult Term.lt
+let ule = ubinary Ule Term.le
+let ord = binary Ord Term.ord
+let uno = binary Uno Term.uno
 
 (* arithmetic *)
 
-let add typ x y =
-  {desc= Ap2 (Add, typ, x, y); term= Term.add x.term y.term}
-  |> check invariant
-
-let sub typ x y =
-  {desc= Ap2 (Sub, typ, x, y); term= Term.sub x.term y.term}
-  |> check invariant
-
-let mul typ x y =
-  {desc= Ap2 (Mul, typ, x, y); term= Term.mul x.term y.term}
-  |> check invariant
-
-let div typ x y =
-  {desc= Ap2 (Div, typ, x, y); term= Term.div x.term y.term}
-  |> check invariant
-
-let rem typ x y =
-  {desc= Ap2 (Rem, typ, x, y); term= Term.rem x.term y.term}
-  |> check invariant
-
-let udiv typ x y =
-  {desc= Ap2 (Udiv, typ, x, y); term= unsigned typ Term.div x.term y.term}
-  |> check invariant
-
-let urem typ x y =
-  {desc= Ap2 (Urem, typ, x, y); term= unsigned typ Term.rem x.term y.term}
-  |> check invariant
+let add = binary Add Term.add
+let sub = binary Sub Term.sub
+let mul = binary Mul Term.mul
+let div = binary Div Term.div
+let rem = binary Rem Term.rem
+let udiv = ubinary Udiv Term.div
+let urem = ubinary Urem Term.rem
 
 (* boolean / bitwise *)
 
-let and_ typ x y =
-  {desc= Ap2 (And, typ, x, y); term= Term.and_ x.term y.term}
-  |> check invariant
-
-let or_ typ x y =
-  {desc= Ap2 (Or, typ, x, y); term= Term.or_ x.term y.term}
-  |> check invariant
+let and_ = binary And Term.and_
+let or_ = binary Or Term.or_
 
 (* bitwise *)
 
-let xor typ x y =
-  {desc= Ap2 (Xor, typ, x, y); term= Term.xor x.term y.term}
-  |> check invariant
-
-let shl typ x y =
-  {desc= Ap2 (Shl, typ, x, y); term= Term.shl x.term y.term}
-  |> check invariant
-
-let lshr typ x y =
-  {desc= Ap2 (Lshr, typ, x, y); term= Term.lshr x.term y.term}
-  |> check invariant
-
-let ashr typ x y =
-  {desc= Ap2 (Ashr, typ, x, y); term= Term.ashr x.term y.term}
-  |> check invariant
+let xor = binary Xor Term.xor
+let shl = binary Shl Term.shl
+let lshr = binary Lshr Term.lshr
+let ashr = binary Ashr Term.ashr
 
 (* if-then-else *)
 
-let conditional typ ~cnd ~thn ~els =
+let conditional ?typ ~cnd ~thn ~els =
+  let typ = match typ with Some typ -> typ | None -> typ_of thn in
   { desc= Ap3 (Conditional, typ, cnd, thn, els)
   ; term= Term.conditional ~cnd:cnd.term ~thn:thn.term ~els:els.term }
   |> check invariant

sledge/src/llair/exp.mli

@@ -141,40 +141,40 @@ val float : Typ.t -> string -> t
 val convert : ?unsigned:bool -> dst:Typ.t -> src:Typ.t -> t -> t
 
 (* comparisons *)
-val eq : Typ.t -> t -> t -> t
-val dq : Typ.t -> t -> t -> t
-val gt : Typ.t -> t -> t -> t
-val ge : Typ.t -> t -> t -> t
-val lt : Typ.t -> t -> t -> t
-val le : Typ.t -> t -> t -> t
-val ugt : Typ.t -> t -> t -> t
-val uge : Typ.t -> t -> t -> t
-val ult : Typ.t -> t -> t -> t
-val ule : Typ.t -> t -> t -> t
-val ord : Typ.t -> t -> t -> t
-val uno : Typ.t -> t -> t -> t
+val eq : ?typ:Typ.t -> t -> t -> t
+val dq : ?typ:Typ.t -> t -> t -> t
+val gt : ?typ:Typ.t -> t -> t -> t
+val ge : ?typ:Typ.t -> t -> t -> t
+val lt : ?typ:Typ.t -> t -> t -> t
+val le : ?typ:Typ.t -> t -> t -> t
+val ugt : ?typ:Typ.t -> t -> t -> t
+val uge : ?typ:Typ.t -> t -> t -> t
+val ult : ?typ:Typ.t -> t -> t -> t
+val ule : ?typ:Typ.t -> t -> t -> t
+val ord : ?typ:Typ.t -> t -> t -> t
+val uno : ?typ:Typ.t -> t -> t -> t
 
 (* arithmetic *)
-val add : Typ.t -> t -> t -> t
-val sub : Typ.t -> t -> t -> t
-val mul : Typ.t -> t -> t -> t
-val div : Typ.t -> t -> t -> t
-val rem : Typ.t -> t -> t -> t
-val udiv : Typ.t -> t -> t -> t
-val urem : Typ.t -> t -> t -> t
+val add : ?typ:Typ.t -> t -> t -> t
+val sub : ?typ:Typ.t -> t -> t -> t
+val mul : ?typ:Typ.t -> t -> t -> t
+val div : ?typ:Typ.t -> t -> t -> t
+val rem : ?typ:Typ.t -> t -> t -> t
+val udiv : ?typ:Typ.t -> t -> t -> t
+val urem : ?typ:Typ.t -> t -> t -> t
 
 (* boolean / bitwise *)
-val and_ : Typ.t -> t -> t -> t
-val or_ : Typ.t -> t -> t -> t
+val and_ : ?typ:Typ.t -> t -> t -> t
+val or_ : ?typ:Typ.t -> t -> t -> t
 
 (* bitwise *)
-val xor : Typ.t -> t -> t -> t
-val shl : Typ.t -> t -> t -> t
-val lshr : Typ.t -> t -> t -> t
-val ashr : Typ.t -> t -> t -> t
+val xor : ?typ:Typ.t -> t -> t -> t
+val shl : ?typ:Typ.t -> t -> t -> t
+val lshr : ?typ:Typ.t -> t -> t -> t
+val ashr : ?typ:Typ.t -> t -> t -> t
 
 (* if-then-else *)
-val conditional : Typ.t -> cnd:t -> thn:t -> els:t -> t
+val conditional : ?typ:Typ.t -> cnd:t -> thn:t -> els:t -> t
 
 (* records (struct / array values) *)
 val record : Typ.t -> t vector -> t
@@ -199,6 +199,5 @@ val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a
 (** Query *)
 
 val term : t -> Term.t
-val typ : t -> Typ.t
 val is_true : t -> bool
 val is_false : t -> bool

sledge/src/llair/frontend.ml

@@ -331,12 +331,12 @@ let ptr_fld x ~ptr ~fld ~lltyp =
   let offset =
     Llvm_target.DataLayout.offset_of_element lltyp fld x.lldatalayout
   in
-  Exp.add Typ.ptr ptr (Exp.integer Typ.siz (Z.of_int64 offset))
+  Exp.add ~typ:Typ.ptr ptr (Exp.integer Typ.siz (Z.of_int64 offset))
 
 let ptr_idx x ~ptr ~idx ~llelt =
   let stride = Llvm_target.DataLayout.abi_size llelt x.lldatalayout in
-  Exp.add Typ.ptr ptr
-    (Exp.mul Typ.siz (Exp.integer Typ.siz (Z.of_int64 stride)) idx)
+  Exp.add ~typ:Typ.ptr ptr
+    (Exp.mul ~typ:Typ.siz (Exp.integer Typ.siz (Z.of_int64 stride)) idx)
 
 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
@@ -457,13 +457,14 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
     let arg = xlate_value x rand in
     Exp.convert ?unsigned ~dst ~src arg
   in
-  let binary mk =
+  let binary (mk : ?typ:_ -> _) =
     Lazy.force check_vector ;
     let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 0)) in
-    mk typ (xlate_rand 0) (xlate_rand 1)
+    mk ~typ (xlate_rand 0) (xlate_rand 1)
   in
   let unordered_or mk =
-    binary (fun typ e f -> Exp.or_ Typ.bool (Exp.uno typ e f) (mk typ e f))
+    binary (fun ?typ e f ->
+        Exp.or_ ~typ:Typ.bool (Exp.uno ?typ e f) (mk ?typ e f) )
   in
   ( match opcode with
   | AddrSpaceCast | BitCast -> cast ()
@@ -484,7 +485,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
     | Ule -> binary Exp.ule )
   | FCmp -> (
     match Llvm.fcmp_predicate llv with
-    | None | Some False -> binary (fun _ _ _ -> Exp.false_)
+    | None | Some False -> binary (fun ?typ:_ _ _ -> Exp.false_)
     | Some Oeq -> binary Exp.eq
     | Some Ogt -> binary Exp.gt
     | Some Oge -> binary Exp.ge
@@ -499,7 +500,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
     | Some Ult -> unordered_or Exp.lt
     | Some Ule -> unordered_or Exp.le
     | Some Une -> unordered_or Exp.dq
-    | Some True -> binary (fun _ _ _ -> Exp.true_) )
+    | Some True -> binary (fun ?typ:_ _ _ -> Exp.true_) )
   | Add | FAdd -> binary Exp.add
   | Sub | FSub -> binary Exp.sub
   | Mul | FMul -> binary Exp.mul
@@ -515,7 +516,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
   | Xor -> binary Exp.xor
   | Select ->
       let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 1)) in
-      Exp.conditional typ ~cnd:(xlate_rand 0) ~thn:(xlate_rand 1)
+      Exp.conditional ~typ ~cnd:(xlate_rand 0) ~thn:(xlate_rand 1)
         ~els:(xlate_rand 2)
   | ExtractElement | InsertElement ->
       todo "vector operations: %a" pp_llvalue llv ()
@@ -1150,7 +1151,7 @@ let xlate_instr :
           in
           let match_filter i rev_blocks =
             jump_unwind i
-              (Exp.sub i32 (Exp.integer i32 Z.zero) typeid)
+              (Exp.sub ~typ:i32 (Exp.integer i32 Z.zero) typeid)
               rev_blocks
           in
           let xlate_clause i rev_blocks =
@@ -1167,9 +1168,9 @@ let xlate_instr :
                     let rec xlate_filter i =
                       let tiI = xlate_value x (Llvm.operand clause i) in
                       if i < num_tis - 1 then
-                        Exp.and_ Typ.bool (Exp.dq tip tiI ti)
+                        Exp.and_ ~typ:Typ.bool (Exp.dq ~typ:tip tiI ti)
                           (xlate_filter (i + 1))
-                      else Exp.dq tip tiI ti
+                      else Exp.dq ~typ:tip tiI ti
                     in
                     let key = xlate_filter 0 in
                     let nzero, rev_blocks = match_filter i rev_blocks in
@@ -1180,9 +1181,9 @@ let xlate_instr :
                   let typ = xlate_type x (Llvm.type_of clause) in
                   let clause = xlate_value x clause in
                   let key =
-                    Exp.or_ Typ.bool
-                      (Exp.eq typ clause Exp.null)
-                      (Exp.eq typ clause ti)
+                    Exp.or_ ~typ:Typ.bool
+                      (Exp.eq ~typ clause Exp.null)
+                      (Exp.eq ~typ clause ti)
                   in
                   let nzero, rev_blocks = jump_unwind i typeid rev_blocks in
                   ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))

sledge/src/llair/term_test.ml

@@ -35,7 +35,7 @@ let%test_module _ =
 
     let%test "boolean overflow" =
       Term.is_true
-        (Exp.eq Typ.bool
+        (Exp.eq
            (Exp.integer Typ.bool Z.minus_one)
            (Exp.convert ~dst:Typ.bool ~src:Typ.siz
               (Exp.integer Typ.siz Z.one)))
@@ -43,7 +43,7 @@ let%test_module _ =
 
     let%test "unsigned boolean overflow" =
       Term.is_true
-        (Exp.uge Typ.bool
+        (Exp.uge
            (Exp.integer Typ.bool Z.minus_one)
            (Exp.convert ~dst:Typ.bool ~src:Typ.siz
               (Exp.integer Typ.siz Z.one)))