Refactor MUL instruction

This instruction had a bit of a case of 'boolean blindness' code smell,
where the mul operation was represented as a triple of booleans. This
commit refactors the implemention to use a struct with named fields for
high, signed1, and signed2.

The C_MUL instruction in Zcb also needs to be changed appropriately

The mul_op struct was added in riscv_types

While there do some housekeeping w.r.t the comment about a workaround for
Sail < 0.15.1, as this is no longer needed.

model/riscv_insts_mext.sail

@@ -11,27 +11,26 @@
 
 /* ****************************************************************** */
 
-union clause ast = MUL : (regidx, regidx, regidx, bool, bool, bool)
+union clause ast = MUL : (regidx, regidx, regidx, mul_op)
 
-mapping encdec_mul_op : (bool, bool, bool) <-> bits(3) = {
- (false, true, true)  <-> 0b000,
- (true, true, true)  <-> 0b001,
- (true, true, false)  <-> 0b010,
- (true, false, false) <-> 0b011
+mapping encdec_mul_op : mul_op <-> bits(3) = {
+ struct { high = false, signed1 = true,  signed2 = true } <-> 0b000,
+ struct { high = true,  signed1 = true,  signed2 = true } <-> 0b001,
+ struct { high = true,  signed1 = true,  signed2 = false } <-> 0b010,
+ struct { high = true,  signed1 = false, signed2 = false } <-> 0b011
 }
 
-/* for some reason the : bits(3) here is still necessary - BUG */
-mapping clause encdec = MUL(rs2, rs1, rd, high, signed1, signed2)
- <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(high, signed1, signed2) : bits(3) @ rd @ 0b0110011
+mapping clause encdec = MUL(rs2, rs1, rd, mul_op)
+ <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011
 
-function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = {
+function clause execute (MUL(rs2, rs1, rd, mul_op)) = {
  if haveMulDiv() | haveZmmul() then {
  let rs1_val = X(rs1);
  let rs2_val = X(rs2);
- let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val);
- let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val);
+ let rs1_int : int = if mul_op.signed1 then signed(rs1_val) else unsigned(rs1_val);
+ let rs2_int : int = if mul_op.signed2 then signed(rs2_val) else unsigned(rs2_val);
  let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int);
- let result = if high
+ let result = if mul_op.high
  then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)]
  else result_wide[(sizeof(xlen) - 1) .. 0];
  X(rd) = result;
@@ -42,15 +41,15 @@ function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = {
  }
 }
 
-mapping mul_mnemonic : (bool, bool, bool) <-> string = {
- (false, true, true)  <-> "mul",
- (true, true, true)  <-> "mulh",
- (true, true, false)  <-> "mulhsu",
- (true, false, false) <-> "mulhu"
+mapping mul_mnemonic : mul_op <-> string = {
+ struct { high = false, signed1 = true,  signed2 = true } <-> "mul",
+ struct { high = true,  signed1 = true,  signed2 = true } <-> "mulh",
+ struct { high = true,  signed1 = true,  signed2 = false } <-> "mulhsu",
+ struct { high = true,  signed1 = false, signed2 = false } <-> "mulhu"
 }
 
-mapping clause assembly = MUL(rs2, rs1, rd, high, signed1, signed2)
- <-> mul_mnemonic(high, signed1, signed2) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+mapping clause assembly = MUL(rs2, rs1, rd, mul_op)
+ <-> mul_mnemonic(mul_op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 /* ****************************************************************** */
 union clause ast = DIV : (regidx, regidx, regidx, bool)

model/riscv_insts_zcb.sail

@@ -206,5 +206,5 @@ mapping clause assembly = C_MUL(rsdc, rs2c) <->
 function clause execute C_MUL(rsdc, rs2c) = {
  let rd = creg2reg_idx(rsdc);
  let rs = creg2reg_idx(rs2c);
- execute(MUL(rs, rd, rd, false, true, true))
+ execute(MUL(rs, rd, rd, struct { high = false, signed1 = true, signed2 = true }))
 }

model/riscv_types.sail

@@ -389,6 +389,12 @@ mapping size_bytes : word_width <-> {1, 2, 4, 8} = {
  DOUBLE <-> 8,
 }
 
+struct mul_op = {
+ high : bool,
+ signed1 : bool,
+ signed2 : bool
+}
+
 /*!
  * Raise an internal error reporting that width w is invalid for access kind, k,
  * and current xlen. The file name and line number should be passed in as the
@@ -399,17 +405,6 @@ mapping size_bytes : word_width <-> {1, 2, 4, 8} = {
  */
 val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a
 function report_invalid_width(f , l, w, k) -> 'a = {
- /*
- * Ideally we would call internal_error here but this triggers a Sail bug,
- * https://github.com/rems-project/sail/issues/203 in versions < 0.15.1, so
- * we work around this by manually inlining.
- * TODO when we are happy to require Sail >= 0.15.1 uncomment the following
- * and remove the rest of the function.
- */
- // internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^
- // " with xlen=" ^ dec_str(sizeof(xlen)));
- assert (false, f ^ ":" ^ dec_str(l) ^ ": " ^ "Invalid width, "
- ^ size_mnemonic(w) ^ ", for " ^ k ^ " with xlen="
- ^ dec_str(sizeof(xlen)));
- throw Error_internal_error()
+ internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^
+ " with xlen=" ^ dec_str(sizeof(xlen)))
 }