Skip to content

Commit 651c725

Browse files
nwf-msrnwf-msr
committed
Explict cap-auth load/store as-user instructions
1 parent 5202ae1 commit 651c725

File tree

1 file changed

+164
-0
lines changed

1 file changed

+164
-0
lines changed

‎src/cheri_insts.sail

+164
Original file line numberDiff line numberDiff line change
@@ -1486,6 +1486,28 @@ function clause execute (LoadDataCap(rd, cs1, is_unsigned, width)) = {
14861486
handle_load_data_via_cap(rd, 0b0 @ cs1, cs1_val, vaddr, is_unsigned, width, PrivDefault())
14871487
}
14881488

1489+
union clause ast = LoadUDataCap : (regidx, regidx, bool, word_width)
1490+
/*!
1491+
* Integer register *rd* is replaced with the signed or unsigned byte,
1492+
* halfword, word or doubleword located in memory at *cs1*.**address**.
1493+
* Memory access is performed as if the processor is executing in user mode,
1494+
* regardless of **mstatus**.
1495+
*
1496+
* ## Exceptions
1497+
*
1498+
* An exception is raised if:
1499+
* - *cs1*.**tag** is not set.
1500+
* - *cs1* is sealed.
1501+
* - *cs1*.**perms** does not grant **Permit_Load**.
1502+
* - *cs1*.**address** $\lt$ *cs1*.**base**.
1503+
* - *cs1*.**address** $+$ *size* $\gt$ *cs1*.**top**.
1504+
*/
1505+
function clause execute (LoadDataCap(rd, cs1, is_unsigned, width)) = {
1506+
let cs1_val = C(cs1);
1507+
let vaddr = cs1_val.address;
1508+
handle_load_data_via_cap(rd, 0b0 @ cs1, cs1_val, vaddr, is_unsigned, width, PrivOverride(User))
1509+
}
1510+
14891511
/*!
14901512
* Perform a capability load via a capability, returning either Some pair of
14911513
* the physical address used in the load and the resulting capability or None,
@@ -1592,6 +1614,32 @@ function clause execute (LoadCapCap(cd, cs1)) = {
15921614
handle_load_cap_via_cap(cd, 0b0 @ cs1, cs1_val, vaddr, PrivDefault())
15931615
}
15941616

1617+
union clause ast = LoadUCapCap : (regidx, regidx, bool, word_width)
1618+
/*!
1619+
* Capability register *cd* is replaced with the capability located in memory
1620+
* at *cs1*.**address**, and if *cs1*.**perms** does not grant
1621+
* **Permit_Load_Capability** then *cd*.**tag** is cleared.
1622+
* Memory access is performed as if the processor is executing in user mode,
1623+
* regardless of **mstatus**.
1624+
*
1625+
* ## Exceptions
1626+
*
1627+
* An exception is raised if:
1628+
* - *cs1*.**tag** is not set.
1629+
* - *cs1* is sealed.
1630+
* - *cs1*.**perms** does not grant **Permit_Load**.
1631+
* - *cs1*.**address** $\lt$ *cs1*.**base**.
1632+
* - *cs1*.**address** $+$ **CLEN** $/$ 8 $\gt$ *cs1*.**top**.
1633+
* - *cs1*.**address** is unaligned, regardless of whether the implementation
1634+
* supports unaligned data accesses.
1635+
*/
1636+
function clause execute (LoadUCapCap(rd, cs1, is_unsigned, width)) = {
1637+
let cs1_val = C(cs1);
1638+
let vaddr = cs1_val.address;
1639+
handle_load_cap_via_cap(rd, 0b0 @ cs1, cs1_val, vaddr, is_unsigned, width, PrivOverride(User))
1640+
}
1641+
1642+
15951643
union clause ast = CLoadTags : (regidx, regidx)
15961644
/*
15971645
* XXX: [LC] should be [LC](LoadCapImm) but that syntax does not generate
@@ -1865,6 +1913,18 @@ function clause execute (LoadResCap(rd, cs1, width)) = {
18651913
}
18661914
}
18671915

1916+
union clause ast = LoadResUCap : (regidx, regidx, word_width)
1917+
function clause execute (LoadResUCap(rd, cs1, width)) = {
1918+
if haveAtomics() then {
1919+
let cs1_val = C(cs1);
1920+
let vaddr = cs1_val.address;
1921+
handle_loadres_data_via_cap(rd, 0b0 @ cs1, cs1_val, vaddr, width, PrivOverride(User))
1922+
} else {
1923+
handle_illegal();
1924+
RETIRE_FAIL
1925+
}
1926+
}
1927+
18681928
union clause ast = LoadResCapCap : (regidx, regidx)
18691929
function clause execute (LoadResCapCap(cd, cs1)) = {
18701930
if haveAtomics() then {
@@ -1892,6 +1952,18 @@ function clause execute (LoadResCapMode(cd, rs1_cs1, aq, rl)) = {
18921952
}
18931953
}
18941954

1955+
union clause ast = LoadResUCapCap : (regidx, regidx)
1956+
function clause execute (LoadResUCapCap(cd, cs1)) = {
1957+
if haveAtomics() then {
1958+
let cs1_val = C(cs1);
1959+
let vaddr = cs1_val.address + X(cs1);
1960+
handle_loadres_cap_via_cap(cd, 0b0 @ cs1, cs1_val, vaddr, false, false, PrivOverride(User))
1961+
} else {
1962+
handle_illegal();
1963+
RETIRE_FAIL
1964+
}
1965+
}
1966+
18951967
val handle_store_data_via_cap : (regidx, capreg_idx, Capability, xlenbits, word_width, OptPrivilege) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
18961968
function handle_store_data_via_cap(rs2, auth_idx, auth_val, vaddrBits, width, optpriv) = {
18971969
let size = word_width_bytes(width);
@@ -1978,6 +2050,28 @@ function clause execute (StoreDataCap(rs2, cs1, width)) = {
19782050
handle_store_data_via_cap(rs2, 0b0 @ cs1, cs1_val, vaddr, width, PrivDefault())
19792051
}
19802052

2053+
union clause ast = StoreUDataCap : (regidx, regidx, word_width)
2054+
/*!
2055+
* The byte, halfword, word or doubleword located in memory at
2056+
* *cs1*.**address** is replaced with integer register *rs2*.
2057+
* Memory access is performed as if the processor is executing in user mode,
2058+
* regardless of **mstatus**.
2059+
*
2060+
* ## Exceptions
2061+
*
2062+
* An exception is raised if:
2063+
* - *cs1*.**tag** is not set.
2064+
* - *cs1* is sealed.
2065+
* - *cs1*.**perms** does not grant **Permit_Store**.
2066+
* - *cs1*.**address** $\lt$ *cs1*.**base**.
2067+
* - *cs1*.**address** $+$ *size* $\gt$ *cs1*.**top**.
2068+
*/
2069+
function clause execute (StoreUDataCap(rs2, cs1, width)) = {
2070+
let cs1_val = C(cs1);
2071+
let vaddr = cs1_val.address;
2072+
handle_store_data_via_cap(rs2, 0b0 @ cs1, cs1_val, vaddr, width, PrivOverride(User))
2073+
}
2074+
19812075
val handle_store_cap_via_cap : (regidx, capreg_idx, Capability, xlenbits, OptPrivilege) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wreg, wmvt}
19822076
function handle_store_cap_via_cap(cs2, auth_idx, auth_val, vaddrBits, optpriv) = {
19832077
let cs2_val = C(cs2);
@@ -2071,6 +2165,32 @@ function clause execute (StoreCapCap(cs2, cs1)) = {
20712165
handle_store_cap_via_cap(cs2, 0b0 @ cs1, cs1_val, vaddr, PrivDefault())
20722166
}
20732167

2168+
union clause ast = StoreUCapCap : (regidx, regidx)
2169+
/*!
2170+
* The capability located in memory at *cs1*.**address** is replaced with
2171+
* capability register *cs2*.
2172+
* Memory access is performed as if the processor is executing in user mode,
2173+
* regardless of **mstatus**.
2174+
*
2175+
* ## Exceptions
2176+
*
2177+
* An exception is raised if:
2178+
* - *cs1*.**tag** is not set.
2179+
* - *cs1* is sealed.
2180+
* - *cs1*.**perms** does not grant **Permit_Store**.
2181+
* - *cs1*.**perms** does not grant **Permit_Store_Capability** and
2182+
* *cs2*.**tag** is set.
2183+
* - *cs1*.**perms** does not grant **Permit_Store_Local_Capability**,
2184+
* *cs2*.**tag** is set and *cs2*.**perms** does not grant **Global**.
2185+
* - *cs1*.**address** $\lt$ *cs1*.**base**.
2186+
* - *cs1*.**address** $+$ **CLEN** $\gt$ *cs1*.**top**.
2187+
*/
2188+
function clause execute (StoreUCapCap(cs2, cs1)) = {
2189+
let cs1_val = C(cs1);
2190+
let vaddr = cs1_val.address;
2191+
handle_store_cap_via_cap(cs2, 0b0 @ cs1, cs1_val, vaddr, PrivDefault())
2192+
}
2193+
20742194
union clause ast = LoadCapImm : (regidx, regidx, bits(12))
20752195
/*!
20762196
* In integer mode, capability register *cd* is replaced with the capability
@@ -2680,3 +2800,47 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if (size == BYTE) | (size
26802800
<-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if (size == BYTE) | (size == HALF)
26812801
mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if (size == BYTE) | (size == HALF)
26822802
<-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if (size == BYTE) | (size == HALF)
2803+
2804+
/* As-User loads */
2805+
2806+
mapping clause encdec = LoadUDataCap(rd, cs1, false, BYTE) if (haveXcheri()) <-> 0b1111001 @ 0b01000 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri()) /* lb.cap */
2807+
mapping clause encdec = LoadUDataCap(rd, cs1, false, HALF) if (haveXcheri()) <-> 0b1111001 @ 0b01001 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri()) /* lh.cap */
2808+
mapping clause encdec = LoadUDataCap(rd, cs1, false, WORD) if (haveXcheri()) <-> 0b1111001 @ 0b01010 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri()) /* lw.cap */
2809+
mapping clause encdec = LoadUDataCap(rd, cs1, false, DOUBLE) if (haveXcheri() & haveRV64) <-> 0b1111001 @ 0b01011 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri() & haveRV64) /* ld.cap */
2810+
mapping clause encdec = LoadUDataCap(rd, cs1, true, BYTE) if (haveXcheri()) <-> 0b1111001 @ 0b01100 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri()) /* lbu.cap */
2811+
mapping clause encdec = LoadUDataCap(rd, cs1, true, HALF) if (haveXcheri()) <-> 0b1111001 @ 0b01101 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri()) /* lhu.cap */
2812+
mapping clause encdec = LoadUDataCap(rd, cs1, true, WORD) if (haveXcheri() & haveRV64) <-> 0b1111001 @ 0b01110 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri() & haveRV64) /* lwu.cap */
2813+
mapping clause encdec = LoadUDataCap(rd, cs1, true, DOUBLE) if (haveXcheri() & haveRV128) <-> 0b1111001 @ 0b01111 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri() & haveRV128) /* ldu.cap */
2814+
2815+
mapping clause assembly = LoadUDataCap(rd, cs1, u, w) <-> "l" ^ size_mnemonic(w) ^ maybe_u(u) ^ ".u.cap" ^ spc() ^ reg_name(rd) ^ sep() ^ "(" ^ opt_spc() ^ cap_reg_name(cs1) ^ opt_spc() ^ ")"
2816+
2817+
mapping clause encdec = LoadUCapCap(cd, cs1) if (haveXcheri() & sizeof(xlen) == 64) <-> 0b1111001 @ 0b11111 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri() & sizeof(xlen) == 64) /* lc.cap */
2818+
mapping clause encdec = LoadUCapCap(cd, cs1) if (haveXcheri() & sizeof(xlen) == 32) <-> 0b1111001 @ 0b01011 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri() & sizeof(xlen) == 32) /* lc.cap */
2819+
2820+
mapping clause assembly = LoadUCapCap(rd, cs1) <-> "lc.u.cap" ^ spc() ^ reg_name(rd) ^ sep() ^ "(" ^ opt_spc() ^ cap_reg_name(cs1) ^ opt_spc() ^ ")"
2821+
2822+
mapping clause encdec = LoadResUCap(rd, cs1, BYTE) if (haveXcheri() & haveAtomics()) <-> 0b1111001 @ 0b11000 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri() & haveAtomics()) /* lr.b.cap */
2823+
mapping clause encdec = LoadResUCap(rd, cs1, HALF) if (haveXcheri() & haveAtomics()) <-> 0b1111001 @ 0b11001 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri() & haveAtomics()) /* lr.h.cap */
2824+
mapping clause encdec = LoadResUCap(rd, cs1, WORD) if (haveXcheri() & haveAtomics()) <-> 0b1111001 @ 0b11010 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri() & haveAtomics()) /* lr.w.cap */
2825+
mapping clause encdec = LoadResUCap(rd, cs1, DOUBLE) if (haveXcheri() & haveAtomics() & haveRV64) <-> 0b1111001 @ 0b11011 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri() & haveAtomics() & haveRV64) /* lr.d.cap */
2826+
mapping clause encdec = LoadResUCapCap(cd, cs1) if (haveXcheri() & haveAtomics() & sizeof(xlen) == 32) <-> 0b1111001 @ 0b11011 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri() & haveAtomics() & sizeof(xlen) == 32) /* lr.c.cap */
2827+
mapping clause encdec = LoadResUCapCap(cd, cs1) if (haveXcheri() & haveAtomics() & sizeof(xlen) == 64) <-> 0b1111001 @ 0b11100 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri() & haveAtomics() & sizeof(xlen) == 64) /* lr.c.cap */
2828+
2829+
mapping clause assembly = LoadResUCap(rd, cs1, w) <-> "lr." ^ size_mnemonic(w) ^ ".u.cap" ^ spc() ^ reg_name(rd) ^ sep() ^ "(" ^ opt_spc() ^ cap_reg_name(cs1) ^ opt_spc() ^ ")"
2830+
mapping clause assembly = LoadResUCapCap(cd, cs1) <-> "lr.c.u.cap" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ "(" ^ opt_spc() ^ cap_reg_name(cs1) ^ opt_spc() ^ ")"
2831+
2832+
/* As-User stores */
2833+
2834+
mapping clause encdec = StoreUDataCap(rs2, cs1, BYTE) if (haveXcheri()) <-> 0b1111000 @ rs2 @ cs1 @ 0b000 @ 0b01000 @ 0b1011011 if (haveXcheri()) /* sb.cap */
2835+
mapping clause encdec = StoreUDataCap(rs2, cs1, HALF) if (haveXcheri()) <-> 0b1111000 @ rs2 @ cs1 @ 0b000 @ 0b01001 @ 0b1011011 if (haveXcheri()) /* sh.cap */
2836+
mapping clause encdec = StoreUDataCap(rs2, cs1, WORD) if (haveXcheri()) <-> 0b1111000 @ rs2 @ cs1 @ 0b000 @ 0b01010 @ 0b1011011 if (haveXcheri()) /* sw.cap */
2837+
mapping clause encdec = StoreUDataCap(rs2, cs1, DOUBLE) if (haveXcheri() & haveRV64) <-> 0b1111000 @ rs2 @ cs1 @ 0b000 @ 0b01011 @ 0b1011011 if (haveXcheri() & haveRV64) /* sd.cap */
2838+
mapping clause encdec = StoreUCapCap(cs2, cs1) if (haveXcheri() & sizeof(xlen) == 64) <-> 0b1111000 @ cs2 @ cs1 @ 0b000 @ 0b01100 @ 0b1011011 if (haveXcheri() & sizeof(xlen) == 64) /* sc.cap */
2839+
mapping clause encdec = StoreUCapCap(cs2, cs1) if (haveXcheri() & sizeof(xlen) == 32) <-> 0b1111000 @ cs2 @ cs1 @ 0b000 @ 0b01011 @ 0b1011011 if (haveXcheri() & sizeof(xlen) == 32) /* sc.cap */
2840+
2841+
mapping clause encdec = StoreCondUCap(rs2, cs1, BYTE) if (haveXcheri() & haveAtomics()) <-> 0b1111000 @ rs2 @ cs1 @ 0b000 @ 0b11000 @ 0b1011011 if (haveXcheri() & haveAtomics()) /* sc.b.cap */
2842+
mapping clause encdec = StoreCondUCap(rs2, cs1, HALF) if (haveXcheri() & haveAtomics()) <-> 0b1111000 @ rs2 @ cs1 @ 0b000 @ 0b11001 @ 0b1011011 if (haveXcheri() & haveAtomics()) /* sc.h.cap */
2843+
mapping clause encdec = StoreCondUCap(rs2, cs1, WORD) if (haveXcheri() & haveAtomics()) <-> 0b1111000 @ rs2 @ cs1 @ 0b000 @ 0b11010 @ 0b1011011 if (haveXcheri() & haveAtomics()) /* sc.w.cap */
2844+
mapping clause encdec = StoreCondUCap(rs2, cs1, DOUBLE) if (haveXcheri() & haveAtomics() & haveRV64) <-> 0b1111000 @ rs2 @ cs1 @ 0b000 @ 0b11011 @ 0b1011011 if (haveXcheri() & haveAtomics()& haveRV64) /* sc.d.cap */
2845+
mapping clause encdec = StoreCondUCapCap(cs2, cs1) if (haveXcheri() & haveAtomics() & sizeof(xlen) == 32) <-> 0b1111000 @ cs2 @ cs1 @ 0b000 @ 0b11011 @ 0b1011011 if (haveXcheri() & haveAtomics() & sizeof(xlen) == 32) /* sc.c.cap */
2846+
mapping clause encdec = StoreCondUCapCap(cs2, cs1) if (haveXcheri() & haveAtomics() & sizeof(xlen) == 64) <-> 0b1111000 @ cs2 @ cs1 @ 0b000 @ 0b11100 @ 0b1011011 if (haveXcheri() & haveAtomics() & sizeof(xlen) == 64) /* sc.c.cap */

0 commit comments

Comments
 (0)