Replace zero_extend(0b0) with zeros()

I left a couple where it made sense, e.g. in STORECON.

model/riscv_freg_type.sail

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

model/riscv_insts_zca.sail

@@ -498,7 +498,7 @@ mapping clause encdec_compressed = C_JR(rs1)
       if rs1 != zreg & extensionEnabled(Ext_Zca)
 
 function clause execute (C_JR(rs1)) =
-  execute(RISCV_JALR(zero_extend(0b0), rs1, zreg))
+  execute(RISCV_JALR(zeros(), rs1, zreg))
 
 mapping clause assembly = C_JR(rs1)
       if rs1 != zreg
@@ -514,7 +514,7 @@ mapping clause encdec_compressed = C_JALR(rs1)
       if rs1 != zreg & extensionEnabled(Ext_Zca)
 
 function clause execute (C_JALR(rs1)) =
-  execute(RISCV_JALR(zero_extend(0b0), rs1, ra))
+  execute(RISCV_JALR(zeros(), rs1, ra))
 
 mapping clause assembly = C_JALR(rs1)
       if rs1 != zreg

model/riscv_platform.sail

@@ -309,7 +309,7 @@ register htif_payload_writes : bits(4)
 function reset_htif () -> unit = {
   htif_cmd_write = bitzero;
   htif_payload_writes = 0x0;
-  htif_tohost = zero_extend(0b0);
+  htif_tohost = zeros();
 }
 
 /* Since the htif tohost port is only available at a single address,
@@ -437,11 +437,11 @@ function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, widt
 /* Platform initialization and ticking. */
 
 function init_platform() -> unit = {
-  htif_tohost = zero_extend(0b0);
+  htif_tohost = zeros();
   htif_done   = false;
-  htif_exit_code = zero_extend(0b0);
+  htif_exit_code = zeros();
   htif_cmd_write = bitzero;
-  htif_payload_writes = zero_extend(0b0);
+  htif_payload_writes = zeros();
 }
 
 function tick_platform() -> unit = {

model/riscv_reg_type.sail

@@ -10,7 +10,7 @@
 type regtype = xlenbits
 
 /* default zero register */
-let zero_reg : regtype = zero_extend(0x0)
+let zero_reg : regtype = zeros()
 
 /* default register printer */
 val RegStr : regtype -> string

model/riscv_sys_control.sail

@@ -275,7 +275,7 @@ union ctl_result = {
 function tval(excinfo : option(xlenbits)) -> xlenbits = {
   match (excinfo) {
     Some(e) => e,
-    None()  => zero_extend(0b0)
+    None()  => zeros()
   }
 }
 
@@ -416,8 +416,8 @@ function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
 function init_sys() -> unit = {
   cur_privilege = Machine;
 
-  mhartid     = zero_extend(0b0);
-  mconfigptr  = zero_extend(0b0);
+  mhartid     = zeros();
+  mconfigptr  = zeros();
 
   misa[MXL] = arch_to_bits(if xlen == 32 then RV32 else RV64);
   misa[A]   = 0b1;                             /* atomics */
@@ -447,41 +447,41 @@ function init_sys() -> unit = {
   if xlen == 64 then {
     mstatus = Mk_Mstatus([mstatus.bits with 37 .. 36 = 0b00])
   };
-  mstatush.bits = zero_extend(0b0);
+  mstatush.bits = zeros();
 
-  mip.bits     = zero_extend(0b0);
-  mie.bits     = zero_extend(0b0);
-  mideleg.bits = zero_extend(0b0);
-  medeleg.bits = zero_extend(0b0);
-  mtvec.bits   = zero_extend(0b0);
-  mcause.bits  = zero_extend(0b0);
-  mepc            = zero_extend(0b0);
-  mtval           = zero_extend(0b0);
-  mscratch        = zero_extend(0b0);
+  mip.bits     = zeros();
+  mie.bits     = zeros();
+  mideleg.bits = zeros();
+  medeleg.bits = zeros();
+  mtvec.bits   = zeros();
+  mcause.bits  = zeros();
+  mepc            = zeros();
+  mtval           = zeros();
+  mscratch        = zeros();
 
-  mcycle          = zero_extend(0b0);
-  mtime           = zero_extend(0b0);
+  mcycle          = zeros();
+  mtime           = zeros();
 
-  mcounteren.bits = zero_extend(0b0);
+  mcounteren.bits = zeros();
 
-  minstret           = zero_extend(0b0);
+  minstret           = zeros();
   minstret_increment = true;
 
-  menvcfg.bits = zero_extend(0b0);
-  senvcfg.bits = zero_extend(0b0);
+  menvcfg.bits = zeros();
+  senvcfg.bits = zeros();
   /* initialize vector csrs */
   elen               = 0b1; /* ELEN=64 as the common case */
   vlen               = 0b0100; /* VLEN=512 as a default value */
   vlenb              = to_bits(xlen, 2 ^ (get_vlen_pow() - 3)); /* vlenb holds the constant value VLEN/8 */
   /* VLEN value needs to be manually changed currently.
    * See riscv_vlen.sail for details.
    */
-  vstart             = zero_extend(0b0);
-  vl                 = zero_extend(0b0);
+  vstart             = zeros();
+  vl                 = zeros();
   vcsr[vxrm]       = 0b00;
   vcsr[vxsat]      = 0b0;
   vtype[vill]      = 0b1;
-  vtype[reserved]  = zero_extend(0b0);
+  vtype[reserved]  = zeros();
   vtype[vma]       = 0b0;
   vtype[vta]       = 0b0;
   vtype[vsew]      = 0b000;
@@ -492,7 +492,7 @@ function init_sys() -> unit = {
 
   // log compatibility with spike
   if   get_config_print_reg()
-  then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")")
+  then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zeros() : xlenbits) ^ ")")
 }
 
 /* memory access exceptions, defined here for use by the platform model. */

model/riscv_sys_regs.sail

@@ -550,7 +550,7 @@ function set_sstatus_UXL(s : Sstatus, a : arch_xlen) -> Sstatus = {
 }
 
 function lower_mstatus(m : Mstatus) -> Sstatus = {
-  let s = Mk_Sstatus(zero_extend(0b0));
+  let s = Mk_Sstatus(zeros());
   let s = [s with SD = m[SD]];
   let s = set_sstatus_UXL(s, get_mstatus_UXL(m));
 
@@ -599,7 +599,7 @@ bitfield Sinterrupts : xlenbits = {
 
 /* Provides the sip read view of mip (m) as delegated by mideleg (d). */
 function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
-  let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0));
+  let s : Sinterrupts = Mk_Sinterrupts(zeros());
 
   [s with
     SEI = m[SEI] & d[SEI],
@@ -610,7 +610,7 @@ function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
 
 /* Provides the sie read view of mie (m) as delegated by mideleg (d). */
 function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
-  let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0));
+  let s : Sinterrupts = Mk_Sinterrupts(zeros());
 
   [s with
     SEI = m[SEI] & d[SEI],

model/rvfi_dii.sail

@@ -202,13 +202,13 @@ register rvfi_mem_data_present : bool
 val rvfi_zero_exec_packet : unit -> unit
 
 function rvfi_zero_exec_packet () = {
-  rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(zero_extend(0b0));
-  rvfi_pc_data = Mk_RVFI_DII_Execution_Packet_PC(zero_extend(0b0));
-  rvfi_int_data = Mk_RVFI_DII_Execution_Packet_Ext_Integer(zero_extend(0x0));
+  rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(zeros());
+  rvfi_pc_data = Mk_RVFI_DII_Execution_Packet_PC(zeros());
+  rvfi_int_data = Mk_RVFI_DII_Execution_Packet_Ext_Integer(zeros());
   // magic = "int-data" -> 0x617461642d746e69 (big-endian)
   rvfi_int_data = update_magic(rvfi_int_data, 0x617461642d746e69);
   rvfi_int_data_present = false;
-  rvfi_mem_data = Mk_RVFI_DII_Execution_Packet_Ext_MemAccess(zero_extend(0x0));
+  rvfi_mem_data = Mk_RVFI_DII_Execution_Packet_Ext_MemAccess(zeros());
   // magic = "mem-data" -> 0x617461642d6d656d (big-endian)
   rvfi_mem_data = update_magic(rvfi_mem_data, 0x617461642d6d656d);
   rvfi_mem_data_present = false;
@@ -223,7 +223,7 @@ function rvfi_halt_exec_packet () =
 
 val rvfi_get_v2_support_packet : unit -> bits(704)
 function rvfi_get_v2_support_packet () = {
-  let rvfi_exec = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0));
+  let rvfi_exec = Mk_RVFI_DII_Execution_Packet_V1(zeros());
   // Returning 0x3 (using the unused high bits) in halt instead of 0x1 means
   // that we support the version 2 wire format. This is required to keep
   // backwards compatibility with old implementations that do not support
@@ -234,7 +234,7 @@ function rvfi_get_v2_support_packet () = {
 
 val rvfi_get_exec_packet_v1 : unit -> bits(704)
 function rvfi_get_exec_packet_v1 () = {
-  let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0));
+  let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zeros());
   // Convert the v2 packet to a v1 packet
   let v1_packet = update_rvfi_intr(v1_packet, rvfi_inst_data[rvfi_intr]);
   let v1_packet = update_rvfi_halt(v1_packet, rvfi_inst_data[rvfi_halt]);
@@ -273,7 +273,7 @@ val rvfi_get_exec_packet_v2 : unit -> bits(512)
 function rvfi_get_exec_packet_v2 () = {
   // TODO: add the other data
   // TODO: find a way to return a variable-length bitvector
-  let packet = Mk_RVFI_DII_Execution_PacketV2(zero_extend(0b0));
+  let packet = Mk_RVFI_DII_Execution_PacketV2(zeros());
   let packet = update_magic(packet, 0x32762d6563617274); // ASCII "trace-v2" (BE)
   let packet = update_basic_data(packet, rvfi_inst_data.bits);
   let packet = update_pc_data(packet, rvfi_pc_data.bits);