[sledge] Add result type to Exp.{add,sub,mul}

Summary:
Require Exp clients to provide the type of the result of arithmetic
operations.

Reviewed By: mbouaziz

Differential Revision: D12854511

fbshipit-source-id: cc91a39ca

sledge/src/llair/exp.ml

@@ -823,9 +823,9 @@ let ult = app2 Ult
 let ule = app2 Ule
 let ord = app2 Ord
 let uno = app2 Uno
-let add = app2 Add
+let add typ = app2 Add
-let sub = app2 Sub
+let sub typ = app2 Sub
-let mul = app2 Mul
+let mul typ = app2 Mul
 let div = app2 Div
 let udiv = app2 Udiv
 let rem = app2 Rem

sledge/src/llair/exp.mli

@@ -149,9 +149,9 @@ val ult : t -> t -> t
 val ule : t -> t -> t
 val ord : t -> t -> t
 val uno : t -> t -> t
-val add : t -> t -> t
+val add : Typ.t -> t -> t -> t
-val sub : t -> t -> t
+val sub : Typ.t -> t -> t -> t
-val mul : t -> t -> t
+val mul : Typ.t -> t -> t -> t
 val div : t -> t -> t
 val udiv : t -> t -> t
 val rem : t -> t -> t

sledge/src/llair/exp_test.ml

@@ -10,7 +10,7 @@ let%test_module _ =
     let pf = Format.printf "%t%a@." (fun _ -> Trace.flush ()) Exp.pp
     let char = Typ.integer ~bits:8
     let ( ! ) i = Exp.integer (Z.of_int i) char
-    let ( + ) = Exp.add
+    let ( + ) = Exp.add char
     let ( && ) = Exp.and_
     let ( || ) = Exp.or_
 

sledge/src/llair/frontend.ml

@@ -316,11 +316,12 @@ let ptr_fld x ~ptr ~fld ~lltyp =
   let offset =
     Llvm_target.DataLayout.offset_of_element lltyp fld x.lldatalayout
   in
-  Exp.add ptr (Exp.integer (Z.of_int64 offset) Typ.siz)
+  Exp.add Typ.ptr ptr (Exp.integer (Z.of_int64 offset) Typ.siz)
 
 let ptr_idx x ~ptr ~idx ~llelt =
   let stride = Llvm_target.DataLayout.abi_size llelt x.lldatalayout in
-  Exp.add ptr (Exp.mul (Exp.integer (Z.of_int64 stride) Typ.siz) idx)
+  Exp.add Typ.ptr ptr
+    (Exp.mul Typ.siz (Exp.integer (Z.of_int64 stride) Typ.siz) 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
@@ -420,10 +421,11 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
   [%Trace.call fun {pf} -> pf "%a" pp_llvalue llv]
   ;
   let xlate_rand i = xlate_value x (Llvm.operand llv i) in
+  let typ = lazy (xlate_type x (Llvm.type_of llv)) in
   let cast () = xlate_rand 0 in
   let convert signed =
     let rand = Llvm.operand llv 0 in
-    let dst = xlate_type x (Llvm.type_of llv) in
+    let dst = Lazy.force typ in
     let src = xlate_type x (Llvm.type_of rand) in
     let arg = xlate_value x rand in
     Exp.convert ~signed ~dst ~src arg
@@ -472,9 +474,9 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
     | Some Ule -> unordered_or Exp.le
     | Some Une -> unordered_or Exp.dq
     | Some True -> binary (fun _ _ -> Exp.bool true) )
-  | Add | FAdd -> binary Exp.add
+  | Add | FAdd -> binary (Exp.add (Lazy.force typ))
-  | Sub | FSub -> binary Exp.sub
+  | Sub | FSub -> binary (Exp.sub (Lazy.force typ))
-  | Mul | FMul -> binary Exp.mul
+  | Mul | FMul -> binary (Exp.mul (Lazy.force typ))
   | SDiv | FDiv -> binary Exp.div
   | UDiv -> binary Exp.udiv
   | SRem | FRem -> binary Exp.rem
@@ -1187,7 +1189,7 @@ let xlate_instr :
             Llair.Block.mk ~lbl:(lbl i) ~params:[] ~cmnd:Vector.empty ~term
           in
           let match_filter =
-            jump_unwind (Exp.sub (Exp.integer Z.zero i32) typeid)
+            jump_unwind (Exp.sub i32 (Exp.integer Z.zero i32) typeid)
           in
           let xlate_clause i =
             let clause = Llvm.operand instr i in

sledge/src/symbheap/congruence.ml

@@ -126,9 +126,9 @@ let invariant r =
 
 let map_sum e ~f =
   match e with
-  | Exp.App {op= App {op= Add; arg= a}; arg= Integer _ as i} ->
+  | Exp.App {op= App {op= Add; arg= a}; arg= Integer {typ} as i} ->
       let a' = f a in
-      if a' == a then e else Exp.add a' i
+      if a' == a then e else Exp.add typ a' i
   | a -> f a
 
 let fold_sum e ~init ~f =
@@ -143,8 +143,8 @@ let base_of = function
 (** solve a+i = b for a, yielding a = b-i *)
 let solve_for_base ai b =
   match ai with
-  | Exp.App {op= App {op= Add; arg= a}; arg= Integer _ as i} ->
+  | Exp.App {op= App {op= Add; arg= a}; arg= Integer {typ} as i} ->
-      (a, Exp.sub b i)
+      (a, Exp.sub typ b i)
   | _ -> (ai, b)
 
 (** [norm r a+i] = [a'+k] where [r] implies [a+i=a'+k] and [a'] is a rep *)

sledge/src/symbheap/congruence_test.ml

@@ -15,8 +15,8 @@ let%test_module _ =
     let i8 = Typ.integer ~bits:8
     let i64 = Typ.integer ~bits:64
     let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz
-    let ( + ) = Exp.add
+    let ( + ) = Exp.add Typ.siz
-    let ( - ) = Exp.sub
+    let ( - ) = Exp.sub Typ.siz
     let f = Exp.convert ~dst:i64 ~src:i8
     let g = Exp.xor
     let wrt = Var.Set.empty

sledge/src/symbheap/exec.ml

@@ -39,7 +39,7 @@ let assume cnd pre =
  *)
 let alloc_spec us reg num len =
   let loc = Exp.var reg in
-  let siz = Exp.mul num len in
+  let siz = Exp.mul Typ.siz num len in
   let {xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in
   let post = Sh.seg seg in
   let foot = Sh.extend_us xs Sh.emp in
@@ -160,9 +160,9 @@ let memmov_foot us dst src len =
   let arr_dst, us, xs = fresh_var "a" us xs in
   let arr_mid, us, xs = fresh_var "a" us xs in
   let arr_src, us, xs = fresh_var "a" us xs in
-  let src_dst = Exp.sub src dst in
+  let src_dst = Exp.sub Typ.siz src dst in
   let mem_dst = Exp.memory ~siz:src_dst ~arr:arr_dst in
-  let siz_mid = Exp.sub len src_dst in
+  let siz_mid = Exp.sub Typ.siz len src_dst in
   let mem_mid = Exp.memory ~siz:siz_mid ~arr:arr_mid in
   let mem_src = Exp.memory ~siz:src_dst ~arr:arr_src in
   let mem_mid_src = Exp.concat mem_mid mem_src in
@@ -179,7 +179,8 @@ let memmov_foot us dst src len =
   in
   let foot =
     Sh.and_ eq_mem_dst_mid_src
-      (Sh.and_ (Exp.lt dst src) (Sh.and_ (Exp.lt src (Exp.add dst len)) seg))
+      (Sh.and_ (Exp.lt dst src)
+         (Sh.and_ (Exp.lt src (Exp.add Typ.ptr dst len)) seg))
   in
   (xs, bas, siz, mem_dst, mem_mid, mem_src, foot)
 
@@ -249,7 +250,11 @@ let strlen_spec us reg ptr =
   let {xs; seg} = fresh_seg ~loc:ptr us in
   let foot = Sh.seg seg in
   let {Sh.loc= p; bas= b; len= m} = seg in
-  let ret = Exp.sub (Exp.add (Exp.sub b p) m) (Exp.integer Z.one Typ.siz) in
+  let ret =
+    Exp.sub Typ.siz
+      (Exp.add Typ.siz (Exp.sub Typ.siz b p) m)
+      (Exp.integer Z.one Typ.siz)
+  in
   let post = Sh.and_ (Exp.eq (Exp.var reg) ret) foot in
   {xs; foot; post}
 

sledge/src/symbheap/solver.ml

@@ -118,7 +118,8 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
             (Exp.memory ~siz:n ~arr:a0)
             (Exp.memory ~siz:o_n ~arr:a1)))
       (Sh.star
-         (Sh.seg {loc= Exp.add k n; bas= b; len= m; siz= o_n; arr= a1})
+         (Sh.seg
+            {loc= Exp.add Typ.ptr k n; bas= b; len= m; siz= o_n; arr= a1})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -163,7 +164,11 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
                (Exp.memory ~siz:n ~arr:a'))
             (Sh.star
                (Sh.seg
-                  {loc= Exp.add l o; bas= b'; len= m'; siz= n_o; arr= a1'})
+                  { loc= Exp.add Typ.ptr l o
+                  ; bas= b'
+                  ; len= m'
+                  ; siz= n_o
+                  ; arr= a1' })
                (Sh.rem_seg ssg sub))))
   in
   {goal with us; com; min; xs; sub; zs}
@@ -233,7 +238,7 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
   let l_k = Exp.integer l_k Typ.siz and ko_ln = Exp.integer ko_ln Typ.siz in
-  let ln = Exp.add l n in
+  let ln = Exp.add Typ.ptr l n in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
@@ -285,7 +290,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let l_k = Exp.integer l_k Typ.siz in
   let ko_l = Exp.integer ko_l Typ.siz in
   let ln_ko = Exp.integer ln_ko Typ.siz in
-  let ko = Exp.add k o in
+  let ko = Exp.add Typ.ptr k o in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
@@ -382,7 +387,7 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
   let k_l = Exp.integer k_l Typ.siz in
   let ln_ko = Exp.integer ln_ko Typ.siz in
-  let ko = Exp.add k o in
+  let ko = Exp.add Typ.ptr k o in
   let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
   let com = Sh.star (Sh.seg msg) com in
@@ -430,7 +435,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let k_l = Exp.integer k_l Typ.siz in
   let ln_k = Exp.integer ln_k Typ.siz in
   let ko_ln = Exp.integer ko_ln Typ.siz in
-  let ln = Exp.add l n in
+  let ln = Exp.add Typ.ptr l n in
   let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
@@ -473,8 +478,8 @@ let excise_seg ({sub} as goal) msg ssg =
   match[@warning "-p"] Z.sign k_l with
   (* k-l < 0 so k < l *)
   | -1 -> (
-      let ko = Exp.add k o in
+      let ko = Exp.add Typ.ptr k o in
-      let ln = Exp.add l n in
+      let ln = Exp.add Typ.ptr l n in
       Congruence.difference sub.cong ko ln
       >>= fun ko_ln ->
       match[@warning "-p"] Z.sign ko_ln with
@@ -513,8 +518,8 @@ let excise_seg ({sub} as goal) msg ssg =
       | 1 -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) )
   (* k-l > 0 so k > l *)
   | 1 -> (
-      let ko = Exp.add k o in
+      let ko = Exp.add Typ.ptr k o in
-      let ln = Exp.add l n in
+      let ln = Exp.add Typ.ptr l n in
       Congruence.difference sub.cong ko ln
       >>= fun ko_ln ->
       match[@warning "-p"] Z.sign ko_ln with