diff options
| author | Thomas Bauereiss | 2017-08-24 20:32:17 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-08-24 20:32:17 +0100 |
| commit | a42684821d6c0487c248900a89e1f464737da771 (patch) | |
| tree | f03faa7491fef95e88f2c70975757f1ca289a11e /cheri | |
| parent | 8a8165d8689547c80e0725bedab945a471a3294b (diff) | |
Fix some bugs related to the CHERI spec
- Correctly pass exponentials to Z3
- Infer types of functional record updates
- Support "def Nat"
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} - |