[sledge] Change: Use mulq instead of mul where possible

Summary:
Multiplication by a constant is primitive in the linear arithmetic
solver, while general multiplication is not, so for clarity and
predictability, use constants where possible.

Reviewed By: jvillard

Differential Revision: D21721020

fbshipit-source-id: 3497d06c9

sledge/bin/frontend.ml

@@ -955,7 +955,7 @@ let xlate_instr :
       let prefix, arg = xlate_value x rand in
       let num = convert_to_siz (xlate_type x (Llvm.type_of rand)) arg in
       assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ;
-      let len = xlate_size_of x instr in
+      let len = size_of x (Llvm.type_of instr) in
       emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc)
   | Call -> (
       let maybe_llfunc = Llvm.operand instr (Llvm.num_operands instr - 1) in
@@ -998,14 +998,14 @@ let xlate_instr :
             let num =
               convert_to_siz (xlate_type x (Llvm.type_of num_operand)) arg
             in
-            let len = Exp.integer Typ.siz (Z.of_int 1) in
+            let len = 1 in
             emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc)
         | ["_Znwm" (* operator new(size_t num) *)]
          |[ "_ZnwmSt11align_val_t"
             (* operator new(unsigned long, std::align_val_t) *) ] ->
             let reg = xlate_name x instr in
             let prefix, num = xlate_value x (Llvm.operand instr 0) in
-            let len = xlate_size_of x instr in
+            let len = size_of x (Llvm.type_of instr) in
             emit_inst ~prefix (Inst.alloc ~reg ~num ~len ~loc)
         | ["_ZdlPv" (* operator delete(void* ptr) *)]
          |[ "_ZdlPvSt11align_val_t"
@@ -1126,7 +1126,7 @@ let xlate_instr :
         when num_actuals > 0 ->
           let reg = xlate_name x instr in
           let pre_0, num = xlate_value x (Llvm.operand instr 0) in
-          let len = xlate_size_of x instr in
+          let len = size_of x (Llvm.type_of instr) in
           let prefix, dst, blocks = xlate_jump x instr return_blk loc [] in
           emit_term
             ~prefix:(pre_0 @ (Inst.alloc ~reg ~num ~len ~loc :: prefix))

sledge/src/domain_sh.ml

@@ -68,8 +68,7 @@ let exec_inst pre inst =
       Exec.memmov pre ~dst:(Term.of_exp dst) ~src:(Term.of_exp src)
         ~len:(Term.of_exp len)
   | Alloc {reg; num; len; _} ->
-      Exec.alloc pre ~reg:(Var.of_reg reg) ~num:(Term.of_exp num)
+      Exec.alloc pre ~reg:(Var.of_reg reg) ~num:(Term.of_exp num) ~len
-        ~len:(Term.of_exp len)
   | Free {ptr; _} -> Exec.free pre ~ptr:(Term.of_exp ptr)
   | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:Var.of_reg reg))
   | Abort _ -> Exec.abort pre )

sledge/src/equality_test.ml

@@ -24,7 +24,7 @@ let%test_module _ =
     let ( ! ) i = Term.integer (Z.of_int i)
     let ( + ) = Term.add
     let ( - ) = Term.sub
-    let ( * ) = Term.mul
+    let ( * ) i e = Term.mulq (Q.of_int i) e
     let f = Term.unsigned 8
     let g = Term.rem
     let wrt = Var.Set.empty
@@ -310,7 +310,7 @@ let%test_module _ =
     let%test _ =
       entails_eq (of_eqs [(g w x, g y w); (x, z)]) (g w x) (g w z)
 
-    let r8 = of_eqs [(x + !42, (!3 * y) + (!13 * z)); (!13 * z, x)]
+    let r8 = of_eqs [(x + !42, (3 * y) + (13 * z)); (13 * z, x)]
 
     let%expect_test _ =
       pp_classes r8 ;

sledge/src/exec.ml

@@ -242,7 +242,7 @@ let memmov_specs us dst src len =
  *)
 let alloc_spec us reg num len =
   let foot = Sh.emp in
-  let siz = Term.mul num len in
+  let siz = Term.mulq (Q.of_int len) num in
   let sub, ms, us = assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) ~us in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -489,8 +489,7 @@ let nallocx_spec us reg siz =
   let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in
   {xs; foot; sub; ms; post}
 
-let size_of_int_mul =
+let size_of_int_mul = Term.mulq (Q.of_int Llair.Typ.(size_of siz))
-  Term.mul (Term.integer (Z.of_int Llair.Typ.(size_of siz)))
 
 (* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 }
  *   mallctl r i w n

sledge/src/exec.mli

@@ -15,7 +15,7 @@ val store : Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> Sh.t option
 val memset : Sh.t -> dst:Term.t -> byt:Term.t -> len:Term.t -> Sh.t option
 val memcpy : Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> Sh.t option
 val memmov : Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> Sh.t option
-val alloc : Sh.t -> reg:Var.t -> num:Term.t -> len:Term.t -> Sh.t option
+val alloc : Sh.t -> reg:Var.t -> num:Term.t -> len:int -> Sh.t option
 val free : Sh.t -> ptr:Term.t -> Sh.t option
 val nondet : Sh.t -> Var.t option -> Sh.t
 val abort : Sh.t -> Sh.t option

sledge/src/llair/llair.ml

@@ -22,7 +22,7 @@ type inst =
   | Memset of {dst: Exp.t; byt: Exp.t; len: Exp.t; loc: Loc.t}
   | Memcpy of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
   | Memmov of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
-  | Alloc of {reg: Reg.t; num: Exp.t; len: Exp.t; loc: Loc.t}
+  | Alloc of {reg: Reg.t; num: Exp.t; len: int; loc: Loc.t}
   | Free of {ptr: Exp.t; loc: Loc.t}
   | Nondet of {reg: Reg.t option; msg: string; loc: Loc.t}
   | Abort of {loc: Loc.t}
@@ -148,8 +148,8 @@ let pp_inst fs inst =
       pf "@[<2>memmov %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp src
         Loc.pp loc
   | Alloc {reg; num; len; loc} ->
-      pf "@[<2>%a@ := alloc [%a x %a];@]\t%a" Reg.pp reg Exp.pp num Exp.pp
+      pf "@[<2>%a@ := alloc [%a x %i];@]\t%a" Reg.pp reg Exp.pp num len
-        len Loc.pp loc
+        Loc.pp loc
   | Free {ptr; loc} -> pf "@[<2>free %a;@]\t%a" Exp.pp ptr Loc.pp loc
   | Nondet {reg; msg; loc} ->
       pf "@[<2>%anondet \"%s\";@]\t%a"
@@ -281,7 +281,7 @@ module Inst = struct
     | Memset {dst; byt; len; loc= _} -> f (f (f init dst) byt) len
     | Memcpy {dst; src; len; loc= _} | Memmov {dst; src; len; loc= _} ->
         f (f (f init dst) src) len
-    | Alloc {reg= _; num; len; loc= _} -> f (f init num) len
+    | Alloc {reg= _; num; len= _; loc= _} -> f init num
     | Free {ptr; loc= _} -> f init ptr
     | Nondet {reg= _; msg= _; loc= _} -> init
     | Abort {loc= _} -> init

sledge/src/llair/llair.mli

@@ -31,7 +31,7 @@ type inst = private
           if ranges overlap. *)
   | Memmov of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t}
       (** Copy [len] bytes starting from address [src] to [dst]. *)
-  | Alloc of {reg: Reg.t; num: Exp.t; len: Exp.t; loc: Loc.t}
+  | Alloc of {reg: Reg.t; num: Exp.t; len: int; loc: Loc.t}
       (** Allocate a block of memory large enough to store [num] elements of
           [len] bytes each and bind [reg] to the first address. *)
   | Free of {ptr: Exp.t; loc: Loc.t}
@@ -115,7 +115,7 @@ module Inst : sig
   val memset : dst:Exp.t -> byt:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val memcpy : dst:Exp.t -> src:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val memmov : dst:Exp.t -> src:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
-  val alloc : reg:Reg.t -> num:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
+  val alloc : reg:Reg.t -> num:Exp.t -> len:int -> loc:Loc.t -> inst
   val free : ptr:Exp.t -> loc:Loc.t -> inst
   val nondet : reg:Reg.t option -> msg:string -> loc:Loc.t -> inst
   val abort : loc:Loc.t -> inst

sledge/src/solver_test.ml

@@ -31,7 +31,7 @@ let%test_module _ =
     let ( ! ) i = Term.integer (Z.of_int i)
     let ( + ) = Term.add
     let ( - ) = Term.sub
-    let ( * ) = Term.mul
+    let ( * ) i e = Term.mulq (Q.of_int i) e
     let wrt = Var.Set.empty
     let a_, wrt = Var.fresh "a" ~wrt
     let a2_, wrt = Var.fresh "a" ~wrt
@@ -220,13 +220,9 @@ let%test_module _ =
 
     let seg_split_symbolically =
       Sh.star
-        (Sh.seg {loc= l; bas= l; len= !16; siz= !8 * n; arr= a2})
+        (Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; arr= a2})
         (Sh.seg
-           { loc= l + (!8 * n)
+           {loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); arr= a3})
-           ; bas= l
-           ; len= !16
-           ; siz= !16 - (!8 * n)
-           ; arr= a3 })
 
     let%expect_test _ =
       check_frame

sledge/src/term.ml

@@ -951,6 +951,7 @@ let add e f = simp_add2 e f |> check invariant
 let addN args = simp_add args |> check invariant
 let sub e f = simp_sub e f |> check invariant
 let mul e f = simp_mul2 e f |> check invariant
+let mulq q e = mul (rational q) e
 let mulN args = simp_mul args |> check invariant
 let div = norm2 Div
 let rem = norm2 Rem

sledge/src/term.mli

@@ -199,6 +199,7 @@ val uno : t -> t -> t
 val neg : t -> t
 val add : t -> t -> t
 val sub : t -> t -> t
+val mulq : Q.t -> t -> t
 val mul : t -> t -> t
 val div : t -> t -> t
 val rem : t -> t -> t