Merge remote-tracking branch 'origin' into mono-experiments

# Conflicts:
#	src/type_internal.ml

36 files changed, 1128 insertions, 110 deletions

diff --git a/.merlin b/.merlin
new file mode 100644
index 00000000..d76ab020
--- /dev/null
+++ b/.merlin
@@ -0,0 +1,8 @@
+S src
+S src/contrib/**
+S src/gen_lib/**
+S src/lem_interp/**
+S src/pprint/**
+S src/test/**
+B src/_build/**
+PKG num str unix uint zarith
\ No newline at end of file
diff --git a/mips/hgen/regs_out_in.hgen b/mips/hgen/regs_out_in.hgen
deleted file mode 100644
index 8e1fd093..00000000
--- a/mips/hgen/regs_out_in.hgen
+++ /dev/null
@@ -1,5 +0,0 @@
-(* for each instruction instance, identify the role of the registers
-   and possible branching: (outputs, inputs, voidstars, branch) *)
-
-| `MIPSAdd ->
-      ([], [], [], [Next])
diff --git a/risc-v/Makefile b/risc-v/Makefile
new file mode 100644
index 00000000..856a48eb
--- /dev/null
+++ b/risc-v/Makefile
@@ -0,0 +1,13 @@
+
+SAIL:=../src/sail.native
+SOURCES:=riscv.sail ../etc/regfp.sail riscv_regfp.sail
+all: lem_ast shallow
+
+lem_ast: $(SOURCES) $(SAIL)
+	$(SAIL) -lem_ast $(SOURCES)
+
+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
new file mode 100644
index 00000000..8983b5ae
--- /dev/null
+++ b/risc-v/hgen/ast.hgen
@@ -0,0 +1,13 @@
+| `RISCVUTYPE of bit20 * reg * riscvUop
+| `RISCVJAL   of bit20 * reg
+| `RISCVJALR  of bit12 * reg * reg
+| `RISCVBType of bit12 * reg * reg * riscvBop
+| `RISCVIType of bit12 * reg * reg * riscvIop
+| `RISCVShiftIop of bit6 * reg * reg * riscvSop
+| `RISCVRType of reg * reg * reg * riscvRop
+| `RISCVLoad of bit12 * reg * reg * bool * wordWidth
+| `RISCVStore of bit12 * reg * reg * wordWidth
+| `RISCVADDIW of bit12 * reg * reg
+| `RISCVSHIFTW of bit5 * reg * reg * riscvSop
+| `RISCVRTYPEW of reg * reg * reg * riscvRopw
+| `RISCVFENCE of bit4 * bit4
diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen
new file mode 100644
index 00000000..03318805
--- /dev/null
+++ b/risc-v/hgen/fold.hgen
@@ -0,0 +1,13 @@
+| `RISCVThreadStart               -> (y_reg, y_sreg)
+| `RISCVUTYPE (_, r0, _)          -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJAL (_, r0)               -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJALR (_, r0, r1)          -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVBType (_, r0, r1, _)      -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVIType (_, r0, r1, _)      -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVShiftIop (_, r0, r1, _)   -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRType (r0, r1, r2, _)     -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
+| `RISCVLoad (_, r0, r1, _, _)    -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVStore (_, r0, r1, _)      -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVADDIW (_, r0, r1)         -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVSHIFTW (_, r0, r1, _)     -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRTYPEW (r0, r1, r2, _)    -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
new file mode 100644
index 00000000..50026612
--- /dev/null
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -0,0 +1,60 @@
+| `RISCVStopFetching -> EBREAK
+| `RISCVUTYPE(imm, rd, op) -> UTYPE(
+      translate_imm20 "imm" imm,
+      translate_reg "rd" rd,
+      translate_uop op)
+| `RISCVJAL(imm, rd) -> JAL0(
+      translate_imm21 "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_imm13 "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 "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 "rd" rd,
+      translate_wordWidth width)
+| `RISCVADDIW(imm, rs, rd) -> ADDIW(
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd)
+| `RISCVSHIFTW(imm, rs, rd, op) -> SHIFTW(
+      translate_imm5 "imm" imm,
+      translate_reg "rs" rs,
+      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)
+| `RISCVFENCE(pred, succ) -> FENCE(
+  translate_imm4 "pred" pred,
+  translate_imm4 "succ" succ)
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
new file mode 100644
index 00000000..4d8bd87a
--- /dev/null
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -0,0 +1,79 @@
+let is_inc = false
+
+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_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_bool name = function
+  | true -> Sail_values.B1
+  | false -> Sail_values.B0
+
+let translate_imm21 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 21,Nat_big_num.of_int value)
+
+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_imm13 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 13,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_imm6 name value = 
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 6,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_imm4 name value =
+    Sail_values.to_vec0 is_inc (Nat_big_num.of_int 4,Nat_big_num.of_int value)
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
new file mode 100644
index 00000000..5f2c8326
--- /dev/null
+++ b/risc-v/hgen/lexer.hgen
@@ -0,0 +1,64 @@
+"lui"   , UTYPE { op=RISCVLUI   };
+"auipc" , UTYPE { op=RISCVAUIPC };
+
+"jal",  JAL ();
+"jalr", JALR ();
+
+"beq",  BTYPE {op=RISCVBEQ};
+"bne",  BTYPE {op=RISCVBNE};
+"blt",  BTYPE {op=RISCVBLT};
+"bge",  BTYPE {op=RISCVBGE};
+"bltu", BTYPE {op=RISCVBLTU};
+"bgeu", BTYPE {op=RISCVBGEU};
+
+"addi",  ITYPE {op=RISCVADDI};
+"stli",  ITYPE {op=RISCVSLTI};
+"sltiu", ITYPE {op=RISCVSLTIU};
+"xori",  ITYPE {op=RISCVXORI};
+"ori",   ITYPE {op=RISCVORI};
+"andi",  ITYPE {op=RISCVANDI};
+
+"slli", SHIFTIOP{op=RISCVSLLI};
+"srli", SHIFTIOP{op=RISCVSRLI};
+"srai", SHIFTIOP{op=RISCVSRAI};
+
+"add",  RTYPE{op=RISCVADD};
+"sub",  RTYPE{op=RISCVSUB};
+"sll",  RTYPE{op=RISCVSLL};
+"slt",  RTYPE{op=RISCVSLT};
+"sltu", RTYPE{op=RISCVSLT};
+"xor",  RTYPE{op=RISCVXOR};
+"srl",  RTYPE{op=RISCVSRL};
+"sra",  RTYPE{op=RISCVSRA};
+"or",   RTYPE{op=RISCVOR};
+"and",  RTYPE{op=RISCVAND};
+
+"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=RISCVBYTE};
+"sh", STORE{width=RISCVHALF};
+"sw", STORE{width=RISCVWORD};
+"sd", STORE{width=RISCVDOUBLE};
+
+"addiw", ADDIW ();
+
+"slliw", SHIFTW{op=RISCVSLLI};
+"srliw", SHIFTW{op=RISCVSRLI};
+"sraiw", SHIFTW{op=RISCVSRAI};
+
+"addw", RTYPEW{op=RISCVADDW};
+"subw", RTYPEW{op=RISCVSUBW};
+"sslw", RTYPEW{op=RISCVSLLW};
+"srlw", RTYPEW{op=RISCVSRLW};
+"sraw", RTYPEW{op=RISCVSRAW};
+
+"fence", FENCE ();
+"r",  FENCEOPTION Fence_R;
+"w",  FENCEOPTION Fence_W;
+"rw", FENCEOPTION Fence_RW;
diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen
new file mode 100644
index 00000000..ff14c428
--- /dev/null
+++ b/risc-v/hgen/map.hgen
@@ -0,0 +1,12 @@
+| `RISCVUTYPE (x, r0, y)          -> `RISCVUTYPE (x, map_reg r0, y)
+| `RISCVJAL (x, r0)               -> `RISCVJAL (x, map_reg r0)
+| `RISCVJALR (x, r0, r1)          -> `RISCVJALR (x, map_reg r0, map_reg r1)
+| `RISCVBType (x, r0, r1, y)      -> `RISCVBType (x, map_reg r0, map_reg r1, y)
+| `RISCVIType (x, r0, r1, y)      -> `RISCVIType (x, map_reg r0, map_reg r1, y)
+| `RISCVShiftIop (x, r0, r1, y)   -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y)
+| `RISCVRType (r0, r1, r2, y)     -> `RISCVRType (r0, map_reg r1, map_reg r2, y)
+| `RISCVLoad (x, r0, r1, y, z)    -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z)
+| `RISCVStore (x, r0, r1, y)      -> `RISCVStore (x, map_reg r0, map_reg r1, y)
+| `RISCVADDIW (x, r0, r1)         -> `RISCVADDIW (x, map_reg r0, map_reg r1)
+| `RISCVSHIFTW (x, r0, r1, y)     -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y)
+| `RISCVRTYPEW (r0, r1, r2, x)    -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x)
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
new file mode 100644
index 00000000..37fd8d8d
--- /dev/null
+++ b/risc-v/hgen/parser.hgen
@@ -0,0 +1,36 @@
+| UTYPE reg COMMA NUM
+  { `RISCVUTYPE($4, $2, $1.op) }
+| JAL reg COMMA NUM
+  { `RISCVJAL($4, $2) }
+| JALR reg COMMA reg COMMA NUM
+  { `RISCVJALR($6, $4, $2) }
+| BTYPE reg COMMA reg COMMA NUM
+  { `RISCVBType($6, $4, $2, $1.op) }
+| ITYPE reg COMMA reg COMMA NUM
+  { `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, $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, $2, $6, $1.width) }
+| ADDIW reg COMMA reg COMMA NUM
+  { `RISCVADDIW ($6, $4, $2) }
+| SHIFTW reg COMMA reg COMMA NUM
+  { `RISCVSHIFTW ($6, $4, $2, $1.op) }
+| RTYPEW reg COMMA reg COMMA reg
+  { `RISCVRTYPEW ($6, $4, $2, $1.op) }
+| FENCE FENCEOPTION COMMA FENCEOPTION
+  { match ($2, $4) with
+    | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011)
+    | (Fence_R,  Fence_RW) -> `RISCVFENCE (0b0010, 0b0011)
+    | (Fence_RW, Fence_W)  -> `RISCVFENCE (0b0011, 0b0001)
+    | (Fence_RW, Fence_R)  -> failwith "'fence rw,r' is not supported"
+    | (Fence_R,  Fence_R)  -> failwith "'fence r,r' is not supported"
+    | (Fence_R,  Fence_W)  -> failwith "'fence r,w' is not supported"
+    | (Fence_W,  Fence_RW) -> failwith "'fence w,rw' is not supported"
+    | (Fence_W,  Fence_R)  -> failwith "'fence w,r' is not supported"
+    | (Fence_W,  Fence_W)  -> failwith "'fence w,w' is not supported"
+  }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
new file mode 100644
index 00000000..1da3ef11
--- /dev/null
+++ b/risc-v/hgen/pretty.hgen
@@ -0,0 +1,15 @@
+| `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
+| `RISCVBType(imm, rs2, rs1, op)  -> sprintf "%s %s, %s, %d" (pp_riscv_bop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVIType(imm, rs2, rs1, op)  -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRType (rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
+| `RISCVLoad(imm, rs, rd, unsigned, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width)) (pp_reg rd) imm (pp_reg rs)
+| `RISCVStore(imm, rs2, rs1, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rs2) imm (pp_reg rs1)
+| `RISCVADDIW(imm, rs, rd)        -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
+| `RISCVSHIFTW(imm, rs, rd, op)   -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRTYPEW(rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
+| `RISCVFENCE(pred, succ)         -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ)
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
new file mode 100644
index 00000000..dca5bea1
--- /dev/null
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -0,0 +1,14 @@
+| ("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_simm21 imm, translate_out_ireg  rd)
+| ("JALR", [imm; rs; rd])         -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| ("BTYPE", [imm; rs2; rs1; op])  -> `RISCVBType(translate_out_simm13 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)
+| ("FENCE", [pred; succ])         -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
new file mode 100644
index 00000000..6158ebd7
--- /dev/null
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -0,0 +1,14 @@
+| 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_simm21 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_simm13 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)
+| FENCE( pred, succ)          -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
new file mode 100644
index 00000000..a891d7d0
--- /dev/null
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -0,0 +1,73 @@
+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 = 
+    let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+    if (i >= (1 lsl (bits - 1))) then
+    (i - (1 lsl bits)) else
+    i
+
+let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_uop op = match op with
+  | LUI0  -> RISCVLUI  
+  | AUIPC -> RISCVAUIPC
+
+let translate_out_bop op = match op with
+  | BEQ0 -> RISCVBEQ 
+  | BNE  -> RISCVBNE 
+  | BLT  -> RISCVBLT 
+  | BGE  -> RISCVBGE 
+  | BLTU -> RISCVBLTU
+  | BGEU -> RISCVBGEU
+
+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_simm21 imm = translate_out_signed_int imm 21
+let translate_out_simm20 imm = translate_out_signed_int imm 20
+let translate_out_simm13 imm = translate_out_signed_int imm 13
+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
+let translate_out_imm4 imm = translate_out_int imm
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
new file mode 100644
index 00000000..2980b985
--- /dev/null
+++ b/risc-v/hgen/token_types.hgen
@@ -0,0 +1,15 @@
+type token_UTYPE    = {op : riscvUop }
+type token_JAL      = unit
+type token_JALR     = unit
+type token_BType    = {op : riscvBop }
+type token_IType    = {op : riscvIop }
+type token_ShiftIop = {op : riscvSop }
+type token_RTYPE    = {op : riscvRop }
+type token_Load     = {unsigned: bool; width : wordWidth }
+type token_Store    = {width : wordWidth }
+type token_ADDIW    = unit
+type token_SHIFTW   = {op : riscvSop }
+type token_RTYPEW   = {op : riscvRopw }
+type token_FENCE    = unit
+
+type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
new file mode 100644
index 00000000..f952cf77
--- /dev/null
+++ b/risc-v/hgen/tokens.hgen
@@ -0,0 +1,14 @@
+%token <RISCVHGenBase.token_UTYPE>    UTYPE   
+%token <RISCVHGenBase.token_JAL>      JAL     
+%token <RISCVHGenBase.token_JALR>     JALR    
+%token <RISCVHGenBase.token_BType>    BTYPE   
+%token <RISCVHGenBase.token_IType>    ITYPE   
+%token <RISCVHGenBase.token_ShiftIop> SHIFTIOP
+%token <RISCVHGenBase.token_RTYPE>    RTYPE   
+%token <RISCVHGenBase.token_Load>     LOAD    
+%token <RISCVHGenBase.token_Store>    STORE   
+%token <RISCVHGenBase.token_ADDIW>    ADDIW   
+%token <RISCVHGenBase.token_SHIFTW>   SHIFTW  
+%token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
+%token <RISCVHGenBase.token_FENCE>    FENCE
+%token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
new file mode 100644
index 00000000..df22d9dc
--- /dev/null
+++ b/risc-v/hgen/trans_sail.hgen
@@ -0,0 +1,112 @@
+| `RISCVStopFetching       -> ("EBREAK", [], [])
+| `RISCVUTYPE(imm, rd, op) -> 
+    ("UTYPE",
+      [
+      translate_imm20 "imm" imm;
+      translate_reg "rd" rd;
+      translate_uop "op" op;
+       ],
+      [])
+| `RISCVJAL(imm, rd) -> 
+   ("JAL",
+    [
+      translate_imm21 "imm" imm;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVJALR(imm, rs, rd) -> 
+   ("JALR",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rd;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVBType(imm, rs2, rs1, op)  -> 
+   ("BTYPE",
+    [
+      translate_imm13 "imm" imm;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_bop "op" op;
+    ],
+    [])
+| `RISCVIType(imm, rs1, rd, op)  -> 
+   ("ITYPE",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_iop "op" op;
+    ],
+    [])
+| `RISCVShiftIop(imm, rs, rd, op) -> 
+   ("SHIFTIOP",
+    [
+      translate_imm6 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_sop "op" op;
+    ],
+    [])
+| `RISCVRType (rs2, rs1, rd, op)  -> 
+   ("RTYPE",
+    [
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_rop "op" op;
+    ],
+    [])
+| `RISCVLoad(imm, rs, rd, unsigned, width) -> 
+   ("LOAD",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_bool "unsigned" unsigned;
+      translate_width "width" width;
+    ],
+    [])
+| `RISCVStore(imm, rs2, rs1, width) -> 
+   ("STORE",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+    ],
+    [])
+| `RISCVADDIW(imm, rs, rd)        -> 
+   ("ADDIW",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVSHIFTW(imm, rs, rd, op)   -> 
+   ("SHIFTW",
+    [
+      translate_imm5 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_sop "op" op;
+    ],
+    [])
+| `RISCVRTYPEW(rs2, rs1, rd, op)  -> 
+   ("RTYPEW",
+    [
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_ropw "op" op;
+    ],
+    [])
+| `RISCVFENCE(pred, succ) ->
+  ("FENCE", 
+  [
+     translate_imm4 "pred" pred;
+     translate_imm4 "succ" succ;
+  ], 
+  [])
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
new file mode 100644
index 00000000..87fc9b95
--- /dev/null
+++ b/risc-v/hgen/types.hgen
@@ -0,0 +1,123 @@
+type bit20 = int
+type bit12 = int
+type bit6  = int
+type bit5  = int
+type bit4  = int
+
+type riscvUop =  (* upper immediate ops *)
+| RISCVLUI
+| RISCVAUIPC
+
+let pp_riscv_uop = function
+| RISCVLUI   -> "lui"
+| RISCVAUIPC -> "auipc"
+
+
+type riscvBop =  (* branch ops *)
+| RISCVBEQ 
+| RISCVBNE
+| RISCVBLT
+| RISCVBGE
+| RISCVBLTU
+| RISCVBGEU
+
+let pp_riscv_bop = function
+| RISCVBEQ  -> "beq"
+| RISCVBNE  -> "bne"
+| RISCVBLT  -> "blt"
+| RISCVBGE  -> "bge"
+| RISCVBLTU -> "bltu"
+| RISCVBGEU -> "bgeu"
+
+type riscvIop = (* immediate ops *)
+| RISCVADDI
+| RISCVSLTI
+| RISCVSLTIU
+| RISCVXORI
+| RISCVORI
+| RISCVANDI
+
+let pp_riscv_iop = function
+| RISCVADDI  -> "addi"
+| RISCVSLTI  -> "slti"
+| RISCVSLTIU -> "sltiu"
+| RISCVXORI  -> "xori"
+| RISCVORI   -> "ori"
+| RISCVANDI  -> "andi"
+
+type riscvSop = (* shift ops *)
+| RISCVSLLI
+| RISCVSRLI
+| RISCVSRAI
+
+let pp_riscv_sop = function
+| RISCVSLLI -> "slli"
+| RISCVSRLI -> "srli"
+| RISCVSRAI -> "srai"
+
+type riscvRop = (* reg-reg ops *)
+| RISCVADD
+| RISCVSUB
+| RISCVSLL
+| RISCVSLT 
+| RISCVSLTU
+| RISCVXOR
+| RISCVSRL
+| RISCVSRA
+| RISCVOR
+| RISCVAND
+
+let pp_riscv_rop = function
+| RISCVADD  -> "add"
+| RISCVSUB  -> "sub"
+| RISCVSLL  -> "sll"
+| RISCVSLT  -> "slt"
+| RISCVSLTU -> "sltu"
+| RISCVXOR  -> "xor"
+| RISCVSRL  -> "srl"
+| RISCVSRA  -> "sra"
+| RISCVOR   -> "or"
+| RISCVAND  -> "and"
+
+type riscvRopw = (* reg-reg 32-bit ops *)
+| RISCVADDW
+| RISCVSUBW
+| RISCVSLLW
+| RISCVSRLW
+| RISCVSRAW
+
+let pp_riscv_ropw = function
+| RISCVADDW -> "addw"
+| RISCVSUBW -> "subw"
+| RISCVSLLW -> "sllw"
+| RISCVSRLW -> "srlw"
+| RISCVSRAW -> "sraw"
+
+type wordWidth = 
+  | RISCVBYTE
+  | RISCVHALF
+  | RISCVWORD
+  | RISCVDOUBLE
+
+let pp_riscv_load_op (unsigned, width) = match (unsigned, width) with
+  | (false, RISCVBYTE)    -> "lb"
+  | (true,  RISCVBYTE)    -> "lbu"
+  | (false, RISCVHALF)    -> "lh"
+  | (true,  RISCVHALF)    -> "lhu"
+  | (false, RISCVWORD)    -> "lw"
+  | (true,  RISCVWORD)    -> "lwu"
+  | (_, RISCVDOUBLE)      -> "ld"
+  | _                          -> failwith "unexpected load op"
+
+let pp_riscv_store_op width = match width with
+| RISCVBYTE -> "sb"
+| RISCVHALF -> "sh"
+| RISCVWORD -> "sw"
+| RISCVDOUBLE -> "sd"
+| _ -> failwith "unexpected store op"
+
+let pp_riscv_fence_option = function
+  | 0b0011 -> "rw"
+  | 0b0010 -> "r"
+  | 0b0001 -> "w"
+  | _ -> failwith "unexpected fence option"
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen
new file mode 100644
index 00000000..e22110d0
--- /dev/null
+++ b/risc-v/hgen/types_sail_trans_out.hgen
@@ -0,0 +1,86 @@
+let translate_out_big_bit = function
+  | (name, Bvector _, bits) -> IInt.integer_of_bit_list bits
+  | _ -> assert false
+
+let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
+let translate_out_signed_int inst bits = 
+    let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+    if (i >= (1 lsl (bits - 1))) then
+    (i - (1 lsl bits)) else
+    i
+
+let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_simm21 imm = translate_out_signed_int imm 21
+let translate_out_simm20 imm = translate_out_signed_int imm 20
+let translate_out_simm13 imm = translate_out_signed_int imm 13
+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
+let translate_out_imm4 imm = translate_out_int imm
+
+let translate_out_bool = function
+  | (name, Bit, [Bitc_one])  -> true
+  | (name, Bit, [Bitc_zero]) -> false
+  | _ -> assert false
+
+let translate_out_enum (name,_,bits) =
+    Nat_big_num.to_int (IInt.integer_of_bit_list bits)
+
+let translate_out_wordWidth w = 
+    match translate_out_enum w with
+    | 0 -> RISCVBYTE
+    | 1 -> RISCVHALF
+    | 2 -> RISCVWORD
+    | 3 -> RISCVDOUBLE
+    | _ -> failwith "Unknown wordWidth in sail translate out"
+
+let translate_out_uop op = match translate_out_enum op with
+    | 0 -> RISCVLUI
+    | 1 -> RISCVAUIPC
+    | _ -> failwith "Unknown uop in sail translate out"
+
+let translate_out_bop op = match translate_out_enum op with
+| 0 -> RISCVBEQ 
+| 1 -> RISCVBNE 
+| 2 -> RISCVBLT 
+| 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 
+| 1 -> RISCVSLTI 
+| 2 -> RISCVSLTIU
+| 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 
+| 1 -> RISCVSUB 
+| 2 -> RISCVSLL 
+| 3 -> RISCVSLT 
+| 4 -> RISCVSLTU
+| 5 -> RISCVXOR 
+| 6 -> RISCVSRL 
+| 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
+| 1 -> RISCVSUBW
+| 2 -> RISCVSLLW
+| 3 -> RISCVSRLW
+| 4 -> RISCVSRAW
+| _ -> failwith "Unknown ropw in sail translate out"
diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen
new file mode 100644
index 00000000..1bf174fa
--- /dev/null
+++ b/risc-v/hgen/types_trans_sail.hgen
@@ -0,0 +1,39 @@
+let translate_enum enum_values name value =
+  let rec bit_count n =
+    if n = 0 then 0
+    else 1 + (bit_count (n lsr 1)) in
+  let rec find_index element = function
+    | h::tail -> if h = element then 0 else 1 + (find_index element tail)
+    | _ -> failwith "translate_enum could not find value"
+    in
+  let size = bit_count (List.length enum_values) in
+  let index = find_index value enum_values in
+  (name, Range0 (Some size),  IInt.bit_list_of_integer size (Nat_big_num.of_int index))
+
+let translate_uop = translate_enum [RISCVLUI; RISCVAUIPC]
+let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *)
+let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *)
+let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *)
+let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *)
+let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *)
+let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] 
+let translate_reg name value = 
+    (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value)))
+let translate_imm21 name value = 
+    (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value))
+let translate_imm20 name value = 
+    (name, Bvector (Some 20), bit_list_of_integer 20 (Nat_big_num.of_int value))
+let translate_imm16 name value = 
+    (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value))
+let translate_imm13 name value = 
+    (name, Bvector (Some 13), bit_list_of_integer 13 (Nat_big_num.of_int value))
+let translate_imm12 name value = 
+    (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value))
+let translate_imm6 name value = 
+    (name, Bvector (Some 6), bit_list_of_integer 6 (Nat_big_num.of_int value))
+let translate_imm5 name value = 
+    (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value))
+let translate_imm4 name value = 
+    (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value))
+let translate_bool name value =
+  (name, Bit, [if value then Bitc_one else Bitc_zero])
diff --git a/risc-v/risc-v.sail b/risc-v/riscv.sail
index edf95c62..4a80adb0 100644
--- a/risc-v/risc-v.sail
+++ b/risc-v/riscv.sail
@@ -52,9 +52,17 @@ function unit wGPR((regno) r, (regval) v) =
     if (r != 0) then
         GPRs[r] := v
 
+function forall 'a. 'a effect { escape } not_implemented((string) message) =
+{
+  exit message;
+}
+
 val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
 val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
 val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
+val extern unit -> unit effect { barr } MEM_fence_rw_rw
+val extern unit -> unit effect { barr } MEM_fence_r_rw
+val extern unit -> unit effect { barr } MEM_fence_rw_w
 
 (* Ideally these would be sail builtin *)
 function (bit[64]) shift_right_arith64 ((bit[64]) v, (bit[6]) shift) =
@@ -72,6 +80,8 @@ typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *)
 typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *)
 typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *)
 
+typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE}
+
 scattered function unit execute
 scattered typedef ast = const union
 
@@ -92,10 +102,10 @@ function clause execute (UTYPE(imm, rd, op)) =
     } in
     wGPR(rd, ret)
 
-union ast member ((bit[20]), regno) JAL
-function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm, rd))
+union ast member ((bit[21]), regno) JAL
+function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd))
 function clause execute (JAL(imm, rd)) =
-    let (bit[64]) offset = EXTS(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0) in {
+    let (bit[64]) offset = EXTS(imm) in {
       nextPC :=  PC + offset;
       wGPR(rd, PC + 4);
     }
@@ -109,13 +119,13 @@ function clause execute (JALR(imm, rs1, rd)) =
       wGPR(rd, PC + 4);
     }
 
-union ast member ((bit[12]), regno, regno, bop) BTYPE
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BEQ))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BNE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLT))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BLTU))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1], rs2, rs1, BGEU))
+union ast member ((bit[13]), regno, regno, bop) BTYPE
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BEQ))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BNE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b100 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLT))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b101 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b110 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BLTU))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b111 : (bit[5]) imm5 : 0b1100011) = Some(BTYPE(imm7[6] : imm5[0] : imm7[5..0] : imm5[4..1] : 0b0, rs2, rs1, BGEU))
 
 function clause execute (BTYPE(imm, rs2, rs1, op)) =
   let rs1_val = rGPR(rs1) in
@@ -126,10 +136,10 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) =
     case BLT  -> rs1_val <_s rs2_val
     case BGE  -> rs1_val >=_s rs2_val
     case BLTU -> rs1_val <_u rs2_val
-    case BGEU -> rs1_val >= rs2_val (* XXX is this signed or unsigned? *)
+    case BGEU -> unsigned(rs1_val) >= unsigned(rs2_val) (* XXX sail missing >=_u *)
   } in
   if (taken) then
-      nextPC := PC + EXTS(imm : 0b0)
+      nextPC := PC + EXTS(imm)
 
 union ast member ((bit[12]), regno, regno, iop) ITYPE
 function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0010011) = Some(ITYPE(imm, rs1, rd, ADDI))
@@ -192,31 +202,52 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) =
   } in
   wGPR(rd, result)
 
-union ast member ((bit[12]), regno, regno, bool, [|8|]) LOAD
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 1))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 2))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 4))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, 8))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  1))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  2))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  4))
+union ast member ((bit[12]), regno, regno, bool, word_width) LOAD
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  BYTE))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  HALF))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  WORD))
 function clause execute(LOAD(imm, rs1, rd, unsigned, width)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in
     let (bit[64]) result = if unsigned then 
-        EXTZ(MEMr(addr, width))
+        switch (width) {
+          case BYTE   -> EXTZ(MEMr(addr, 1))
+          case HALF   -> EXTZ(MEMr(addr, 2))
+          case WORD   -> EXTZ(MEMr(addr, 4))
+          case DOUBLE -> MEMr(addr, 8)
+        }
       else
-        EXTS(MEMr(addr, width)) in
+        switch (width) {
+          case BYTE   -> EXTS(MEMr(addr, 1))
+          case HALF   -> EXTS(MEMr(addr, 2))
+          case WORD   -> EXTS(MEMr(addr, 4))
+          case DOUBLE -> MEMr(addr, 8)
+        } in
     wGPR(rd, result)
 
-union ast member ((bit[12]), regno, regno, [|8|]) STORE
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 1))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 2))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 4))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, 8))
+union ast member ((bit[12]), regno, regno, word_width) STORE
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, BYTE))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE))
 function clause execute (STORE(imm, rs2, rs1, width)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in {
-      MEMea(addr, width);
-      MEMval(addr, width, rGPR(rs2));
+      switch (width) {
+        case BYTE   -> MEMea(addr, 1)
+        case HALF   -> MEMea(addr, 2)
+        case WORD   -> MEMea(addr, 4)
+        case DOUBLE -> MEMea(addr, 8)
+      };
+      let rs2_val = rGPR(rs2) in
+      switch (width) {
+        case BYTE   -> MEMval(addr, 1, rs2_val[7..0])
+        case HALF   -> MEMval(addr, 2, rs2_val[15..0])
+        case WORD   -> MEMval(addr, 4, rs2_val[31..0])
+        case DOUBLE -> MEMval(addr, 8, rs2_val)
+      }
     }
 
 union ast member ((bit[12]), regno, regno) ADDIW
@@ -258,6 +289,32 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
   } in
   wGPR(rd, EXTS(result))
 
+union ast member (bit[4], bit[4]) FENCE
+function clause decode (0b0000 : (bit[4]) pred : (bit[4]) succ : 0b00000 : 0b000 : 0b00000 : 0b0001111) = Some(FENCE (pred, succ))
+function clause execute (FENCE(pred, succ)) = {
+  switch(pred, succ) {
+    case (0b0011, 0b0011) -> MEM_fence_rw_rw()
+    case (0b0010, 0b0011) -> MEM_fence_r_rw()
+    case (0b0011, 0b0001) -> MEM_fence_rw_w()
+    case _ -> not_implemented("unsupported fence")
+  }
+}
+
+union ast member unit FENCEI
+function clause decode (0b0000 : 0b0000 : 0b0000 : 0b00000 : 0b001 : 0b00000 : 0b0001111) = Some(FENCEI)
+function clause execute FENCEI = () (* XXX TODO *)
+
+union ast member unit ECALL
+function clause decode (0b000000000000 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(ECALL ())
+function clause execute ECALL = ()
+
+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
 end decode
 end execute
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
new file mode 100644
index 00000000..aa5d8fb8
--- /dev/null
+++ b/risc-v/riscv_extras.lem
@@ -0,0 +1,60 @@
+open import Pervasives
+open import Interp_ast
+open import Interp_interface
+open import Sail_impl_base
+open import Interp_inter_imp
+import Set_extra
+
+let memory_parameter_transformer mode v =
+  match v with
+  | Interp_ast.V_tuple [location;length] ->
+    let (v,loc_regs) = extern_with_track mode extern_vector_value location in
+
+    match length with
+    | Interp_ast.V_lit (L_aux (L_num len) _) ->
+      (v,(natFromInteger len),loc_regs)
+    | Interp_ast.V_track (Interp_ast.V_lit (L_aux (L_num len) _)) size_regs ->
+      match loc_regs with
+      | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
+      | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
+      end
+    | _ -> Assert_extra.failwith "expected 'V_lit (L_aux (L_num _) _)' or 'V_track (V_lit (L_aux (L_num len) _)) _'"
+    end
+  | _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
+  end
+
+let memory_parameter_transformer_option_address _mode v =
+  match v with
+  | Interp_ast.V_tuple [location;_] ->
+     Just (extern_vector_value location)
+  | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
+  end
+
+
+let read_memory_functions : memory_reads =
+  [ ("MEMr",             (MR Read_plain              memory_parameter_transformer));
+    ("MEMr_reserve",     (MR Read_reserve            memory_parameter_transformer));
+  ]
+
+let memory_writes : memory_writes =
+  []
+
+let memory_eas : memory_write_eas =
+  [ ("MEMea",                 (MEA Write_plain           memory_parameter_transformer));
+    ("MEMea_conditional",     (MEA Write_conditional     memory_parameter_transformer));
+  ]
+
+let memory_vals : memory_write_vals =
+  [ ("MEMval",      (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_conditional", (MV memory_parameter_transformer_option_address
+                           (Just 
+                           (fun (IState interp context) b -> 
+                             let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
+                             (IState (Interp.add_answer_to_stack interp bit) context)))));
+  ]
+
+let barrier_functions =
+  [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw);
+    ("MEM_fence_r_rw",  Barrier_RISCV_r_rw);
+    ("MEM_fence_rw_w",  Barrier_RISCV_rw_w);
+  ]
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
new file mode 100644
index 00000000..1146d1cd
--- /dev/null
+++ b/risc-v/riscv_extras_embed.lem
@@ -0,0 +1,36 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+open import Prompt
+
+val MEMr             : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserve     : (vector bitU * integer) -> M (vector bitU)
+
+let MEMr (addr,size)             = read_mem false Read_plain addr size
+let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
+
+val MEMea                 : (vector bitU * integer) -> M unit
+val MEMea_conditional     : (vector bitU * integer) -> M unit
+
+let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
+let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
+
+val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
+
+let MEMval (_,_,v)                 = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)     = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+
+val MEM_fence_rw_rw : unit -> M unit
+val MEM_fence_r_rw  : unit -> M unit
+val MEM_fence_rw_w  : unit -> M unit
+
+let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
+let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
+let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
+
+let duplicate (bit,len) =
+  let bits = repeat [bit] len in
+  let start = len - 1 in
+  Vector bits start false
diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
new file mode 100644
index 00000000..f6709ff7
--- /dev/null
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -0,0 +1,37 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+open import State
+
+val MEMr             : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserve     : (vector bitU * integer) -> M (vector bitU)
+
+let MEMr (addr,size)             = read_mem false Read_plain addr size
+let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
+
+val MEMea                 : (vector bitU * integer) -> M unit
+val MEMea_conditional     : (vector bitU * integer) -> M unit
+
+let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
+let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
+
+
+val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
+
+let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+
+val MEM_fence_rw_rw : unit -> M unit
+val MEM_fence_r_rw  : unit -> M unit
+val MEM_fence_rw_w  : unit -> M unit
+
+let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
+let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
+let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
+
+let duplicate (bit,len) =
+  let bits = repeat [bit] len in
+  let start = len - 1 in
+  Vector bits start false
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
new file mode 100644
index 00000000..0c7a67d8
--- /dev/null
+++ b/risc-v/riscv_regfp.sail
@@ -0,0 +1,84 @@
+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])) ||]; (* XXX this should br rs + offset... *)
+     }
+     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;
+     }
+     case (FENCE(pred, succ)) -> {
+          ik := IK_barrier (Barrier_MIPS_SYNC);
+     }
+  };
+  (iR,oR,aR,Nias,Dia,ik)
+}
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index abf5983b..3aa5dc61 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -378,7 +378,7 @@ let hardware_quot (a:integer) (b:integer) : integer =
   if ((a<0) = (b<0)) then
     q  (* same sign -- result positive *)
   else
-    ~q (* different sign -- result negative *)
+    integerNegate q (* different sign -- result negative *)
 
 let quot_signed = hardware_quot
 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 937db466..dcc9f537 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -259,7 +259,7 @@ type outcome =
 
 
 (* Functions to build up the initial state for interpretation *)
-val build_context : specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> barriers -> excl_res -> external_functions -> context
+val build_context : bool -> specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> barriers -> excl_res -> external_functions -> context
 val initial_instruction_state : context -> string -> list register_value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index a51598b3..9f1ea3e3 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -127,36 +127,6 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
   ;;
 
 
-let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function
- | Interp_ast.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory)
- | Interp_ast.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
- | Interp_ast.V_tuple l ->
-     let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in
-     sprintf "(%s)" repr
- | Interp_ast.V_list l ->
-     let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in
-     sprintf "[||%s||]" repr
- | Interp_ast.V_vector (first_index, inc, l) ->
-     let last_index = (if (Interp_ast.IInc = inc) then List.length l - 1 else 1 - List.length l) + first_index  in
-     let repr =
-       try bitvec_to_string l
-       with Failure _ ->
-         sprintf "[%s]" (String.concat "; " (List.map (val_to_string_internal mem) l)) in
-     sprintf "%s [%s..%s]" repr (string_of_int first_index) (string_of_int last_index)
- | (Interp_ast.V_vector_sparse(first_index,last_index,inc,l,default) as v) -> 
-   val_to_string_internal mem (Interp_lib.fill_in_sparse v)
- | Interp_ast.V_record(_, l) ->
-     let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal mem value) in
-     let repr = String.concat "; " (List.map  pp l) in
-     sprintf "{%s}" repr
- | Interp_ast.V_ctor (id,_,_, value) ->
-     sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value)
- | Interp_ast.V_register _ | Interp_ast.V_register_alias _ ->
-     sprintf "reg-as-value" 
- | Interp_ast.V_unknown -> "unknown"
- | Interp_ast.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v)
-;;
-
 (****************************************************************************
  * PPrint-based source-to-source pretty printer
 ****************************************************************************)
@@ -582,7 +552,7 @@ let doc_exp, doc_let =
   (* XXX missing case *)
   | E_comment _ | E_comment_struc _ -> string ""
   | E_internal_value v ->
-     string (val_to_string_internal mem v)
+     string (Interp.string_of_value v)
   | _-> failwith "internal expression escaped"
 
   and let_exp env mem add_red show_hole_contents (LB_aux(lb,_)) = match lb with
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 79a86113..a19256a2 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -49,7 +49,6 @@ open Interp_interface ;;
 
 open Nat_big_num ;;
 
-let val_to_string_internal = Pretty_interp.val_to_string_internal ;;
 let lit_to_string = Pretty_interp.lit_to_string ;;
 let id_to_string = Pretty_interp.id_to_string ;;
 let loc_to_string = Pretty_interp.loc_to_string ;;
@@ -451,7 +450,7 @@ let local_variables_to_string (IState(stack,_)) =
       String.concat ", " (option_map (fun (id,value)-> 
 	match id with
 	  | "0" -> None (*Let's not print out the context hole again*)
-	  | _ -> Some (id ^ "=" ^ val_to_string_internal mem value)) (Pmap.bindings_list env))
+	  | _ -> Some (id ^ "=" ^ Interp.string_of_value value)) (Pmap.bindings_list env))
 
 let instr_parm_to_string (name, typ, value) = 
   name ^"="^
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index 85744d61..f1a0cd4a 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -10,7 +10,6 @@ val loc_to_string : l -> string
 val get_loc : tannot exp -> string
 (*interp_interface.value to string*)
 val reg_value_to_string : register_value -> string
-val val_to_string_internal : Interp.lmem -> Interp_ast.value -> string
 
 (*(*Force all representations to hex strings instead of a mixture of hex and binary strings*)
 val val_to_hex_string : value0 -> string*)
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 6f5ca07a..f61d9aaf 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -114,33 +114,6 @@ let rec reg_to_string = function
   | SubReg (id,r,_) -> sprintf "%s.%s" (reg_to_string r) (id_to_string id)
 ;;
 
-let rec val_to_string_internal = function
- | V_boxref(n, t) -> sprintf "boxref %d" n
- | V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
- | V_tuple l ->
-     let repr = String.concat ", " (List.map val_to_string_internal l) in
-     sprintf "(%s)" repr
- | V_list l ->
-     let repr = String.concat "; " (List.map val_to_string_internal l) in
-     sprintf "[||%s||]" repr
- | V_vector (first_index, inc, l) ->
-     let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index  in
-     let repr =
-       try bitvec_to_string (* (if inc then l else List.rev l)*) l
-       with Failure _ ->
-         sprintf "[%s]" (String.concat "; " (List.map val_to_string_internal l)) in
-     sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index)
- | V_record(_, l) ->
-     let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal value) in
-     let repr = String.concat "; " (List.map  pp l) in
-     sprintf "{%s}" repr
- | V_ctor (id,_, value) ->
-     sprintf "%s %s" (id_to_string id) (val_to_string_internal value)
- | V_register r ->
-     sprintf "reg-as-value %s" (reg_to_string r)
- | V_unknown -> "unknown"
-;;
-
 let rec top_frame_exp_state = function
   | Top -> raise (Invalid_argument "top_frame_exp")
   | Hole_frame(_, e, _, env, mem, Top) 
@@ -210,7 +183,7 @@ let id_compare i1 i2 =
 module Reg = struct
   include Map.Make(struct type t = id let compare = id_compare end)
   let to_string id v =
-    sprintf "%s -> %s" (id_to_string id) (val_to_string_internal v)
+    sprintf "%s -> %s" (id_to_string id) (string_of_value v)
   let find id m =
 (*    eprintf "reg_find called with %s\n" (id_to_string id);*)
     let v = find id m in
@@ -255,7 +228,7 @@ module Mem = struct
     v
   *)
   let to_string idx v =
-    sprintf "[%s] -> %s" (string_of_big_int idx) (val_to_string_internal v)
+    sprintf "[%s] -> %s" (string_of_big_int idx) (string_of_value v)
 end ;;
 
 
@@ -412,7 +385,7 @@ let run
   in
   let rec loop mode env = function
   | Value v ->
-      debugf "%s: %s %s\n" (grey name) (blue "return") (val_to_string_internal v);
+      debugf "%s: %s %s\n" (grey name) (blue "return") (string_of_value v);
       true, mode, env
   | Action (a, s) ->
       let (top_exp,(top_env,top_mem)) = top_frame_exp_state s in
@@ -429,25 +402,25 @@ let run
       let left = "<-" and right = "->" in
       let (mode',env',s) = begin match a with
       | Read_reg (reg, sub) ->
-          show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (val_to_string_internal return);
+          show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (string_of_value return);
           step (),env',s
       | Write_reg (reg, sub, value) ->
           assert (return = unit_lit);
-          show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (val_to_string_internal value);
+          show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (string_of_value value);
           step (),env',s
       | Read_mem (id, args, sub) ->
-          show "read_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) right (val_to_string_internal return);
+          show "read_mem" (id_to_string id ^ string_of_value args ^ sub_to_string sub) right (string_of_value return);
           step (),env',s
       | Write_mem (id, args, sub, value) ->
           assert (return = unit_lit);
-          show "write_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) left (val_to_string_internal value);
+          show "write_mem" (id_to_string id ^ string_of_value args ^ sub_to_string sub) left (string_of_value value);
           step (),env',s
       (* distinguish single argument for pretty-printing *)
       | Call_extern (f, (V_tuple _ as args)) ->
-          show "call_lib" (f ^ val_to_string_internal args) right (val_to_string_internal return);
+          show "call_lib" (f ^ string_of_value args) right (string_of_value return);
           step (),env',s
       | Call_extern (f, arg) ->
-          show "call_lib" (sprintf "%s(%s)" f (val_to_string_internal arg)) right (val_to_string_internal return);
+          show "call_lib" (sprintf "%s(%s)" f (string_of_value arg)) right (string_of_value return);
           step (),env',s
       | Interp.Step _ ->
           assert (return = unit_lit);
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index d48b7e7b..2a1783db 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -1292,7 +1292,7 @@ let run () =
         startaddr,
         startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
 
-  let context = build_context isa_defs isa_m0 [] isa_m1 isa_m2 isa_m3 [] isa_m4 None isa_externs in
+  let context = build_context false isa_defs isa_m0 [] isa_m1 isa_m2 isa_m3 [] isa_m4 None isa_externs in
   (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, 
           endian mode, and translate function name 
   *)
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index eaf8ddfa..e773bf5b 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -1386,7 +1386,7 @@ let run () =
         startaddr,
         startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
 
-  let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in
+  let context = build_context false isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in
   (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, 
           endian mode, and translate function name 
   *)
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index eca6d342..cd2e7312 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -1386,7 +1386,7 @@ let run () =
         startaddr,
         startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
 
-  let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in
+  let context = build_context false isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in
   (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, 
           endian mode, and translate function name 
   *)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 0cdeb414..cda6702c 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -465,6 +465,11 @@ type barrier_kind =
   | Barrier_TM_COMMIT
   (* MIPS barriers *)
   | Barrier_MIPS_SYNC
+  (* RISC-V barriers *)
+  | Barrier_RISCV_rw_rw
+  | Barrier_RISCV_r_rw
+  | Barrier_RISCV_rw_w
+
 
 instance (Show barrier_kind)
   let show = function
diff --git a/src/test/lib/run_test_interp.ml b/src/test/lib/run_test_interp.ml
index 3446ef9f..5f2ace1b 100644
--- a/src/test/lib/run_test_interp.ml
+++ b/src/test/lib/run_test_interp.ml
@@ -45,7 +45,7 @@ open Interp_inter_imp ;;
 open Sail_impl_base ;;
 
 let doit () =
-  let context = build_context Test_lem_ast.defs [] [] [] [] [] [] [] None [] in
+  let context = build_context false Test_lem_ast.defs [] [] [] [] [] [] [] None [] in
   translate_address context E_little_endian "run" None (address_of_integer (Nat_big_num.of_int 0));;
 
 doit () ;;