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

val cast print_insn : ast -> string
scattered function print_insn

/* ****************************************************************** */
union clause ast = UTYPE : (bits(20), regbits, uop)

function clause decode imm : bits(20) @ rd : regbits @ 0b0110111 = Some(UTYPE(imm, rd, RISCV_LUI))
function clause decode imm : bits(20) @ rd : regbits @ 0b0010111 = Some(UTYPE(imm, rd, RISCV_AUIPC))

function clause execute UTYPE(imm, rd, op) =
    let off : xlenbits = EXTS(imm @ 0x000) in
    let ret : xlenbits   = match op {
      RISCV_LUI   => off,
      RISCV_AUIPC => PC + off
    } in
    X(rd) = ret

function clause print_insn UTYPE(imm, rd, op) =
  match (op) {
    RISCV_LUI   => "lui   " ^ rd ^ ", " ^ BitStr(imm),
    RISCV_AUIPC => "auipc " ^ rd ^ ", " ^ BitStr(imm)
  }

/* ****************************************************************** */
union clause ast = RISCV_JAL : (bits(21), regbits)

function clause decode imm : bits(20) @ rd : regbits @ 0b1101111 = Some (RISCV_JAL(imm[19] @ imm[7..0] @ imm[8] @ imm[18..13] @ imm[12..9] @ 0b0, rd))

function clause execute (RISCV_JAL(imm, rd)) = {
    let pc : xlenbits = PC;
    X(rd) = nextPC;  /* compatible with JAL and C.JAL */
    let offset : xlenbits = EXTS(imm);
    nextPC = pc + offset;
}

function clause print_insn (RISCV_JAL(imm, rd)) =
  "jal   " ^ rd ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
union clause ast = RISCV_JALR : (bits(12), regbits, regbits)

function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b1100111 =
    Some(RISCV_JALR(imm, rs1, rd))

function clause execute (RISCV_JALR(imm, rs1, rd)) = {
    /* write rd before anything else to prevent unintended strength */
    X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
    let newPC : xlenbits = X(rs1) + EXTS(imm);
    nextPC = newPC[63..1] @ 0b0;
}

function clause print_insn (RISCV_JALR(imm, rs1, rd)) =
  "jalr  " ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
union clause ast = BTYPE : (bits(13), regbits, regbits, bop)

function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b000 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BEQ))
function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b001 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BNE))
function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b100 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BLT))
function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b101 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BGE))
function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b110 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BLTU))
function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b111 @ imm5 : bits(5) @ 0b1100011 = Some(BTYPE(imm7[6] @ imm5[0] @ imm7[5..0] @ imm5[4..1] @ 0b0, rs2, rs1, RISCV_BGEU))

function clause execute (BTYPE(imm, rs2, rs1, op)) =
  let rs1_val = X(rs1) in
  let rs2_val = X(rs2) in
  let taken : bool = match op {
    RISCV_BEQ  => rs1_val == rs2_val,
    RISCV_BNE  => rs1_val != rs2_val,
    RISCV_BLT  => rs1_val <_s rs2_val,
    RISCV_BGE  => rs1_val >=_s rs2_val,
    RISCV_BLTU => rs1_val <_u rs2_val,
    RISCV_BGEU => rs1_val >=_u rs2_val
  } in
  if taken then
    nextPC = PC + EXTS(imm)

function clause print_insn (BTYPE(imm, rs2, rs1, op)) =
  let insn : string =
    match (op) {
      RISCV_BEQ  => "beq   ",
      RISCV_BNE  => "bne   ",
      RISCV_BLT  => "blt   ",
      RISCV_BGE  => "bge   ",
      RISCV_BLTU => "bltu  ",
      RISCV_BGEU => "bgeu  "
    } in
  insn ^ rs1 ^ ", " ^ rs2 ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
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 decode imm : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_SLTI))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_SLTIU))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_XORI))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ORI))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0010011 = Some(ITYPE(imm, rs1, rd, RISCV_ANDI))

function clause execute (ITYPE (imm, rs1, rd, op)) =
  let rs1_val = X(rs1) in
  let immext : xlenbits = EXTS(imm) in
  let result : xlenbits = match op {
    RISCV_ADDI  => rs1_val + immext,
    RISCV_SLTI  => EXTZ(rs1_val <_s immext),
    RISCV_SLTIU => EXTZ(rs1_val <_u immext),
    RISCV_XORI  => rs1_val ^ immext,
    RISCV_ORI   => rs1_val | immext,
    RISCV_ANDI  => rs1_val & immext
  } in
  X(rd) = result

function clause print_insn (ITYPE(imm, rs1, rd, op)) =
  let insn : string =
    match (op) {
      RISCV_ADDI  => "addi  ",
      RISCV_SLTI  => "slti  ",
      RISCV_SLTIU => "sltiu ",
      RISCV_XORI  => "xori  ",
      RISCV_ORI   => "ori   ",
      RISCV_ANDI  => "andi  "
    } in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
union clause ast = SHIFTIOP : (bits(6), regbits, regbits, sop)

function clause decode 0b000000 @ shamt : bits(6) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SLLI))
function clause decode 0b000000 @ shamt : bits(6) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRLI))
function clause decode 0b010000 @ shamt : bits(6) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0010011 = Some(SHIFTIOP(shamt, rs1, rd, RISCV_SRAI))

function clause execute (SHIFTIOP(shamt, rs1, rd, op)) =
    let rs1_val = X(rs1) in
    let result : xlenbits = match op {
      RISCV_SLLI => rs1_val << shamt,
      RISCV_SRLI => rs1_val >> shamt,
      RISCV_SRAI => shift_right_arith64(rs1_val, shamt)
    } in
    X(rd) = result


function clause print_insn (SHIFTIOP(shamt, rs1, rd, op)) =
  let insn : string =
    match (op) {
      RISCV_SLLI => "slli  ",
      RISCV_SRLI => "srli  ",
      RISCV_SRAI => "srai  "
    } in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(shamt)

/* ****************************************************************** */
union clause ast = RTYPE : (regbits, regbits, regbits, rop)

function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_ADD))
function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SUB))
function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLL))
function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLT))
function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SLTU))
function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_XOR))
function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SRL))
function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_SRA))
function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_OR))
function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0110011 = Some(RTYPE(rs2, rs1, rd, RISCV_AND))

function clause execute (RTYPE(rs2, rs1, rd, op)) =
  let rs1_val = X(rs1) in
  let rs2_val = X(rs2) in
  let result : xlenbits = match op {
    RISCV_ADD  => rs1_val + rs2_val,
    RISCV_SUB  => rs1_val - rs2_val,
    RISCV_SLL  => rs1_val << (rs2_val[5..0]),
    RISCV_SLT  => EXTZ(rs1_val <_s rs2_val),
    RISCV_SLTU => EXTZ(rs1_val <_u rs2_val),
    RISCV_XOR  => rs1_val ^ rs2_val,
    RISCV_SRL  => rs1_val >> (rs2_val[5..0]),
    RISCV_SRA  => shift_right_arith64(rs1_val, rs2_val[5..0]),
    RISCV_OR   => rs1_val | rs2_val,
    RISCV_AND  => rs1_val & rs2_val
  } in
  X(rd) = result

function clause print_insn (RTYPE(rs2, rs1, rd, op)) =
  let insn : string =
    match (op) {
      RISCV_ADD  => "add   ",
      RISCV_SUB  => "sub   ",
      RISCV_SLL  => "sll   ",
      RISCV_SLT  => "slt   ",
      RISCV_SLTU => "sltu  ",
      RISCV_XOR  => "xor   ",
      RISCV_SRL  => "srl   ",
      RISCV_SRA  => "sra   ",
      RISCV_OR   => "or    ",
      RISCV_AND  => "and   "
    } in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, bool)

function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, BYTE,   false, false))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, HALF,   false, false))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, WORD,   false, false))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  BYTE,   false, false))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  HALF,   false, false))
function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  WORD,   false, false))

val extend_value : forall 'n, 0 < 'n <= 8. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
function extend_value(is_unsigned, value) = match (value) {
  MemValue(v)     => MemValue(if is_unsigned then EXTZ(v) else EXTS(v) : xlenbits),
  MemException(e) => MemException(e)
}

val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit effect {escape, rreg, wreg}
function process_load(rd, addr, value, is_unsigned) =
  match (extend_value(is_unsigned, value)) {
    MemValue(result) => X(rd) = result,
    MemException(e)  => handle_mem_exception(addr, e)
  }

function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
    let vaddr : xlenbits = X(rs1) + EXTS(imm) in
    match translateAddr(vaddr, Read, Data) {
      TR_Failure(e) => handle_mem_exception(vaddr, e),
      TR_Address(addr) =>
        match width {
          BYTE   => process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned),
          HALF   => process_load(rd, vaddr, mem_read(addr, 2, aq, rl, false), is_unsigned),
          WORD   => process_load(rd, vaddr, mem_read(addr, 4, aq, rl, false), is_unsigned),
          DOUBLE => process_load(rd, vaddr, mem_read(addr, 8, aq, rl, false), is_unsigned)
        }
    }

/* FIXME: aq/rl are getting dropped */
function clause print_insn (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
  let insn : string =
    match (width, is_unsigned) {
      (BYTE,   false) => "lb    ",
      (BYTE,   true)  => "lbu   ",
      (HALF,   false) => "lh    ",
      (HALF,   true)  => "lhu   ",
      (WORD,   false) => "lw    ",
      (WORD,   true)  => "lwu   ",
      (DOUBLE, false) => "ld    ",
      (DOUBLE, true)  => "ldu   "
    } in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool)

function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b000 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, BYTE, false, false))
function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b001 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, HALF, false, false))
function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b010 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, WORD, false, false))
function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b011 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false))

/* NOTE: Currently, we only EA if address translation is successful.
   This may need revisiting. */
function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
    let vaddr : xlenbits = X(rs1) + EXTS(imm) in
    match translateAddr(vaddr, Write, Data) {
      TR_Failure(e) => handle_mem_exception(vaddr, e),
      TR_Address(addr) =>
        let eares : MemoryOpResult(unit) = match width {
          BYTE   => mem_write_ea(addr, 1, aq, rl, false),
          HALF   => mem_write_ea(addr, 2, aq, rl, false),
          WORD   => mem_write_ea(addr, 4, aq, rl, false),
          DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
        } in
        match (eares) {
          MemException(e) => handle_mem_exception(addr, e),
          MemValue(_) => {
            let rs2_val = X(rs2) in
            let res : MemoryOpResult(unit) = match width {
              BYTE   => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
              HALF   => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
              WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
              DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
            } in
            match (res) {
              MemValue(_)     => (),
              MemException(e) => handle_mem_exception(addr, e)
            }
          }
        }
    }

/* FIXME: aq/rl are getting dropped */
function clause print_insn (STORE(imm, rs2, rs1, width, aq, rl)) =
  let insn : string =
    match (width) {
      BYTE   => "sb    ",
      HALF   => "sh    ",
      WORD   => "sw    ",
      DOUBLE => "sd    "
    } in
  insn ^ rs2 ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
union clause ast = ADDIW : (bits(12), regbits, regbits)

function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0011011 = Some(ADDIW(imm, rs1, rd))

function clause execute (ADDIW(imm, rs1, rd)) =
  let result : xlenbits = EXTS(imm) + X(rs1) in
  X(rd) = EXTS(result[31..0])

function clause print_insn (ADDIW(imm, rs1, rd)) =
  "addiw " ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
union clause ast = SHIFTW : (bits(5), regbits, regbits, sop)

function clause decode 0b0000000 @ shamt : bits(5) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SLLI))
function clause decode 0b0000000 @ shamt : bits(5) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SRLI))
function clause decode 0b0100000 @ shamt : bits(5) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0011011 = Some(SHIFTW(shamt, rs1, rd, RISCV_SRAI))

function clause execute (SHIFTW(shamt, rs1, rd, op)) =
    let rs1_val = (X(rs1))[31..0] in
    let result : bits(32) = match op {
      RISCV_SLLI => rs1_val << shamt,
      RISCV_SRLI => rs1_val >> shamt,
      RISCV_SRAI => shift_right_arith32(rs1_val, shamt)
    } in
    X(rd) = EXTS(result)

function clause print_insn (SHIFTW(shamt, rs1, rd, op)) =
  let insn : string =
    match (op) {
      RISCV_SLLI => "slli  ",
      RISCV_SRLI => "srli  ",
      RISCV_SRAI => "srai  "
    } in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(shamt)

/* ****************************************************************** */
union clause ast = RTYPEW : (regbits, regbits, regbits, ropw)

function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_ADDW))
function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SUBW))
function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SLLW))
function clause decode 0b0000000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SRLW))
function clause decode 0b0100000 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(RTYPEW(rs2, rs1, rd, RISCV_SRAW))

function clause execute (RTYPEW(rs2, rs1, rd, op)) =
  let rs1_val = (X(rs1))[31..0] in
  let rs2_val = (X(rs2))[31..0] in
  let result : bits(32) = match op {
    RISCV_ADDW => rs1_val + rs2_val,
    RISCV_SUBW => rs1_val - rs2_val,
    RISCV_SLLW => rs1_val << (rs2_val[4..0]),
    RISCV_SRLW => rs1_val >> (rs2_val[4..0]),
    RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0])
  } in
  X(rd) = EXTS(result)

function clause print_insn (RTYPEW(rs2, rs1, rd, op)) =
  let insn : string =
    match (op) {
      RISCV_ADDW => "addw  ",
      RISCV_SUBW => "subw  ",
      RISCV_SLLW => "sllw  ",
      RISCV_SRLW => "srlw  ",
      RISCV_SRAW => "sraw  "
    } in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
/* FIXME: separate these out into separate ast variants */
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 = X(rs1) in
  let rs2_val = X(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
  X(rd) = result

function clause print_insn (MUL(rs2, rs1, rd, high, signed1, signed2)) =
  let insn : string =
    match (high, signed1, signed2) {
      (false, true, true)  => "mul   ",
      (true,  true, true)  => "mulh  ",
      (true,  true, false) => "mulhsu ",
      (true, false, false) => "mulhu"
    } in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
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 = X(rs1) in
  let rs2_val = X(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 > xlen_max_signed then xlen_min_signed else q in /* check for signed overflow */  X(rd) = to_bits(xlen, q')

function clause print_insn (DIV(rs2, rs1, rd, s)) =
  let insn : string = if s then "div   " else "divu  " in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
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 = X(rs1) in
  let rs2_val = X(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 */
  X(rd) = to_bits(xlen, r)

function clause print_insn (REM(rs2, rs1, rd, s)) =
  let insn : string = if s then "rem   " else "remu  " in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
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 = X(rs1)[31..0] in
  let rs2_val = X(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 result : xlenbits = EXTS(result32) in
  X(rd) = result

function clause print_insn (MULW(rs2, rs1, rd)) =
  "mulw  " ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
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 = X(rs1)[31..0] in
  let rs2_val = X(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 */
  X(rd) = EXTS(to_bits(32, q'))

function clause print_insn (DIVW(rs2, rs1, rd, s)) =
  let insn : string = if s then "divw  " else "divuw " in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
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 = X(rs1)[31..0] in
  let rs2_val = X(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 */
  X(rd) = EXTS(to_bits(32, r))

function clause print_insn (REMW(rs2, rs1, rd, s)) =
  let insn : string = if s then "remw  " else "remuw " in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
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))

function clause execute (FENCE(pred, succ)) = {
  match (pred, succ) {
    (0b0011, 0b0011) => MEM_fence_rw_rw(),
    (0b0010, 0b0011) => MEM_fence_r_rw(),
    (0b0010, 0b0010) => MEM_fence_r_r(),
    (0b0011, 0b0001) => MEM_fence_rw_w(),
    (0b0001, 0b0001) => MEM_fence_w_w(),
    _ => { print("FIXME: unsupported fence");
           () }
  }
}

/* FIXME */
function clause print_insn (FENCE(pred, succ)) =
  "fence"

/* ****************************************************************** */
union clause ast = FENCEI : unit

function clause decode 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 = Some(FENCEI())

function clause execute FENCEI() = MEM_fence_i()

function clause print_insn (FENCEI()) =
  "fence.i"

/* ****************************************************************** */
union clause ast = ECALL : unit

function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL())

function clause execute ECALL() =
  let t : sync_exception =
    struct { trap = match (cur_privilege) {
                      User => E_U_EnvCall,
                      Supervisor => E_S_EnvCall,
                      Machine => E_M_EnvCall
		    },
	     excinfo = (None() : option(xlenbits)) } in
  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)

function clause print_insn (ECALL()) =
  "ecall"

/* ****************************************************************** */
union clause ast = MRET : unit

function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET())

function clause execute MRET() = {
  if cur_privilege == Machine then
    nextPC = handle_exception(cur_privilege, CTL_MRET(), PC)
  else
    handle_illegal()
}

function clause print_insn (MRET()) =
  "mret"

/* ****************************************************************** */
union clause ast = SRET : unit

function clause decode 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(SRET())

function clause execute SRET() =
  match cur_privilege {
    User       => handle_illegal(),
    Supervisor => if mstatus.TSR() == true
                  then handle_illegal()
                  else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC),
    Machine    => nextPC = handle_exception(cur_privilege, CTL_SRET(), PC)
  }

function clause print_insn (SRET()) =
  "sret"

/* ****************************************************************** */
union clause ast = EBREAK : unit

function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK())

function clause execute EBREAK() =
  handle_mem_exception(PC, E_Breakpoint)

function clause print_insn (EBREAK()) =
  "ebreak"

/* ****************************************************************** */
union clause ast = WFI : unit

function clause decode 0b000100000101 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(WFI())

function clause execute WFI() = {
  match cur_privilege {
    Machine    => (),
    Supervisor => if mstatus.TW() == true
                  then handle_illegal()
                  else (),
    User       => handle_illegal()
  }
}

function clause print_insn (WFI()) =
  "wfi"

/* ****************************************************************** */
union clause ast = SFENCE_VMA : (regbits, regbits)

function clause decode 0b0001001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ 0b00000 @ 0b1110011 = Some(SFENCE_VMA(rs1, rs2))

function clause execute SFENCE_VMA(rs1, rs2) = {
  /* FIXME: spec leaves unspecified what happens if this is executed in M-mode.
     We assume it is the same as S-mode, which is definitely wrong.
   */
  if cur_privilege == User then handle_illegal()
  else match (architecture(mstatus.SXL()), mstatus.TVM()) {
    (Some(RV64), true)  => handle_illegal(),
    (Some(RV64), false) => {
      let addr : option(vaddr39) = if rs1 == 0 then None() else Some(X(rs1)[38 .. 0]);
      let asid : option(asid64)  = if rs2 == 0 then None() else Some(X(rs2)[15 .. 0]);
      flushTLB(asid, addr)
    },
    (_, _) => internal_error("unimplemented sfence architecture")
  }
}

function clause print_insn (SFENCE_VMA(rs1, rs2)) =
  "sfence.vma " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits)

function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, WORD, rd))
function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))

val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit

function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
  let vaddr : xlenbits = X(rs1) in
  match translateAddr(vaddr, Read, Data) {
    TR_Failure(e) => handle_mem_exception(vaddr, e),
    TR_Address(addr) =>
      match width {
        WORD   => process_load(rd, addr, mem_read(addr, 4, aq, rl, true), false),
        DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, true), false),
        _      => internal_error("LOADRES expected WORD or DOUBLE")
      }
  }

/* FIXME */
function clause print_insn (LOADRES(aq, rl, rs1, width, rd)) =
  let insn : string =
    match (width) {
      WORD   => "lr.w  ",
      DOUBLE => "lr.d  ",
      _      => "lr.bad "
    } in
  insn ^ rd ^ ", " ^ rs1

/* ****************************************************************** */
union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits)

function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
function clause decode 0b00011 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd))

/* NOTE: Currently, we only EA if address translation is successful.
   This may need revisiting. */
function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
  status : bits(1) = if speculate_conditional_success() then 0b0 else 0b1;
  X(rd) = EXTZ(status);

  if status == 0b1 then () else {
    vaddr : xlenbits = X(rs1);
    match translateAddr(vaddr, Write, Data) {
      TR_Failure(e) => handle_mem_exception(vaddr, e),
      TR_Address(addr) => {
        let eares : MemoryOpResult(unit) = match width {
          WORD   => mem_write_ea(addr, 4, aq, rl, true),
          DOUBLE => mem_write_ea(addr, 8, aq, rl, true),
          _      => internal_error("STORECON expected word or double")
        };
        match (eares) {
          MemException(e)  => handle_mem_exception(addr, e),
          MemValue(_) => {
            rs2_val = X(rs2);
            let res : MemoryOpResult(unit) = match width {
              WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
              DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
              _      => internal_error("STORECON expected word or double")
            } in
            match (res) {
              MemValue(_)     => (),
              MemException(e) => handle_mem_exception(addr, e)
            }
          }
        }
      }
    }
  }
}

/* FIXME */
function clause print_insn (STORECON(aq, rl, rs2, rs1, width, rd)) =
  let insn : string =
    match (width) {
      WORD   => "sc.w  ",
      DOUBLE => "sc.d  ",
      _      => "sc.bad "
    } in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
union clause ast = AMO : (amoop, bool, bool, regbits, regbits, word_width, regbits)

function clause decode 0b00001 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD,   rd))
function clause decode 0b00001 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode 0b00000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD,   rd))
function clause decode 0b00000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode 0b00100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD,   rd))
function clause decode 0b00100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode 0b01100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD,   rd))
function clause decode 0b01100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode 0b01000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOOR  , aq, rl, rs2, rs1, WORD,   rd))
function clause decode 0b01000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOOR  , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode 0b10000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD,   rd))
function clause decode 0b10000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode 0b10100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD,   rd))
function clause decode 0b10100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode 0b11000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD,   rd))
function clause decode 0b11000 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD,   rd))
function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))

/* NOTE: Currently, we only EA if address translation is successful.
   This may need revisiting. */
function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
  vaddr : xlenbits = X(rs1);
  match translateAddr(vaddr, ReadWrite, Data) {
    TR_Failure(e) => handle_mem_exception(vaddr, e),
    TR_Address(addr) => {
      let eares : MemoryOpResult(unit) = match width {
        WORD   => mem_write_ea(addr, 4, aq & rl, rl, true),
        DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true),
        _      => internal_error ("AMO expected WORD or DOUBLE")
      };
      match (eares) {
        MemException(e) => handle_mem_exception(addr, e),
        MemValue(_) => {
          let rval : MemoryOpResult(xlenbits) = match width {
            WORD   => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
            DOUBLE => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)),
          _        => internal_error ("AMO expected WORD or DOUBLE")
          };
          match (rval) {
            MemException(e) => handle_mem_exception(addr, e),
            MemValue(loaded) => {
              rs2_val : xlenbits = X(rs2);
              result : xlenbits =
                match op {
                  AMOSWAP => rs2_val,
                  AMOADD  => rs2_val + loaded,
                  AMOXOR  => rs2_val ^ loaded,
                  AMOAND  => rs2_val & loaded,
                  AMOOR   => rs2_val | loaded,

                  /* Have to convert number to vector here. Check this */
                  AMOMIN  => vector64(min(signed(rs2_val),   signed(loaded))),
                  AMOMAX  => vector64(max(signed(rs2_val),   signed(loaded))),
                  AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))),
                  AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded)))
                };

              let wval : MemoryOpResult(unit) = match width {
                WORD   => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
                DOUBLE => mem_write_value(addr, 8, result,        aq & rl, rl, true),
                _      => internal_error("AMO expected WORD or DOUBLE")
              };
              match (wval) {
                MemValue(_) => X(rd) = loaded,
                MemException(e) => handle_mem_exception(addr, e)
              }
            }
          }
        }
      }
    }
  }
}

function clause print_insn (AMO(op, aq, rl, rs2, rs1, width, rd)) =
  let insn : string =
    match (op, width) {
      (AMOSWAP, WORD) => "amoswap.w ",
      (AMOADD , WORD) => "amoadd.w  ",
      (AMOXOR , WORD) => "amoxor.w  ",
      (AMOAND , WORD) => "amoand.w  ",
      (AMOOR  , WORD) => "amoor.w   ",
      (AMOMIN , WORD) => "amomin.w  ",
      (AMOMAX , WORD) => "amomax.w  ",
      (AMOMINU, WORD) => "amominu.w ",
      (AMOMAXU, WORD) => "amomaxu.w ",
      (AMOSWAP, DOUBLE) => "amoswap.d ",
      (AMOADD , DOUBLE) => "amoadd.d  ",
      (AMOXOR , DOUBLE) => "amoxor.d  ",
      (AMOAND , DOUBLE) => "amoand.d  ",
      (AMOOR  , DOUBLE) => "amoor.d   ",
      (AMOMIN , DOUBLE) => "amomin.d  ",
      (AMOMAX , DOUBLE) => "amomax.d  ",
      (AMOMINU, DOUBLE) => "amominu.d ",
      (AMOMAXU, DOUBLE) => "amomaxu.d ",
      (_, _)            => "amo.bad "
    } in
  insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2

/* ****************************************************************** */
union clause ast = CSR  : (bits(12), regbits, regbits, bool, csrop)

function clause decode csr : bits(12) @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, false, CSRRW))
function clause decode csr : bits(12) @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, false, CSRRS))
function clause decode csr : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, false, CSRRC))
function clause decode csr : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRW))
function clause decode csr : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRS))
function clause decode csr : bits(12) @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRC))

function readCSR csr : csreg -> xlenbits =
  match csr {
    /* machine mode */
    0xF11 => mvendorid,
    0xF12 => marchid,
    0xF13 => mimpid,
    0xF14 => mhartid,
    0x300 => mstatus.bits(),
    0x301 => misa.bits(),
    0x302 => medeleg.bits(),
    0x303 => mideleg.bits(),
    0x304 => mie.bits(),
    0x305 => mtvec.bits(),
    0x340 => mscratch,
    0x341 => mepc,
    0x342 => mcause.bits(),
    0x343 => mtval,
    0x344 => mip.bits(),

    /* supervisor mode */
    0x100 => mstatus.bits(), /* FIXME: legalize view*/
    0x102 => sedeleg.bits(),
    0x103 => sideleg.bits(),
    0x104 => lower_mie(mie, mideleg).bits(),
    0x105 => stvec.bits(),
    0x140 => sscratch,
    0x141 => sepc,
    0x142 => scause.bits(),
    0x143 => stval,
    0x144 => lower_mip(mip, mideleg).bits(),
    0x180 => satp,

    /* others */
    0xC00 => mcycle,
    0xC01 => mtime,
    0xC02 => minstret,

    /* trigger/debug */
    0x7a0 => ~(tselect),    /* this indicates we don't have any trigger support */

    _     => { print_bits("unhandled read to CSR ", csr);
               0x0000_0000_0000_0000 }
  }

function writeCSR (csr : csreg, value : xlenbits) -> unit =
  let res : option(xlenbits) =
  match csr {
    /* machine mode */
    0x300 => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits()) },
    0x302 => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits()) },
    0x303 => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits()) },
    0x304 => { mie = legalize_mie(mie, value); Some(mie.bits()) },
    0x305 => { mtvec = legalize_tvec(mtvec, value); Some(mtvec.bits()) },
    0x340 => { mscratch = value; Some(mscratch) },
    0x341 => { mepc = legalize_xepc(value); Some(mepc) },
    0x342 => { mcause->bits() = value; Some(mcause.bits()) },
    0x343 => { mtval = value; Some(mtval) },
    0x344 => { mip = legalize_mip(mip, value); Some(mip.bits()) },

    /* supervisor mode */
    0x100 => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits()) },
    0x102 => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits()) },
    0x103 => { sideleg->bits() = value; Some(sideleg.bits()) }, /* TODO: does this need legalization? */
    0x104 => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) },
    0x105 => { stvec = legalize_tvec(stvec, value); Some(stvec.bits()) },
    0x140 => { sscratch = value; Some(sscratch) },
    0x141 => { sepc = legalize_xepc(value); Some(sepc) },
    0x142 => { scause->bits() = value; Some(scause.bits()) },
    0x143 => { stval = value; Some(stval) },
    0x144 => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) },
    0x180 => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) },

    /* trigger/debug */
    0x7a0 => { tselect = value; Some(tselect) },

    _     => None()
  } in
  match res {
    Some(v) => print("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
    None()  => print_bits("unhandled write to CSR ", csr)
  }

function clause execute CSR(csr, rs1, rd, is_imm, op) =
  let rs1_val : xlenbits = if is_imm then EXTZ(rs1) else X(rs1) in
  let isWrite : bool = match op {
    CSRRW  => true,
    _      => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0
  } in
  if ~ (check_CSR(csr, cur_privilege, isWrite))
  then handle_illegal()
  else {
    let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */
    if isWrite then {
      let new_val : xlenbits = match op {
        CSRRW => rs1_val,
        CSRRS => csr_val | rs1_val,
        CSRRC => csr_val & ~(rs1_val)
      } in
      writeCSR(csr, new_val)
    };
    X(rd) = csr_val
  }

function clause print_insn (CSR(csr, rs1, rd, is_imm, op)) =
  let insn : string =
    match (op, is_imm) {
      (CSRRW, true)  => "csrrwi ",
      (CSRRW, false) => "csrrw  ",
      (CSRRS, true)  => "csrrsi ",
      (CSRRS, false) => "csrrs  ",
      (CSRRC, true)  => "csrrci ",
      (CSRRC, false) => "csrrc  "
    } in
  let rs1_str : string = if is_imm then BitStr(rs1) else reg_name_abi(rs1) in
  insn ^ rd ^ ", " ^ rs1_str ^ ", " ^ csr_name(csr)

/* ****************************************************************** */
union clause ast = NOP : unit

function clause decodeCompressed (0b000 @ nzi1 : bits(1) @ 0b00000 @ (nzi0 : bits(5)) @ 0b01) : bits(16) = {
  if (nzi1 == 0b0) & (nzi0 == 0b00000) then Some(NOP())
  else None()
}

function clause execute NOP() = ()

function clause print_insn (NOP()) =
  "nop"

/* ****************************************************************** */
union clause ast = ILLEGAL : unit

function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b00) : bits(16) = Some(ILLEGAL())

function clause execute ILLEGAL() = handle_illegal ()

function clause print_insn (ILLEGAL()) =
  "illegal"

/* ****************************************************************** */
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))
}

function clause print_insn (C_ADDI4SPN(rdc, nzimm)) =
  "c.addi4spn " ^ creg2reg_bits(rdc) ^ ", " ^ BitStr(nzimm)

/* ****************************************************************** */
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, false, WORD, false, false))
}

function clause print_insn (C_LW(uimm, rsc, rdc)) =
  "c.lw   " ^ creg2reg_bits(rdc) ^ ", " ^ creg2reg_bits(rsc) ^ ", " ^ BitStr(uimm)

/* ****************************************************************** */
union clause ast = C_LD : (bits(5), cregbits, cregbits)

function clause decodeCompressed (0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00) : bits(16) = {
  let uimm = (ui76 @ ui53) : bits(5) in
  Some(C_LD(uimm, rs1, rd))
}

function clause execute (C_LD(uimm, rsc, rdc)) = {
  let imm : bits(12) = EXTZ(uimm @ 0b000) in
  let rd = creg2reg_bits(rdc) in
  let rs = creg2reg_bits(rsc) in
  execute(LOAD(imm, rs, rd, false, DOUBLE, false, false))
}

function clause print_insn (C_LD(uimm, rsc, rdc)) =
  "c.ld   " ^ creg2reg_bits(rdc) ^ ", " ^ creg2reg_bits(rsc) ^ ", " ^ BitStr(uimm)

/* ****************************************************************** */
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))
}

function clause print_insn (C_SW(uimm, rsc1, rsc2)) =
  "c.sw   " ^ creg2reg_bits(rsc1) ^ ", " ^ creg2reg_bits(rsc2) ^ ", " ^ BitStr(uimm)

/* ****************************************************************** */
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))
}

function clause print_insn (C_SD(uimm, rsc1, rsc2)) =
  "c.sd   " ^ creg2reg_bits(rsc1) ^ ", " ^ creg2reg_bits(rsc2) ^ ", " ^ BitStr(uimm)

/* ****************************************************************** */
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))
}

function clause print_insn (C_ADDI(nzi, rsd)) =
  "c.addi   " ^ rsd ^ ", " ^ BitStr(nzi)

/* ****************************************************************** */
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 = X(rsd) in
  let res : bits(32) = rs_val[31..0] + imm in
  X(rsd) = EXTS(res)
}

function clause print_insn (C_JAL(imm)) =
  "c.jal   " ^ BitStr(imm)

function clause print_insn (C_ADDIW(imm, rsd)) =
  "c.addiw " ^ rsd ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
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))
}

function clause print_insn (C_LI(imm, rd)) =
  "c.li  " ^ rd ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
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))
}

function clause print_insn (C_ADDI16SP(imm)) =
  "c.addi16sp  " ^ BitStr(imm)

/* ****************************************************************** */
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))
}

function clause print_insn (C_LUI(imm, rd)) =
  "c.lui  " ^ rd ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
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))
}

function clause print_insn (C_SRLI(shamt, rsd)) =
  "c.srli  " ^ creg2reg_bits(rsd) ^ ", " ^ BitStr(shamt)

/* ****************************************************************** */
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))
}

function clause print_insn (C_SRAI(shamt, rsd)) =
  "c.srai  " ^ creg2reg_bits(rsd) ^ ", " ^ BitStr(shamt)

/* ****************************************************************** */
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))
}

function clause print_insn (C_ANDI(imm, rsd)) =
  "c.andi  " ^ creg2reg_bits(rsd) ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
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))
}

function clause print_insn (C_SUB(rsd, rs2)) =
  "c.sub  " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2)

/* ****************************************************************** */
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_XOR(rsd, rs2)) = {
  let rsd = creg2reg_bits(rsd) in
  let rs2 = creg2reg_bits(rs2) in
  execute(RTYPE(rs2, rsd, rsd, RISCV_XOR))
}

function clause print_insn (C_XOR(rsd, rs2)) =
  "c.xor  " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2)

/* ****************************************************************** */
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))
}

function clause print_insn (C_OR(rsd, rs2)) =
  "c.or   " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2)

/* ****************************************************************** */
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_AND(rsd, rs2)) = {
  let rsd = creg2reg_bits(rsd) in
  let rs2 = creg2reg_bits(rs2) in
  execute(RTYPE(rs2, rsd, rsd, RISCV_AND))
}

function clause print_insn (C_AND(rsd, rs2)) =
  "c.and  " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2)

/* ****************************************************************** */
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(RTYPEW(rs2, rsd, rsd, RISCV_SUBW))
}

function clause print_insn (C_SUBW(rsd, rs2)) =
  "c.subw " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2)

/* ****************************************************************** */
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(RTYPEW(rs2, rsd, rsd, RISCV_ADDW))
}

function clause print_insn (C_ADDW(rsd, rs2)) =
  "c.addw " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2)

/* ****************************************************************** */
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))

function clause print_insn (C_J(imm)) =
  "c.j    " ^ BitStr(imm)

/* ****************************************************************** */
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))

function clause print_insn (C_BEQZ(imm, rs)) =
  "c.beqz " ^ creg2reg_bits(rs) ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
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 print_insn (C_BNEZ(imm, rs)) =
  "c.bnez " ^ creg2reg_bits(rs) ^ ", " ^ BitStr(imm)

/* ****************************************************************** */
union clause ast = C_SLLI : (bits(6), regbits)

function clause decodeCompressed (0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10) = {
  let shamt : bits(6) = nzui5 @ nzui40 in
  if shamt == 0b000000 | rsd == zreg /* TODO: On RV32, also need shamt[5] == 0 */
  then None()
  else Some(C_SLLI(shamt, rsd))
}

function clause execute (C_SLLI(shamt, rsd)) =
  execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI))

function clause print_insn (C_SLLI(shamt, rsd)) =
  "c.slli " ^ rsd ^ ", " ^ BitStr(shamt)

/* ****************************************************************** */
union clause ast = C_LWSP : (bits(6), regbits)

function clause decodeCompressed (0b010 @ ui5 : bits(1) @ rd : regbits @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10) = {
  let uimm : bits(6) = ui76 @ ui5 @ ui42 in
  if  rd == zreg
  then None()
  else Some(C_LWSP(uimm, rd))
}

function clause execute (C_LWSP(uimm, rd)) = {
  let imm : bits(12) = EXTZ(uimm @ 0b00) in
  execute(LOAD(imm, sp, rd, false, WORD, false, false))
}

function clause print_insn (C_LWSP(uimm, rd)) =
  "c.lwsp " ^ rd ^ ", " ^ BitStr(uimm)

/* ****************************************************************** */
union clause ast = C_LDSP : (bits(6), regbits)

function clause decodeCompressed (0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10) = {
  let uimm : bits(6) = ui86 @ ui5 @ ui43 in
  if  rd == zreg
  then None()
  else Some(C_LDSP(uimm, rd))
}

function clause execute (C_LDSP(uimm, rd)) = {
  let imm : bits(12) = EXTZ(uimm @ 0b000) in
  execute(LOAD(imm, sp, rd, false, DOUBLE, false, false))
}

function clause print_insn (C_LDSP(uimm, rd)) =
  "c.ldsp " ^ rd ^ ", " ^ BitStr(uimm)

/* ****************************************************************** */
union clause ast = C_SWSP : (bits(6), regbits)

function clause decodeCompressed (0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regbits @ 0b10) = {
  let uimm : bits(6) = ui76 @ ui52 in
  Some(C_SWSP(uimm, rs2))
}

function clause execute (C_SWSP(uimm, rs2)) = {
  let imm : bits(12) = EXTZ(uimm @ 0b00) in
  execute(STORE(imm, rs2, sp, WORD, false, false))
}

function clause print_insn (C_SWSP(uimm, rd)) =
  "c.swsp " ^ rd ^ ", " ^ BitStr(uimm)

/* ****************************************************************** */
union clause ast = C_SDSP : (bits(6), regbits)

function clause decodeCompressed (0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10) = {
  let uimm : bits(6) = ui86 @ ui53 in
  Some(C_SDSP(uimm, rs2))
}

function clause execute (C_SDSP(uimm, rs2)) = {
  let imm : bits(12) = EXTZ(uimm @ 0b000) in
  execute(STORE(imm, rs2, sp, DOUBLE, false, false))
}

function clause print_insn (C_SDSP(uimm, rd)) =
  "c.sdsp " ^ rd ^ ", " ^ BitStr(uimm)

/* ****************************************************************** */
union clause ast = C_JR : (regbits)

function clause decodeCompressed (0b100 @ 0b0 @ rs1 : regbits @ 0b00000 @ 0b10) = {
  if rs1 == zreg
  then None()
  else Some(C_JR(rs1))
}

function clause execute (C_JR(rs1)) =
  execute(RISCV_JALR(EXTZ(0b0), rs1, zreg))

function clause print_insn (C_JR(rs1)) =
  "c.jr  " ^ rs1

/* ****************************************************************** */
union clause ast = C_JALR : (regbits)

function clause decodeCompressed (0b100 @ 0b1 @ rs1 : regbits @ 0b00000 @ 0b10) = {
  if rs1 == zreg
  then None()
  else Some(C_JALR(rs1))
}

function clause execute (C_JALR(rs1)) =
  execute(RISCV_JALR(EXTZ(0b0), rs1, ra))

function clause print_insn (C_JALR(rs1)) =
  "c.jalr  " ^ rs1

/* ****************************************************************** */
union clause ast = C_MV : (regbits, regbits)

function clause decodeCompressed (0b100 @ 0b0 @ rd : regbits @ rs2 : regbits @ 0b10) = {
  if rs2 == zreg | rd == zreg
  then None()
  else Some(C_MV(rd, rs2))
}

function clause execute (C_MV(rd, rs2)) =
  execute(RTYPE(rs2, zreg, rd, RISCV_ADD))

function clause print_insn (C_MV(rd, rs2)) =
  "c.mv  " ^ rd ^ ", " ^ rs2

/* ****************************************************************** */
union clause ast = C_ADD : (regbits, regbits)

function clause decodeCompressed (0b100 @ 0b1 @ rsd : regbits @ rs2 : regbits @ 0b10) = {
  if rsd == zreg | rs2 == zreg
  then None()
  else Some(C_ADD(rsd, rs2))
}

function clause execute (C_ADD(rsd, rs2)) =
  execute(RTYPE(rs2, rsd, rsd, RISCV_ADD))

function clause print_insn (C_ADD(rsd, rs2)) =
  "c.add  " ^ rsd ^ ", " ^ rs2

/* ****************************************************************** */

function clause decode _ = None()
function clause decodeCompressed _ = None()

end ast
end decode
end decodeCompressed
end execute
end print_insn