Regenerate sail_latex_riscv

Corresponds to commit 77e647e6319d142e0bf101f908b4ba0b954fada9 in
sail-cheri-riscv.

sail_latex_riscv/fclCInvokezexecute33a689e3a631b9b905b85461d3814943.tex

@@ -29,15 +29,15 @@
 } else if cs2_val.permit_execute then {
   #\hyperref[sailRISCVzhandlezycherizyregzyexception]{handle\_cheri\_reg\_exception}#(CapEx_PermitExecuteViolation, cs2);
   RETIRE_FAIL
-} else if #\hyperref[sailRISCVznot]{not}#(#\hyperref[sailRISCVzinCapBounds]{inCapBounds}#(cs1_val, newPC, #\hyperref[sailRISCVzminzyinstructionzybytes]{min\_instruction\_bytes}#())) then {
-  #\hyperref[sailRISCVzhandlezycherizyregzyexception]{handle\_cheri\_reg\_exception}#(CapEx_LengthViolation, cs1);
-  RETIRE_FAIL
-} else if newPCCBase[0] == bitone | (newPCCBase[1] == bitone & ~(#\hyperref[sailRISCVzhaveRVC]{haveRVC}#())) then {
+} else if #\hyperref[sailRISCVzhavezypcczyrelocation]{have\_pcc\_relocation}#() & (newPCCBase[0] == bitone | (newPCCBase[1] == bitone & ~(#\hyperref[sailRISCVzhaveRVC]{haveRVC}#()))) then {
   #\hyperref[sailRISCVzhandlezycherizyregzyexception]{handle\_cheri\_reg\_exception}#(CapEx_UnalignedBase, cs1);
   RETIRE_FAIL
 } else if newPC[1] == bitone & ~(#\hyperref[sailRISCVzhaveRVC]{haveRVC}#()) then {
   #\hyperref[sailRISCVzhandlezymemzyexception]{handle\_mem\_exception}#(newPC,  #\hyperref[sailRISCVzEzyFetchzyAddrzyAlign]{E\_Fetch\_Addr\_Align}#());
   RETIRE_FAIL
+} else if #\hyperref[sailRISCVznot]{not}#(#\hyperref[sailRISCVzinCapBounds]{inCapBounds}#(cs1_val, newPC, #\hyperref[sailRISCVzminzyinstructionzybytes]{min\_instruction\_bytes}#())) then {
+  #\hyperref[sailRISCVzhandlezycherizyregzyexception]{handle\_cheri\_reg\_exception}#(CapEx_LengthViolation, cs1);
+  RETIRE_FAIL
 } else {
   #\hyperref[sailRISCVzC]{C}#(31) = #\hyperref[sailRISCVzunsealCap]{unsealCap}#(cs2_val);
   nextPC = newPC;

sail_latex_riscv/fclCJALRzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -12,15 +12,15 @@
 } else if #\hyperref[sailRISCVznot]{not}#(cs1_val.permit_execute) then {
   #\hyperref[sailRISCVzhandlezycherizyregzyexception]{handle\_cheri\_reg\_exception}#(CapEx_PermitExecuteViolation, cs1);
   RETIRE_FAIL
-} else if #\hyperref[sailRISCVznot]{not}#(#\hyperref[sailRISCVzinCapBounds]{inCapBounds}#(cs1_val, newPC, #\hyperref[sailRISCVzminzyinstructionzybytes]{min\_instruction\_bytes}#())) then {
-  #\hyperref[sailRISCVzhandlezycherizyregzyexception]{handle\_cheri\_reg\_exception}#(CapEx_LengthViolation, cs1);
-  RETIRE_FAIL
-} else if newPCCBase[0] == bitone | (newPCCBase[1] == bitone & ~(#\hyperref[sailRISCVzhaveRVC]{haveRVC}#())) then {
+} else if #\hyperref[sailRISCVzhavezypcczyrelocation]{have\_pcc\_relocation}#() & (newPCCBase[0] == bitone | (newPCCBase[1] == bitone & ~(#\hyperref[sailRISCVzhaveRVC]{haveRVC}#()))) then {
   #\hyperref[sailRISCVzhandlezycherizyregzyexception]{handle\_cheri\_reg\_exception}#(CapEx_UnalignedBase, cs1);
   RETIRE_FAIL
 } else if newPC[1] == bitone & ~(#\hyperref[sailRISCVzhaveRVC]{haveRVC}#()) then {
   #\hyperref[sailRISCVzhandlezymemzyexception]{handle\_mem\_exception}#(newPC,  #\hyperref[sailRISCVzEzyFetchzyAddrzyAlign]{E\_Fetch\_Addr\_Align}#());
   RETIRE_FAIL
+} else if #\hyperref[sailRISCVznot]{not}#(#\hyperref[sailRISCVzinCapBounds]{inCapBounds}#(cs1_val, newPC, #\hyperref[sailRISCVzminzyinstructionzybytes]{min\_instruction\_bytes}#())) then {
+  #\hyperref[sailRISCVzhandlezycherizyregzyexception]{handle\_cheri\_reg\_exception}#(CapEx_LengthViolation, cs1);
+  RETIRE_FAIL
 } else {
   let (success, linkCap) = #\hyperref[sailRISCVzsetCapAddr]{setCapAddr}#(PCC, nextPC); /* Note that nextPC accounts for compressed instructions */
   assert(success, "Link cap should always be representable.");

sail_latex_riscv/fclCSpecialRWzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -62,7 +62,9 @@
       30 => MScratchC = cs1_val,
       31 => MEPCC = cs1_val,
       _  => assert(false, "unreachable")
-    }
+    };
+    if #\hyperref[sailRISCVzgetzyconfigzyprintzyreg]{get\_config\_print\_reg}#() then
+      #\hyperref[sailRISCVzprintzyreg]{print\_reg}#(#\hyperref[sailRISCVzscrzynamezymap]{scr\_name\_map}#(scr) ^ " <- " ^ #\hyperref[sailRISCVzRegStr]{RegStr}#(cs1_val));
   };
   RETIRE_SUCCESS
 }

sail_latex_riscv/fclLoadCapDDCzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -1,3 +1,2 @@
-let ddc_val = DDC;
-let vaddr = ddc_val.address + #\hyperref[sailRISCVzX]{X}#(rs1);
+let (ddc_val, vaddr) = #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}#(#\hyperref[sailRISCVzX]{X}#(rs1));
 #\hyperref[sailRISCVzhandlezyloadzycapzyviazycap]{handle\_load\_cap\_via\_cap}#(cd, DDC_IDX, ddc_val, vaddr)

sail_latex_riscv/fclLoadDataDDCzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -1,3 +1,2 @@
-let ddc_val = DDC;
-let vaddr = ddc_val.address + #\hyperref[sailRISCVzX]{X}#(rs1);
+let (ddc_val, vaddr) = #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}#(#\hyperref[sailRISCVzX]{X}#(rs1));
 #\hyperref[sailRISCVzhandlezyloadzydatazyviazycap]{handle\_load\_data\_via\_cap}#(rd, DDC_IDX, ddc_val, vaddr, is_unsigned, width)

sail_latex_riscv/fclLoadResCapDDCzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -1,6 +1,5 @@
 if #\hyperref[sailRISCVzhaveAtomics]{haveAtomics}#() then {
-  let ddc_val = DDC;
-  let vaddr = ddc_val.address + #\hyperref[sailRISCVzX]{X}#(rs1);
+  let (ddc_val, vaddr) = #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}#(#\hyperref[sailRISCVzX]{X}#(rs1));
   #\hyperref[sailRISCVzhandlezyloadreszycapzyviazycap]{handle\_loadres\_cap\_via\_cap}#(cd, DDC_IDX, ddc_val, vaddr, false, false)
 } else {
   #\hyperref[sailRISCVzhandlezyillegal]{handle\_illegal}#();

sail_latex_riscv/fclLoadResDataDDCzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -1,6 +1,5 @@
 if #\hyperref[sailRISCVzhaveAtomics]{haveAtomics}#() then {
-  let ddc_val = DDC;
-  let vaddr = ddc_val.address + #\hyperref[sailRISCVzX]{X}#(rs1);
+  let (ddc_val, vaddr) = #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}#(#\hyperref[sailRISCVzX]{X}#(rs1));
   #\hyperref[sailRISCVzhandlezyloadreszydatazyviazycap]{handle\_loadres\_data\_via\_cap}#(rd, DDC_IDX, ddc_val, vaddr, width)
 } else {
   #\hyperref[sailRISCVzhandlezyillegal]{handle\_illegal}#();

sail_latex_riscv/fclStoreCapDDCzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -1,3 +1,2 @@
-let ddc_val = DDC;
-let vaddr = ddc_val.address + #\hyperref[sailRISCVzX]{X}#(rs1);
+let (ddc_val, vaddr) = #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}#(#\hyperref[sailRISCVzX]{X}#(rs1));
 #\hyperref[sailRISCVzhandlezystorezycapzyviazycap]{handle\_store\_cap\_via\_cap}#(cs2, DDC_IDX, ddc_val, vaddr)

sail_latex_riscv/fclStoreCondCapDDCzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -5,8 +5,7 @@
   #\hyperref[sailRISCVzC]{C}#(cs2) = #\hyperref[sailRISCVzintzytozycap]{int\_to\_cap}#(#\hyperref[sailRISCVzEXTZ]{EXTZ}#(0b1));
   RETIRE_SUCCESS
 } else if #\hyperref[sailRISCVzhaveAtomics]{haveAtomics}#() then {
-  let ddc_val = DDC;
-  let vaddr = ddc_val.address + #\hyperref[sailRISCVzX]{X}#(rs1);
+  let (ddc_val, vaddr) = #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}#(#\hyperref[sailRISCVzX]{X}#(rs1));
   #\hyperref[sailRISCVzhandlezystorezycondzycapzyviazycap]{handle\_store\_cond\_cap\_via\_cap}#(cs2, cs2, DDC_IDX, ddc_val, vaddr, false, false, true)
 } else {
   #\hyperref[sailRISCVzhandlezyillegal]{handle\_illegal}#();

sail_latex_riscv/fclStoreCondDataDDCzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -5,8 +5,7 @@
   #\hyperref[sailRISCVzX]{X}#(rs2) = #\hyperref[sailRISCVzEXTZ]{EXTZ}#(0b1);
   RETIRE_SUCCESS
 } else if #\hyperref[sailRISCVzhaveAtomics]{haveAtomics}#() then {
-  let ddc_val = DDC;
-  let vaddr = ddc_val.address + #\hyperref[sailRISCVzX]{X}#(rs1);
+  let (ddc_val, vaddr) = #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}#(#\hyperref[sailRISCVzX]{X}#(rs1));
   #\hyperref[sailRISCVzhandlezystorezycondzydatazyviazycap]{handle\_store\_cond\_data\_via\_cap}#(rs2, DDC_IDX, ddc_val, vaddr, width)
 } else {
   #\hyperref[sailRISCVzhandlezyillegal]{handle\_illegal}#();

sail_latex_riscv/fclStoreDataDDCzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -1,3 +1,2 @@
-let ddc_val = DDC;
-let vaddr = ddc_val.address + #\hyperref[sailRISCVzX]{X}#(rs1);
+let (ddc_val, vaddr) = #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}#(#\hyperref[sailRISCVzX]{X}#(rs1));
 #\hyperref[sailRISCVzhandlezystorezydatazyviazycap]{handle\_store\_data\_via\_cap}#(rs2, DDC_IDX, ddc_val, vaddr, width)

sail_latex_riscv/fnzcap_to_integer_pcfb8f9e29d6bb00469db30a7b19649da3.tex

@@ -0,0 +1,3 @@
+function #\hyperref[sailRISCVzcapzytozyintegerzypc]{cap\_to\_integer\_pc}# (cap: Capability) -> xlenbits = {
+  if (#\hyperref[sailRISCVzhavezypcczyrelocation]{have\_pcc\_relocation}#()) then #\hyperref[sailRISCVzgetCapOffsetBits]{getCapOffsetBits}#(cap) else cap.address
+}

sail_latex_riscv/fnzcaptostring7067e2f1e90748309c77a5de3d661e3d.tex

@@ -11,8 +11,8 @@
   #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(#\hyperref[sailRISCVzBitStr]{BitStr}#(0b0 @ #\hyperref[sailRISCVzgetCapPerms]{getCapPerms}#(cap)),
   #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(" type:",
   #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(#\hyperref[sailRISCVzBitStr]{BitStr}#(otype64),
-  #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(" offset:",
-  #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(#\hyperref[sailRISCVzBitStr]{BitStr}#(#\hyperref[sailRISCVzgetCapOffsetBits]{getCapOffsetBits}#(cap)),
+  #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(" address:",
+  #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(#\hyperref[sailRISCVzBitStr]{BitStr}#(cap.address),
   #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(" base:",
   #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(#\hyperref[sailRISCVzBitStr]{BitStr}#(#\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(cap)),
   #\hyperref[sailRISCVzconcatzystr]{concat\_str}#(" length:", len_str)))))))))))))

sail_latex_riscv/fnzchecked_mem_write765e0693788c9f4b01c2243ece39909e.tex

@@ -5,5 +5,5 @@
   then match #\hyperref[sailRISCVzextzycheckzyphyszymemzywrite]{ext\_check\_phys\_mem\_write}# (wk, paddr, width, data, meta) {
     #\hyperref[sailRISCVzExtzyPhysAddrzyOK]{Ext\_PhysAddr\_OK}#() => #\hyperref[sailRISCVzphyszymemzywrite]{phys\_mem\_write}#(wk, paddr, width, data, meta),
     #\hyperref[sailRISCVzExtzyPhysAddrzyError]{Ext\_PhysAddr\_Error}#(e)  => #\hyperref[sailRISCVzMemException]{MemException}#(e)
-  }  
+  }
   else #\hyperref[sailRISCVzMemException]{MemException}#(#\hyperref[sailRISCVzEzySAMOzyAccesszyFault]{E\_SAMO\_Access\_Fault}#())

sail_latex_riscv/fnzddc_and_resulting_addr0f0e2d5c6123a71667b35ed17c44868e.tex

@@ -0,0 +1,4 @@
+function #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}# (addr) = {
+  let ddc_val = DDC in
+  (ddc_val, if (#\hyperref[sailRISCVzhavezyddczyrelocation]{have\_ddc\_relocation}#()) then ddc_val.address + addr else addr)
+}

sail_latex_riscv/fnzext_control_check_addr2d404fc3390578d569e3f547f0d18fce.tex

@@ -1,10 +1,10 @@
 function #\hyperref[sailRISCVzextzycontrolzycheckzyaddr]{ext\_control\_check\_addr}#(pc : xlenbits) -> #\hyperref[sailRISCVzExtzyControlAddrzyCheck]{Ext\_ControlAddr\_Check}#(ext_control_addr_error) = {
-  let pcc_base = #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC);
   /* We are given the addr without any bit[0] clearing, so the addition
    * below may include a set addr[0], and so the bounds checks should
    * be accurate.
    */
-  let target : xlenbits = [pcc_base + pc with 0=bitzero];
+  let pc = if #\hyperref[sailRISCVzhavezypcczyrelocation]{have\_pcc\_relocation}#() then #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC) + pc else pc;
+  let target : xlenbits = [pc with 0=bitzero];
   if   #\hyperref[sailRISCVznot]{not}#(#\hyperref[sailRISCVzinCapBounds]{inCapBounds}#(PCC, target, #\hyperref[sailRISCVzminzyinstructionzybytes]{min\_instruction\_bytes}# ()))
   then #\hyperref[sailRISCVzExtzyControlAddrzyError]{Ext\_ControlAddr\_Error}#(CapEx_LengthViolation, PCC_IDX)
   else #\hyperref[sailRISCVzExtzyControlAddrzyOK]{Ext\_ControlAddr\_OK}#(target)

sail_latex_riscv/fnzext_fail_xret_priva071b88d32f48ad8e720a4cae916da8b.tex

@@ -1,2 +1,2 @@
-function #\hyperref[sailRISCVzextzyfailzyxretzypriv]{ext\_fail\_xret\_priv}# () : unit -> unit = 
+function #\hyperref[sailRISCVzextzyfailzyxretzypriv]{ext\_fail\_xret\_priv}# () : unit -> unit =
   #\hyperref[sailRISCVzhandlezycherizypcczyexception]{handle\_cheri\_pcc\_exception}#(CapEx_AccessSystemRegsViolation)

sail_latex_riscv/fnzext_fetch_check_pc2e82f09c4f4da5465b70e5f9e6f48b77.tex

@@ -1,20 +1,20 @@
 function #\hyperref[sailRISCVzextzyfetchzycheckzypc]{ext\_fetch\_check\_pc}#(start_pc, pc) = {
   if   start_pc == pc
   then {
-    pcc_base = #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC);
+    let pcc_base = #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC);
     /* We need to perform the permission checks only for the first granule. */
     if      #\hyperref[sailRISCVznot]{not}#(PCC.tag)
     then    #\hyperref[sailRISCVzExtzyFetchAddrzyError]{Ext\_FetchAddr\_Error}#(CapEx_TagViolation)
     else if #\hyperref[sailRISCVzisCapSealed]{isCapSealed}#(PCC)
     then    #\hyperref[sailRISCVzExtzyFetchAddrzyError]{Ext\_FetchAddr\_Error}#(CapEx_SealViolation)
     else if #\hyperref[sailRISCVznot]{not}#(PCC.permit_execute)
     then    #\hyperref[sailRISCVzExtzyFetchAddrzyError]{Ext\_FetchAddr\_Error}#(CapEx_PermitExecuteViolation)
+    /* If PCC relocation is enabled, require that PCC.base be as aligned as PC.
+       This is also enforced when setting PCC in most places. */
+    else if #\hyperref[sailRISCVzhavezypcczyrelocation]{have\_pcc\_relocation}#() & (pcc_base[0] != bitzero | (pcc_base[1] != bitzero & ~(#\hyperref[sailRISCVzhaveRVC]{haveRVC}#())))
+    then    #\hyperref[sailRISCVzExtzyFetchAddrzyError]{Ext\_FetchAddr\_Error}#(CapEx_UnalignedBase)
     else if #\hyperref[sailRISCVznot]{not}#(#\hyperref[sailRISCVzinCapBounds]{inCapBounds}#(PCC, pc, 2))
     then    #\hyperref[sailRISCVzExtzyFetchAddrzyError]{Ext\_FetchAddr\_Error}#(CapEx_LengthViolation)
-    /* Require that PCC.base be as aligned as PC. This
-       is also enforced when setting PCC in most places. */
-    else if pcc_base[0] != bitzero | (pcc_base[1] != bitzero & ~(#\hyperref[sailRISCVzhaveRVC]{haveRVC}#()))
-    then    #\hyperref[sailRISCVzExtzyFetchAddrzyError]{Ext\_FetchAddr\_Error}#(CapEx_UnalignedBase)
     else    #\hyperref[sailRISCVzExtzyFetchAddrzyOK]{Ext\_FetchAddr\_OK}#(pc)
   } else {
     /* Perform only the bounds checks on the current granule, i.e. pc. */

sail_latex_riscv/fnzext_init_regs1d9ff00ce58fd5712eb26190e338015a.tex

@@ -51,10 +51,7 @@
   x31 = null_cap;
 
   misa->#\hyperref[sailRISCVzX]{X}#() = 0b1;
-  mccsr->#\hyperref[sailRISCVzd]{d}#() = 0b1;
-  mccsr->#\hyperref[sailRISCVze]{e}#() = 0b1;
-  sccsr->#\hyperref[sailRISCVzd]{d}#() = 0b1;
-  sccsr->#\hyperref[sailRISCVze]{e}#() = 0b1;
-  uccsr->#\hyperref[sailRISCVzd]{d}#() = 0b1;
-  uccsr->#\hyperref[sailRISCVze]{e}#() = 0b1;
+  mccsr = #\hyperref[sailRISCVzlegalizzezyccsr]{legalize\_ccsr}#(mccsr, #\hyperref[sailRISCVzzzeros]{zeros}#());
+  sccsr = #\hyperref[sailRISCVzlegalizzezyccsr]{legalize\_ccsr}#(sccsr, #\hyperref[sailRISCVzzzeros]{zeros}#());
+  uccsr = #\hyperref[sailRISCVzlegalizzezyccsr]{legalize\_ccsr}#(uccsr, #\hyperref[sailRISCVzzzeros]{zeros}#());
 }

sail_latex_riscv/fnzext_initaf8e3807fa5c1bbef01331f40e0f99a4.tex

@@ -1,9 +1,6 @@
 function #\hyperref[sailRISCVzextzyinit]{ext\_init}# () = {
   misa->#\hyperref[sailRISCVzX]{X}#() = 0b1;
-  mccsr->#\hyperref[sailRISCVzd]{d}#() = 0b1;
-  mccsr->#\hyperref[sailRISCVze]{e}#() = 0b1;
-  sccsr->#\hyperref[sailRISCVzd]{d}#() = 0b1;
-  sccsr->#\hyperref[sailRISCVze]{e}#() = 0b1;
-  uccsr->#\hyperref[sailRISCVzd]{d}#() = 0b1;
-  uccsr->#\hyperref[sailRISCVze]{e}#() = 0b1;
+  mccsr = #\hyperref[sailRISCVzlegalizzezyccsr]{legalize\_ccsr}#(mccsr, #\hyperref[sailRISCVzzzeros]{zeros}#());
+  sccsr = #\hyperref[sailRISCVzlegalizzezyccsr]{legalize\_ccsr}#(sccsr, #\hyperref[sailRISCVzzzeros]{zeros}#());
+  uccsr = #\hyperref[sailRISCVzlegalizzezyccsr]{legalize\_ccsr}#(uccsr, #\hyperref[sailRISCVzzzeros]{zeros}#());
 }

sail_latex_riscv/fnzext_veto_disable_cd10c2d1c5077060fa007c1628d7aaa8c.tex

@@ -1 +1,5 @@
-function #\hyperref[sailRISCVzextzyvetozydisablezyC]{ext\_veto\_disable\_C}# () = #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC)[1] == bitone
+function #\hyperref[sailRISCVzextzyvetozydisablezyC]{ext\_veto\_disable\_C}# () = {
+  if #\hyperref[sailRISCVzhavezypcczyrelocation]{have\_pcc\_relocation}#()
+  then #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC)[1] == bitone
+  else false
+}

sail_latex_riscv/fnzget_arch_pc874e1e50a5765cd3e317d37fa710a52d.tex

@@ -1,2 +1,2 @@
 function #\hyperref[sailRISCVzgetzyarchzypc]{get\_arch\_pc}# () =
-  PC - #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC)
+  if #\hyperref[sailRISCVzhavezypcczyrelocation]{have\_pcc\_relocation}#() then PC - #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC) else PC

sail_latex_riscv/fnzget_cheri_mode_cap_addr267a231c94a9ae3cf08d67cb43590a2e.tex

@@ -3,6 +3,6 @@
     let base_cap = #\hyperref[sailRISCVzC]{C}#(base_reg) in
     (base_cap, base_cap.address + offset, 0b0 @ base_reg)
   else
-    let ddc = DDC in
-    (ddc, ddc.address + #\hyperref[sailRISCVzX]{X}#(base_reg) + offset, DDC_IDX);
+    let (ddc_val, addr) = #\hyperref[sailRISCVzddczyandzyresultingzyaddr]{ddc\_and\_resulting\_addr}#(#\hyperref[sailRISCVzX]{X}#(base_reg) + offset) in
+    (ddc_val, addr, DDC_IDX);
 }

sail_latex_riscv/fnzget_mtvec134cdc828faab7bf9f19733fba43da2f.tex

@@ -1,2 +1,2 @@
 function #\hyperref[sailRISCVzgetzymtvec]{get\_mtvec}#() -> xlenbits =
-  #\hyperref[sailRISCVzgetCapOffsetBits]{getCapOffsetBits}#(MTCC)
+  #\hyperref[sailRISCVzcapzytozyintegerzypc]{cap\_to\_integer\_pc}#(MTCC)

sail_latex_riscv/fnzget_next_pc52098782da35f914abcd4b708363813b.tex

@@ -1,2 +1,2 @@
 function #\hyperref[sailRISCVzgetzynextzypc]{get\_next\_pc}#() =
-  nextPC - #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC)
+  if #\hyperref[sailRISCVzhavezypcczyrelocation]{have\_pcc\_relocation}#() then nextPC - #\hyperref[sailRISCVzgetCapBaseBits]{getCapBaseBits}#(PCC) else nextPC

sail_latex_riscv/fnzget_stvec8e871a236060976d6c548af2b67478db.tex

@@ -1,2 +1,2 @@
 function #\hyperref[sailRISCVzgetzystvec]{get\_stvec}#() -> xlenbits =
-  #\hyperref[sailRISCVzgetCapOffsetBits]{getCapOffsetBits}#(STCC)
+  #\hyperref[sailRISCVzcapzytozyintegerzypc]{cap\_to\_integer\_pc}#(STCC)

sail_latex_riscv/fnzget_utvec375b7b6fc923ff7174c10f9b93b1b2cf.tex

@@ -1,2 +1,2 @@
 function #\hyperref[sailRISCVzgetzyutvec]{get\_utvec}#() -> xlenbits =
-  #\hyperref[sailRISCVzgetCapOffsetBits]{getCapOffsetBits}#(UTCC)
+  #\hyperref[sailRISCVzcapzytozyintegerzypc]{cap\_to\_integer\_pc}#(UTCC)

sail_latex_riscv/fnzget_xret_target26ce66652c1cd67f2e91b685c1d44e62.tex

@@ -4,5 +4,5 @@
     Supervisor => SEPCC,
     User       => UEPCC
   };
-  #\hyperref[sailRISCVzlegalizzezyxepc]{legalize\_xepc}#(#\hyperref[sailRISCVzgetCapOffsetBits]{getCapOffsetBits}#(cap))
+  #\hyperref[sailRISCVzlegalizzezyxepc]{legalize\_xepc}#(#\hyperref[sailRISCVzcapzytozyintegerzypc]{cap\_to\_integer\_pc}#(cap))
 }

sail_latex_riscv/fnzhandle_cheri_cap_exceptionc1ff083ca6d0a739fb48243e22ff4898.tex

@@ -1,6 +1,7 @@
 function #\hyperref[sailRISCVzhandlezycherizycapzyexception]{handle\_cheri\_cap\_exception}#(capEx, regnum) =
   {
-    #\hyperref[sailRISCVzprint]{print}#("CHERI " ^ #\hyperref[sailRISCVzstringzyofzycapex]{string\_of\_capex}#(capEx) ^ " Reg=" ^ #\hyperref[sailRISCVzBitStr]{BitStr}#(regnum));
+    if #\hyperref[sailRISCVzgetzyconfigzyprintzyplatform]{get\_config\_print\_platform}#()
+    then #\hyperref[sailRISCVzprintzyplatform]{print\_platform}#("CHERI " ^ #\hyperref[sailRISCVzstringzyofzycapex]{string\_of\_capex}#(capEx) ^ " Reg=" ^ #\hyperref[sailRISCVzBitStr]{BitStr}#(regnum));
     let t : sync_exception = struct {
       trap    = #\hyperref[sailRISCVzEzyExtension]{E\_Extension}#(EXC_CHERI),
       excinfo = #\hyperref[sailRISCVzSome]{Some}#(#\hyperref[sailRISCVzEXTZ]{EXTZ}#(regnum @ #\hyperref[sailRISCVzCapExCode]{CapExCode}#(capEx)) : xlenbits),

sail_latex_riscv/fnzhave_cheri_relocationbbe9a9f5c01227424d0cc8330de5d0b3.tex

@@ -0,0 +1 @@
+function #\hyperref[sailRISCVzhavezycherizyrelocation]{have\_cheri\_relocation}#() = false

sail_latex_riscv/fnzhave_ddc_relocationcdaa2a12594a6d0db423bcedfc636210.tex

@@ -0,0 +1 @@
+function #\hyperref[sailRISCVzhavezyddczyrelocation]{have\_ddc\_relocation}#() = #\hyperref[sailRISCVzhavezycherizyrelocation]{have\_cheri\_relocation}#()

sail_latex_riscv/fnzhave_pcc_relocation8ef276f0f56e5c3343729212dcd97cb5.tex

@@ -0,0 +1 @@
+function #\hyperref[sailRISCVzhavezypcczyrelocation]{have\_pcc\_relocation}#() = #\hyperref[sailRISCVzhavezycherizyrelocation]{have\_cheri\_relocation}#()

sail_latex_riscv/fnzhavezfa170943288777f725fbf88904d27d506e.tex

@@ -0,0 +1 @@
+function #\hyperref[sailRISCVzhaveZfa]{haveZfa}#()  -> bool = true

sail_latex_riscv/fnzhavezfhe5dbd348c0b6c69910aec2c1edb56adf.tex

@@ -1 +1 @@
-function #\hyperref[sailRISCVzhaveZfh]{haveZfh}#()  -> bool = true
+function #\hyperref[sailRISCVzhaveZfh]{haveZfh}#()     -> bool = (misa.#\hyperref[sailRISCVzF]{F}#() == 0b1) & (mstatus.#\hyperref[sailRISCVzFS]{FS}#() != 0b00)

sail_latex_riscv/fnzhavezicond942507aaca8f56a8d3fc5cd08536c028.tex

@@ -0,0 +1 @@
+function #\hyperref[sailRISCVzhaveZicond]{haveZicond}#() -> bool = true

sail_latex_riscv/fnzinit_sysc92898d1b2b72595dd36bce10e6a67fb.tex

@@ -46,7 +46,7 @@
   mcounteren->#\hyperref[sailRISCVzbits]{bits}#() = #\hyperref[sailRISCVzEXTZ]{EXTZ}#(0b0);
 
   minstret           = #\hyperref[sailRISCVzEXTZ]{EXTZ}#(0b0);
-  minstret_written   = false;
+  minstret_increment = true;
 
   #\hyperref[sailRISCVzinitzypmp]{init\_pmp}#();
 

sail_latex_riscv/fnzlegalizze_ccsr8248d36ab83d1808c1e3e0b64d88c1cf.tex

@@ -3,8 +3,10 @@
   // Technically, WPRI does not need a legalizer, since software is
   // assumed to legalize; so we could remove this function.
   let v = #\hyperref[sailRISCVzMkzyccsr]{Mk\_ccsr}#(v);
-  /* For now these bits are not really supported so hardwired to true */
-  let c = #\hyperref[sailRISCVzupdatezyd]{update\_d}#(c, 0b1);
+  /* For now the e bit is not really supported so hardwired to true */
   let c = #\hyperref[sailRISCVzupdatezye]{update\_e}#(c, 0b1);
+  /* Read-only feature bits to allow for software to detect CHERI semantics. */
+  let c = #\hyperref[sailRISCVzupdatezynr]{update\_nr}#(c, #\hyperref[sailRISCVzboolzytozybits]{bool\_to\_bits}#(#\hyperref[sailRISCVznot]{not}#(#\hyperref[sailRISCVzhavezycherizyrelocation]{have\_cheri\_relocation}#())));
+  let c = #\hyperref[sailRISCVzupdatezytc]{update\_tc}#(c, 0b1);
   c
 }