Merge changes to type_check.ml

8 files changed, 620 insertions, 36 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index 7f52dde7..aeba80ef 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -11,6 +11,19 @@ check: $(SAIL_SRCS) main.sail
 riscv: $(SAIL_SRCS) main.sail
 	$(SAIL_DIR)/sail -ocaml -o riscv $^
 
+riscv_duopod_ocaml: prelude.sail riscv_duopod.sail
+	$(SAIL_DIR)/sail -ocaml -o $@ $^
+
+riscv_duopod_embed_sequential.lem: prelude.sail riscv_duopod.sail
+	$(SAIL_DIR)/sail -lem -lem_sequential -lem_mwords -lem_lib Riscv_extras_embed -o riscv_duopod $^
+Riscv_duopod_embed_sequential.thy: riscv_duopod_embed_sequential.lem riscv_extras_embed_sequential.lem
+	lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
+		riscv_extras_embed_sequential.lem \
+		riscv_duopod_embed_types_sequential.lem \
+		riscv_duopod_embed_sequential.lem
+
+riscv_duopod: riscv_duopod_ocaml Riscv_duopod_embed_sequential.thy
+
 Riscv_embed_sequential.thy: riscv_embed_sequential.lem riscv_extras_embed_sequential.lem
 	lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
 		riscv_extras_embed_sequential.lem \
@@ -25,3 +38,4 @@ clean:
 	-rm -f riscv_embed_sequential.lem riscv_embed_types_sequential.lem
 	-rm -f Riscv_embed_sequential.thy Riscv_embed_types_sequential.thy \
 		Riscv_extras_embed_sequential.thy
+	-rm -f Riscv_duopod_embed_sequential.thy Riscv_duopod_embed_types_sequential.thy riscv_duopod_embed_sequential.lem riscv_duopod_embed_types_sequential.lem
diff --git a/riscv/main.sail b/riscv/main.sail
index cc6bb90c..4209b7d1 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -6,12 +6,29 @@ function fetch_and_execute () =
   let tohost = __GetSlice_int(64, elf_tohost(), 0) in
   while true do {
     print_bits("PC: ", PC);
+
+    /* for now, always fetch a 32-bit value.  this would need to
+       change with privileged mode, since we could cross a page
+       boundary with PC only 16-bit aligned in C mode.  */
     let instr = __RISCV_read(PC, 4);
-    nextPC = PC + 4;
-    let instr_ast = decode(instr);
-    match instr_ast {
-      Some(ast) => execute(ast),
-      None      => {print("Decode failed"); exit (())}
+
+    let (instr_ast, instr_sz) : (option(ast), int)=
+       match (instr[1 .. 0]) {
+         0b11 => (decode(instr), 4),
+	 _    => (decodeCompressed(instr[15 .. 0]), 2)
+       };
+    /* check whether a compressed instruction is legal. */
+    if (misa.C() == 0b0 & (instr_sz == 2)) then {
+      let t : sync_exception =
+      struct { trap = Illegal_Instr,
+               excinfo = Some (EXTZ(instr)) } in
+      nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+    } else {
+      nextPC = PC + instr_sz;
+      match instr_ast {
+        Some(ast) => execute(ast),
+        None      => {print("Decode failed"); exit (())}
+      }
     };
     let tohost_val = __RISCV_read(tohost, 4);
     if unsigned(tohost_val) != 0 then {
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index dacde107..a0d3d3a1 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -2,7 +2,6 @@ default Order dec
 
 type bits ('n : Int) = vector('n, dec, bit)
 union option ('a : Type) = {None, Some : 'a}
-infix 4 ==
 
 val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
@@ -91,9 +90,9 @@ overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
 
 val and_bool = "and_bool" : (bool, bool) -> bool
 
-val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
@@ -101,9 +100,9 @@ overload operator & = {and_bool, and_vec}
 
 val or_bool = "or_bool" : (bool, bool) -> bool
 
-val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val or_vec = {lem: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function or_vec (xs, ys) = builtin_or_vec(xs, ys)
 
@@ -152,6 +151,8 @@ val putchar = "putchar" : forall ('a : Type). 'a -> unit
 
 val concat_str = {ocaml: "concat_str", lem: "stringAppend"} : (string, string) -> string
 
+val string_of_int = "string_of_int" : int -> string
+
 val DecStr : int -> string
 
 val HexStr : int -> string
@@ -160,7 +161,7 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
 
 val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val int_power = {lem: "pow"} : (int, int) -> int
+val int_power = {ocaml: "int_power", lem: "pow"} : (int, int) -> int
 
 val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real
 
@@ -251,13 +252,12 @@ val quotient_real = {ocaml: "quotient_real", lem: "realDiv"} : (real, real) -> r
 
 val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
 
-infixl 7 /
-
 overload operator / = {quotient_nat, quotient, quotient_real}
 
-val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int
+val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod"} : (int, int) -> int
 
-infixl 7 %
+val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int
 
 overload operator % = {modulus}
 
@@ -376,6 +376,9 @@ val vector64 : int -> bits(64)
 
 function vector64 n = __raw_GetSlice_int(64, n, 0)
 
+val to_bits : forall 'l.(atom('l), int) -> bits('l)
+function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
+
 function break () : unit -> unit = ()
 
 val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 9ec5734e..37244735 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -3,6 +3,10 @@ scattered union ast
 val decode : bits(32) -> option(ast) effect pure
 scattered function decode
 
+val decodeCompressed : bits(16) -> option(ast) effect pure
+scattered function decodeCompressed
+
+
 val execute : ast -> unit effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
 scattered function execute
 
@@ -29,7 +33,7 @@ function clause decode imm : bits(20) @ rd : regbits @ 0b1101111 = Some (RISCV_J
 
 function clause execute (RISCV_JAL(imm, rd)) = {
     let pc : bits(64) = PC;
-    wGPR(rd, pc + 4);
+    wGPR(rd, nextPC);  /* compatible with JAL and C.JAL */
     let offset : bits(64) = EXTS(imm);
     nextPC = pc + offset;
 }
@@ -155,9 +159,9 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0
 function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  WORD,   false, false))
 
 
-function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) =
+function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
     let addr : bits(64) = rGPR(rs1) + EXTS(imm) in
-    let result : bits(64) = if unsigned then
+    let result : bits(64) = if is_unsigned then
         match width {
 	  BYTE   => EXTZ(mem_read(addr, 1, aq, rl, false)),
 	  HALF   => EXTZ(mem_read(addr, 2, aq, rl, false)),
@@ -248,6 +252,93 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
   wGPR(rd, EXTS(result))
 
 /* ****************************************************************** */
+
+union clause ast = MUL : (regbits, regbits, regbits, bool, bool, bool)
+
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd, false,  true, true))  /* MUL */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd,  true,  true, true))  /* MULH */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd,  true,  true, false)) /* MULHSU */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd,  true, false, false)) /* MULHU */
+function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val) in
+  let result128 = to_bits(128, rs1_int * rs2_int) in
+  let result = if high then result128[127..64] else result128[63..0] in
+  wGPR(rd, result)
+
+/* ****************************************************************** */
+
+union clause ast = DIV : (regbits, regbits, regbits, bool)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0110011 = Some(DIV(rs2, rs1, rd,  true))  /* DIV */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(DIV(rs2, rs1, rd, false))  /* DIVU */
+function clause execute (DIV(rs2, rs1, rd, s)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
+  let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in
+  let q': int = if s & q > (2 ^ 63 - 1) then  (0 - 2^63) else q in /* check for signed overflow */
+  wGPR(rd, to_bits(64, q'))
+
+/* ****************************************************************** */
+
+union clause ast = REM : (regbits, regbits, regbits, bool)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0110011 = Some(REM(rs2, rs1, rd,  true))  /* REM */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0110011 = Some(REM(rs2, rs1, rd, false))  /* REMU */
+function clause execute (REM(rs2, rs1, rd, s)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
+  let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in
+  /* signed overflow case returns zero naturally as required due to -1 divisor */
+  wGPR(rd, to_bits(64, r))
+
+/* ****************************************************************** */
+
+union clause ast = MULW : (regbits, regbits, regbits)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(MULW(rs2, rs1, rd)) /* MULW */
+function clause execute (MULW(rs2, rs1, rd)) =
+  let rs1_val = rGPR(rs1)[31..0] in
+  let rs2_val = rGPR(rs2)[31..0] in
+  let rs1_int : int = signed(rs1_val) in
+  let rs2_int : int = signed(rs2_val) in
+  let result32 = to_bits(64, rs1_int * rs2_int)[31..0] in /* XXX surprising behaviour of to_bits requires exapnsion to 64 bits followed by truncation... */
+  let result64 : regval = EXTS(result32) in
+  wGPR(rd, result64)
+
+/* ****************************************************************** */
+
+union clause ast = DIVW : (regbits, regbits, regbits, bool)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0111011 = Some(DIVW(rs2, rs1, rd,  true))  /* DIVW */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(DIVW(rs2, rs1, rd, false))  /* DIVUW */
+function clause execute (DIVW(rs2, rs1, rd, s)) =
+  let rs1_val = rGPR(rs1)[31..0] in
+  let rs2_val = rGPR(rs2)[31..0] in
+  let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
+  let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in
+  let q': int = if s & q > (2 ^ 31 - 1) then  (0 - 2^31) else q in /* check for signed overflow */
+  wGPR(rd, EXTS(to_bits(32, q')))
+
+/* ****************************************************************** */
+
+union clause ast = REMW : (regbits, regbits, regbits, bool)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0111011 = Some(REMW(rs2, rs1, rd,  true))  /* REMW */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0111011 = Some(REMW(rs2, rs1, rd, false))  /* REMUW */
+function clause execute (REMW(rs2, rs1, rd, s)) =
+  let rs1_val = rGPR(rs1)[31..0] in
+  let rs2_val = rGPR(rs2)[31..0] in
+  let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
+  let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in
+  /* signed overflow case returns zero naturally as required due to -1 divisor */
+  wGPR(rd, EXTS(to_bits(32, r)))
+
+/* ****************************************************************** */
+
 union clause ast = FENCE : (bits(4), bits(4))
 
 function clause decode 0b0000 @ pred : bits(4) @ succ : bits(4) @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111 = Some(FENCE(pred, succ))
@@ -282,7 +373,7 @@ function clause execute ECALL =
                       USER => User_ECall,
 		      MACHINE => Machine_ECall
 		    },
-             badaddr = (None : option(regval)) } in
+             excinfo = (None : option(regval)) } in
   nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
 
 /* ****************************************************************** */
@@ -486,7 +577,7 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
     let instr : regval = EXTZ(__RISCV_read(PC, 4));
     let t : sync_exception =
     struct { trap = Illegal_Instr,
-             badaddr = Some (instr) } in
+             excinfo = Some (instr) } in
     nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
   } else {
     let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */
@@ -503,8 +594,325 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
 
 /* ****************************************************************** */
 
+union clause ast = NOP
+
+function clause decodeCompressed (0b000 @ nzi1 : bits(1) @ 0b00000 @ (nzi0 : bits(5)) @ 0b01) : bits(16) = {
+  if (nzi1 == 0b0) & (nzi0 == 0b00000) then None
+  else Some(NOP)
+}
+
+function clause execute (NOP) = ()
+
+/* ****************************************************************** */
+
+union clause ast = ILLEGAL
+
+function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(ILLEGAL)
+
+function clause execute (ILLEGAL) = {
+  let t : sync_exception =
+  struct { trap = Illegal_Instr,
+           excinfo = Some (EXTZ(0b0)) } in
+  nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_ADDI4SPN : (cregbits, bits(8))
+
+function clause decodeCompressed (0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregbits @ 0b00) : bits(16) = {
+  let nzimm = (nz96 @ nz54 @ nz3 @ nz2) : bits(8) in
+  if nzimm == 0b00000000 then None
+  else Some(C_ADDI4SPN(rd, nzimm))
+}
+
+function clause execute (C_ADDI4SPN(rdc, nzimm)) = {
+  let imm : bits(12) = (0b00 @ nzimm @ 0b00) in
+  let rd = creg2reg_bits(rdc) in
+  execute(ITYPE(imm, sp, rd, RISCV_ADDI))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_LW : (bits(5), cregbits, cregbits)
+
+function clause decodeCompressed (0b010 @ ui53 : bits(3) @ rs1 : cregbits @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregbits @ 0b00) : bits(16) = {
+  let uimm = (ui6 @ ui53 @ ui2) : bits(5) in
+  Some(C_LW(uimm, rs1, rd))
+}
+
+function clause execute (C_LW(uimm, rsc, rdc)) = {
+  let imm : bits(12) = EXTZ(uimm @ 0b00) in
+  let rd = creg2reg_bits(rdc) in
+  let rs = creg2reg_bits(rsc) in
+  execute(LOAD(imm, rs, rd, true, WORD, false, false))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_SW : (bits(5), cregbits, cregbits)
+
+function clause decodeCompressed (0b110 @ ui53 : bits(3) @ rs1 : cregbits @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregbits @ 0b00) : bits(16) = {
+  let uimm = (ui6 @ ui53 @ ui2) : bits(5) in
+  Some(C_SW(uimm, rs1, rs2))
+}
+
+function clause execute (C_SW(uimm, rsc1, rsc2)) = {
+  let imm : bits(12) = EXTZ(uimm @ 0b00) in
+  let rs1 = creg2reg_bits(rsc1) in
+  let rs2 = creg2reg_bits(rsc2) in
+  execute(STORE(imm, rs2, rs1, WORD, false, false))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_SD : (bits(5), cregbits, cregbits)
+
+function clause decodeCompressed (0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00): bits(16) = {
+  let uimm = (ui76 @ ui53) : bits(5) in
+  Some(C_SD(uimm, rs1, rs2))
+}
+
+function clause execute (C_SD(uimm, rsc1, rsc2)) = {
+  let imm : bits(12) = EXTZ(uimm @ 0b000) in
+  let rs1 = creg2reg_bits(rsc1) in
+  let rs2 = creg2reg_bits(rsc2) in
+  execute(STORE(imm, rs2, rs1, DOUBLE, false, false))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_ADDI : (bits(6), regbits)
+
+function clause decodeCompressed (0b000 @ nzi5 : bits(1) @ rsd : regbits @ nzi40 : bits(5) @ 0b01) : bits(16) = {
+  let nzi = (nzi5 @ nzi40) : bits(6) in
+  if (nzi == 0b000000) | (rsd == zreg) then None
+  else Some(C_ADDI(nzi, rsd))
+}
+
+function clause execute (C_ADDI(nzi, rsd)) = {
+  let imm : bits(12) = EXTS(nzi) in
+  execute(ITYPE(imm, rsd, rsd, RISCV_ADDI))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_JAL : (bits(11))
+union clause ast = C_ADDIW : (bits(6), regbits)
+
+/* FIXME: decoding differs for RVC32/RVC64.  Below, we are assuming
+ * RV64, and C_JAL is RV32 only. */
+
+function clause decodeCompressed (0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01) =
+  Some (C_ADDIW((imm5 @ imm40), rsd))
+
+function clause execute (C_JAL(imm)) = {
+  execute(RISCV_JAL(EXTS(imm @ 0b0), ra))
+}
+
+function clause execute (C_ADDIW(imm, rsd)) = {
+  let imm : bits(32) = EXTS(imm) in
+  let rs_val = rGPR(rsd) in
+  let res : bits(32) = rs_val[31..0] + imm in
+  wGPR(rsd, EXTS(res))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_LI : (bits(6), regbits)
+
+function clause decodeCompressed (0b010 @ imm5 : bits(1) @ rd : regbits @ imm40 : bits(5) @ 0b01) = {
+  if (rd == zreg) then None
+  else Some(C_LI(imm5 @ imm40, rd))
+}
+
+function clause execute (C_LI(imm, rd)) = {
+  let imm : bits(12) = EXTS(imm) in
+  execute(ITYPE(imm, zreg, rd, RISCV_ADDI))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_ADDI16SP : (bits(6))
+
+function clause decodeCompressed (0b011 @ nzi9 : bits(1) @ /* x2 */ 0b00010 @ nzi4 : bits(1) @ nzi6 : bits(1) @ nzi87 : bits(2) @ nzi5 : bits(1) @ 0b01) = {
+  let nzimm = nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 in
+  if (nzimm == 0b000000) then None
+  else Some(C_ADDI16SP(nzimm))
+}
+
+function clause execute (C_ADDI16SP(imm)) = {
+  let imm : bits(12) = EXTS(imm @ 0x0) in
+  execute(ITYPE(imm, sp, sp, RISCV_ADDI))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_LUI : (bits(6), regbits)
+
+function clause decodeCompressed (0b011 @ imm17 : bits(1) @ rd : regbits @ imm1612 : bits(5) @ 0b01) = {
+  if (rd == zreg) | (rd == sp) then None
+  else Some(C_LUI(imm17 @ imm1612, rd))
+}
+
+function clause execute (C_LUI(imm, rd)) = {
+  let res : bits(20) = EXTS(imm) in
+  execute(UTYPE(res, rd, RISCV_LUI))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_SRLI : (bits(6), cregbits)
+
+function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = {
+  let shamt : bits(6) = nzui5 @ nzui40 in
+  if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */
+  then None
+  else Some(C_SRLI(shamt, rsd))
+}
+
+function clause execute (C_SRLI(shamt, rsd)) = {
+  let rsd = creg2reg_bits(rsd)  in
+  execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SRLI))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_SRAI : (bits(6), cregbits)
+
+function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = {
+  let shamt : bits(6) = nzui5 @ nzui40 in
+  if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */
+  then None
+  else Some(C_SRAI(shamt, rsd))
+}
+
+function clause execute (C_SRAI(shamt, rsd)) = {
+  let rsd = creg2reg_bits(rsd)  in
+  execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SRAI))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_ANDI : (bits(6), cregbits)
+
+function clause decodeCompressed (0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregbits @ i40 : bits(5) @ 0b01) = Some(C_ANDI(i5 @ i40, rsd))
+
+function clause execute (C_ANDI(imm, rsd)) = {
+  let rsd = creg2reg_bits(rsd) in
+  execute(ITYPE(EXTS(imm), rsd, rsd, RISCV_ANDI))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_SUB : (cregbits, cregbits)
+
+function clause decodeCompressed (0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01) = Some(C_SUB(rsd, rs2))
+
+function clause execute (C_SUB(rsd, rs2)) = {
+  let rsd = creg2reg_bits(rsd) in
+  let rs2 = creg2reg_bits(rs2) in
+  execute(RTYPE(rs2, rsd, rsd, RISCV_SUB))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_XOR : (cregbits, cregbits)
+
+function clause decodeCompressed (0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01) = Some(C_XOR(rsd, rs2))
+
+function clause execute (C_SUB(rsd, rs2)) = {
+  let rsd = creg2reg_bits(rsd) in
+  let rs2 = creg2reg_bits(rs2) in
+  execute(RTYPE(rs2, rsd, rsd, RISCV_XOR))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_OR : (cregbits, cregbits)
+
+function clause decodeCompressed (0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b10 @ rs2 : cregbits @ 0b01) = Some(C_OR(rsd, rs2))
+
+function clause execute (C_OR(rsd, rs2)) = {
+  let rsd = creg2reg_bits(rsd) in
+  let rs2 = creg2reg_bits(rs2) in
+  execute(RTYPE(rs2, rsd, rsd, RISCV_OR))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_AND : (cregbits, cregbits)
+
+function clause decodeCompressed (0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b11 @ rs2 : cregbits @ 0b01) = Some(C_AND(rsd, rs2))
+
+function clause execute (C_OR(rsd, rs2)) = {
+  let rsd = creg2reg_bits(rsd) in
+  let rs2 = creg2reg_bits(rs2) in
+  execute(RTYPE(rs2, rsd, rsd, RISCV_OR))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_SUBW : (cregbits, cregbits)
+
+/* TODO: invalid on RV32 */
+function clause decodeCompressed (0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01) = Some(C_SUBW(rsd, rs2))
+
+function clause execute (C_SUBW(rsd, rs2)) = {
+  let rsd = creg2reg_bits(rsd) in
+  let rs2 = creg2reg_bits(rs2) in
+  execute(RTYPE(rs2, rsd, rsd, RISCV_SUB))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_ADDW : (cregbits, cregbits)
+
+/* TODO: invalid on RV32 */
+function clause decodeCompressed (0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01) = Some(C_ADDW(rsd, rs2))
+
+function clause execute (C_ADDW(rsd, rs2)) = {
+  let rsd = creg2reg_bits(rsd) in
+  let rs2 = creg2reg_bits(rs2) in
+  execute(RTYPE(rs2, rsd, rsd, RISCV_ADD))
+}
+
+/* ****************************************************************** */
+
+union clause ast = C_J : (bits(11))
+
+function clause decodeCompressed (0b101 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01) =
+  Some(C_J(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31))
+
+function clause execute (C_J(imm)) =
+  execute(RISCV_JAL(EXTS(imm @ 0b0), zreg))
+
+/* ****************************************************************** */
+
+union clause ast = C_BEQZ : (bits(8), cregbits)
+
+function clause decodeCompressed (0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregbits @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01) =
+  Some(C_BEQZ(i8 @ i76 @ i5 @ i43 @ i21, rs))
+
+function clause execute (C_BEQZ(imm, rs)) =
+  execute(BTYPE(EXTS(imm @ 0b0), zreg, creg2reg_bits(rs), RISCV_BEQ))
+
+/* ****************************************************************** */
+
+union clause ast = C_BNEZ : (bits(8), cregbits)
+
+function clause decodeCompressed (0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregbits @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01) =
+  Some(C_BNEZ(i8 @ i76 @ i5 @ i43 @ i21, rs))
+
+function clause execute (C_BNEZ(imm, rs)) =
+  execute(BTYPE(EXTS(imm @ 0b0), zreg, creg2reg_bits(rs), RISCV_BNE))
+
+/* ****************************************************************** */
+
 function clause decode _ = None
+function clause decodeCompressed _ = None
 
 end ast
 end decode
+end decodeCompressed
 end execute
diff --git a/riscv/riscv_duopod.sail b/riscv/riscv_duopod.sail
new file mode 100644
index 00000000..e0eaf949
--- /dev/null
+++ b/riscv/riscv_duopod.sail
@@ -0,0 +1,82 @@
+
+type xlen = atom(64)
+type xlen_t = bits(64)
+
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regbits = bits(5)
+
+val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+function regbits_to_regno b = let 'r = unsigned(b) in r
+
+/* Architectural state */
+
+register PC : xlen_t
+register nextPC : xlen_t
+
+register Xs : vector(32, dec, xlen_t)
+
+/* Getters and setters for X registers (special case for zeros register, x0) */
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlen_t effect {rreg}
+
+function rX 0 = 0x0000000000000000
+and rX (r if r > 0) = Xs[r]
+
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlen_t) -> unit effect {wreg}
+
+function wX (r, v) =
+  if (r != 0) then {
+     Xs[r] = v;
+  }
+
+overload X = {rX, wX}
+
+/* Accessors for memory */
+
+val MEMr : forall 'n. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem}
+function MEMr (addr, width) = __RISCV_read(addr, width)
+
+/* Instruction decode and execute */
+enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI} /* immediate ops */
+scattered union ast
+
+val decode : bits(32) -> option(ast) effect pure
+scattered function decode
+
+val execute : ast -> unit effect {rmem, rreg, wreg}
+scattered function execute
+
+/* ****************************************************************** */
+
+/* ADDI */
+
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0010011
+  = Some(ITYPE(imm, rs1, rd, RISCV_ADDI))
+
+function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
+  let rs1_val = X(rs1) in
+  let imm_ext : xlen_t = EXTS(imm) in
+  let result = rs1_val + imm_ext in
+  X(rd) = result
+
+/* ****************************************************************** */
+
+/* Load double */
+union clause ast = LOAD : (bits(12), regbits, regbits)
+
+function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0000011
+  = Some(LOAD(imm, rs1, rd))
+
+function clause execute(LOAD(imm, rs1, rd)) =
+    let addr : xlen_t = X(rs1) + EXTS(imm) in
+    let result : xlen_t = MEMr(addr, 8) in
+    X(rd) = result
+
+/* ****************************************************************** */
+
+function clause decode _ = None
+
+end ast
+end decode
+end execute
diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras_embed_sequential.lem
index 044b2aa3..4ef3ed36 100644
--- a/riscv/riscv_extras_embed_sequential.lem
+++ b/riscv/riscv_extras_embed_sequential.lem
@@ -2,8 +2,11 @@ open import Pervasives
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
-open import Sail_operators
+open import Sail_operators_mwords
 open import State
+open import State_monad
+
+type bitvector 'a = mword 'a
 
 let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
 let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
@@ -12,6 +15,13 @@ let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
 let MEM_fence_w_w   () = barrier Barrier_RISCV_w_w
 let MEM_fence_i     () = barrier Barrier_RISCV_i
 
+val MEMea                            : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_release                    : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_strong_release             : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_conditional                : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_conditional_release        : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+val MEMea_conditional_strong_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
+
 let MEMea addr size                      = write_mem_ea Write_plain addr size
 let MEMea_release addr size              = write_mem_ea Write_RISCV_release addr size
 let MEMea_strong_release addr size       = write_mem_ea Write_RISCV_strong_release addr size
@@ -20,26 +30,35 @@ let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_
 let MEMea_conditional_strong_release addr size
                                           = write_mem_ea Write_RISCV_conditional_strong_release addr size
 
+val write_ram : forall 'a 'b 'r 'e. Size 'a, Size 'b =>
+  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> M 'r unit 'e
 let write_ram addrsize size hexRAM address value =
   write_mem_ea Write_plain address size >>
   write_mem_val value >>= fun _ ->
   return ()
 
+val read_ram : forall 'a 'b 'r 'e. Size 'a, Size 'b =>
+  integer -> integer -> bitvector 'a -> bitvector 'a -> M 'r (bitvector 'b) 'e
 let read_ram addrsize size hexRAM address =
   read_mem Read_plain address size
 
 let speculate_conditional_success () = excl_result ()
 
+val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> bitvector 'a
 let get_slice_int len n lo =
   (* TODO: Is this the intended behaviour? *)
   let hi = lo + len - 1 in
   let bits = bits_of_int (hi + 1) n in
   of_bits (get_bits false bits hi lo)
 
+val sign_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b
 let sign_extend v len = exts_vec len v
+val zero_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b
 let zero_extend v len = extz_vec len v
 
+val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
 let shift_bits_right v m = shiftr v (unsigned m)
+val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
 let shift_bits_left v m = shiftl v (unsigned m)
 
 val prerr_endline : string -> unit
@@ -49,7 +68,7 @@ declare ocaml target_rep function prerr_endline = `prerr_endline`
 val print_int : string -> integer -> unit
 let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
 
-val print_bits : forall 'a. Bitvector 'a => string -> 'a -> unit
+val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
 let print_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
 
 val putchar : integer -> unit
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 0eaadec4..68ef7a55 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -68,6 +68,38 @@ function exc_to_bits e =
 
 /* FIXME: currently we have only those used by riscv-tests. */
 
+bitfield Misa : bits(64) = {
+  MXL  : 63 .. 62,
+
+  Z    : 25,
+  Y    : 24,
+  X    : 23,
+  W    : 22,
+  V    : 21,
+  U    : 20,
+  T    : 19,
+  S    : 18,
+  R    : 17,
+  Q    : 16,
+  P    : 15,
+  O    : 14,
+  N    : 13,
+  M    : 12,
+  L    : 11,
+  K    : 10,
+  J    : 9,
+  I    : 8,
+  H    : 7,
+  G    : 6,
+  F    : 5,
+  E    : 4,
+  D    : 3,
+  C    : 2,
+  B    : 1,
+  A    : 0
+}
+register misa : Misa
+
 bitfield Mstatus : bits(64) = {
   SD   : 63,
 
@@ -180,7 +212,7 @@ register mhartid : regval
 
 struct sync_exception = {
   trap : ExceptionCode,
-  badaddr : option(regval)
+  excinfo : option(regval)
 }
 
 union ctl_result = {
@@ -228,19 +260,19 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
 
       match (e.trap) {
         Misaligned_Fetch => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
         },
         Fetch_Access => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
         },
         Illegal_Instr => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
@@ -249,25 +281,25 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
         Breakpoint => not_implemented("breakpoint"),
 
         Misaligned_Load => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
         },
         Load_Access => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
         },
         Misaligned_Store => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
         },
         Store_Access => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
@@ -284,23 +316,24 @@ function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
         },
 
         Fetch_PageFault => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
         },
         Load_PageFault => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
         },
         Store_PageFault => {
-          match (e.badaddr) {
+          match (e.excinfo) {
             Some(a) => mtval = a,
             None    => throw(Error_internal_error)
           }
-        }
+        },
+        _ => throw(Error_internal_error) /* Don't expect ReservedExc0 etc. here */
       };
       /* TODO: make register read explicit */
       mtvec
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index e627518d..477b4902 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -12,10 +12,14 @@ type regval = bits(64)
 
 type regno ('n : Int), 0 <= 'n < 32 = atom('n)
 type regbits = bits(5)
+type cregbits = bits(3)
 
 val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
 function regbits_to_regno b = let 'r = unsigned(b) in r
 
+val creg2reg_bits : cregbits -> regbits
+function creg2reg_bits(creg) = 0b10 @ creg
+
 /* register x0 : regval is hard-wired zero */
 register x1 : regval
 register x2 : regval
@@ -49,6 +53,11 @@ register x29 : regval
 register x30 : regval
 register x31 : regval
 
+/* some arch and ABI relevant registers */
+let zreg : regbits = 0b00000
+let ra : regbits = 0b00001  /* x1 */
+let sp : regbits = 0b00010  /* x2 */
+
 register PC : bits(64)
 register nextPC : bits(64)
 
@@ -75,8 +84,7 @@ val wGPR : forall 'n, 0 <= 'n < 32. (regno('n), regval) -> unit effect {wreg}
 function wGPR (r, v) = 
   if (r != 0) then {
      (*GPRs[r - 1]) = v;
-     print_int("GPR ", r);
-     print_bits("<- ", v);
+     print_string("x", concat_str(string_of_int(r), concat_str(" <- ", BitStr(v))));
   }
 
 function check_alignment (addr : bits(64), width : atom('n)) -> forall 'n. unit =