diff options
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_insts.sail | 4 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 6 |
2 files changed, 7 insertions, 3 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 8b5d9dd0..0a286070 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -1101,7 +1101,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) = else { cursor := getCapCursor(cb_val); - vAddr := cursor + unsigned(rGPR(rt)) + (16 * signed(offset)); + vAddr := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset)); vAddr64:= (bit[64]) vAddr; if ((vAddr + cap_size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) @@ -1148,7 +1148,7 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) = else { cursor := getCapCursor(cb_val); - vAddr := cursor + unsigned(rGPR(rt)) + (16*signed(offset)); + vAddr := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset)); vAddr64:= (bit[64]) vAddr; if ((vAddr + cap_size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index f41d9c14..ee9a91ac 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -35,6 +35,11 @@ (* 256 bit cap + tag *) typedef CapReg = bit[257] +val cast bool -> bit effect pure cast_bool_bit +val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_bool_vec + +typedef uint64 = range<0, (2** 64) - 1> + typedef CapStruct = const struct { bool tag; bit[8] padding; @@ -204,4 +209,3 @@ function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65 function CapStruct int_to_cap ((bit[64]) offset) = {null_cap with offset = offset} - |