Mmx

CHANGELOG.md

@@ -5,6 +5,16 @@
 
 - Fix printing of `while` loops [PR #131](https://github.com/jasmin-lang/jasmin/pull/131).
 
+## New features
+
+- provide access to mmx registers:
+	declaration:
+	  normal register:  #mmx reg u64 x
+	  mmx    register:       reg u64 m
+	move from/to normal register: x = m; m = x;
+	             using intrasic : x = MOVX(m); m = MOVX(x);
+	add the instruction MOVX_32 and MOVX_64
+
 # Jasmin 22.0
 
 This release is the result of more than two years of active development. It thus

compiler/src/arch_full.ml

@@ -5,6 +5,7 @@ open Prog
 
 module type Core_arch = sig
   type reg
+  type regx
   type xreg
   type rflag
   type cond
@@ -13,12 +14,13 @@ module type Core_arch = sig
   type fresh_vars
   type lowering_options
 
-  val asm_e : (reg, xreg, rflag, cond, asm_op, extra_op) asm_extra
-  val aparams : (reg, xreg, rflag, cond, asm_op, extra_op, fresh_vars, lowering_options) Arch_params.architecture_params
+  val asm_e : (reg, regx, xreg, rflag, cond, asm_op, extra_op) asm_extra
+  val aparams : (reg, regx, xreg, rflag, cond, asm_op, extra_op, fresh_vars, lowering_options) Arch_params.architecture_params
 
   val rsp : reg
 
   val allocatable : reg list
+  val extra_allocatable : regx list
   val xmm_allocatable : xreg list
   val arguments : reg list
   val xmm_arguments : xreg list
@@ -30,11 +32,11 @@ module type Core_arch = sig
   val lowering_vars : 'a Conv.coq_tbl -> fresh_vars
   val lowering_opt : lowering_options
 
-  val pp_asm : 'info Conv.coq_tbl -> Format.formatter -> (reg, xreg, rflag, cond, asm_op) Arch_decl.asm_prog -> unit
+  val pp_asm : 'info Conv.coq_tbl -> Format.formatter -> (reg, regx, xreg, rflag, cond, asm_op) Arch_decl.asm_prog -> unit
   val analyze :
-    (unit, (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
-    (unit, (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
-    (unit, (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.prog ->
+    (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
+    (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
+    (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.prog ->
     unit
 end
 
@@ -44,17 +46,19 @@ module type Arch = sig
   val reg_size : Wsize.wsize
   val rip : var
 
-  val asmOp      : (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op Sopn.asmOp
-  val asmOp_sopn : (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op Sopn.sopn Sopn.asmOp
+  val asmOp      : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op Sopn.asmOp
+  val asmOp_sopn : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op Sopn.sopn Sopn.asmOp
 
   val reg_vars : var list
+  val regx_vars : var list
   val xreg_vars : var list
   val flag_vars : var list
   val argument_vars : var list
   val xmm_argument_vars : var list
   val ret_vars : var list
   val xmm_ret_vars : var list
   val allocatable_vars : var list
+  val extra_allocatable_vars : var list
   val xmm_allocatable_vars : var list
   val callee_save_vars : var list
   val rsp_var : var
@@ -68,7 +72,7 @@ module Arch_from_Core_arch (A : Core_arch) : Arch = struct
   let xreg_size = A.asm_e._asm._arch_decl.xreg_size
 
   (* not sure it is the best place to define [rip], but we need to know [reg_size] *)
-  let rip = V.mk "RIP" (Reg Direct) (tu reg_size) L._dummy []
+  let rip = V.mk "RIP" (Reg (Normal, Direct)) (tu reg_size) L._dummy []
 
   let asmOp = Arch_extra.asm_opI A.asm_e
   let asmOp_sopn = Sopn.asmOp_sopn reg_size asmOp
@@ -78,19 +82,31 @@ module Arch_from_Core_arch (A : Core_arch) : Arch = struct
 
   let reg_vars =
     let l = A.asm_e._asm._arch_decl.toS_r.strings in
-    let reg_k = Prog.Reg Prog.Direct in
+    let reg_k = Reg (Normal, Direct) in
     List.map (fun (s, _) -> V.mk (Conv.string_of_string0 s) reg_k (tu reg_size) L._dummy []) l
 
   let var_of_reg r =
     let s = string_of_reg r in
     List.find (fun x -> x.v_name = s) reg_vars
 
+  let string_of_regx r =
+    Conv.string_of_string0 (A.asm_e._asm._arch_decl.toS_rx.to_string r)
+
+  let regx_vars =
+    let l = A.asm_e._asm._arch_decl.toS_rx.strings in
+    let reg_k = Reg (Extra, Direct) in
+    List.map (fun (s, _) -> V.mk (Conv.string_of_string0 s) reg_k (tu reg_size) L._dummy []) l
+
+  let var_of_regx r =
+    let s = string_of_regx r in
+    List.find (fun x -> x.v_name = s) regx_vars
+
   let string_of_xreg r =
     Conv.string_of_string0 (A.asm_e._asm._arch_decl.toS_x.to_string r)
 
   let xreg_vars =
     let l = A.asm_e._asm._arch_decl.toS_x.strings in
-    let reg_k = Prog.Reg Prog.Direct in
+    let reg_k = Reg (Normal, Direct) in
     List.map (fun (s, _) -> V.mk (Conv.string_of_string0 s) reg_k (tu xreg_size) L._dummy []) l
 
   let var_of_xreg r =
@@ -102,7 +118,7 @@ module Arch_from_Core_arch (A : Core_arch) : Arch = struct
 
   let flag_vars =
     let l = A.asm_e._asm._arch_decl.toS_f.strings in
-    let reg_k = Prog.Reg Prog.Direct in
+    let reg_k = Reg (Normal, Direct) in
     List.map (fun (s, _) -> V.mk (Conv.string_of_string0 s) reg_k (Bty Bool) L._dummy []) l
 
   let var_of_flag f =
@@ -124,6 +140,9 @@ module Arch_from_Core_arch (A : Core_arch) : Arch = struct
   let allocatable_vars =
     List.map var_of_reg A.allocatable
 
+  let extra_allocatable_vars =
+    List.map var_of_regx A.extra_allocatable
+
   let xmm_allocatable_vars =
     List.map var_of_xreg A.xmm_allocatable
 
@@ -132,6 +151,6 @@ module Arch_from_Core_arch (A : Core_arch) : Arch = struct
 
   let rsp_var = var_of_reg A.rsp
 
-  let all_registers = reg_vars @ xreg_vars @ flag_vars
+  let all_registers = reg_vars @ regx_vars @ xreg_vars @ flag_vars
 
 end

compiler/src/arch_full.mli

@@ -3,6 +3,7 @@ open Prog
 
 module type Core_arch = sig
   type reg
+  type regx 
   type xreg
   type rflag
   type cond
@@ -11,12 +12,13 @@ module type Core_arch = sig
   type fresh_vars
   type lowering_options
 
-  val asm_e : (reg, xreg, rflag, cond, asm_op, extra_op) asm_extra
-  val aparams : (reg, xreg, rflag, cond, asm_op, extra_op, fresh_vars, lowering_options) Arch_params.architecture_params
+  val asm_e : (reg, regx, xreg, rflag, cond, asm_op, extra_op) asm_extra
+  val aparams : (reg, regx, xreg, rflag, cond, asm_op, extra_op, fresh_vars, lowering_options) Arch_params.architecture_params
 
   val rsp : reg
 
   val allocatable : reg list
+  val extra_allocatable : regx list
   val xmm_allocatable : xreg list
   val arguments : reg list
   val xmm_arguments : xreg list
@@ -28,11 +30,11 @@ module type Core_arch = sig
   val lowering_vars : 'a Conv.coq_tbl -> fresh_vars
   val lowering_opt : lowering_options
 
-  val pp_asm : 'info Conv.coq_tbl -> Format.formatter -> (reg, xreg, rflag, cond, asm_op) Arch_decl.asm_prog -> unit
+  val pp_asm : 'info Conv.coq_tbl -> Format.formatter -> (reg, regx, xreg, rflag, cond, asm_op) Arch_decl.asm_prog -> unit
   val analyze :
-    (unit, (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
-    (unit, (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
-    (unit, (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.prog ->
+    (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
+    (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.func ->
+    (unit, (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) Prog.prog ->
     unit
 end
 
@@ -42,17 +44,19 @@ module type Arch = sig
   val reg_size : Wsize.wsize
   val rip : var
 
-  val asmOp      : (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op Sopn.asmOp
-  val asmOp_sopn : (reg, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op Sopn.sopn Sopn.asmOp
+  val asmOp      : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op Sopn.asmOp
+  val asmOp_sopn : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op Sopn.sopn Sopn.asmOp
 
   val reg_vars : var list
+  val regx_vars : var list
   val xreg_vars : var list
   val flag_vars : var list
   val argument_vars : var list
   val xmm_argument_vars : var list
   val ret_vars : var list
   val xmm_ret_vars : var list
   val allocatable_vars : var list
+  val extra_allocatable_vars : var list
   val xmm_allocatable_vars : var list
   val callee_save_vars : var list
   val rsp_var : var

compiler/src/array_expand.ml

@@ -7,7 +7,7 @@ let init_tbl fc =
     let ws, sz = array_kind v.v_ty in
     let ty = Bty (U ws) in
     let vi i =
-      V.mk (v.v_name ^ "#" ^ string_of_int i) (Reg Direct) ty v.v_dloc v.v_annot in
+      V.mk (v.v_name ^ "#" ^ string_of_int i) (Reg(reg_kind v.v_kind, Direct)) ty v.v_dloc v.v_annot in
     let t = Array.init sz vi in
     Hv.add tbl v (ws, t) in
   let fv = vars_fc fc in

compiler/src/insert_copy_and_fix_length.ml

@@ -22,8 +22,8 @@ let is_array_copy (x:lval) (e:expr) =
         begin match y.v_ty with
         | Arr(yws, yn) ->
            assert (arr_size xws xn <= arr_size yws yn);
-           if x.v_kind = Reg Direct then Some (xws, xn)
-           else if y.v_kind = Reg Direct then Some (yws, arr_size xws xn / size_of_ws yws)
+           if x.v_kind = Reg(Normal, Direct) then Some (xws, xn)
+           else if y.v_kind = Reg(Normal, Direct) then Some (yws, arr_size xws xn / size_of_ws yws)
            else None
         | _ -> None
         end

compiler/src/latex_printer.ml

@@ -207,7 +207,7 @@ let pp_pointer = function
 let pp_storage fmt s =
   latex "storageclass" fmt
     (match s with
-     | `Reg ptr -> "reg" ^ (pp_pointer ptr)
+     | `Reg(ptr) -> "reg" ^ (pp_pointer ptr)
      | `Stack ptr -> "stack" ^ (pp_pointer ptr)
      | `Inline -> "inline"
      | `Global -> "global")
@@ -260,6 +260,7 @@ let pp_sidecond fmt =
 let pp_vardecls fmt d =
   F.fprintf fmt "%a%a;" indent 1 pp_args d; F.fprintf fmt eol
 
+(* TODO: print annot *)
 let rec pp_instr depth fmt (_annot, p) =
   indent fmt depth;
   match L.unloc p with

compiler/src/main_compiler.ml

@@ -82,7 +82,7 @@ let main () =
 
   let lowering_vars tbl = X86_lowering.(
     let f ty n = 
-      let v = V.mk n (Reg Direct) ty L._dummy [] in
+      let v = V.mk n (Reg(Normal, Direct)) ty L._dummy [] in
       Conv.cvar_of_var tbl v in
     let b = f tbool in
     { fresh_OF = (b "OF").vname
@@ -327,8 +327,8 @@ let main () =
     let is_var_in_memory cv : bool =
       let v = Conv.vari_of_cvari tbl cv |> L.unloc in
       match v.v_kind with
-      | Stack _ | Reg (Pointer _) | Global -> true
-      | Const | Inline | Reg Direct -> false
+      | Stack _ | Reg (_, Pointer _) | Global -> true
+      | Const | Inline | Reg(_, Direct) -> false
      in
 
     let pp_cuprog s cp =

compiler/src/parser.mly

@@ -391,7 +391,7 @@ ptr:
    } 
 
 storage:
-| REG    ptr=ptr { `Reg ptr}
+| REG    ptr=ptr { `Reg ptr }
 | STACK  ptr=ptr { `Stack ptr }
 | INLINE         { `Inline }
 | GLOBAL         { `Global }

compiler/src/ppasm.ml

@@ -92,6 +92,21 @@ let pp_register ~(reg_pre:string) (ws : rsize) (reg : X86_decl.register) =
     | RSpecial x, `U64 -> Printf.sprintf "%s%s%s" "r" (ssp x) "" in
   Printf.sprintf "%s%s" reg_pre s   
 
+(* -------------------------------------------------------------------- *)
+
+let pp_register_ext ~(reg_pre:string) (_ws: W.wsize) (r: X86_decl.register_ext) : string =
+  Format.sprintf "%smm%d" 
+    reg_pre
+    (match r with
+     | MM0 -> 0
+     | MM1 -> 1
+     | MM2 -> 2
+     | MM3 -> 3
+     | MM4 -> 4
+     | MM5 -> 5
+     | MM6 -> 6
+     | MM7 -> 7)
+
 (* -------------------------------------------------------------------- *)
 let pp_xmm_register ~(reg_pre:string) (ws: W.wsize) (r: X86_decl.xmm_register) : string =
   Format.sprintf "%s%smm%d" 
@@ -223,7 +238,7 @@ module type BPrinter = sig
   val imm_pre         : string
   val reg_pre         : string
   val indirect_pre    : string
-  val pp_address      : W.wsize -> (X86_decl.register, 'a, 'b, 'c) Arch_decl.address -> string
+  val pp_address      : W.wsize -> (X86_decl.register, 'a, 'b, 'c, 'd) Arch_decl.address -> string
   val rev_args        : 'a list -> 'a list
   val pp_iname_ext    : W.wsize -> string
   val pp_iname2_ext   : char list -> W.wsize -> W.wsize -> string
@@ -244,7 +259,7 @@ module ATT : BPrinter = struct
   let indirect_pre = "*"
 
   (* -------------------------------------------------------------------- *)
-  let pp_reg_address (addr : (_, _, _, _) Arch_decl.reg_address) =
+  let pp_reg_address (addr : (_, _, _, _, _) Arch_decl.reg_address) =
     let disp = Conv.z_of_int64 addr.ad_disp in
     let base = addr.ad_base in
     let off  = addr.ad_offset in
@@ -267,7 +282,7 @@ module ATT : BPrinter = struct
           Printf.sprintf "%s(%s,%s,%s)" disp base off (pp_scale scal)
     end
 
-  let pp_address _ws (addr : (_, _, _, _) Arch_decl.address) =
+  let pp_address _ws (addr : (_, _, _, _, _) Arch_decl.address) =
     match addr with
     | Areg ra -> pp_reg_address ra
     | Arip d ->
@@ -306,7 +321,7 @@ module Intel : BPrinter = struct
   let pp_xmm_register = pp_xmm_register
 
   (* -------------------------------------------------------------------- *)
-  let pp_reg_address (addr : (_, _, _, _) Arch_decl.reg_address) =
+  let pp_reg_address (addr : (_, _, _, _, _) Arch_decl.reg_address) =
     let disp = Conv.z_of_int64 addr.ad_disp in
     let base = addr.ad_base in
     let off  = addr.ad_offset in
@@ -334,7 +349,7 @@ module Intel : BPrinter = struct
     | U128 -> "xmmword"
     | U256 -> "ymmword"
 
-  let pp_address ws (addr : (_, _, _, _) Arch_decl.address) =
+  let pp_address ws (addr : (_, _, _, _, _) Arch_decl.address) =
     match addr with
     | Areg ra -> Printf.sprintf "%s ptr[%s]" (pp_address_size ws) (pp_reg_address ra)
     | Arip d ->
@@ -363,11 +378,12 @@ module Printer (BP:BPrinter) = struct
     Format.sprintf "%s%s" imm_pre (Z.to_string imm)
 
   (* -------------------------------------------------------------------- *)
-  let pp_asm_arg ((ws,op):(W.wsize * (_, _, _, _) Arch_decl.asm_arg)) =
+  let pp_asm_arg ((ws,op):(W.wsize * (_, _, _, _, _) Arch_decl.asm_arg)) =
     match op with
     | Condt  _   -> assert false
     | Imm(ws, w) -> pp_imm (Conv.z_of_word ws w)
     | Reg r      -> pp_register ~reg_pre (rsize_of_wsize ws) r
+    | Regx r     -> pp_register_ext ~reg_pre ws r
     | Addr addr  -> BP.pp_address ws addr
     | XReg r     -> pp_xmm_register ~reg_pre ws r
 
@@ -391,7 +407,7 @@ module Printer (BP:BPrinter) = struct
     Printf.sprintf "%s%s" (Conv.string_of_string0 pp_op.pp_aop_name) (pp_ext pp_op.pp_aop_ext)
 
   (* -------------------------------------------------------------------- *)
-  let pp_instr tbl name (i : (_, _, _, _, _) Arch_decl.asm_i) =
+  let pp_instr tbl name (i : (_, _, _, _, _, _) Arch_decl.asm_i) =
     match i with
     | ALIGN ->
       `Instr (".p2align", ["5"])
@@ -425,11 +441,11 @@ module Printer (BP:BPrinter) = struct
       `Instr(name, args)
 
   (* -------------------------------------------------------------------- *)
-  let pp_instr tbl name (fmt : Format.formatter) (i : (_, _, _, _, _) Arch_decl.asm_i) =
+  let pp_instr tbl name (fmt : Format.formatter) (i : (_, _, _, _, _, _) Arch_decl.asm_i) =
     pp_gen fmt (pp_instr tbl name i)
 
   (* -------------------------------------------------------------------- *)
-  let pp_instrs tbl name (fmt : Format.formatter) (is : (_, _, _, _, _) Arch_decl.asm_i list) =
+  let pp_instrs tbl name (fmt : Format.formatter) (is : (_, _, _, _, _, _) Arch_decl.asm_i list) =
     List.iter (Format.fprintf fmt "%a\n%!" (pp_instr tbl name)) is
 
   (* -------------------------------------------------------------------- *)  

compiler/src/ppasm.mli

@@ -8,7 +8,7 @@ val mangle : string -> string
 (* -------------------------------------------------------------------- *)
 val pp_instr :
   'info Conv.coq_tbl -> string -> Format.formatter ->
-  (X86_decl.register, X86_decl.xmm_register, X86_decl.rflag, X86_decl.condt, X86_instr_decl.x86_op) Arch_decl.asm_i ->
+  (X86_decl.register, X86_decl.register_ext, X86_decl.xmm_register, X86_decl.rflag, X86_decl.condt, X86_instr_decl.x86_op) Arch_decl.asm_i ->
   unit
 
 val pp_prog  :