further riscv rmem integration.

14 files changed, 293 insertions, 371 deletions

diff --git a/risc-v/Makefile b/risc-v/Makefile
index 2f6af138..856a48eb 100644
--- a/risc-v/Makefile
+++ b/risc-v/Makefile
@@ -1,13 +1,13 @@
 
 SAIL:=../src/sail.native
-
+SOURCES:=riscv.sail ../etc/regfp.sail riscv_regfp.sail
 all: lem_ast shallow
 
-lem_ast: riscv.sail $(SAIL)
-	$(SAIL) -lem_ast $<
+lem_ast: $(SOURCES) $(SAIL)
+	$(SAIL) -lem_ast $(SOURCES)
 
-shallow: riscv.sail $(SAIL)
-	$(SAIL) -lem_lib Riscv_extras_embed -lem $<
+shallow: $(SOURCES) $(SAIL)
+	$(SAIL) -lem_lib Riscv_extras_embed -lem $(SOURCES)
 
 clean:
 	rm -f riscv.lem riscv_embed*.lem
diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index ee7cb3e1..62e7cf4b 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -1,4 +1,3 @@
-| `RISCVThreadStart
 | `RISCVUTYPE of bit20 * reg * riscvUop
 | `RISCVJAL   of bit20 * reg
 | `RISCVJALR  of bit12 * reg * reg
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
index e614b714..ac6f22bd 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -1,122 +1,57 @@
-(*| `MIPSThreadStart ->
-    SYSCALL_THREAD_START
-
-| `MIPSStopFetching ->
-    ImplementationDefinedStopFetching0
-
-(* Note different argument order, which reflects difference
-   between instruction encoding and asm format  *)
-| `MIPSRType (op, rd, rs, rt) ->
-    (translate_rtype_op op)
-      (
+| `RISCVStopFetching -> EBREAK
+| `RISCVUTYPE(imm, rd, op) -> UTYPE(
+      translate_imm20 "imm" imm,
+      translate_reg "rd" rd,
+      translate_uop op)
+| `RISCVJAL(imm, rd) -> JAL0(
+      translate_imm20 "imm" imm,
+      translate_reg "rd" rd)
+| `RISCVJALR(imm, rs, rd) -> JALR0(
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rd,
+      translate_reg "rd" rd)
+| `RISCVBType(imm, rs2, rs1, op) -> BTYPE(
+      translate_imm12 "imm" imm,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_bop op)
+| `RISCVIType(imm, rs1, rd, op) -> ITYPE(
+      translate_imm12 "imm" imm,
+      translate_reg "rs1" rs1,
+      translate_reg "rd" rd,
+      translate_iop op)
+| `RISCVShiftIop(imm, rs, rd, op) -> SHIFTIOP(
+      translate_imm6 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd,
+      translate_sop op)
+| `RISCVRType (rs2, rs1, rd, op) -> RTYPE (
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_reg "rd" rd,
+      translate_rop op)
+| `RISCVLoad(imm, rs, rd, unsigned, width) -> LOAD(
+      translate_imm12 "imm" imm,
       translate_reg "rs" rs,
-      translate_reg "rt" rt,
-      translate_reg "rd" rd
-       )
-      
-
-(* Note different argument order similar to above *)
-| `MIPSIType (op, rt, rs, imm) ->
-    (translate_itype_op op)
-      (
+      translate_reg "rd" rd,
+      translate_bool "unsigned" unsigned,
+      translate_wordWidth width)
+| `RISCVStore(imm, rs, rd, width) -> STORE (
+      translate_imm12 "imm" imm,
       translate_reg "rs" rs,
-      translate_reg "rt" rt,
-      translate_imm16 "imm" imm
-       )
-      
-
-| `MIPSShiftI (op, rd, rt, sa) ->
-    (translate_shifti_op op)
-      (
-      translate_reg "rt" rt,
       translate_reg "rd" rd,
-      translate_imm5 "sa" sa
-       )
-      
-
-| `MIPSShiftV (op, rd, rt, rs) ->
-    (translate_shiftv_op op)
-      (
+      translate_wordWidth width)
+| `RISCVADDIW(imm, rs, rd) -> ADDIW(
+      translate_imm12 "imm" imm,
       translate_reg "rs" rs,
-      translate_reg "rt" rt,
-      translate_reg "rd" rd
-      )
-      
-
-| `MIPSMulDiv (op, rs, rt) ->
-    (translate_muldiv_op op)
-      (
+      translate_reg "rd" rd)
+| `RISCVSHIFTW(imm, rs, rd, op) -> SHIFTW(
+      translate_imm5 "imm" imm,
       translate_reg "rs" rs,
-      translate_reg "rt" rt
-      )
-      
-
-| `MIPSMFHiLo (op, rs) ->
-    (translate_mfhilo_op op)
-      (
-      translate_reg "rs" rs
-      )
-      
-| `MIPSLUI (rt, imm) ->
-  LUI
-      (
-      translate_reg "rt" rt,
-      translate_imm16 "imm" imm
-      )
-      
-| `MIPSLoad (width, signed, linked, base, rt, offset) ->
-  Load
-      (
-      translate_wordsize "width" width,
-      translate_bool "signed" signed,
-      translate_bool "linked" linked,
-      translate_reg "base" base,
-      translate_reg "rt" rt,
-      translate_imm16 "offset" offset
-      )
-      
-| `MIPSStore (width, conditional, base, rt, offset) ->
-  Store
-      (
-      translate_wordsize "width" width,
-      translate_bool "conditional" conditional,
-      translate_reg "base" base,
-      translate_reg "rt" rt,
-      translate_imm16 "offset" offset
-      )
-      
-| `MIPSLSLR (store, double, left, base, rt, offset) ->
-  (translate_lslr_op store double left)
-      (
-      translate_reg "base" base,
-      translate_reg "rt" rt,
-      translate_imm16 "offset" offset
-      )
-      
-| `MIPSSYNC -> SYNC
-| `MIPSBEQ (rs, rt, offset, ne, likely) ->
-  BEQ
-  (translate_reg "rs" rs,
-   translate_reg "rt" rt,
-   translate_imm16 "offset" offset,
-   translate_bool "ne" ne,
-   translate_bool "likely" likely
-   ) 
-
-| `MIPSBCMPZ (rs, offset, cmp, link, likely) ->
-  BCMPZ
-  (translate_reg "rs" rs,
-   translate_imm16 "offset" offset,
-   translate_cmp "cmp" cmp,
-   translate_bool "link" link,
-   translate_bool "likely" likely
-   ) 
-| `MIPSJ (offset) ->
-  J (translate_imm26 "offset" offset) 
-| `MIPSJAL (offset) ->
-  JAL (translate_imm26 "offset" offset) 
-| `MIPSJR(rd) ->
-  JR (translate_reg "rd" rd) 
-| `MIPSJALR(rd, rs) ->
-  JALR (translate_reg "rd" rd, translate_reg "rs" rs) 
-*)
\ No newline at end of file
+      translate_reg "rd" rd,
+      translate_sop op)
+| `RISCVRTYPEW(rs2, rs1, rd, op) -> RTYPEW(
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_reg "rd" rd,
+      translate_ropw op)
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
index 1c925e2b..c4a1fd37 100644
--- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -1,121 +1,71 @@
 let is_inc = false
-(*
-let translate_rtype_op op  = uppercase (pp_rtype_op op)
 
-let translate_rtype_op op x = match op with
-  | MIPSROpADD    -> ADD x
-  | MIPSROpADDU   -> ADDU x
-  | MIPSROpAND    -> AND x
-  | MIPSROpDADD   -> DADD x
-  | MIPSROpDADDU  -> DADDU x
-  | MIPSROpDSUB   -> DSUB x
-  | MIPSROpDSUBU  -> DSUBU x
-  | MIPSROpMOVN   -> MOVN x
-  | MIPSROpMOVZ   -> MOVZ x
-  | MIPSROpMUL    -> MUL x
-  | MIPSROpNOR    -> NOR x
-  | MIPSROpOR     -> OR x
-  | MIPSROpSLT    -> SLT x 
-  | MIPSROpSLTU   -> SLTU x
-  | MIPSROpSUB    -> SUB x
-  | MIPSROpSUBU   -> SUBU x
-  | MIPSROpXOR    -> XOR x
-
-let translate_itype_op op x = match op with
-  | MIPSIOpADDI   -> ADDI x
-  | MIPSIOpADDIU  -> ADDIU x
-  | MIPSIOpANDI   -> ANDI x
-  | MIPSIOpDADDI  -> DADDI x
-  | MIPSIOpDADDIU -> DADDIU x
-  | MIPSIOpORI    -> ORI x
-  | MIPSIOpSLTI   -> SLTI x
-  | MIPSIOpSLTIU  -> SLTIU x
-  | MIPSIOpXORI   -> XORI x
-
-let translate_shifti_op op x = match op with
-  | MIPSDSLL   -> DSLL x 
-  | MIPSDSLL32 -> DSLL32 x
-  | MIPSDSRA   -> DSRA x
-  | MIPSDSRA32 -> DSRA32 x
-  | MIPSDSRL   -> DSRL x
-  | MIPSDSRL32 -> DSRL32 x
-  | MIPSSLL    -> SLL x
-  | MIPSSRA    -> SRA x 
-  | MIPSSRL    -> SRL x 
-
-let translate_shiftv_op op x = match op with
-  | MIPSDSLLV -> DSLLV x
-  | MIPSDSRAV -> DSRAV x
-  | MIPSDSRLV -> DSRLV x
-  | MIPSSLLV  -> SLLV x 
-  | MIPSSRAV  -> SRAV x 
-  | MIPSSRLV  -> SRLV x 
-
-let translate_muldiv_op op x = match op with
-  | MIPSDDIV   -> DDIV x  
-  | MIPSDDIVU  -> DDIVU x 
-  | MIPSDIV    -> DIV x   
-  | MIPSDIVU   -> DIVU x  
-  | MIPSDMULT  -> DMULT x 
-  | MIPSDMULTU -> DMULTU x
-  | MIPSMADD   -> MADD x  
-  | MIPSMADDU  -> MADDU x 
-  | MIPSMSUB   -> MSUB x  
-  | MIPSMSUBU  -> MSUBU x 
-  | MIPSMULT   -> MULT x  
-  | MIPSMULTU  -> MULTU x 
-
-let translate_mfhilo_op op x = match op with
-  | MIPSMFHI -> MFHI x
-  | MIPSMFLO -> MFLO x
-  | MIPSMTHI -> MTHI x
-  | MIPSMTLO -> MTLO x
-
-let translate_load_op width signed linked = uppercase (pp_load_op width signed linked)
+let translate_reg name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int (reg_to_int value))
 
-let translate_store_op width conditional  = uppercase (pp_store_op width conditional)
+let translate_uop op = match op with
+  | RISCVLUI   -> LUI0
+  | RISCVAUIPC -> AUIPC
+
+let translate_bop op = match op with
+  | RISCVBEQ  -> BEQ0
+  | RISCVBNE  -> BNE
+  | RISCVBLT  -> BLT
+  | RISCVBGE  -> BGE
+  | RISCVBLTU -> BLTU
+  | RISCVBGEU -> BGEU
+
+let translate_iop op = match op with
+  | RISCVADDI  -> ADDI0 
+  | RISCVSLTI  -> SLTI0
+  | RISCVSLTIU -> SLTIU0
+  | RISCVXORI  -> XORI0
+  | RISCVORI   -> ORI0
+  | RISCVANDI  -> ANDI0
+
+let translate_sop op = match op with
+  | RISCVSLLI -> SLLI
+  | RISCVSRLI -> SRLI
+  | RISCVSRAI -> SRAI
+
+let translate_rop op = match op with
+  | RISCVADD  -> ADD0 
+  | RISCVSUB  -> SUB0 
+  | RISCVSLL  -> SLL0 
+  | RISCVSLT  -> SLT0 
+  | RISCVSLTU -> SLTU0
+  | RISCVXOR  -> XOR0 
+  | RISCVSRL  -> SRL0 
+  | RISCVSRA  -> SRA0 
+  | RISCVOR   -> OR0  
+  | RISCVAND  -> AND0 
+
+let translate_ropw op = match op with
+  | RISCVADDW -> ADDW 
+  | RISCVSUBW -> SUBW 
+  | RISCVSLLW -> SLLW 
+  | RISCVSRLW -> SRLW 
+  | RISCVSRAW -> SRAW 
+
+let translate_wordWidth op = match op with
+  | RISCVBYTE   -> BYTE  
+  | RISCVHALF   -> HALF  
+  | RISCVWORD   -> WORD  
+  | RISCVDOUBLE -> DOUBLE
 
-let translate_lslr_op store double left x = match (store,double,left) with
-  | (false, false, true ) -> LWL x
-  | (false, false, false) -> LWR x
-  | (false, true , true ) -> LDL x
-  | (false, true , false) -> LDR x
-  | (true , false, true ) -> SWL x
-  | (true , false, false) -> SWR x
-  | (true , true , true ) -> SDL x
-  | (true , true , false) -> SDR x
+let translate_bool name = function
+  | true -> Sail_values.B1
+  | false -> Sail_values.B0
 
-let translate_beq_op ne likely            = uppercase (pp_beq_op ne likely)
 
-let translate_bcmpz_op cmp link likely    = uppercase (pp_bcmpz_op cmp link likely)
+let translate_imm20 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 20,Nat_big_num.of_int value)
 
+let translate_imm12 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 12,Nat_big_num.of_int value)
 
-let translate_reg name value = 
-    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int (reg_to_int value))
+let translate_imm6 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 6,Nat_big_num.of_int value)
 
-let translate_imm26 name value = 
-    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 26,Nat_big_num.of_int value)
-let translate_imm16 name value = 
-    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 16,Nat_big_num.of_int value)
 let translate_imm5 name value = 
     Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value)
-let translate_bool name = function
-  | true -> Sail_values.B1
-  | false -> Sail_values.B0
-
-let translate_wordsize _ = function
- | MIPSByte -> Mips_embed_types.B2
- | MIPSHalf -> Mips_embed_types.H
- | MIPSWord -> Mips_embed_types.W
- | MIPSDouble -> Mips_embed_types.D
-
-let translate_cmp _ = function
-  | MIPS_EQ  -> EQ'
-  | MIPS_NE  -> NE
-  | MIPS_GE  -> GE
-  | MIPS_GEU -> GEU
-  | MIPS_GT  -> GT'
-  | MIPS_LE  -> LE
-  | MIPS_LT  -> LT'
-  | MIPS_LTU -> LTU
-*)
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
index a75eef9f..75d890e4 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -1,8 +1,8 @@
-"lwu"   , UTYPE { op=RSICVLUI   };
-"auipc" , UTYPE { op=RSICVAUIPC };
+"lwu"   , UTYPE { op=RISCVLUI   };
+"auipc" , UTYPE { op=RISCVAUIPC };
 
-"jal",  JAL;
-"jalr", JALR;
+"jal",  JAL ();
+"jalr", JALR ();
 
 "beq",  BTYPE {op=RISCVBEQ};
 "bne",  BTYPE {op=RISCVBNE};
@@ -12,7 +12,7 @@
 "bgeu", BTYPE {op=RISCVBGEU};
 
 "addi",  ITYPE {op=RISCVADDI};
-"stli",  ITYPE {op=RISCVSTLI};
+"stli",  ITYPE {op=RISCVSLTI};
 "sltiu", ITYPE {op=RISCVSLTIU};
 "xori",  ITYPE {op=RISCVXORI};
 "ori",   ITYPE {op=RISCVORI};
@@ -33,24 +33,24 @@
 "or",   RTYPE{op=RISCVOR};
 "and",  RTYPE{op=RISCVAND};
 
-"lb",  LOAD{unsigned=false; width=RISCBYTE};
-"lbu", LOAD{unsigned=true;  width=RISCBYTE};
+"lb",  LOAD{unsigned=false; width=RISCVBYTE};
+"lbu", LOAD{unsigned=true;  width=RISCVBYTE};
 "lh",  LOAD{unsigned=false; width=RISCVHALF};
 "lhu", LOAD{unsigned=true;  width=RISCVHALF};
 "lw",  LOAD{unsigned=false; width=RISCVWORD};
 "lwu", LOAD{unsigned=true;  width=RISCVWORD};
 "ld",  LOAD{unsigned=false; width=RISCVDOUBLE};
 
-"sb", STORE{width=RISCBYTE};
+"sb", STORE{width=RISCVBYTE};
 "sh", STORE{width=RISCVHALF};
 "sw", STORE{width=RISCVWORD};
 "sd", STORE{width=RISCVDOUBLE};
 
-"addiw", ADDIW;
+"addiw", ADDIW ();
 
-"slliw", SHIFTW{op=RISCVSLL};
-"srliw", SHIFTW{op=RISCVSRL};
-"sraiw", SHIFTW{op=RISCVSRA};
+"slliw", SHIFTW{op=RISCVSLLI};
+"srliw", SHIFTW{op=RISCVSRLI};
+"sraiw", SHIFTW{op=RISCVSRAI};
 
 "addw", RTYPEW{op=RISCVADDW};
 "subw", RTYPEW{op=RISCVSUBW};
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index ba4dcac7..abd87c7f 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -1,5 +1,5 @@
 | UTYPE reg COMMA NUM
-  { `RISCVUTYPE($4, $2, $1.o) }
+  { `RISCVUTYPE($4, $2, $1.op) }
 | JAL reg COMMA NUM
   { `RISCVJAL($4, $2) }
 | JALR reg COMMA reg COMMA NUM
@@ -7,15 +7,15 @@
 | BTYPE reg COMMA reg COMMA NUM
   { `RISCVBType($6, $4, $2, $1.op) }
 | ITYPE reg COMMA reg COMMA NUM
-  { `RISCVIType(o$6, $4, $2, $1.op) }
+  { `RISCVIType($6, $4, $2, $1.op) }
 | SHIFTIOP reg COMMA reg COMMA NUM
   { `RISCVShiftIop($6, $4, $2, $1.op) }
 | RTYPE reg COMMA reg COMMA reg
-  { `RISCVRType ($6, $3, $2, $1.op) }
+  { `RISCVRType ($6, $4, $2, $1.op) }
 | LOAD reg COMMA NUM LPAR reg RPAR
   { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width) }
 | STORE reg COMMA NUM LPAR reg RPAR
-  { `RISCVStore($4, $6, $2, $1.width) } (* reg order? *)
+  { `RISCVStore($4, $6, $2, $1.width) }
 | ADDIW reg COMMA reg COMMA NUM
   { `RISCVADDIW ($6, $4, $2) }
 | SHIFTW reg COMMA reg COMMA NUM
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index f8cb0e30..0587c321 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -1,3 +1,5 @@
+| `RISCVThreadStart               -> "start"
+| `RISCVStopFetching              -> "stop"
 | `RISCVUTYPE(imm, rd, op)        -> sprintf "%s %s, %d" (pp_riscv_uop op) (pp_reg rd) imm
 | `RISCVJAL(imm, rd)              -> sprintf "jal  %s, %d" (pp_reg rd) imm
 | `RISCVJALR(imm, rs, rd)         -> sprintf "jalr %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index 8064aa19..7f1ae8ea 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -1,3 +1,4 @@
+| ("EBREAK", [])                  -> `RISCVStopFetching
 | ("UTYPE", [imm; rd; op])        -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
 | ("JAL", [imm; rd])              -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg  rd)
 | ("JALR", [imm; rs; rd])         -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index 9473d011..9dc80a98 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -1,99 +1,13 @@
-(*| SYSCALL_THREAD_START -> `MIPSThreadStart
-| (ADD    (rs, rt, rd)) -> `MIPSRType (MIPSROpADD   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (ADDU   (rs, rt, rd)) -> `MIPSRType (MIPSROpADDU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (AND    (rs, rt, rd)) -> `MIPSRType (MIPSROpAND   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (DADD   (rs, rt, rd)) -> `MIPSRType (MIPSROpDADD  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (DADDU  (rs, rt, rd)) -> `MIPSRType (MIPSROpDADDU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (DSUB   (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUB  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (DSUBU  (rs, rt, rd)) -> `MIPSRType (MIPSROpDSUBU , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (MOVN   (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVN  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (MOVZ   (rs, rt, rd)) -> `MIPSRType (MIPSROpMOVZ  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (MUL    (rs, rt, rd)) -> `MIPSRType (MIPSROpMUL   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (NOR    (rs, rt, rd)) -> `MIPSRType (MIPSROpNOR   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (OR     (rs, rt, rd)) -> `MIPSRType (MIPSROpOR    , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (SLT    (rs, rt, rd)) -> `MIPSRType (MIPSROpSLT   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (SLTU   (rs, rt, rd)) -> `MIPSRType (MIPSROpSLTU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (SUB    (rs, rt, rd)) -> `MIPSRType (MIPSROpSUB   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (SUBU   (rs, rt, rd)) -> `MIPSRType (MIPSROpSUBU  , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-| (XOR    (rs, rt, rd)) -> `MIPSRType (MIPSROpXOR   , (translate_out_ireg rd), (translate_out_ireg rs), (translate_out_ireg rt))
-
-| (ADDI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
-| (ADDIU  (rs, rt, imm)) -> `MIPSIType (MIPSIOpADDIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
-| (ANDI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpANDI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
-| (DADDI  (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDI ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
-| (DADDIU (rs, rt, imm)) -> `MIPSIType (MIPSIOpDADDIU,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
-| (ORI    (rs, rt, imm)) -> `MIPSIType (MIPSIOpORI   ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
-| (SLTI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
-| (SLTIU  (rs, rt, imm)) -> `MIPSIType (MIPSIOpSLTIU ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_simm16 imm))
-| (XORI   (rs, rt, imm)) -> `MIPSIType (MIPSIOpXORI  ,(translate_out_ireg rt), (translate_out_ireg rs), (translate_out_imm16 imm))
-
-| (DSLL    (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
-| (DSLL32  (rt, rd, sa)) -> `MIPSShiftI (MIPSDSLL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
-| (DSRA    (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
-| (DSRA32  (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRA32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
-| (DSRL    (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL   , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
-| (DSRL32  (rt, rd, sa)) -> `MIPSShiftI (MIPSDSRL32 , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
-| (SLL     (rt, rd, sa)) -> `MIPSShiftI (MIPSSLL    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
-| (SRA     (rt, rd, sa)) -> `MIPSShiftI (MIPSSRA    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
-| (SRL     (rt, rd, sa)) -> `MIPSShiftI (MIPSSRL    , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_imm5 sa))
-
-| DSLLV  (rs, rt, rd) -> `MIPSShiftV (MIPSDSLLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
-| DSRAV  (rs, rt, rd) -> `MIPSShiftV (MIPSDSRAV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
-| DSRLV  (rs, rt, rd) -> `MIPSShiftV (MIPSDSRLV , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
-| SLLV   (rs, rt, rd) -> `MIPSShiftV (MIPSSLLV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
-| SRAV   (rs, rt, rd) -> `MIPSShiftV (MIPSSRAV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
-| SRLV   (rs, rt, rd) -> `MIPSShiftV (MIPSSRLV  , (translate_out_ireg rd), (translate_out_ireg rt), (translate_out_ireg rs))
-
-| DDIV   (rs, rt) -> `MIPSMulDiv (MIPSDDIV   , (translate_out_ireg rs), (translate_out_ireg rt))
-| DDIVU  (rs, rt) -> `MIPSMulDiv (MIPSDDIVU  , (translate_out_ireg rs), (translate_out_ireg rt))
-| DIV    (rs, rt) -> `MIPSMulDiv (MIPSDIV    , (translate_out_ireg rs), (translate_out_ireg rt))
-| DIVU   (rs, rt) -> `MIPSMulDiv (MIPSDIVU   , (translate_out_ireg rs), (translate_out_ireg rt))
-| DMULT  (rs, rt) -> `MIPSMulDiv (MIPSDMULT  , (translate_out_ireg rs), (translate_out_ireg rt))
-| DMULTU (rs, rt) -> `MIPSMulDiv (MIPSDMULTU , (translate_out_ireg rs), (translate_out_ireg rt))
-| MADD   (rs, rt) -> `MIPSMulDiv (MIPSMADD   , (translate_out_ireg rs), (translate_out_ireg rt))
-| MADDU  (rs, rt) -> `MIPSMulDiv (MIPSMADDU  , (translate_out_ireg rs), (translate_out_ireg rt))
-| MSUB   (rs, rt) -> `MIPSMulDiv (MIPSMSUB   , (translate_out_ireg rs), (translate_out_ireg rt))
-| MSUBU  (rs, rt) -> `MIPSMulDiv (MIPSMSUBU  , (translate_out_ireg rs), (translate_out_ireg rt))
-| MULT   (rs, rt) -> `MIPSMulDiv (MIPSMULT   , (translate_out_ireg rs), (translate_out_ireg rt))
-| MULTU  (rs, rt) -> `MIPSMulDiv (MIPSMULTU  , (translate_out_ireg rs), (translate_out_ireg rt))
-
-| MFHI  (rs)  -> `MIPSMFHiLo (MIPSMFHI, (translate_out_ireg rs))
-| MFLO  (rs)  -> `MIPSMFHiLo (MIPSMFLO, (translate_out_ireg rs))
-| MTHI  (rs)  -> `MIPSMFHiLo (MIPSMTHI, (translate_out_ireg rs))
-| MTLO  (rs)  -> `MIPSMFHiLo (MIPSMTLO, (translate_out_ireg rs))
-
-| LUI  (rt, imm) -> `MIPSLUI ((translate_out_ireg rt), (translate_out_imm16 imm))
-| Load (width, signed, linked, base, rt, offset) ->
-  `MIPSLoad (
-     (translate_out_wordWidth width), 
-     (translate_out_bool signed),
-     (translate_out_bool linked),
-     (translate_out_ireg  base),
-     (translate_out_ireg  rt),
-     (translate_out_simm16 offset)
-   )
-| Store (width, conditional, base, rt, offset) ->
-  `MIPSStore (
-     (translate_out_wordWidth width), 
-     (translate_out_bool conditional),
-     (translate_out_ireg  base),
-     (translate_out_ireg  rt),
-     (translate_out_simm16  offset)
-   )
-| LWL (base, rt, offset) -> `MIPSLSLR (false, false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
-| LWR (base, rt, offset) -> `MIPSLSLR (false, false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
-| LDL (base, rt, offset) -> `MIPSLSLR (false, true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
-| LDR (base, rt, offset) -> `MIPSLSLR (false, true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
-| SWL (base, rt, offset) -> `MIPSLSLR (true , false, true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
-| SWR (base, rt, offset) -> `MIPSLSLR (true , false, false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
-| SDL (base, rt, offset) -> `MIPSLSLR (true , true , true , (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
-| SDR (base, rt, offset) -> `MIPSLSLR (true , true , false, (translate_out_ireg base), (translate_out_ireg rt), (translate_out_simm16 offset))
-| SYNC -> `MIPSSYNC
-| BEQ (rs, rt, offset, ne, likely) -> `MIPSBEQ ((translate_out_ireg rs), (translate_out_ireg rt), (translate_out_simm16 offset), (translate_out_bool ne), (translate_out_bool likely))
-| BCMPZ (rs, offset, cmp, link, likely) -> `MIPSBCMPZ ((translate_out_ireg rs), (translate_out_simm16 offset), (translate_out_cmp cmp), (translate_out_bool link), (translate_out_bool likely))
-| J (offset) -> `MIPSJ (translate_out_imm26 offset)
-| JAL (offset) -> `MIPSJAL (translate_out_imm26 offset)
-| JR (rd) -> `MIPSJR (translate_out_ireg rd)
-| JALR (rd, rs) -> `MIPSJALR (translate_out_ireg rd, translate_out_ireg rs)
-
-*)
\ No newline at end of file
+| EBREAK                      -> `RISCVStopFetching
+| UTYPE( imm, rd, op)         -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
+| JAL0( imm, rd)              -> `RISCVJAL(translate_out_simm20 imm, translate_out_ireg  rd)
+| JALR0( imm, rs, rd)         -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| BTYPE( imm, rs2, rs1, op)   -> `RISCVBType(translate_out_simm12 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
+| ITYPE( imm, rs1, rd, op)    -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
+| SHIFTIOP( imm, rs, rd, op)  -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| RTYPE( rs2, rs1, rd, op)    -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
+| LOAD( imm, rs, rd, unsigned, width) -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width)
+| STORE( imm, rs, rd, width)  -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width)
+| ADDIW( imm, rs, rd)         -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| SHIFTW( imm, rs, rd, op)    -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| RTYPEW( rs2, rs1, rd, op)   -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
index 2c2efd8e..d635efde 100644
--- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -1,4 +1,4 @@
-(*let translate_out_big_bit = Sail_values.unsigned
+let translate_out_big_bit = Sail_values.unsigned
 
 let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
 let translate_out_signed_int inst bits = 
@@ -9,32 +9,62 @@ let translate_out_signed_int inst bits =
 
 let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
 
-let translate_out_imm26 imm = translate_out_int imm
+let translate_out_uop op = match op with
+  | LUI0  -> RISCVLUI  
+  | AUIPC -> RISCVAUIPC
 
-let translate_out_imm16 imm = translate_out_int imm
-let translate_out_simm16 imm = translate_out_signed_int imm 16
+let translate_out_bop op = match op with
+  | BEQ0 -> RISCVBEQ 
+  | BNE  -> RISCVBNE 
+  | BLT  -> RISCVBLT 
+  | BGE  -> RISCVBGE 
+  | BLTU -> RISCVBLTU
+  | BGEU -> RISCVBGEU
 
-let translate_out_imm5 imm = translate_out_int imm
+let translate_out_iop op = match op with
+  | ADDI0  -> RISCVADDI 
+  | SLTI0  -> RISCVSLTI 
+  | SLTIU0 -> RISCVSLTIU
+  | XORI0  -> RISCVXORI 
+  | ORI0   -> RISCVORI  
+  | ANDI0  -> RISCVANDI 
+
+let translate_out_sop op = match op with
+  | SLLI -> RISCVSLLI
+  | SRLI -> RISCVSRLI
+  | SRAI -> RISCVSRAI
+
+let translate_out_rop op = match op with
+  | ADD0  -> RISCVADD 
+  | SUB0  -> RISCVSUB 
+  | SLL0  -> RISCVSLL 
+  | SLT0  -> RISCVSLT 
+  | SLTU0 -> RISCVSLTU
+  | XOR0  -> RISCVXOR 
+  | SRL0  -> RISCVSRL 
+  | SRA0  -> RISCVSRA 
+  | OR0   -> RISCVOR  
+  | AND0  -> RISCVAND 
+
+let translate_out_ropw op = match op with
+  | ADDW  -> RISCVADDW
+  | SUBW  -> RISCVSUBW
+  | SLLW  -> RISCVSLLW
+  | SRLW  -> RISCVSRLW
+  | SRAW  -> RISCVSRAW
+
+let translate_out_wordWidth op = match op with
+  | BYTE   -> RISCVBYTE  
+  | HALF   -> RISCVHALF  
+  | WORD   -> RISCVWORD  
+  | DOUBLE -> RISCVDOUBLE
 
 let translate_out_bool = function
   | Sail_values.B1  -> true
   | Sail_values.B0 -> false
   | _ -> failwith "translate_out_bool Undef"
 
-
-let translate_out_wordWidth = function
-    | Mips_embed_types.B2 -> MIPSByte
-    | Mips_embed_types.H -> MIPSHalf
-    | Mips_embed_types.W -> MIPSWord
-    | Mips_embed_types.D -> MIPSDouble
-
-let translate_out_cmp = function
-    | Mips_embed_types.EQ' -> MIPS_EQ  (* equal *)
-    | Mips_embed_types.NE -> MIPS_NE  (* not equal *)
-    | Mips_embed_types.GE -> MIPS_GE  (* signed greater than or equal *)
-    | Mips_embed_types.GEU -> MIPS_GEU (* unsigned greater than or equal *) 
-    | Mips_embed_types.GT' -> MIPS_GT  (* signed strictly greater than *) 
-    | Mips_embed_types.LE -> MIPS_LE  (* signed less than or equal *) 
-    | Mips_embed_types.LT' -> MIPS_LT  (* signed strictly less than *) 
-    | Mips_embed_types.LTU -> MIPS_LTU (* unsigned less than or qual *) 
-*)
\ No newline at end of file
+let translate_out_simm20 imm = translate_out_signed_int imm 20
+let translate_out_simm12 imm = translate_out_signed_int imm 12
+let translate_out_imm6 imm = translate_out_int imm
+let translate_out_imm5 imm = translate_out_int imm
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index 3b825af2..fd51c81f 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -1,3 +1,4 @@
+| `RISCVStopFetching       -> ("EBREAK", [], [])
 | `RISCVUTYPE(imm, rd, op) -> 
     ("UTYPE",
       [
@@ -68,7 +69,7 @@
     ],
     [])
 | `RISCVStore(imm, rs, rd, width) -> 
-   ("LOAD",
+   ("STORE",
     [
       translate_imm12 "imm" imm;
       translate_reg "rs" rs;
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen
index 99d3d375..e034cf37 100644
--- a/risc-v/hgen/types_sail_trans_out.hgen
+++ b/risc-v/hgen/types_sail_trans_out.hgen
@@ -44,6 +44,7 @@ let translate_out_bop op = match translate_out_enum op with
 | 3 -> RISCVBGE 
 | 4 -> RISCVBLTU
 | 5 -> RISCVBGEU
+| _ -> failwith "Unknown bop in sail translate out"
 
 let translate_out_iop op = match translate_out_enum op with
 | 0 -> RISCVADDI 
@@ -52,11 +53,13 @@ let translate_out_iop op = match translate_out_enum op with
 | 3 -> RISCVXORI 
 | 4 -> RISCVORI  
 | 5 -> RISCVANDI 
+| _ -> failwith "Unknown iop in sail translate out"
 
 let translate_out_sop op = match translate_out_enum op with 
 | 0 -> RISCVSLLI
 | 1 -> RISCVSRLI
 | 2 -> RISCVSRAI
+| _ -> failwith "Unknown sop in sail translate out"
 
 let translate_out_rop op = match translate_out_enum op with
 | 0 -> RISCVADD 
@@ -69,6 +72,7 @@ let translate_out_rop op = match translate_out_enum op with
 | 7 -> RISCVSRA 
 | 8 -> RISCVOR  
 | 9 -> RISCVAND 
+| _ -> failwith "Unknown rop in sail translate out"
 
 let translate_out_ropw op = match translate_out_enum op with
 | 0 -> RISCVADDW
@@ -76,3 +80,4 @@ let translate_out_ropw op = match translate_out_enum op with
 | 2 -> RISCVSLLW
 | 3 -> RISCVSRLW
 | 4 -> RISCVSRAW
+| _ -> failwith "Unknown ropw in sail translate out"
\ No newline at end of file
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index c91a0104..5234d128 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -281,6 +281,10 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
   } in
   wGPR(rd, EXTS(result))
 
+union ast member unit EBREAK
+function clause decode (0b000000000001 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(EBREAK ())
+function clause execute EBREAK = { exit () }
+
 function clause decode _ = None
 
 end ast
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
new file mode 100644
index 00000000..1dff5064
--- /dev/null
+++ b/risc-v/riscv_regfp.sail
@@ -0,0 +1,81 @@
+let (vector <0, 32, inc, string >) GPRstr =
+  [ "x0", "x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8", "x9", "x10",
+  "x11", "x12", "x13", "x14", "x15", "x16", "x17", "x18", "x19", "x20",
+  "x21", "x22", "x23", "x24", "x25", "x26", "x27", "x28", "x29", "x30", "x31"
+  ]
+
+let CIA_fp = RFull("CIA")
+let NIA_fp = RFull("NIA")
+
+function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (instr) = {
+  iR := [|| ||];
+  oR := [|| ||];
+  aR := [|| ||];
+  ik := IK_simple;
+  Nias := [|| NIAFP_successor ||];
+  Dia := DIAFP_none;
+
+  switch instr {
+     case (EBREAK) -> ()
+     case (UTYPE ( imm, rd, op)) -> {
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+     }
+     case (JAL ( imm, rd)) -> {
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+            let (bit[64]) offset = EXTS(imm) in
+            Nias := [|| NIAFP_concrete_address (PC + offset) ||]
+     }
+     case (JALR ( imm, rs, rd)) -> {
+            if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+            let (bit[64]) offset = EXTS(imm) in
+            Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||];
+     }
+     case (BTYPE ( imm, rs2, rs1, op)) -> {
+            if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR;
+            if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
+            ik := IK_cond_branch;
+            let (bit[64]) offset = EXTS(imm) in
+            Nias := NIAFP_concrete_address(PC + offset) :: Nias;
+     }
+     case (ITYPE ( imm, rs, rd, op)) -> {
+            if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+     }
+     case (SHIFTIOP ( imm, rs, rd, op)) -> {
+            if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+     }
+     case (RTYPE ( rs2, rs1, rd, op)) -> {
+            if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR;
+            if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+     }
+     case (LOAD ( imm, rs, rd, unsign, width)) -> { (* XXX "unsigned" causes name conflict in lem shallow embedding... *)
+            if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+            aR := iR;
+            ik := IK_mem_read (Read_plain);
+     }
+     case (STORE( imm, rs2, rs1, width)) -> {
+            if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR;
+            if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
+            if (rs1 == 0) then () else aR := RFull(GPRstr[rs1]) :: aR;
+            ik := IK_mem_write (Write_plain);
+     }
+     case (ADDIW ( imm, rs, rd)) -> {
+            if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+     }
+     case (SHIFTW ( imm, rs, rd, op)) -> {
+            if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+     } 
+     case (RTYPEW ( rs2, rs1, rd, op))-> {
+            if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR;
+            if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+     }
+  };
+  (iR,oR,aR,Nias,Dia,ik)
+}