k1c -> kvx changes

1 files changed, 636 insertions, 0 deletions

diff --git a/kvx/Asmexpand.ml b/kvx/Asmexpand.ml
new file mode 100644
index 00000000..5d4fd2f5
--- /dev/null
+++ b/kvx/Asmexpand.ml
@@ -0,0 +1,636 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(* Expanding built-ins and some pseudo-instructions by rewriting
+   of the RISC-V assembly code. *)
+
+open Asm
+open Asmexpandaux
+open AST
+open Camlcoq
+
+exception Error of string
+                  
+(* Useful constants and helper functions *)
+
+let _0  = Integers.Int.zero
+let _1  = Integers.Int.one
+let _2  = coqint_of_camlint 2l
+let _4  = coqint_of_camlint 4l
+let _8  = coqint_of_camlint 8l
+let _16  = coqint_of_camlint 16l
+let _m1 = coqint_of_camlint (-1l)
+
+let wordsize = if Archi.ptr64 then 8 else 4
+
+let align n a = (n + a - 1) land (-a)
+
+let stack_pointer = Asmvliw.GPR12
+                  
+(* Emit instruction sequences that set or offset a register by a constant. *)
+(*
+  let expand_loadimm32 dst n =
+  List.iter emit (Asmgen.loadimm32 dst n [])
+*)
+let expand_addptrofs dst src n =
+  List.iter emit (basic_to_instruction (Asmvliw.PArith (Asmblockgen.addptrofs dst src n)) :: [])
+let expand_storeind_ptr src base ofs =
+  List.iter emit (basic_to_instruction (Asmblockgen.storeind_ptr src base ofs) :: [])
+let expand_loadind_ptr dst base ofs =
+  List.iter emit (basic_to_instruction (Asmblockgen.loadind_ptr base ofs dst) :: [])
+
+(* Built-ins.  They come in two flavors:
+   - annotation statements: take their arguments in registers or stack
+     locations; generate no code;
+   - inlined by the compiler: take their arguments in arbitrary
+     registers.
+*)
+
+(* Fix-up code around calls to variadic functions.  Floating-point arguments
+   residing in FP registers need to be moved to integer registers. *)
+
+let int_param_regs   = let open Asmvliw in [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7; GPR8; GPR9; GPR10; GPR11 |]
+(* let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |] *)
+let float_param_regs = [| |]
+
+let fixup_variadic_call pos tyl = assert false
+(*if pos < 8 then
+    match tyl with
+    | [] ->
+        ()
+    | (Tint | Tany32) :: tyl ->
+        fixup_variadic_call (pos + 1) tyl
+    | Tsingle :: tyl ->
+        let rs =float_param_regs.(pos)
+        and rd = int_param_regs.(pos) in
+        emit (Pfmvxs(rd, rs));
+        fixup_variadic_call (pos + 1) tyl
+    | Tlong :: tyl ->
+        let pos' = if Archi.ptr64 then pos + 1 else align pos 2 + 2 in
+        fixup_variadic_call pos' tyl
+    | (Tfloat | Tany64) :: tyl ->
+        if Archi.ptr64 then begin
+          let rs = float_param_regs.(pos)
+          and rd = int_param_regs.(pos) in
+          emit (Pfmvxd(rd, rs));
+          fixup_variadic_call (pos + 1) tyl
+        end else begin
+          let pos = align pos 2 in
+          if pos < 8 then begin
+            let rs = float_param_regs.(pos)
+            and rd1 = int_param_regs.(pos)
+            and rd2 = int_param_regs.(pos + 1) in
+            emit (Paddiw(X2, X X2, Integers.Int.neg _16));
+            emit (Pfsd(rs, X2, Ofsimm _0));
+            emit (Plw(rd1, X2, Ofsimm _0));
+            emit (Plw(rd2, X2, Ofsimm _4));
+            emit (Paddiw(X2, X X2, _16));
+            fixup_variadic_call (pos + 2) tyl
+          end
+        end
+*)
+        
+let fixup_call sg =
+  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 sg.sig_args
+
+(* Handling of annotations *)
+
+let expand_annot_val kind txt targ args res =
+  emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none));
+  match args, res with
+  | [BA(Asmvliw.IR src)], BR(Asmvliw.IR dst) ->
+     if dst <> src then emit (Pmv (dst, src))
+  | _, _ ->
+     raise (Error "ill-formed __builtin_annot_val")
+
+(* Handling of memcpy *)
+
+let emit_move dst r =
+  if dst <> r
+  then emit (Paddil(dst, r, Z.zero));;
+
+(* FIXME DMonniaux this is probably not complete *)
+let get_builtin_arg dst arg =
+  match arg with
+  | BA (Asmvliw.IR reg) -> emit_move dst reg
+  | BA (ireg) ->  failwith "get_builtin_arg: BA_int(not ireg)"
+  | BA_int _ -> failwith "get_builtin_arg: BA_int"
+  | BA_long _ -> failwith "get_builtin_arg: BA_long"
+  | BA_float _ -> failwith "get_builtin_arg: BA_float"
+  | BA_single _ -> failwith "get_builtin_arg: BA_single"
+  | BA_loadstack _ -> failwith "get_builtin_arg: BA_loadstack"
+  | BA_addrstack ofs -> emit (Paddil(dst, stack_pointer, ofs))
+  | BA_loadglobal _ -> failwith "get_builtin_arg: BA_loadglobal"
+  | BA_addrglobal _ -> failwith "get_builtin_arg: BA_addrglobal"
+  | BA_splitlong _ -> failwith "get_builtin_arg: BA_splitlong"
+  | BA_addptr _ -> failwith "get_builtin_arg: BA_addptr";;
+
+let smart_memcpy = true
+                 
+(* FIXME DMonniaux this is really suboptimal (byte per byte) *)
+let expand_builtin_memcpy_big sz al src dst =
+  assert (sz > Z.zero);
+  let dstptr = Asmvliw.GPR62
+  and srcptr = Asmvliw.GPR63
+  and tmpbuf = Asmvliw.GPR61
+  and tmpbuf2 = Asmvliw.R60R61
+  and caml_sz = camlint64_of_coqint sz in
+  get_builtin_arg dstptr dst;
+  get_builtin_arg srcptr src;
+  let caml_sz_div16 = Int64.shift_right caml_sz 4
+  and sixteen = coqint_of_camlint64 16L in
+  if smart_memcpy
+  then
+    let remaining = ref caml_sz
+    and offset = ref 0L in
+    let cpy buf size load store =
+      (if !remaining >= size
+      then
+        let zofs = coqint_of_camlint64 !offset in
+        begin
+          emit Psemi;
+          emit (load buf srcptr (AOff zofs));
+          emit Psemi;
+          emit (store buf dstptr (AOff zofs));
+          remaining := Int64.sub !remaining size;
+          offset := Int64.add !offset size
+        end) in
+    begin
+      (if caml_sz_div16 >= 2L
+      then
+        begin
+          emit (Pmake (tmpbuf, (coqint_of_camlint64 caml_sz_div16)));
+          emit Psemi; 
+          let lbl = new_label() in
+          emit (Ploopdo (tmpbuf, lbl));
+          emit Psemi;
+          emit (Plq (tmpbuf2, srcptr, AOff Z.zero));
+          emit (Paddil (srcptr, srcptr, sixteen));
+          emit Psemi;
+          emit (Psq (tmpbuf2, dstptr, AOff Z.zero));
+          emit (Paddil (dstptr, dstptr, sixteen));
+          emit Psemi;
+          emit (Plabel lbl);
+          remaining := Int64.sub !remaining (Int64.shift_left caml_sz_div16 4)
+        end);
+    
+      cpy tmpbuf2 16L (fun x y z -> Plq(x, y, z)) (fun x y z -> Psq(x, y, z));
+      cpy tmpbuf 8L (fun x y z -> Pld(TRAP, x, y, z)) (fun x y z -> Psd(x, y, z));
+      cpy tmpbuf 4L (fun x y z -> Plw(TRAP, x, y, z)) (fun x y z -> Psw(x, y, z));
+      cpy tmpbuf 2L (fun x y z -> Plh(TRAP, x, y, z)) (fun x y z -> Psh(x, y, z));
+      cpy tmpbuf 1L (fun x y z -> Plb(TRAP, x, y, z)) (fun x y z -> Psb(x, y, z));
+      assert (!remaining = 0L)
+    end
+  else
+    begin
+      emit (Pmake (tmpbuf, sz));
+      emit Psemi; 
+      let lbl = new_label() in
+      emit (Ploopdo (tmpbuf, lbl));
+      emit Psemi;
+      emit (Plb (TRAP, tmpbuf, srcptr, AOff Z.zero));
+      emit (Paddil (srcptr, srcptr, Z.one));
+      emit Psemi;
+      emit (Psb (tmpbuf, dstptr, AOff Z.zero));
+      emit (Paddil (dstptr, dstptr, Z.one));
+      emit Psemi;
+      emit (Plabel lbl);
+    end;;
+  
+let expand_builtin_memcpy  sz al args =
+  match args with
+  | [dst; src] ->
+    expand_builtin_memcpy_big sz al src dst
+  | _ -> assert false;;
+
+(* Handling of volatile reads and writes *)
+(* FIXME probably need to check for size of displacement *)
+let expand_builtin_vload_common chunk base ofs res =
+  match chunk, res with
+  | Mint8unsigned, BR(Asmvliw.IR res) ->
+     emit (Plbu (TRAP, res, base, AOff ofs))
+  | Mint8signed, BR(Asmvliw.IR res) ->
+     emit (Plb  (TRAP, res, base, AOff ofs))
+  | Mint16unsigned, BR(Asmvliw.IR res) ->
+     emit (Plhu (TRAP, res, base, AOff ofs))
+  | Mint16signed, BR(Asmvliw.IR res) ->
+     emit (Plh  (TRAP, res, base, AOff ofs))
+  | Mint32, BR(Asmvliw.IR res) ->
+     emit (Plw  (TRAP, res, base, AOff ofs))
+  | Mint64, BR(Asmvliw.IR res) ->
+     emit (Pld  (TRAP, res, base, AOff ofs))
+  | Mint64, BR_splitlong(BR(Asmvliw.IR res1), BR(Asmvliw.IR res2)) ->
+     let ofs' = Integers.Ptrofs.add ofs _4 in
+     if base <> res2 then begin
+         emit (Plw (TRAP, res2, base, AOff ofs));
+         emit (Plw (TRAP, res1, base, AOff ofs'))
+       end else begin
+         emit (Plw (TRAP, res1, base, AOff ofs'));
+         emit (Plw (TRAP, res2, base, AOff ofs))
+       end
+  | Mfloat32, BR(Asmvliw.IR res) ->
+     emit (Pfls (TRAP, res, base, AOff ofs))
+  | Mfloat64, BR(Asmvliw.IR res) ->
+     emit (Pfld (TRAP, res, base, AOff ofs))
+  | _ ->
+     assert false
+
+let expand_builtin_vload chunk args res =
+  match args with
+  | [BA(Asmvliw.IR addr)] ->
+      expand_builtin_vload_common chunk addr _0 res
+  | [BA_addrstack ofs] ->
+     expand_builtin_vload_common chunk stack_pointer ofs res
+  | [BA_addptr(BA(Asmvliw.IR addr), (BA_int ofs | BA_long ofs))] ->
+     expand_builtin_vload_common chunk addr ofs res
+  | _ ->
+      assert false
+
+
+let expand_builtin_vstore_common chunk base ofs src =
+  match chunk, src with
+  | (Mint8signed | Mint8unsigned), BA(Asmvliw.IR src) ->
+     emit (Psb (src, base, AOff ofs))
+  | (Mint16signed | Mint16unsigned), BA(Asmvliw.IR src) ->
+     emit (Psh (src, base, AOff ofs))
+  | Mint32, BA(Asmvliw.IR src) ->
+     emit (Psw (src, base, AOff ofs))
+  | Mint64, BA(Asmvliw.IR src) ->
+     emit (Psd (src, base, AOff ofs))
+  | Mint64, BA_splitlong(BA(Asmvliw.IR src1), BA(Asmvliw.IR src2)) ->
+     let ofs' = Integers.Ptrofs.add ofs _4 in
+     emit (Psw (src2, base, AOff ofs));
+     emit (Psw (src1, base, AOff ofs'))
+  | Mfloat32, BA(Asmvliw.IR src) ->
+     emit (Pfss (src, base, AOff ofs))
+  | Mfloat64, BA(Asmvliw.IR src) ->
+     emit (Pfsd (src, base, AOff ofs))
+  | _ ->
+     assert false
+
+let expand_builtin_vstore chunk args =
+  match args with
+  | [BA(Asmvliw.IR addr); src] ->
+      expand_builtin_vstore_common chunk addr _0 src
+  | [BA_addrstack ofs; src] ->
+     expand_builtin_vstore_common chunk stack_pointer ofs src
+  | [BA_addptr(BA(Asmvliw.IR addr), (BA_int ofs | BA_long ofs)); src] ->
+     expand_builtin_vstore_common chunk addr ofs src
+  | _ ->
+      assert false
+
+(* Handling of varargs *)
+
+(* Size in words of the arguments to a function.  This includes both
+   arguments passed in registers and arguments passed on stack. *)
+
+let rec args_size sz = function
+  | [] -> sz
+  | (Tint | Tsingle | Tany32) :: l ->
+      args_size (sz + 1) l
+  | (Tlong | Tfloat | Tany64) :: l ->
+      args_size (if Archi.ptr64 then sz + 1 else align sz 2 + 2) l
+
+let arguments_size sg =
+  args_size 0 sg.sig_args
+
+let _nbregargs_ = 12
+let _alignment_ = 8
+
+let save_arguments first_reg base_ofs = let open Asmvliw in
+  for i = first_reg to (_nbregargs_ - 1) do begin
+    expand_storeind_ptr
+      int_param_regs.(i)
+      GPR12
+      (Integers.Ptrofs.repr (Z.add base_ofs (Z.of_uint ((i - first_reg) * wordsize))));
+    emit Psemi
+  end done
+
+let vararg_start_ofs : Z.t option ref = ref None
+
+let expand_builtin_va_start r = (* assert false *)
+match !vararg_start_ofs with
+  | None ->
+      invalid_arg "Fatal error: va_start used in non-vararg function"
+  | Some ofs ->
+      expand_addptrofs Asmvliw.GPR32 stack_pointer (Integers.Ptrofs.repr ofs);
+      emit Psemi;
+      expand_storeind_ptr Asmvliw.GPR32 r Integers.Ptrofs.zero
+
+(* Auxiliary for 64-bit integer arithmetic built-ins.  They expand to
+   two instructions, one computing the low 32 bits of the result,
+   followed by another computing the high 32 bits.  In cases where
+   the first instruction would overwrite arguments to the second
+   instruction, we must go through X31 to hold the low 32 bits of the result.
+*)
+
+let expand_int64_arith conflict rl fn = assert false
+(*if conflict then (fn X31; emit (Pmv(rl, X31))) else fn rl *)
+
+(* Byte swaps.  There are no specific instructions, so we use standard,
+   not-very-efficient formulas. *)
+
+let expand_bswap16 d s = let open Asmvliw in
+  (* d = (s & 0xFF) << 8 | (s >> 8) & 0xFF *)
+  emit (Pandiw(GPR32, s, coqint_of_camlint 0xFFl)); emit Psemi;
+  emit (Pslliw(GPR32, GPR32, _8)); emit Psemi;
+  emit (Psrliw(d, s, _8)); emit Psemi;
+  emit (Pandiw(d, d, coqint_of_camlint 0xFFl));
+  emit (Porw(d, GPR32, d)); emit Psemi
+
+let expand_bswap32 d s = let open Asmvliw in
+  (* d = (s << 24)
+       | (((s >> 8) & 0xFF) << 16)
+       | (((s >> 16) & 0xFF) << 8)
+       | (s >> 24)  *)
+  emit (Pslliw(GPR16, s, coqint_of_camlint 24l)); emit Psemi;
+  emit (Psrliw(GPR32, s, _8)); emit Psemi;
+  emit (Pandiw(GPR32, GPR32, coqint_of_camlint 0xFFl)); emit Psemi;
+  emit (Pslliw(GPR32, GPR32, _16)); emit Psemi;
+  emit (Porw(GPR16, GPR16, GPR31)); emit Psemi;
+  emit (Psrliw(GPR32, s, _16)); emit Psemi;
+  emit (Pandiw(GPR32, GPR32, coqint_of_camlint 0xFFl)); emit Psemi;
+  emit (Pslliw(GPR32, GPR32, _8)); emit Psemi;
+  emit (Porw(GPR16, GPR16, GPR32)); emit Psemi;
+  emit (Psrliw(GPR32, s, coqint_of_camlint 24l)); emit Psemi;
+  emit (Porw(d, GPR16, GPR32)); emit Psemi
+
+let expand_bswap64 d s = let open Asmvliw in
+  (* d = s << 56
+         | (((s >> 8) & 0xFF) << 48)
+         | (((s >> 16) & 0xFF) << 40)
+         | (((s >> 24) & 0xFF) << 32)
+         | (((s >> 32) & 0xFF) << 24)
+         | (((s >> 40) & 0xFF) << 16)
+         | (((s >> 48) & 0xFF) << 8)
+         | s >> 56 *)
+  emit (Psllil(GPR16, s, coqint_of_camlint 56l)); emit Psemi;
+  List.iter
+    (fun (n1, n2) ->
+      emit (Psrlil(GPR32, s, coqint_of_camlint n1)); emit Psemi;
+      emit (Pandil(GPR32, GPR32, coqint_of_camlint 0xFFl)); emit Psemi;
+      emit (Psllil(GPR32, GPR32, coqint_of_camlint n2)); emit Psemi;
+      emit (Porl(GPR16, GPR16, GPR32)); emit Psemi;)
+    [(8l,48l); (16l,40l); (24l,32l); (32l,24l); (40l,16l); (48l,8l)];
+  emit (Psrlil(GPR32, s, coqint_of_camlint 56l)); emit Psemi;
+  emit (Porl(d, GPR16, GPR32)); emit Psemi
+
+(* Handling of compiler-inlined builtins *)
+let last_system_register = 511l
+let not_system_register cn  =cn<0l || cn>last_system_register
+  
+let expand_builtin_inline name args res = let open Asmvliw in
+  match name, args, res with
+  (* Synchronization *)
+  | "__builtin_membar", [], _ ->
+     ()
+  (* Vararg stuff *)
+  | "__builtin_va_start", [BA(IR a)], _ ->
+     expand_builtin_va_start a
+  | "__builtin_clzll", [BA(IR a)], BR(IR res) ->
+     emit (Pclzll(res, a))
+  | "__builtin_kvx_stsud", [BA(IR a1); BA(IR a2)], BR(IR res) ->
+     emit (Pstsud(res, a1, a2))
+  | "__builtin_kvx_get", [BA_int(n)], BR(IR res) ->
+     let cn = camlint_of_coqint n in
+     (if not_system_register cn
+      then failwith (Printf.sprintf "__builtin_kvx_get(n): n must be between 0 and %ld, was %ld" last_system_register cn)
+      else emit (Pgetn(n, res)))
+  | "__builtin_kvx_set", [BA_int(n); BA(IR src)], _ ->
+     let cn = camlint_of_coqint n in
+     (if not_system_register cn
+      then failwith (Printf.sprintf "__builtin_kvx_set(n, val): n must be between 0 and %ld, was %ld" last_system_register cn)
+      else emit (Psetn(n, src)))
+  | "__builtin_kvx_wfxl", [BA_int(n); BA(IR src)], _ ->
+     let cn = camlint_of_coqint n in
+     (if not_system_register cn
+      then failwith (Printf.sprintf "__builtin_kvx_wfxl(n, val): n must be between 0 and %ld, was %ld" last_system_register cn)
+      else emit (Pwfxl(n, src)))
+  | "__builtin_kvx_wfxm", [BA_int(n); BA(IR src)], _ ->
+     let cn = camlint_of_coqint n in
+     (if not_system_register cn
+      then failwith (Printf.sprintf "__builtin_kvx_wfxm(n, val): n must be between 0 and %ld, was %ld" last_system_register cn)
+      else emit (Pwfxm(n, src)))
+  | "__builtin_kvx_ldu", [BA(IR addr)], BR(IR res) ->
+     emit (Pldu(res, addr))
+  | "__builtin_kvx_lbzu", [BA(IR addr)], BR(IR res) ->
+     emit (Plbzu(res, addr))
+  | "__builtin_kvx_lhzu", [BA(IR addr)], BR(IR res) ->
+     emit (Plhzu(res, addr))
+  | "__builtin_kvx_lwzu", [BA(IR addr)], BR(IR res) ->
+     emit (Plwzu(res, addr))
+  | "__builtin_kvx_alclrd", [BA(IR addr)], BR(IR res) ->
+     emit (Palclrd(res, addr))
+  | "__builtin_kvx_alclrw", [BA(IR addr)], BR(IR res) ->
+     emit (Palclrw(res, addr))
+  | "__builtin_kvx_await", [], _ ->
+     emit Pawait
+  | "__builtin_kvx_sleep", [], _ ->
+     emit Psleep
+  | "__builtin_kvx_stop", [], _ ->
+     emit Pstop
+  | "__builtin_kvx_barrier", [], _ ->
+     emit Pbarrier
+  | "__builtin_kvx_fence", [], _ ->
+     emit Pfence
+  | "__builtin_kvx_dinval", [], _ ->
+     emit Pdinval
+  | "__builtin_kvx_dinvall", [BA(IR addr)], _ ->
+     emit (Pdinvall addr)
+  | "__builtin_kvx_dtouchl", [BA(IR addr)], _ ->
+     emit (Pdtouchl addr)
+  | "__builtin_kvx_iinval", [], _ ->
+     emit Piinval
+  | "__builtin_kvx_iinvals", [BA(IR addr)], _ ->
+     emit (Piinvals addr)
+  | "__builtin_kvx_itouchl", [BA(IR addr)], _ ->
+     emit (Pitouchl addr)
+  | "__builtin_kvx_dzerol", [BA(IR addr)], _ ->
+     emit (Pdzerol addr)
+(*| "__builtin_kvx_afaddd", [BA(IR addr); BA (IR incr_res)], BR(IR res) ->
+     (if res <> incr_res
+      then (emit (Asm.Pmv(res, incr_res)); emit Psemi));
+     emit (Pafaddd(addr, res))
+  | "__builtin_kvx_afaddw", [BA(IR addr); BA (IR incr_res)], BR(IR res) ->
+     (if res <> incr_res
+      then (emit (Asm.Pmv(res, incr_res)); emit Psemi));
+     emit (Pafaddw(addr, res)) *) (* see #157 *)
+  | "__builtin_alclrd", [BA(IR addr)], BR(IR res) ->
+     emit (Palclrd(res, addr))
+  | "__builtin_alclrw", [BA(IR addr)], BR(IR res) ->
+     emit (Palclrw(res, addr))
+  | "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
+     expand_bswap16 res a1
+  | ("__builtin_bswap"| "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
+     expand_bswap32 res a1
+  | "__builtin_bswap64", [BA(IR src)], BR(IR res) ->
+     expand_bswap64 res src
+	  
+  (* Byte swaps *)
+(*| "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
+     expand_bswap16 res a1
+  | "__builtin_fabs",  [BA(FR a1)], BR(FR res) ->
+     emit (Pfabsd(res, a1))
+*)
+  (* Catch-all *)
+  | _ ->
+     raise (Error ("unrecognized builtin " ^ name))
+
+(* Expansion of instructions *)
+
+let expand_instruction instr =
+  match instr with
+  | Pallocframe (sz, ofs) ->
+      let sg = get_current_function_sig() in
+      emit (Pmv (Asmvliw.GPR17, stack_pointer));
+      if sg.sig_cc.cc_vararg then begin
+        let n = arguments_size sg in
+        let extra_sz = if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) in
+        let full_sz = Z.add sz (Z.of_uint extra_sz) in
+        expand_addptrofs stack_pointer stack_pointer (Integers.Ptrofs.repr (Z.neg full_sz));
+        emit Psemi;
+        expand_storeind_ptr Asmvliw.GPR17 stack_pointer ofs;
+        emit Psemi;
+        let va_ofs =
+          let extra_ofs = if n <= _nbregargs_ then 0 else ((n - _nbregargs_) * wordsize) in
+          Z.add sz (Z.of_sint extra_ofs) in
+        vararg_start_ofs := Some va_ofs;
+        save_arguments n va_ofs
+      end else begin
+        let below = Integers.Ptrofs.repr (Z.neg sz) in
+        expand_addptrofs stack_pointer stack_pointer below;
+        emit Psemi; (* Psemi required to fit in resource constraints *)
+        expand_storeind_ptr stack_pointer stack_pointer (Integers.Ptrofs.add ofs below);
+        vararg_start_ofs := None
+      end
+  | Pfreeframe (sz, ofs) ->
+     let sg = get_current_function_sig() in
+     let extra_sz =
+      if sg.sig_cc.cc_vararg then begin
+        let n = arguments_size sg in
+        if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize)
+      end else 0 in
+     expand_addptrofs stack_pointer stack_pointer (Integers.Ptrofs.repr (Z.add sz (Z.of_uint extra_sz)))
+
+(*| Pseqw(rd, rs1, rs2) ->
+      (* emulate based on the fact that x == 0 iff x <u 1 (unsigned cmp) *)
+      if rs2 = X0 then begin
+        emit (Psltiuw(rd, rs1, Int.one))
+      end else begin
+        emit (Pxorw(rd, rs1, rs2)); emit (Psltiuw(rd, X rd, Int.one))
+      end
+  | Psnew(rd, rs1, rs2) ->
+      (* emulate based on the fact that x != 0 iff 0 <u x (unsigned cmp) *)
+      if rs2 = X0 then begin
+        emit (Psltuw(rd, X0, rs1))
+      end else begin
+        emit (Pxorw(rd, rs1, rs2)); emit (Psltuw(rd, X0, X rd))
+      end
+  | Pseql(rd, rs1, rs2) ->
+      (* emulate based on the fact that x == 0 iff x <u 1 (unsigned cmp) *)
+      if rs2 = X0 then begin
+        emit (Psltiul(rd, rs1, Int64.one))
+      end else begin
+        emit (Pxorl(rd, rs1, rs2)); emit (Psltiul(rd, X rd, Int64.one))
+      end
+  | Psnel(rd, rs1, rs2) ->
+      (* emulate based on the fact that x != 0 iff 0 <u x (unsigned cmp) *)
+      if rs2 = X0 then begin
+        emit (Psltul(rd, X0, rs1))
+      end else begin
+        emit (Pxorl(rd, rs1, rs2)); emit (Psltul(rd, X0, X rd))
+      end
+*)| Pcvtl2w (rd, rs) ->
+      assert Archi.ptr64;
+      emit (Paddiw (rd, rs, Integers.Int.zero))  (* 32-bit sign extension *)
+
+(*| Pjal_r(r, sg) ->
+      fixup_call sg; emit instr
+  | Pjal_s(symb, sg) ->
+      fixup_call sg; emit instr
+  | Pj_r(r, sg) when r <> X1 ->
+      fixup_call sg; emit instr
+  | Pj_s(symb, sg) ->
+      fixup_call sg; emit instr
+
+*)| Pbuiltin (ef,args,res) ->
+     begin match ef with
+     | EF_builtin (name,sg) ->
+        expand_builtin_inline (camlstring_of_coqstring name) args res
+     | EF_vload chunk ->
+        expand_builtin_vload chunk args res
+     | EF_vstore chunk ->
+        expand_builtin_vstore chunk args
+(*     | EF_annot_val (kind,txt,targ) ->
+        expand_annot_val kind txt targ args res *)
+     | EF_memcpy(sz, al) ->
+        expand_builtin_memcpy sz al args
+ (*  | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
+        emit instr
+    *)
+     | EF_malloc -> failwith "asmexpand: malloc"
+     | EF_free -> failwith "asmexpand: free"
+     | EF_debug _ -> failwith "asmexpand: debug"
+     | EF_annot _ -> emit instr
+     | EF_annot_val (kind, txt, targ) -> expand_annot_val kind txt targ args res
+     | EF_external _ -> failwith "asmexpand: external"
+     | EF_inline_asm _ -> emit instr
+     | EF_runtime _ -> failwith "asmexpand: runtime"
+     | EF_profiling _ -> emit instr
+     end
+  | _ ->
+     emit instr
+
+(* NOTE: Dwarf register maps for RV32G are not yet specified
+   officially.  This is just a placeholder.  *)
+let int_reg_to_dwarf = let open Asmvliw in function
+   | GPR0  -> 1   | GPR1  -> 2   | GPR2  -> 3   | GPR3  -> 4   | GPR4  -> 5
+   | GPR5  -> 6   | GPR6  -> 7   | GPR7  -> 8   | GPR8  -> 9   | GPR9  -> 10
+   | GPR10 -> 11  | GPR11 -> 12  | GPR12 -> 13  | GPR13 -> 14  | GPR14 -> 15
+   | GPR15 -> 16  | GPR16 -> 17  | GPR17 -> 18  | GPR18 -> 19  | GPR19 -> 20
+   | GPR20 -> 21  | GPR21 -> 22  | GPR22 -> 23  | GPR23 -> 24  | GPR24 -> 25
+   | GPR25 -> 26  | GPR26 -> 27  | GPR27 -> 28  | GPR28 -> 29  | GPR29 -> 30
+   | GPR30 -> 31  | GPR31 -> 32  | GPR32 -> 33  | GPR33 -> 34  | GPR34 -> 35
+   | GPR35 -> 36  | GPR36 -> 37  | GPR37 -> 38  | GPR38 -> 39  | GPR39 -> 40
+   | GPR40 -> 41  | GPR41 -> 42  | GPR42 -> 43  | GPR43 -> 44  | GPR44 -> 45
+   | GPR45 -> 46  | GPR46 -> 47  | GPR47 -> 48  | GPR48 -> 49  | GPR49 -> 50
+   | GPR50 -> 51  | GPR51 -> 52  | GPR52 -> 53  | GPR53 -> 54  | GPR54 -> 55
+   | GPR55 -> 56  | GPR56 -> 57  | GPR57 -> 58  | GPR58 -> 59  | GPR59 -> 60
+   | GPR60 -> 61  | GPR61 -> 62  | GPR62 -> 63  | GPR63 -> 64
+
+let preg_to_dwarf = let open Asmvliw in function
+   | IR r -> int_reg_to_dwarf r
+   | RA   -> 65 (* FIXME - No idea what is $ra DWARF number in k1-gdb *)
+   | _ -> assert false
+
+let expand_function id fn =
+  try
+    set_current_function fn;
+    expand id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code;
+    Errors.OK (get_current_function ())
+  with Error s ->
+    Errors.Error (Errors.msg (coqstring_of_camlstring s))
+
+let expand_fundef id = function
+  | Internal f ->
+      begin match expand_function id f with
+      | Errors.OK tf -> Errors.OK (Internal tf)
+      | Errors.Error msg -> Errors.Error msg
+      end
+  | External ef ->
+      Errors.OK (External ef)
+
+let expand_program (p: Asm.program) : Asm.program Errors.res =
+  AST.transform_partial_program2 expand_fundef (fun id v -> Errors.OK v) p