Rename EXTZ and EXTS

Rename EXTZ to zero_extend and EXTS to sign_extend. Two main reasons
for doing this - it means that the source more closely follows the
descriptions in the documentation with more readable names, and EXTS
and EXTZ are visually very close to each other with just the S and Z.
They are also following an odd convention where they are ALLCAPS rather
than snake_case like other functions in the spec.

I think this convention comes from early Power specs in Sail, which
influenced Sail MIPS and CHERI-MIPS, but I don't think it's a very
good convention we should be keeping in sail-riscv

model/prelude.sail

@@ -187,11 +187,11 @@ function get_config_print_reg () = false
 function get_config_print_mem () = false
 function get_config_print_platform () = false
 
-val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
-val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
+val sign_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
+val zero_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
 
-function EXTS(m, v) = sail_sign_extend(v, m)
-function EXTZ(m, v) = sail_zero_extend(v, m)
+function sign_extend(m, v) = sail_sign_extend(v, m)
+function zero_extend(m, v) = sail_zero_extend(v, m)
 
 val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
 function zeros_implicit (n) = sail_zeros(n)
@@ -245,11 +245,11 @@ overload operator << = {shift_bits_left, shiftl}
 /* Ideally these would be sail builtin */
 
 function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) =
- let v128 : bits(128) = EXTS(v) in
+ let v128 : bits(128) = sign_extend(v) in
  (v128 >> shift)[63..0]
 
 function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
- let v64 : bits(64) = EXTS(v) in
+ let v64 : bits(64) = sign_extend(v) in
  (v64 >> shift)[31..0]
 
 infix 7 >>>

model/riscv_analysis.sail

@@ -98,22 +98,22 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
  },
  RISCV_JAL(imm, rd) => {
  if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
- let offset : bits(64) = EXTS(imm) in
+ let offset : bits(64) = sign_extend(imm) in
  Nias = [| NIAFP_concrete_address (PC + offset) |];
  ik = IK_branch();
  },
  RISCV_JALR(imm, rs, rd) => {
  if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
  if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
- let offset : bits(64) = EXTS(imm) in
+ let offset : bits(64) = sign_extend(imm) in
  Nias = [| NIAFP_indirect_address() |];
  ik = IK_branch();
  },
  BTYPE(imm, rs2, rs1, op) => {
  if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
  if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
  ik = IK_branch();
- let offset : bits(64) = EXTS(imm) in
+ let offset : bits(64) = sign_extend(imm) in
  Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
  },
  ITYPE(imm, rs, rd, op) => {
@@ -271,22 +271,22 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
  },
  RISCV_JAL(imm, rd) => {
  if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
- let offset : bits(64) = EXTS(imm) in
+ let offset : bits(64) = sign_extend(imm) in
  Nias = [| NIAFP_concrete_address (PC + offset) |];
  ik = IK_branch();
  },
  RISCV_JALR(imm, rs, rd) => {
  if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
  if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
- let offset : bits(64) = EXTS(imm) in
+ let offset : bits(64) = sign_extend(imm) in
  Nias = [| NIAFP_indirect_address() |];
  ik = IK_branch();
  },
  BTYPE(imm, rs2, rs1, op) => {
  if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
  if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
  ik = IK_branch();
- let offset : bits(64) = EXTS(imm) in
+ let offset : bits(64) = sign_extend(imm) in
  Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
  },
  ITYPE(imm, rs, rd, op) => {

model/riscv_fdext_control.sail

@@ -83,12 +83,12 @@ function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx()
 function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx()
 function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveZfinx()
 
-function clause ext_read_CSR (0x001) = Some (EXTZ (fcsr.FFLAGS()))
-function clause ext_read_CSR (0x002) = Some (EXTZ (fcsr.FRM()))
-function clause ext_read_CSR (0x003) = Some (EXTZ (fcsr.bits()))
+function clause ext_read_CSR (0x001) = Some (zero_extend (fcsr.FFLAGS()))
+function clause ext_read_CSR (0x002) = Some (zero_extend (fcsr.FRM()))
+function clause ext_read_CSR (0x003) = Some (zero_extend (fcsr.bits()))
 
-function clause ext_write_CSR (0x001, value) = { ext_write_fcsr (fcsr.FRM(), value [4..0]); Some(EXTZ(fcsr.FFLAGS())) }
-function clause ext_write_CSR (0x002, value) = { ext_write_fcsr (value [2..0], fcsr.FFLAGS()); Some(EXTZ(fcsr.FRM())) }
-function clause ext_write_CSR (0x003, value) = { ext_write_fcsr (value [7..5], value [4..0]); Some(EXTZ(fcsr.bits())) }
+function clause ext_write_CSR (0x001, value) = { ext_write_fcsr (fcsr.FRM(), value [4..0]); Some(zero_extend(fcsr.FFLAGS())) }
+function clause ext_write_CSR (0x002, value) = { ext_write_fcsr (value [2..0], fcsr.FFLAGS()); Some(zero_extend(fcsr.FRM())) }
+function clause ext_write_CSR (0x003, value) = { ext_write_fcsr (value [7..5], value [4..0]); Some(zero_extend(fcsr.bits())) }
 
 /* **************************************************************** */

model/riscv_fdext_regs.sail

@@ -356,7 +356,7 @@ function wF_or_X_H(i, data) = {
  assert(sys_enable_fdext() != sys_enable_zfinx());
  if sys_enable_fdext()
  then F_H(i) = data
- else X(i) = EXTS(data)
+ else X(i) = sign_extend(data)
 }
 
 val wF_or_X_S : (bits(5), bits(32)) -> unit effect {escape, wreg}
@@ -365,7 +365,7 @@ function wF_or_X_S(i, data) = {
  assert(sys_enable_fdext() != sys_enable_zfinx());
  if sys_enable_fdext()
  then F_S(i) = data
- else X(i) = EXTS(data)
+ else X(i) = sign_extend(data)
 }
 
 val wF_or_X_D : (bits(5), bits(64)) -> unit effect {escape, wreg}
@@ -375,7 +375,7 @@ function wF_or_X_D(i, data) = {
  if sys_enable_fdext()
  then F_D(i) = data
  else if sizeof(xlen) >= 64
- then X(i) = EXTS(data)
+ then X(i) = sign_extend(data)
  else {
  assert (i[0] == bitzero);
  if i != zeros() then {

model/riscv_fetch_rvfi.sail

@@ -70,9 +70,9 @@
 
 function fetch() -> FetchResult = {
  rvfi_inst_data->rvfi_order() = minstret;
- rvfi_pc_data->rvfi_pc_rdata() = EXTZ(get_arch_pc());
- rvfi_inst_data->rvfi_mode() = EXTZ(privLevel_to_bits(cur_privilege));
- rvfi_inst_data->rvfi_ixl() = EXTZ(misa.MXL());
+ rvfi_pc_data->rvfi_pc_rdata() = zero_extend(get_arch_pc());
+ rvfi_inst_data->rvfi_mode() = zero_extend(privLevel_to_bits(cur_privilege));
+ rvfi_inst_data->rvfi_ixl() = zero_extend(misa.MXL());
 
  /* First allow extensions to check pc */
  match ext_fetch_check_pc(PC, PC) {
@@ -85,7 +85,7 @@ function fetch() -> FetchResult = {
  TR_Failure(e, _) => F_Error(e, PC),
  TR_Address(_, _) => {
  let i = rvfi_instruction.rvfi_insn();
- rvfi_inst_data->rvfi_insn() = EXTZ(i);
+ rvfi_inst_data->rvfi_insn() = zero_extend(i);
  if (i[1 .. 0] != 0b11)
  then F_RVC(i[15 .. 0])
  else {

model/riscv_freg_type.sail

@@ -74,7 +74,7 @@
 type fregtype = flenbits
 
 /* default zero register */
-let zero_freg : fregtype = EXTZ(0x0)
+let zero_freg : fregtype = zero_extend(0x0)
 
 /* default register printer */
 val FRegStr : fregtype -> string

model/riscv_insts_aext.sail

@@ -179,7 +179,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
  /* should only happen in rmem
  * rmem: allow SC to fail very early
  */
- X(rd) = EXTZ(0b1); RETIRE_SUCCESS
+ X(rd) = zero_extend(0b1); RETIRE_SUCCESS
  } else {
  if haveAtomics() then {
  /* normal non-rmem case
@@ -206,7 +206,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
  else {
  if match_reservation(vaddr) == false then {
  /* cannot happen in rmem */
- X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS
+ X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
  } else {
  match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here:
  * both result in a SAMO exception */
@@ -231,8 +231,8 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
  _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double")
  };
  match (res) {
- MemValue(true) => { X(rd) = EXTZ(0b0); cancel_reservation(); RETIRE_SUCCESS },
- MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS },
+ MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
+ MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
  MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
  }
  }
@@ -297,9 +297,9 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
  _ => false
  };
  let rs2_val : xlenbits = match width {
- BYTE => if is_unsigned then EXTZ(X(rs2)[7..0]) else EXTS(X(rs2)[7..0]),
- HALF => if is_unsigned then EXTZ(X(rs2)[15..0]) else EXTS(X(rs2)[15..0]),
- WORD => if is_unsigned then EXTZ(X(rs2)[31..0]) else EXTS(X(rs2)[31..0]),
+ BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]),
+ HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]),
+ WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]),
  DOUBLE => X(rs2)
  };
  match (eares) {
@@ -332,9 +332,9 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
  AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded)))
  };
  let rval : xlenbits = match width {
- BYTE => EXTS(loaded[7..0]),
- HALF => EXTS(loaded[15..0]),
- WORD => EXTS(loaded[31..0]),
+ BYTE => sign_extend(loaded[7..0]),
+ HALF => sign_extend(loaded[15..0]),
+ WORD => sign_extend(loaded[31..0]),
  DOUBLE => loaded
  };
  let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) {

model/riscv_insts_base.sail

@@ -84,7 +84,7 @@ mapping clause encdec = UTYPE(imm, rd, op)
  <-> imm @ rd @ encdec_uop(op)
 
 function clause execute UTYPE(imm, rd, op) = {
- let off : xlenbits = EXTS(imm @ 0x000);
+ let off : xlenbits = sign_extend(imm @ 0x000);
  let ret : xlenbits = match op {
  RISCV_LUI => off,
  RISCV_AUIPC => get_arch_pc() + off
@@ -120,7 +120,7 @@ but this is difficult
 */
 
 function clause execute (RISCV_JAL(imm, rd)) = {
- let t : xlenbits = PC + EXTS(imm);
+ let t : xlenbits = PC + sign_extend(imm);
  /* Extensions get the first checks on the prospective target address. */
  match ext_control_check_pc(t) {
  Ext_ControlAddr_Error(e) => {
@@ -184,7 +184,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
  RISCV_BLTU => rs1_val <_u rs2_val,
  RISCV_BGEU => rs1_val >=_u rs2_val
  };
- let t : xlenbits = PC + EXTS(imm);
+ let t : xlenbits = PC + sign_extend(imm);
  if taken then {
  /* Extensions get the first checks on the prospective target address. */
  match ext_control_check_pc(t) {
@@ -234,11 +234,11 @@ mapping clause encdec = ITYPE(imm, rs1, rd, op)
 
 function clause execute (ITYPE (imm, rs1, rd, op)) = {
  let rs1_val = X(rs1);
- let immext : xlenbits = EXTS(imm);
+ let immext : xlenbits = sign_extend(imm);
  let result : xlenbits = match op {
  RISCV_ADDI => rs1_val + immext,
- RISCV_SLTI => EXTZ(bool_to_bits(rs1_val <_s immext)),
- RISCV_SLTIU => EXTZ(bool_to_bits(rs1_val <_u immext)),
+ RISCV_SLTI => zero_extend(bool_to_bits(rs1_val <_s immext)),
+ RISCV_SLTIU => zero_extend(bool_to_bits(rs1_val <_u immext)),
  RISCV_ANDI => rs1_val & immext,
  RISCV_ORI => rs1_val | immext,
  RISCV_XORI => rs1_val ^ immext
@@ -318,8 +318,8 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = {
  let rs2_val = X(rs2);
  let result : xlenbits = match op {
  RISCV_ADD => rs1_val + rs2_val,
- RISCV_SLT => EXTZ(bool_to_bits(rs1_val <_s rs2_val)),
- RISCV_SLTU => EXTZ(bool_to_bits(rs1_val <_u rs2_val)),
+ RISCV_SLT => zero_extend(bool_to_bits(rs1_val <_s rs2_val)),
+ RISCV_SLTU => zero_extend(bool_to_bits(rs1_val <_u rs2_val)),
  RISCV_AND => rs1_val & rs2_val,
  RISCV_OR => rs1_val | rs2_val,
  RISCV_XOR => rs1_val ^ rs2_val,
@@ -364,7 +364,7 @@ mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (
 
 val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (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),
+ MemValue(v) => MemValue(if is_unsigned then zero_extend(v) else sign_extend(v) : xlenbits),
  MemException(e) => MemException(e)
 }
 
@@ -385,7 +385,7 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
  }
 
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
- let offset : xlenbits = EXTS(imm);
+ let offset : xlenbits = sign_extend(imm);
  /* Get the address, X(rs1) + offset.
  Some extensions perform additional checks on address validity. */
  match ext_data_get_addr(rs1, offset, Read(Data), width) {
@@ -441,7 +441,7 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, 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 offset : xlenbits = EXTS(imm);
+ let offset : xlenbits = sign_extend(imm);
  /* Get the address, X(rs1) + offset.
  Some extensions perform additional checks on address validity. */
  match ext_data_get_addr(rs1, offset, Write(Data), width) {
@@ -494,8 +494,8 @@ mapping clause encdec = ADDIW(imm, rs1, rd)
  if sizeof(xlen) == 64
 
 function clause execute (ADDIW(imm, rs1, rd)) = {
- let result : xlenbits = EXTS(imm) + X(rs1);
- X(rd) = EXTS(result[31..0]);
+ let result : xlenbits = sign_extend(imm) + X(rs1);
+ X(rd) = sign_extend(result[31..0]);
  RETIRE_SUCCESS
 }
 
@@ -527,7 +527,7 @@ function clause execute (SHIFTW(shamt, rs1, rd, op)) = {
  RISCV_SRLI => rs1_val >> shamt,
  RISCV_SRAI => shift_right_arith32(rs1_val, shamt)
  };
- X(rd) = EXTS(result);
+ X(rd) = sign_extend(result);
  RETIRE_SUCCESS
 }
 
@@ -576,7 +576,7 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = {
  RISCV_SRLW => rs1_val >> (rs2_val[4..0]),
  RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0])
  };
- X(rd) = EXTS(result);
+ X(rd) = sign_extend(result);
  RETIRE_SUCCESS
 }
 
@@ -616,7 +616,7 @@ function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = {
  RISCV_SRLIW => rs1_val[31..0] >> shamt,
  RISCV_SRAIW => shift_right_arith32(rs1_val[31..0], shamt)
  };
- X(rd) = EXTS(result);
+ X(rd) = sign_extend(result);
  RETIRE_SUCCESS
 }
 

model/riscv_insts_cdext.sail

@@ -84,7 +84,7 @@ mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd)
  if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FLDSP(uimm, rd)) = {
- let imm : bits(12) = EXTZ(uimm @ 0b000);
+ let imm : bits(12) = zero_extend(uimm @ 0b000);
  execute(LOAD_FP(imm, sp, rd, DOUBLE))
 }
 
@@ -102,7 +102,7 @@ mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2)
  if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FSDSP(uimm, rs2)) = {
- let imm : bits(12) = EXTZ(uimm @ 0b000);
+ let imm : bits(12) = zero_extend(uimm @ 0b000);
  execute(STORE_FP(imm, rs2, sp, DOUBLE))
 }
 
@@ -120,7 +120,7 @@ mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd)
  if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FLD(uimm, rsc, rdc)) = {
- let imm : bits(12) = EXTZ(uimm @ 0b000);
+ let imm : bits(12) = zero_extend(uimm @ 0b000);
  let rd = creg2reg_idx(rdc);
  let rs = creg2reg_idx(rsc);
  execute(LOAD_FP(imm, rs, rd, DOUBLE))
@@ -140,7 +140,7 @@ mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2)
  if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FSD(uimm, rsc1, rsc2)) = {
- let imm : bits(12) = EXTZ(uimm @ 0b000);
+ let imm : bits(12) = zero_extend(uimm @ 0b000);
  let rs1 = creg2reg_idx(rsc1);
  let rs2 = creg2reg_idx(rsc2);
  execute(STORE_FP(imm, rs2, rs1, DOUBLE))