rename EXTS and EXTZ to sign_extend and zero_extend because it is more obviosu and to more closely match existing cheri pseudocode.

2 files changed, 18 insertions, 18 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index fa6ae0fd..6e2b2282 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -203,7 +203,7 @@ function clause execute (CGetPerm(rd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) = EXTZ(getCapPerms(capVal));
+    wGPR(rd) = zero_extend(getCapPerms(capVal));
   /* END_CGetPerms */
 }
 
@@ -216,7 +216,7 @@ function clause execute (CGetType(rd, cb)) =
   else
     let capVal = readCapReg(cb) in
     wGPR(rd) = if (capVal.sealed)
-      then EXTZ(capVal.otype)
+      then zero_extend(capVal.otype)
       else (bitone ^^ 64)
   /* END_CGetType */
 }
@@ -266,7 +266,7 @@ function clause execute (CGetTag(rd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) = EXTZ(capVal.tag);
+    wGPR(rd) = zero_extend(capVal.tag);
   /* END_CGetTag */
 }
 
@@ -278,7 +278,7 @@ function clause execute (CGetSealed(rd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) = EXTZ(capVal.sealed);
+    wGPR(rd) = zero_extend(capVal.sealed);
   /* END_CGetSealed */
 }
 
@@ -325,7 +325,7 @@ function clause execute (CGetCause(rd)) =
   if not (pcc_access_system_regs ()) then
     raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation)
   else
-    wGPR(rd) = EXTZ(CapCause.bits())
+    wGPR(rd) = zero_extend(CapCause.bits())
   /* END_CGetCause */
 }
 
@@ -462,7 +462,7 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
         CEXEQ  => cb_val == ct_val,
         CNEXEQ => cb_val != ct_val
       };
-      wGPR(rd) = EXTZ (cmp)
+      wGPR(rd) = zero_extend (cmp)
     }
   /* END_CPtrCmp */
 }
@@ -495,7 +495,7 @@ function clause execute (CIncOffsetImmediate(cd, cb, imm)) =
   /* START_CIncOffsetImmediate */
   checkCP2usable();
   let cb_val = readCapReg(cb);
-  let imm64 : bits(64) = EXTS(imm) in
+  let imm64 : bits(64) = sign_extend(imm) in
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -787,7 +787,7 @@ function clause execute (CCheckPerm(cs, rt)) =
   /* START_CCheckPerm */
   checkCP2usable();
   cs_val = readCapReg(cs);
-  cs_perms : bits(64) = EXTZ(getCapPerms(cs_val));
+  cs_perms : bits(64) = zero_extend(getCapPerms(cs_val));
   rt_perms = rGPR(rt);
   if (register_inaccessible(cs)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
@@ -856,7 +856,7 @@ function clause execute (CTestSubset(rd, cb, ct)) =
              0b0
         else
              0b1;
-     wGPR(rd) = EXTZ(result);
+     wGPR(rd) = zero_extend(result);
   }
   /* END_CTestSubset */
 }
@@ -1087,7 +1087,7 @@ function clause execute (CBX(cb, imm, notset)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if (((readCapReg(cb)).tag) ^ notset) then
     {
-      let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in
+      let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
       delayedPC     = PC + offset;
       branchPending = 0b1;
     }
@@ -1103,7 +1103,7 @@ function clause execute (CBZ(cb, imm, notzero)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else if (((readCapReg(cb)) == null_cap) ^ notzero) then
     {
-      let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in
+      let offset : bits(64) = (sign_extend(imm @ 0b00) + 4) in
       delayedPC     = PC + offset;
       branchPending = 0b1;
     }
@@ -1237,7 +1237,7 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
                     }
                 else
                   false;
-              wGPR(rd) = EXTZ(success);
+              wGPR(rd) = zero_extend(success);
             }
             else
           match width
@@ -1295,7 +1295,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
                   MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val))
                 else
                   false;
-              wGPR(rd) = EXTZ(success);
+              wGPR(rd) = zero_extend(success);
             }
           else
             MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val));
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index f0e96a14..9f91ae77 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -188,7 +188,7 @@ function memBitsToCapBits(tag, b) : (bool, bits(128)) -> bits(129) =
   memBitsToCapBits128(tag, b ^ null_cap_bits)
 
 function getCapPerms(cap) : CapStruct -> bits(31) = 
-    let perms : bits(15) = EXTS(getCapHardPerms(cap)) in /* NB access_system copied into 14-11 */
+    let perms : bits(15) = sign_extend(getCapHardPerms(cap)) in /* NB access_system copied into 14-11 */
     (0x000 /* uperms 30-19 */
   @ cap.uperms
   @ perms)
@@ -219,7 +219,7 @@ function sealCap(cap, otype) : (CapStruct, bits(24)) -> (bool, CapStruct) =
 function a_top_correction(a_mid, R, bound) : (bits(20), bits(20), bits(20)) -> bits(65) =
     match (a_mid <_u R, bound <_u R) {
       (false, false)  => zeros(),
-      (false, true)   => EXTZ(0b1),
+      (false, true)   => zero_extend(0b1),
       (true, false)   => ones(),
       (true, true)    => zeros()
     }
@@ -227,7 +227,7 @@ function a_top_correction(a_mid, R, bound) : (bits(20), bits(20), bits(20)) -> b
 function getCapBase(c) : CapStruct -> uint64 =
     let E = min(unsigned(c.E), 48) in
     let Bc : bits(20) = c.B in
-    let a : bits(65) = EXTZ(c.address) in
+    let a : bits(65) = zero_extend(c.address) in
     let R : bits(20) = Bc - 0x01000 in /* wraps */
     let a_mid : bits(20) = mask(a >> E) in
     let correction = a_top_correction(a_mid, R, Bc) in
@@ -239,7 +239,7 @@ function getCapTop (c) : CapStruct -> CapLen =
     let E = min(unsigned(c.E), 48) in
     let Bc : bits(20) = c.B in
     let T : bits(20) = c.T in
-    let a : bits(65) = EXTZ(c.address)  in
+    let a : bits(65) = zero_extend(c.address)  in
     let R : bits(20) = Bc - 0x01000 in /* wraps */
     let a_mid : bits(20) = mask(a >> E) in
     let correction = a_top_correction(a_mid, R, T) in
@@ -326,7 +326,7 @@ function setCapBounds(cap, base, top) : (CapStruct, bits(64), bits(65)) -> (bool
     let 'e = computeE(top - (0b0 @ base)) in
     let Bc : bits(20) = mask(base >> e) in
     let T : bits(20) = mask(top >> e) in
-    let e_mask : bits(65) = EXTZ(replicate_bits(0b1, e)) in
+    let e_mask : bits(65) = zero_extend(replicate_bits(0b1, e)) in
     let e_bits = top & e_mask in
     let T2 : bits(20) = T + (if unsigned(e_bits) == 0 then 0x00000 else 0x00001) in
     let newCap  = {cap with E=to_bits(6, e), B=Bc, T=T2} in