From 26c7468c15c15424535afebc12e995a3a746476f Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 14 Mar 2018 16:05:37 +0000 Subject: rename EXTS and EXTZ to sign_extend and zero_extend because it is more obviosu and to more closely match existing cheri pseudocode. --- cheri/cheri_insts.sail | 26 +++++++++++++------------- cheri/cheri_prelude_128.sail | 10 +++++----- 2 files changed, 18 insertions(+), 18 deletions(-) (limited to 'cheri') 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 -- cgit v1.2.3