From f03900fa201311233715fdcc3f59de4cfdc5a9ab Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sat, 16 Dec 2023 15:18:37 -0600 Subject: [PATCH 01/10] CSRs infra. update - prep for Zicfiss - Separate legalizers for menvcfg and senvcfg - Add a getter for senvcfg as fields in senvcfg depend on menvcfg --- model/riscv_insts_zicsr.sail | 2 +- model/riscv_sys_regs.sail | 12 ++++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index f2980fb9e..c1fe6ef2e 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -81,7 +81,7 @@ function readCSR csr : csreg -> xlenbits = { (0x104, _) => lower_mie(mie, mideleg).bits, (0x105, _) => get_stvec(), (0x106, _) => zero_extend(scounteren.bits), - (0x10A, _) => senvcfg.bits[sizeof(xlen) - 1 .. 0], + (0x10A, _) => get_senvcfg()[sizeof(xlen) - 1 .. 0], (0x140, _) => sscratch, (0x141, _) => get_xret_target(Supervisor) & pc_alignment_mask(), (0x142, _) => scause.bits, diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 65d141923..9b82eb183 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -848,6 +848,18 @@ function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = { o } +function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { + let v = Mk_Envcfg(v); + let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); + // Other extensions are not implemented yet so all other fields are read only zero. + o +} + +function get_senvcfg() -> bits(64) = { + let o : Envcfg = senvcfg; + o.bits() +} + // Return whether or not FIOM is currently active, based on the current // privilege and the menvcfg/senvcfg settings. This means that I/O fences // imply memory fence. From 8390b75c727ead3aec359545da442516751b8eb1 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sat, 16 Dec 2023 15:23:00 -0600 Subject: [PATCH 02/10] Add Zimop and Zcmop extension Zicfiss instructions use codepoints defined by Zimop/Zcmop extension. Add the baseline Zimop/Zcmop as preparation to be extended by Zicfiss. --- model/riscv_insts_zcmop.sail | 100 ++++++++++++++++++++++++ model/riscv_insts_zimop.sail | 144 +++++++++++++++++++++++++++++++++++ model/riscv_sys_regs.sail | 6 ++ 3 files changed, 250 insertions(+) create mode 100644 model/riscv_insts_zcmop.sail create mode 100644 model/riscv_insts_zimop.sail diff --git a/model/riscv_insts_zcmop.sail b/model/riscv_insts_zcmop.sail new file mode 100644 index 000000000..7e4529c3a --- /dev/null +++ b/model/riscv_insts_zcmop.sail @@ -0,0 +1,100 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Ved Shanbhogue */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + +/* ********************************************************************* */ +/* This file specifies the compressed insts. in the 'Zcmop' extension. */ + +/* These instructions are only legal if misa.C() is true and is checked in + * the fetch-execute logic. + */ +/* ****************************************************************** */ + +union clause ast = ZCMOP : (bits(3)) +mapping clause encdec_compressed = ZCMOP(mop) if haveZcmop() + <-> 0b01100 @ mop : bits(3) @ 0b100000 @ 0b01 if haveZcmop() + +mapping zcmop_mnemonic : bits(3) <-> string = { + 0b000 <-> "c.mop.1", + 0b001 <-> "c.mop.3", + 0b010 <-> "c.mop.5", + 0b011 <-> "c.mop.7", + 0b100 <-> "c.mop.9", + 0b101 <-> "c.mop.11", + 0b110 <-> "c.mop.13", + 0b111 <-> "c.mop.15" +} + +mapping clause assembly = ZCMOP(mop) + <-> zcmop_mnemonic(mop) + +function clause execute ZCMOP(mop) = { + RETIRE_SUCCESS +} diff --git a/model/riscv_insts_zimop.sail b/model/riscv_insts_zimop.sail new file mode 100644 index 000000000..66c0857e3 --- /dev/null +++ b/model/riscv_insts_zimop.sail @@ -0,0 +1,144 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Ved Shanbhogue */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + +/* ****************************************************************** */ +/* This file specifies the instructions in the Zimop extension. */ +/* mop.r.0-31: 1-00--0111--sssss100ddddd1110011 */ +/* mop.rr.0-7: 1-00--1tttttsssss100ddddd1110011 */ +union clause ast = ZIMOP_MOP_R : (bits(5), regidx, regidx) +union clause ast = ZIMOP_MOP_RR : (bits(3), regidx, regidx, regidx) + +mapping clause encdec = ZIMOP_MOP_R(mop_30 @ mop_27_26 @ mop_21_20, rs1, rd) if haveZimop() + <-> 0b1 @ mop_30 : bits(1) @ 0b00 @ mop_27_26 : bits(2) @ 0b0111 @ mop_21_20 : bits(2) @ rs1 @ 0b100 @ rd @ 0b1110011 if haveZimop() + +mapping clause encdec = ZIMOP_MOP_RR(mop_30 @ mop_27_26, rs2, rs1, rd) if haveZimop() + <-> 0b1 @ mop_30 : bits(1) @ 0b00 @ mop_27_26 : bits(2) @ 0b1 @ rs2 @ rs1 @ 0b100 @ rd @ 0b1110011 if haveZimop() + +mapping zimop_r_mnemonic : bits(5) <-> string = { + 0b00000 <-> "mop.r.0", + 0b00001 <-> "mop.r.1", + 0b00010 <-> "mop.r.2", + 0b00011 <-> "mop.r.3", + 0b00100 <-> "mop.r.4", + 0b00101 <-> "mop.r.5", + 0b00110 <-> "mop.r.6", + 0b00111 <-> "mop.r.7", + 0b01000 <-> "mop.r.8", + 0b01001 <-> "mop.r.9", + 0b01010 <-> "mop.r.10", + 0b01011 <-> "mop.r.11", + 0b01100 <-> "mop.r.12", + 0b01101 <-> "mop.r.13", + 0b01110 <-> "mop.r.14", + 0b01111 <-> "mop.r.15", + 0b10000 <-> "mop.r.16", + 0b10001 <-> "mop.r.17", + 0b10010 <-> "mop.r.18", + 0b10011 <-> "mop.r.19", + 0b10100 <-> "mop.r.20", + 0b10101 <-> "mop.r.21", + 0b10110 <-> "mop.r.22", + 0b10111 <-> "mop.r.23", + 0b11000 <-> "mop.r.24", + 0b11001 <-> "mop.r.25", + 0b11010 <-> "mop.r.26", + 0b11011 <-> "mop.r.27", + 0b11100 <-> "mop.r.28", + 0b11101 <-> "mop.r.29", + 0b11110 <-> "mop.r.30", + 0b11111 <-> "mop.r.31" +} + +mapping zimop_rr_mnemonic : bits(3) <-> string = { + 0b000 <-> "mop.rr.0", + 0b001 <-> "mop.rr.1", + 0b010 <-> "mop.rr.2", + 0b011 <-> "mop.rr.3", + 0b100 <-> "mop.rr.4", + 0b101 <-> "mop.rr.5", + 0b110 <-> "mop.rr.6", + 0b111 <-> "mop.rr.7" +} + +mapping clause assembly = ZIMOP_MOP_R(mop, rs1, rd) + <-> zimop_r_mnemonic(mop) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) + +mapping clause assembly = ZIMOP_MOP_RR(mop, rs2, rs1, rd) + <-> zimop_rr_mnemonic(mop) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + +function clause execute ZIMOP_MOP_R(mop, rs1, rd) = { + X(rd) = zeros(); + RETIRE_SUCCESS +} +function clause execute ZIMOP_MOP_RR(mop, rs2, rs1, rd) = { + X(rd) = zeros(); + RETIRE_SUCCESS +} diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 9b82eb183..5483b2921 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -168,6 +168,12 @@ function haveZalrsc() -> bool = haveAtomics() /* Zicond extension support */ function haveZicond() -> bool = true +/* Zimop extension support */ +function haveZimop() -> bool = true + +/* Zcmop extension support */ +function haveZcmop() -> bool = true + /* * Illegal values legalized to least privileged mode supported. * Note: the only valid combinations of supported modes are M, M+U, M+S+U. From a918a053adb097879ba1369947904b00dcf46162 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sat, 16 Dec 2023 15:27:51 -0600 Subject: [PATCH 03/10] Add CSR and CSR fields introduced by Zicfiss - SSE field in menvcfg - SSE field in senvcfg - New CSR ssp --- model/riscv_csr_map.sail | 2 + model/riscv_sys_regs.sail | 28 ++++---- model/riscv_zicfiss_control.sail | 107 +++++++++++++++++++++++++++++++ model/riscv_zicfiss_regs.sail | 72 +++++++++++++++++++++ 4 files changed, 198 insertions(+), 11 deletions(-) create mode 100644 model/riscv_zicfiss_control.sail create mode 100644 model/riscv_zicfiss_regs.sail diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 22cffd5a6..7e23f279d 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -176,6 +176,8 @@ mapping clause csr_name_map = 0x00F <-> "vcsr" mapping clause csr_name_map = 0xC20 <-> "vl" mapping clause csr_name_map = 0xC21 <-> "vtype" mapping clause csr_name_map = 0xC22 <-> "vlenb" +/* Zicfiss csrs */ +mapping clause csr_name_map = 0x011 <-> "ssp" val csr_name : csreg -> string overload to_str = {csr_name} diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 5483b2921..3addb2d20 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -174,6 +174,9 @@ function haveZimop() -> bool = true /* Zcmop extension support */ function haveZcmop() -> bool = true +/* Zicfiss extension support */ +function haveZicfiss() -> bool = true + /* * Illegal values legalized to least privileged mode supported. * Note: the only valid combinations of supported modes are M, M+U, M+S+U. @@ -818,8 +821,10 @@ bitfield MEnvcfg : bits(64) = { CBCFE : 6, // Cache Block Invalidate instruction Enable CBIE : 5 .. 4, + // Zicfiss: Shadow stack enable + SSE : 3, // Reserved WPRI bits. - wpri_0 : 3 .. 1, + wpri_0 : 2 .. 1, // Fence of I/O implies Memory FIOM : 0, } @@ -831,8 +836,10 @@ bitfield SEnvcfg : xlenbits = { CBCFE : 6, // Cache Block Invalidate instruction Enable CBIE : 5 .. 4, + // Zicfiss: Shadow stack enable + SSE : 3, // Reserved WPRI bits. - wpri_0 : 3 .. 1, + wpri_0 : 2 .. 1, // Fence of I/O implies Memory FIOM : 0, } @@ -843,6 +850,8 @@ register senvcfg : SEnvcfg function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = { let v = Mk_MEnvcfg(v); let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; + // Zicfiss - SSE: shadow stack enable + let o = [o with SSE = if haveZicfiss() then v[SSE] else 0b0]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -850,19 +859,16 @@ function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = { function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = { let v = Mk_SEnvcfg(v); let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; + // Zicfiss - SSE: shadow stack enable - is ROZ in senvcfg if menvcfg.SSE is 0 + let o = update_SSE(o, if haveZicfiss() & menvcfg.SSE() == 0b1 then v.SSE() else 0b0); // Other extensions are not implemented yet so all other fields are read only zero. o } -function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { - let v = Mk_Envcfg(v); - let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); - // Other extensions are not implemented yet so all other fields are read only zero. - o -} - -function get_senvcfg() -> bits(64) = { - let o : Envcfg = senvcfg; +function get_senvcfg() -> xlenbits = { + let o : SEnvcfg = senvcfg; + // Zicfiss - SSE: shadow stack enable - is ROZ in senvcfg if menvcfg.SSE is 0 + let o = [o with SSE = if haveZicfiss() & menvcfg[SSE] == 0b1 then o[SSE] else 0b0]; o.bits() } diff --git a/model/riscv_zicfiss_control.sail b/model/riscv_zicfiss_control.sail new file mode 100644 index 000000000..6baae058d --- /dev/null +++ b/model/riscv_zicfiss_control.sail @@ -0,0 +1,107 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + +/* Architectural state for the Zicfiss extension. */ +function clause ext_is_CSR_defined(0x011, priv) = { // ssp + /* Attempts to access the ssp CSR may result in either an illegal-instruction exception + * or a virtual instruction exception, contingent upon the state of the xenvcfg.SSE + * fields. The conditions are specified as follows: + * 1 If the privilege mode is less than M and menvcfg.SSE is 0, an illegal-instruction + * exception is raised. + * 2 Otherwise, if in U-mode and senvcfg.SSE is 0, an illegal-instruction exception + * is raised. + * 3 Otherwise, if in VS-mode and henvcfg.SSE is 0, a virtual instruction exception + * is raised. + * 4 Otherwise, if in VU-mode and either henvcfg.SSE or senvcfg.SSE is 0, a virtual + * instruction exception is raised. + * 5 Otherwise, the access is allowed. + * Sail does not implement H extension and the conditions 3 and 4 are not + * implemented at the moment. + */ + if priv == Machine + then true + else if priv == Supervisor + then menvcfg[SSE] == 0b1 + else if haveSupMode() + then senvcfg.SSE() == 0b1 + else false +} +function clause ext_read_CSR(0x011) = Some(ssp) +function clause ext_write_CSR(0x011, value) = { + ssp = value; + ssp[1 .. 0] = 0b00; + /* if UXL/SXL can be set to 32 in RV64, the bit 2 is not read-only zero; + * Sail model does not support dynamic switching of UXL/SXL so that is + * not considered in the following algorithm yet. + */ + if ( architecture(misa.MXL()) == Some(RV64) ) then + ssp[2 .. 2] = 0b0; + Some(ssp); +} diff --git a/model/riscv_zicfiss_regs.sail b/model/riscv_zicfiss_regs.sail new file mode 100644 index 000000000..9a613efc1 --- /dev/null +++ b/model/riscv_zicfiss_regs.sail @@ -0,0 +1,72 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + +/* Architectural state for the Zicfiss extension. */ +register ssp : xlenbits From b854aacd72aa18ed1b67cfb336abe283eced236a Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sat, 16 Dec 2023 15:34:55 -0600 Subject: [PATCH 04/10] Add software check exception - Zicfiss instructions can generate software check exceptions with xtval set to SHADOW_STACK_FAULT. --- model/riscv_sys_control.sail | 7 +++++++ model/riscv_types.sail | 20 ++++++++++++++++++++ 2 files changed, 27 insertions(+) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 95ed4d6a5..8267c24f4 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -462,6 +462,13 @@ function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = { set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC)) } +function handle_sw_check_exception(code : SWCheckCodes) -> unit = { + let t : sync_exception = struct { trap = E_SW_Check_Fault(), + excinfo = Some(sw_check_code_to_bits(code)), + ext = None() } in + set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC)) +} + function handle_exception(e: ExceptionType) -> unit = { let t : sync_exception = struct { trap = e, excinfo = None(), diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 2b1c132ec..3ed49b0ef 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -183,6 +183,9 @@ union ExceptionType = { E_Load_Page_Fault : unit, E_Reserved_14 : unit, E_SAMO_Page_Fault : unit, + E_Reserved_16 : unit, + E_Reserved_17 : unit, + E_SW_Check_Fault : unit, /* extensions */ E_Extension : ext_exc_type @@ -207,6 +210,9 @@ function exceptionType_to_bits(e) = E_Load_Page_Fault() => 0x0d, E_Reserved_14() => 0x0e, E_SAMO_Page_Fault() => 0x0f, + E_Reserved_16() => 0x10, + E_Reserved_17() => 0x11, + E_SW_Check_Fault() => 0x12, /* extensions */ E_Extension(e) => ext_exc_type_to_bits(e) @@ -231,6 +237,9 @@ function num_of_ExceptionType(e) = E_Load_Page_Fault() => 13, E_Reserved_14() => 14, E_SAMO_Page_Fault() => 15, + E_Reserved_16() => 16, + E_Reserved_17() => 17, + E_SW_Check_Fault() => 18, /* extensions */ E_Extension(e) => num_of_ext_exc_type(e) @@ -256,6 +265,9 @@ function exceptionType_to_str(e) = E_Load_Page_Fault() => "load-page-fault", E_Reserved_14() => "reserved-1", E_SAMO_Page_Fault() => "store/amo-page-fault", + E_Reserved_16() => "reserved-2", + E_Reserved_17() => "reserved-3", + E_SW_Check_Fault() => "software-check-fault", /* extensions */ E_Extension(e) => ext_exc_type_to_str(e) @@ -263,6 +275,14 @@ function exceptionType_to_str(e) = overload to_str = {exceptionType_to_str} +/* SW check exception codes */ +enum SWCheckCodes = {SHADOW_STACK_FAULT} + +function sw_check_code_to_bits (c : SWCheckCodes) -> xlenbits = + match (c) { + SHADOW_STACK_FAULT => zero_extend(0b011) + } + /* trap modes */ type tv_mode = bits(2) From 51756e19af3a1a01f10c5ee2c086964acccb8c2d Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sat, 16 Dec 2023 16:39:34 -0600 Subject: [PATCH 05/10] Add plumbing for PTEs to cause access fault With Zicfiss, PTE based checks may cause a page-fault or an access fault. Extend the PTE permission checks plumbing to be able to signal both. --- model/riscv_vmem_ptw.sail | 46 +++++++++++++++++++++++---------------- 1 file changed, 27 insertions(+), 19 deletions(-) diff --git a/model/riscv_vmem_ptw.sail b/model/riscv_vmem_ptw.sail index ab73b1909..374aca0d8 100644 --- a/model/riscv_vmem_ptw.sail +++ b/model/riscv_vmem_ptw.sail @@ -40,27 +40,35 @@ function ptw_error_to_str(e : PTW_Error) -> string = { // PUBLIC overload to_str = {ptw_error_to_str} -// hook for (non-standard) extensions to customize errors reported by page-table -// walks during address translation; it typically works in conjunction -// with any customization to check_PTE_permission(). - -// PRIVATE -function ext_get_ptw_error(eptwf : ext_ptw_fail) -> PTW_Error = +/* hook for extensions to customize errors reported by page-table + * walks during address translation; it typically works in conjunction + * with any customization to check_PTE_permission(). + */ +function ext_get_ptw_permission_error(eptwf : ext_ptw_fail) -> PTW_Error = PTW_No_Permission() -// Convert translation/PTW failures into architectural exceptions -function translationException(a : AccessType(ext_access_type), - f : PTW_Error) - -> ExceptionType = { +function ext_get_ptw_access_error(eptwf : ext_ptw_fail) -> PTW_Error = + PTW_Access() + +/* conversion of these translation/PTW failures into architectural exceptions */ +function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> ExceptionType = { + let e : ExceptionType = match (a, f) { - (_, PTW_Ext_Error(e)) => E_Extension(ext_translate_exception(e)), - (ReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(), - (ReadWrite(_), _) => E_SAMO_Page_Fault(), - (Read(_), PTW_Access()) => E_Load_Access_Fault(), - (Read(_), _) => E_Load_Page_Fault(), - (Write(_), PTW_Access()) => E_SAMO_Access_Fault(), - (Write(_), _) => E_SAMO_Page_Fault(), - (Execute(), PTW_Access()) => E_Fetch_Access_Fault(), - (Execute(), _) => E_Fetch_Page_Fault() + (_, PTW_Ext_Error(e)) => E_Extension(ext_translate_exception(e)), + (ReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(), + (ReadWrite(_), _) => E_SAMO_Page_Fault(), + (Read(_), PTW_Access()) => E_Load_Access_Fault(), + (Read(_), _) => E_Load_Page_Fault(), + (Write(_), PTW_Access()) => E_SAMO_Access_Fault(), + (Write(_), _) => E_SAMO_Page_Fault(), + (Execute(), PTW_Access()) => E_Fetch_Access_Fault(), + (Execute(), _) => E_Fetch_Page_Fault(), + /* Zicfiss: shadow stack store/amo exceptions */ + (SSReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(), + (SSReadWrite(_), _) => E_SAMO_Page_Fault(), + (SSRead(_), PTW_Access()) => E_SAMO_Access_Fault(), + (SSRead(_), _) => E_SAMO_Page_Fault(), + (SSWrite(_), PTW_Access()) => E_SAMO_Access_Fault(), + (SSWrite(_), _) => E_SAMO_Page_Fault() } } From 601fd3c1bcbbe2ddc2eb4d0c3107504cc5d7673b Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sat, 16 Dec 2023 16:56:22 -0600 Subject: [PATCH 06/10] Add SS page type and SS access types - SS pages are encoded in pte as XWR=010b. - Add rules for access to such pages by non-SS load/store/AMO and inst. fetch. - Add rules for access to such pages by SS load/store/AMO. - SS access not allowed in Svbare. When virtual memory system is not active, all shadow stack accesses cause an access violation. - Add rules for PMP access checks by shadow stack accesses --- model/riscv_pmp_control.sail | 10 +++- model/riscv_types.sail | 6 +- model/riscv_vmem.sail | 68 +++++++++++++--------- model/riscv_vmem_pte.sail | 109 +++++++++++++++++++++++------------ model/riscv_vmem_ptw.sail | 5 +- model/riscv_vmem_types.sail | 6 +- 6 files changed, 137 insertions(+), 67 deletions(-) diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index ce53caf06..e011753fd 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -44,7 +44,11 @@ function pmpCheckRWX(ent, acc) = { Read(_) => ent[R] == 0b1, Write(_) => ent[W] == 0b1, ReadWrite(_) => ent[R] == 0b1 & ent[W] == 0b1, - Execute() => ent[X] == 0b1 + Execute() => ent[X] == 0b1, + /* Zicfiss: ss read/write require write perms */ + SSRead(_) => ent[W] == 0b1, + SSWrite(_) => ent[W] == 0b1, + SSReadWrite(_) => ent[R] == 0b1 & ent[W] == 0b1 } } @@ -109,6 +113,10 @@ function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType = Write(_) => E_SAMO_Access_Fault(), ReadWrite(_) => E_SAMO_Access_Fault(), Execute() => E_Fetch_Access_Fault(), + /* Zicfiss - shadow stack accesses cause SAMO access fault */ + SSRead(_) => E_SAMO_Access_Fault(), + SSWrite(_) => E_SAMO_Access_Fault(), + SSReadWrite(_) => E_SAMO_Access_Fault() } function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: int('n), acc: AccessType(ext_access_type), priv: Privilege) diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 3ed49b0ef..eb81a9cee 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -131,7 +131,11 @@ union AccessType ('a : Type) = { Read : 'a, Write : 'a, ReadWrite : ('a, 'a), - Execute : unit + Execute : unit, + /* Zicfiss: Access types for shadow stack */ + SSRead : 'a, + SSWrite : 'a, + SSReadWrite : ('a, 'a) } enum word_width = {BYTE, HALF, WORD, DOUBLE} diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index 2bb96fe7a..288b87cb2 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -143,8 +143,10 @@ function pt_walk(sv_params, let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags, ext_pte, ext_ptw); match pte_check { - PTE_Check_Failure(ext_ptw, ext_ptw_fail) => - PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw), + PTE_Check_Failure_Permission(ext_ptw, ext_ptw_fail) => + PTW_Failure(ext_get_ptw_permission_error(ext_ptw_fail), ext_ptw), + PTE_Check_Failure_No_Access(ext_ptw, ext_ptw_fail) => + PTW_Failure(ext_get_ptw_access_error(ext_ptw_fail), ext_ptw), PTE_Check_Success(ext_ptw) => if level > 0 then { // Superpage; construct mask for lower-level PPNs from the PTE @@ -302,8 +304,10 @@ function translate_TLB_hit(sv_params : SV_Params, ext_pte, ext_ptw); match pte_check { - PTE_Check_Failure(ext_ptw, ext_ptw_fail) => - TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw), + PTE_Check_Failure_Permission(ext_ptw, ext_ptw_fail) => + TR_Failure(ext_get_ptw_permission_error(ext_ptw_fail), ext_ptw), + PTE_Check_Failure_No_Access(ext_ptw, ext_ptw_fail) => + TR_Failure(ext_get_ptw_access_error(ext_ptw_fail), ext_ptw), PTE_Check_Success(ext_ptw) => match update_PTE_Bits(sv_params, pte, ac) { None() => TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw), @@ -416,30 +420,42 @@ function translateAddr(vAddr : xlenbits, // See riscv_sys_regs.sail for effectivePrivilege() and cur_privilege let effPriv : Privilege = effectivePrivilege(ac, mstatus, cur_privilege); let mode : SATPMode = translationMode(effPriv); - let (valid_va, sv_params) : (bool, SV_Params) = match mode { - Sbare => return TR_Address(vAddr, init_ext_ptw), - Sv32 => (true, sv32_params), - Sv39 => (is_valid_vAddr(sv39_params, vAddr_64b), sv39_params), - Sv48 => (is_valid_vAddr(sv48_params, vAddr_64b), sv48_params), - // Sv57 => (is_valid_vAddr(sv57_params, vAddr_64b), sv57_params), // TODO + + // Zicfiss: Shadow stack accesses cause access fault in Bare mode + let ss_access_fault : bool = match ac { + SSRead(_) => if mode == Sbare then true else false, + SSWrite(_) => if mode == Sbare then true else false, + SSReadWrite(_, _) => if mode == Sbare then true else false, + _ => false }; - if not(valid_va) then - TR_Failure(translationException(ac, PTW_Invalid_Addr()), init_ext_ptw) + if ss_access_fault then + TR_Failure(translationException(ac, PTW_Access()), init_ext_ptw) else { - let mxr = mstatus[MXR] == 0b1; - let do_sum = mstatus[SUM] == 0b1; - let asid : asidbits = satp_to_asid(satp); - let ptb : bits(64) = satp_to_PT_base(satp); - let tr_result1 = translate(sv_params, - asid, - ptb, - vAddr_64b, - ac, effPriv, mxr, do_sum, - init_ext_ptw); - // Fixup result PA or exception - match tr_result1 { - TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, sizeof(xlen)), ext_ptw), - TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) + let (valid_va, sv_params) : (bool, SV_Params) = match mode { + Sbare => return TR_Address(vAddr, init_ext_ptw), + Sv32 => (true, sv32_params), + Sv39 => (is_valid_vAddr(sv39_params, vAddr_64b), sv39_params), + Sv48 => (is_valid_vAddr(sv48_params, vAddr_64b), sv48_params), + // Sv57 => (is_valid_vAddr(sv57_params, vAddr_64b), sv57_params), // TODO + }; + if not(valid_va) then + TR_Failure(translationException(ac, PTW_Invalid_Addr()), init_ext_ptw) + else { + let mxr = mstatus[MXR] == 0b1; + let do_sum = mstatus[SUM] == 0b1; + let asid : asidbits = satp_to_asid(satp); + let ptb : bits(64) = satp_to_PT_base(satp); + let tr_result1 = translate(sv_params, + asid, + ptb, + vAddr_64b, + ac, effPriv, mxr, do_sum, + init_ext_ptw); + // Fixup result PA or exception + match tr_result1 { + TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, sizeof(xlen)), ext_ptw), + TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) + } } } } diff --git a/model/riscv_vmem_pte.sail b/model/riscv_vmem_pte.sail index 07a94a3ed..f17fb385d 100644 --- a/model/riscv_vmem_pte.sail +++ b/model/riscv_vmem_pte.sail @@ -51,10 +51,15 @@ function pte_is_ptr(pte_flags : PTE_Flags) -> bool = (pte_flags[X] == 0b0) & (pte_flags[W] == 0b0) & (pte_flags[R] == 0b0) +// PRIVATE: Zicfiss: ss pte -> rwx=010b +val is_shadow_stack_PTE_enable : unit -> bool +function is_ss_pte(p : PTE_Flags) -> bool = + (p[R] == 0b0 & p[W] == 0b1 & p[X] == 0b0 & is_shadow_stack_PTE_enable()) + // PRIVATE: check if a PTE is valid -function pte_is_invalid(pte_flags : PTE_Flags) -> bool = (pte_flags[V] == 0b0) - | ((pte_flags[W] == 0b1) - & (pte_flags[R] == 0b0)) +function pte_is_invalid(pte_flags : PTE_Flags) -> bool = + (pte_flags[V] == 0b0) | + (((pte_flags[W] == 0b1) & (pte_flags[R] == 0b0)) & not(is_ss_pte(pte_flags))) // ---------------- // Check access permissions in PTE @@ -64,8 +69,26 @@ function pte_is_invalid(pte_flags : PTE_Flags) -> bool = (pte_flags[V] == 0b0) // in ext_ptw. It should return the updated ext_ptw in both success and failure cases. union PTE_Check = { - PTE_Check_Success : ext_ptw, - PTE_Check_Failure : (ext_ptw, ext_ptw_fail) + PTE_Check_Success : ext_ptw, + PTE_Check_Failure_Permission : (ext_ptw, ext_ptw_fail), + PTE_Check_Failure_No_Access : (ext_ptw, ext_ptw_fail) +} + +// Zicfiss: access-fault conditions +function is_read_only_pte(p : PTE_Flags) -> bool = + (p[R] == 0b1 & p[W] == 0b0 & p[X] == 0b0) +function is_shadow_stack_pte_access_fault(ac : AccessType(ext_access_type), + p : PTE_Flags) -> bool = { + match (haveZicfiss(), ac) { + (false, _) => false, + (_, Read(_)) => false, + (_, SSRead(_)) => not(is_ss_pte(p)) & not(is_read_only_pte(p)), + (_, Write(_)) => is_ss_pte(p), + (_, SSWrite(_)) => not(is_ss_pte(p)) & not(is_read_only_pte(p)), + (_, ReadWrite(_, _)) => is_ss_pte(p), + (_, SSReadWrite(_, _)) => not(is_ss_pte(p)) & not(is_read_only_pte(p)), + (_, Execute()) => is_ss_pte(p) + } } // PRIVATE @@ -76,33 +99,44 @@ function check_PTE_permission(ac : AccessType(ext_access_type), pte_flags : PTE_Flags, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = { - let pte_U = pte_flags[U]; - let pte_R = pte_flags[R]; - let pte_W = pte_flags[W]; - let pte_X = pte_flags[X]; - let success : bool = - match (ac, priv) { - (Read(_), User) => (pte_U == 0b1) - & ((pte_R == 0b1) - | ((pte_X == 0b1 & mxr))), - (Write(_), User) => (pte_U == 0b1) & (pte_W == 0b1), - (ReadWrite(_, _), User) => (pte_U == 0b1) - & (pte_W == 0b1) - & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), - (Execute(), User) => (pte_U == 0b1) & (pte_X == 0b1), - (Read(_), Supervisor) => ((pte_U == 0b0) | do_sum) - & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), - (Write(_), Supervisor) => ((pte_U == 0b0) | do_sum) - & (pte_W == 0b1), - (ReadWrite(_, _), Supervisor) => ((pte_U == 0b0) | do_sum) - & (pte_W == 0b1) - & ((pte_R == 0b1) - | ((pte_X == 0b1) & mxr)), - (Execute(), Supervisor) => (pte_U == 0b0) & (pte_X == 0b1), - (_, Machine) => internal_error(__FILE__, __LINE__, - "m-mode mem perm check")}; - if success then PTE_Check_Success(()) - else PTE_Check_Failure((), ()) + if is_shadow_stack_pte_access_fault(ac, pte_flags) then { + PTE_Check_Failure_No_Access((), ()) + } else { + let pte_U = pte_flags[U]; + let pte_R = pte_flags[R]; + let pte_W = pte_flags[W]; + let pte_X = pte_flags[X]; + + let success : bool = + match (ac, priv) { + (Read(_), User) => (pte_U == 0b1) + & ((pte_R == 0b1) + | ((pte_X == 0b1 & mxr))), + (SSRead(_), User) => (pte_U == 0b1) & (pte_W == 0b1), + (Write(_), User) => (pte_U == 0b1) & (pte_W == 0b1), + (SSWrite(_), User) => (pte_U == 0b1) & (pte_W == 0b1), + (ReadWrite(_, _), User) => (pte_U == 0b1) + & (pte_W == 0b1) + & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), + (SSReadWrite(_), User) => (pte_U == 0b1) & (pte_W == 0b1), + (Execute(), User) => (pte_U == 0b1) & (pte_X == 0b1), + (Read(_), Supervisor) => ((pte_U == 0b0) | do_sum) + & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), + (SSRead(_), Supervisor) => ((pte_U == 0b0) | do_sum) & (pte_W == 0b1), + (Write(_), Supervisor) => ((pte_U == 0b0) | do_sum) + & (pte_W == 0b1), + (SSWrite(_), Supervisor) => ((pte_U == 0b0) | do_sum) & (pte_W == 0b1), + (ReadWrite(_, _), Supervisor) => ((pte_U == 0b0) | do_sum) + & (pte_W == 0b1) + & ((pte_R == 0b1) + | ((pte_X == 0b1) & mxr)), + (SSReadWrite(_), Supervisor) => ((pte_U == 0b0) | do_sum) & (pte_W == 0b1), + (Execute(), Supervisor) => (pte_U == 0b0) & (pte_X == 0b1), + (_, Machine) => internal_error(__FILE__, __LINE__, + "m-mode mem perm check")}; + if success then PTE_Check_Success(()) + else PTE_Check_Failure_Permission((), ()) + } } // Update PTE bits if needed; return new PTE if updated @@ -116,10 +150,13 @@ function update_PTE_Bits(sv_params : SV_Params, // Update 'dirty' bit? let update_d : bool = (pte_flags[D] == 0b0) & (match a { - Execute() => false, - Read() => false, - Write(_) => true, - ReadWrite(_, _) => true + Execute() => false, + Read() => false, + SSRead() => false, + Write(_) => true, + SSWrite(_) => true, + ReadWrite(_, _) => true, + SSReadWrite(_, _) => true }); // Update 'accessed'-bit? let update_a = (pte_flags[A] == 0b0); diff --git a/model/riscv_vmem_ptw.sail b/model/riscv_vmem_ptw.sail index 374aca0d8..94ddea35a 100644 --- a/model/riscv_vmem_ptw.sail +++ b/model/riscv_vmem_ptw.sail @@ -51,8 +51,9 @@ function ext_get_ptw_access_error(eptwf : ext_ptw_fail) -> PTW_Error = PTW_Access() /* conversion of these translation/PTW failures into architectural exceptions */ -function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> ExceptionType = { - let e : ExceptionType = +function translationException(a : AccessType(ext_access_type), + f : PTW_Error) + -> ExceptionType = { match (a, f) { (_, PTW_Ext_Error(e)) => E_Extension(ext_translate_exception(e)), (ReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(), diff --git a/model/riscv_vmem_types.sail b/model/riscv_vmem_types.sail index da1e053d6..3ff356e9a 100644 --- a/model/riscv_vmem_types.sail +++ b/model/riscv_vmem_types.sail @@ -20,7 +20,11 @@ function accessType_to_str (a) = Read(_) => "R", Write(_) => "W", ReadWrite(_, _) => "RW", - Execute() => "X" + Execute() => "X", + // Zicfiss: shadow stack read and writes + SSRead(_) => "SS_R", + SSWrite(_) => "SS_W", + SSReadWrite(_, _) => "SS_RW" } overload to_str = {accessType_to_str} From 7e9c7bf37e9dc0fa48643e065cd1500db396b91b Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sat, 16 Dec 2023 17:09:12 -0600 Subject: [PATCH 07/10] Update Makefile --- Makefile | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Makefile b/Makefile index af355efc1..fb655481f 100644 --- a/Makefile +++ b/Makefile @@ -48,6 +48,9 @@ SAIL_DEFAULT_INST += riscv_insts_zbkb.sail SAIL_DEFAULT_INST += riscv_insts_zbkx.sail SAIL_DEFAULT_INST += riscv_insts_zicond.sail +SAIL_DEFAULT_INST += riscv_insts_zimop.sail # Zimop instructions +SAIL_DEFAULT_INST += riscv_insts_zcmop.sail # Zcmop instructions +SAIL_DEFAULT_INST += riscv_insts_zicfiss.sail # Zicfiss instructions SAIL_DEFAULT_INST += riscv_insts_vext_utils.sail SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail @@ -72,6 +75,7 @@ SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exceptio SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail +SAIL_SYS_SRCS += riscv_zicfiss_control.sail # Zicfiss CSRs SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling @@ -96,6 +100,7 @@ PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metada SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail +SAIL_REGS_SRCS += riscv_zicfiss_regs.sail # Zicfiss state SAIL_REGS_SRCS += riscv_ext_regs.sail $(SAIL_CHECK_SRCS) SAIL_REGS_SRCS += riscv_vreg_type.sail riscv_vext_regs.sail From 725c2867b6c7e9f99e161a8204831513ad6e784e Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sun, 17 Dec 2023 07:41:14 -0600 Subject: [PATCH 08/10] Add extension hooks to zimop and zcmop - Some zimop and zcmop codepoints may be used by extensions such as Zicfiss. Add generic infrastructure to support this. --- model/riscv_insts_zcmop.sail | 21 +++++++++++++++-- model/riscv_insts_zimop.sail | 44 +++++++++++++++++++++++++++++++----- 2 files changed, 57 insertions(+), 8 deletions(-) diff --git a/model/riscv_insts_zcmop.sail b/model/riscv_insts_zcmop.sail index 7e4529c3a..4df15c8ac 100644 --- a/model/riscv_insts_zcmop.sail +++ b/model/riscv_insts_zcmop.sail @@ -76,10 +76,25 @@ * the fetch-execute logic. */ /* ****************************************************************** */ +/* Zcmops may be redefined by other extensions */ +function is_ext_defined_cmop(mop : bits(3)) -> bool = { + /* Zicfiss uses the following cmop codepoints: + * mop.rr.7 rd=x0, rs2=x1/x5, rs1=x0 => sspush rs2 + * c.mop.1 => c.sspush x1 + * c.mop.5 => c.sspopchk x5 + */ + match mop { + 0b000 => haveZicfiss(), + 0b010 => haveZicfiss(), + _ => false + } +} union clause ast = ZCMOP : (bits(3)) -mapping clause encdec_compressed = ZCMOP(mop) if haveZcmop() - <-> 0b01100 @ mop : bits(3) @ 0b100000 @ 0b01 if haveZcmop() +mapping clause encdec_compressed = ZCMOP(mop) + if haveZcmop() & not(is_ext_defined_cmop(mop)) + <-> 0b01100 @ mop : bits(3) @ 0b100000 @ 0b01 + if haveZcmop() & not(is_ext_defined_cmop(mop)) mapping zcmop_mnemonic : bits(3) <-> string = { 0b000 <-> "c.mop.1", @@ -93,7 +108,9 @@ mapping zcmop_mnemonic : bits(3) <-> string = { } mapping clause assembly = ZCMOP(mop) + if haveZcmop() & not(is_ext_defined_cmop(mop)) <-> zcmop_mnemonic(mop) + if haveZcmop() & not(is_ext_defined_cmop(mop)) function clause execute ZCMOP(mop) = { RETIRE_SUCCESS diff --git a/model/riscv_insts_zimop.sail b/model/riscv_insts_zimop.sail index 66c0857e3..68f837a89 100644 --- a/model/riscv_insts_zimop.sail +++ b/model/riscv_insts_zimop.sail @@ -76,11 +76,39 @@ union clause ast = ZIMOP_MOP_R : (bits(5), regidx, regidx) union clause ast = ZIMOP_MOP_RR : (bits(3), regidx, regidx, regidx) -mapping clause encdec = ZIMOP_MOP_R(mop_30 @ mop_27_26 @ mop_21_20, rs1, rd) if haveZimop() - <-> 0b1 @ mop_30 : bits(1) @ 0b00 @ mop_27_26 : bits(2) @ 0b0111 @ mop_21_20 : bits(2) @ rs1 @ 0b100 @ rd @ 0b1110011 if haveZimop() - -mapping clause encdec = ZIMOP_MOP_RR(mop_30 @ mop_27_26, rs2, rs1, rd) if haveZimop() - <-> 0b1 @ mop_30 : bits(1) @ 0b00 @ mop_27_26 : bits(2) @ 0b1 @ rs2 @ rs1 @ 0b100 @ rd @ 0b1110011 if haveZimop() +/* Zimops mop.r may be redefined by other extensions */ +function is_ext_defined_mop_r(mop : bits(5), rs1 : regidx, rd: regidx) -> bool = { + /* Zicfiss uses the following mop.r.28 codepoints: + * mop.r.28 rd=x0, rs1=x1/x5 => sspopchk rs1 + * mop.r.28 rd!=x0, rs1=x0 => ssrdp rd + */ + match (mop, rs1, rd) { + (0b11100, 0b00001, 0b00000) => haveZicfiss(), + (0b11100, 0b00101, 0b00000) => haveZicfiss(), + (0b11100, 0b00000, _) if rd == zreg => false, + (0b11100, 0b00000, _) if rd != zreg => haveZicfiss(), + (_, _, _) => false + } +} +/* Zimops mop.rr may be redefined by other extensions */ +function is_ext_defined_mop_rr(mop : bits(3), rs2 : regidx, rs1 : regidx, rd: regidx) -> bool = { + /* Zicfiss uses the following mop.rr.7 codepoints: + * mop.rr.7 rd=x0, rs2=x1/x5, rs1=x0 => sspush rs2 + */ + match (mop, rs2, rs1, rd) { + (0b111, 0b00001, 0b00000, 0b00000) => haveZicfiss(), + (0b111, 0b00101, 0b00000, 0b00000) => haveZicfiss(), + (_, _, _, _) => false + } +} +mapping clause encdec = ZIMOP_MOP_R(mop_30 @ mop_27_26 @ mop_21_20, rs1, rd) + if haveZimop() & not(is_ext_defined_mop_r(mop_30 @ mop_27_26 @ mop_21_20, rs1, rd)) + <-> 0b1 @ mop_30 : bits(1) @ 0b00 @ mop_27_26 : bits(2) @ 0b0111 @ mop_21_20 : bits(2) @ rs1 @ 0b100 @ rd @ 0b1110011 + if haveZimop() & not(is_ext_defined_mop_r(mop_30 @ mop_27_26 @ mop_21_20, rs1, rd)) +mapping clause encdec = ZIMOP_MOP_RR(mop_30 @ mop_27_26, rs2, rs1, rd) + if haveZimop() & not(is_ext_defined_mop_rr(mop_30 @ mop_27_26, rs2, rs1, rd)) + <-> 0b1 @ mop_30 : bits(1) @ 0b00 @ mop_27_26 : bits(2) @ 0b1 @ rs2 @ rs1 @ 0b100 @ rd @ 0b1110011 + if haveZimop() & not(is_ext_defined_mop_rr(mop_30 @ mop_27_26, rs2, rs1, rd)) mapping zimop_r_mnemonic : bits(5) <-> string = { 0b00000 <-> "mop.r.0", @@ -129,10 +157,14 @@ mapping zimop_rr_mnemonic : bits(3) <-> string = { } mapping clause assembly = ZIMOP_MOP_R(mop, rs1, rd) - <-> zimop_r_mnemonic(mop) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) + if haveZimop() & not(is_ext_defined_mop_r(mop, rs1, rd)) + <-> zimop_r_mnemonic(mop) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) + if haveZimop() & not(is_ext_defined_mop_r(mop, rs1, rd)) mapping clause assembly = ZIMOP_MOP_RR(mop, rs2, rs1, rd) + if haveZimop() & not(is_ext_defined_mop_rr(mop, rs2, rs1, rd)) <-> zimop_rr_mnemonic(mop) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + if haveZimop() & not(is_ext_defined_mop_rr(mop, rs2, rs1, rd)) function clause execute ZIMOP_MOP_R(mop, rs1, rd) = { X(rd) = zeros(); From bb9e337a14ae819b78f1096868e191d91faa58d7 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sun, 17 Dec 2023 07:41:33 -0600 Subject: [PATCH 09/10] Add Zicfiss instructions - Add sspush/sspopchk/ssrdp/ssamoswap - Add c_sspush/c_sspopchk --- model/riscv_insts_zicfiss.sail | 356 +++++++++++++++++++++++++++++++++ 1 file changed, 356 insertions(+) create mode 100644 model/riscv_insts_zicfiss.sail diff --git a/model/riscv_insts_zicfiss.sail b/model/riscv_insts_zicfiss.sail new file mode 100644 index 000000000..32a0e32f5 --- /dev/null +++ b/model/riscv_insts_zicfiss.sail @@ -0,0 +1,356 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Ved Shanbhogue */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + +/* ****************************************************************** */ +/* This file specifies the instructions in the 'Zicfiss' extension. */ +/* ****************************************************************** */ +/* Backward-edge CFI: Shadow stack */ + +/* Sail does not yet support H extension - this needs to be updated to + support henvcfg for VS when H extension support is included */ +function zicfiss_xSSE(priv : Privilege) -> bool = { + /* When S-mode is implemented + * Priv xSSE + * M 0 + * S/HS menvcfg.SSE + * VS henvcfg.SSE + * U/VU senvcfg.SSE + * When S-mode is not implemented xSSE is 0 + */ + if priv == Machine + then false + else if priv == Supervisor + then menvcfg[SSE] == 0b1 + else if haveSupMode() + then senvcfg.SSE() == 0b1 + else false +} + +function is_shadow_stack_PTE_enable() -> bool = + zicfiss_xSSE(effectivePrivilege(SSWrite(Data), mstatus, cur_privilege)) + +/* ****************************************************************** */ +/* SSPUSH and C.SSPUSH operation + * if (xSSE == 1) + * mem[ssp - (XLEN/8)] = X(src) + * ssp = ssp - (XLEN/8) + * endif + */ +/* ****************************************************************** */ +union clause ast = SSPUSH : (regidx) +mapping clause encdec = SSPUSH(rs2) + if haveZicfiss() & (rs2 == 0b00001 | rs2 == 0b00101) + <-> 0b1100111 @ rs2 @ 0b00000 @ 0b100 @ 0b00000 @ 0b1110011 + if haveZicfiss() & (rs2 == 0b00001 | rs2 == 0b00101) +mapping clause assembly = SSPUSH(rs2) + if haveZicfiss() & (rs2 == 0b00001 | rs2 == 0b00101) + <-> "sspush" ^ spc() ^ reg_name(rs2) + if haveZicfiss() & (rs2 == 0b00001 | rs2 == 0b00101) +union clause ast = C_SSPUSH : (regidx) +mapping clause encdec_compressed = C_SSPUSH(0b00001) if haveZicfiss() + <-> 0b0110000010000001 if haveZicfiss() +mapping clause assembly = C_SSPUSH(rs2) + if haveZicfiss() + <-> "c.sspush" ^ spc() ^ reg_name(rs2) + if haveZicfiss() +/* ****************************************************************** */ +function clause execute SSPUSH(rs2) = { + let width : word_width = match sizeof(xlen) { + 32 => WORD, + 64 => DOUBLE, + _ => internal_error(__FILE__, __LINE__, "Unexpected xlen width") + }; + + if not(zicfiss_xSSE(cur_privilege)) + then {RETIRE_SUCCESS} + else { + let vaddr : xlenbits = match sizeof(xlen) { + 32 => ssp - 4, + 64 => ssp - 8, + _ => internal_error(__FILE__, __LINE__, "Unexpected xlen width") + }; + let aligned : bool = match width { + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000, + _ => internal_error(__FILE__, __LINE__, "Unexpected xlen width") + }; + if not(aligned) + then { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL } + else { + match translateAddr(vaddr, SSWrite(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let eares : MemoryOpResult(unit) = match width { + WORD => mem_write_ea(addr, 4, false, false, false), + DOUBLE => mem_write_ea(addr, 8, false, false, false), + _ => internal_error(__FILE__, __LINE__, "unexpected width") + }; + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + rs2_val = X(rs2); + let res : MemoryOpResult(bool) = match sizeof(xlen) { + 32 => mem_write_value(addr, 4, rs2_val, false, false, false), + 64 => mem_write_value(addr, 8, rs2_val, false, false, false), + _ => internal_error(__FILE__, __LINE__, "unexpected width") + }; + match res { + MemValue(true) => { ssp = vaddr; RETIRE_SUCCESS }, + MemValue(false) => internal_error(__FILE__, __LINE__, "sspush got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + }; + } + } + } + } + } + } +} +function clause execute (C_SSPUSH(rs2)) = execute(SSPUSH(rs2)) + +/* ****************************************************************** */ +/* SSPOPCHK and C.SSPOPCHK operation + * if (xSSE == 1) + * temp = mem[ssp] + * if temp != X(src) then software-check exception + * else ssp = ssp + (XLEN/8) + * endif + * SSPOPCHK requires write permission as shadow stacks are encoded as + * pte.xwr = 010b + */ +/* ****************************************************************** */ +union clause ast = SSPOPCHK : (regidx) +mapping clause encdec = SSPOPCHK(rs1) + if haveZicfiss() & (rs1 == 0b00001 | rs1 == 0b00101) + <-> 0b110011011100 @ rs1 @ 0b100 @ 0b00000 @ 0b1110011 + if haveZicfiss() & (rs1 == 0b00001 | rs1 == 0b00101) +mapping clause assembly = SSPOPCHK(rs1) + if haveZicfiss() & (rs1 == 0b00001 | rs1 == 0b00101) + <-> "sspopchk" ^ spc() ^ reg_name(rs1) + if haveZicfiss() & (rs1 == 0b00001 | rs1 == 0b00101) +union clause ast = C_SSPOPCHK : (regidx) +mapping clause encdec_compressed = C_SSPOPCHK(0b00101) + if haveZicfiss() + <-> 0b0110001010000001 + if haveZicfiss() +mapping clause assembly = C_SSPOPCHK(rs1) + if haveZicfiss() + <-> "c.sspopchk" ^ spc() ^ reg_name(rs1) + if haveZicfiss() +/* ****************************************************************** */ +function clause execute SSPOPCHK(rs1) = { + let width : word_width = match sizeof(xlen) { + 32 => WORD, + 64 => DOUBLE, + _ => internal_error(__FILE__, __LINE__, "Unexpected xlen width") + }; + let new_ssp : xlenbits = match sizeof(xlen) { + 32 => ssp + 4, + 64 => ssp + 8, + _ => internal_error(__FILE__, __LINE__, "Unexpected xlen width") + }; + if not(zicfiss_xSSE(cur_privilege)) + then {RETIRE_SUCCESS} + else { + let vaddr : xlenbits = ssp; + let aligned : bool = match width { + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000, + _ => internal_error(__FILE__, __LINE__, "Unexpected xlen width") + }; + if not(aligned) + then { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL } + else match translateAddr(vaddr, SSWrite(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let mval : MemoryOpResult(xlenbits) = match sizeof(xlen) { + 32 => mem_read(SSRead(Data), addr, 4, false, false, false), + 64 => mem_read(SSRead(Data), addr, 8, false, false, false), + _ => internal_error(__FILE__, __LINE__, "Unexpected xlen width") + }; + match (mval) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(loaded) => { + if X(rs1) != loaded + then { handle_sw_check_exception(SHADOW_STACK_FAULT); RETIRE_FAIL } + else { ssp = new_ssp; RETIRE_SUCCESS } + } + } + } + } + } +} +function clause execute (C_SSPOPCHK(rs1)) = execute(SSPOPCHK(rs1)) + +/* ****************************************************************** */ +/* SSRDP operation: + * X(rd) = (xSSE == 1) ? ssp : 0 + */ +/* ****************************************************************** */ +union clause ast = SSRDP : (regidx) +mapping clause encdec = SSRDP(rd) + if haveZicfiss() & rd != zreg + <-> 0b110011011100 @ 0b00000 @ 0b100 @ rd @ 0b1110011 + if haveZicfiss() & rd != zreg +mapping clause assembly = SSRDP(rd) + if haveZicfiss() & rd != zreg + <-> "ssrdp" ^ spc() ^ reg_name(rd) + if haveZicfiss() & rd != zreg +/* ****************************************************************** */ +function clause execute SSRDP(rd) = { + if zicfiss_xSSE(cur_privilege) + then { X(rd) = ssp } + else { X(rd) = X(0) }; + RETIRE_SUCCESS +} +/* ****************************************************************** */ +/* SSAMOSWAP operation: + * if privilege_mode != M && menvcfg.SSE == 0 + * raise illegal-instruction exception + * if S-mode is not implemented + * raise illegal-instruction exception + * else if privilege_mode == U && senvcfg.SSE == 0 + * raise illegal-instruction exception + * else if privilege_mode == VS && henvcfg.SSE == 0 + * raise virtual instruction exception + * else if privilege_mode == VU && senvcfg.SSE == 0 + * raise virtual instruction exception + * else + * X(rd) = mem[X(rs1)] + * mem[X(rs1)] = X(rs2) + * endif + * + * The model does not presently support H extension. The + * parts of algorithm dealing with VS and VU should be + * introduced when H extension is introduced. + */ +/* ****************************************************************** */ +function ssamoswap_width_valid(size : word_width) -> bool = { + match(size) { + WORD => true, + DOUBLE => sizeof(xlen) >= 64, + _ => false + } +} +union clause ast = SSAMOSWAP : (bool, bool, regidx, regidx, word_width, regidx) +mapping clause encdec = SSAMOSWAP(aq, rl, rs2, rs1, size, rd) + if haveZicfiss() & ssamoswap_width_valid(size) + <-> 0b01001 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 + if haveZicfiss() & ssamoswap_width_valid(size) +mapping clause assembly = SSAMOSWAP(aq, rl, rs2, rs1, size, rd) + if haveZicfiss() & ssamoswap_width_valid(size) + <-> "ssamoswap" ^ "." ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() + ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")" + if haveZicfiss() & ssamoswap_width_valid(size) +/* ****************************************************************** */ +function clause execute (SSAMOSWAP(aq, rl, rs2, rs1, width, rd)) = { + let width_bytes = size_bytes(width); + + assert(width_bytes <= sizeof(xlen_bytes)); + + if cur_privilege != Machine & menvcfg[SSE] == 0b0 + then { handle_illegal(); RETIRE_FAIL } + else if not(haveSupMode()) + then { handle_illegal(); RETIRE_FAIL } + else if cur_privilege == User & senvcfg[SSE] == 0b0 + then { handle_illegal(); RETIRE_FAIL } + else { + match ext_data_get_addr(rs1, zeros(), SSReadWrite(Data, Data), width_bytes) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + if not(is_aligned(vaddr, width)) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr, SSReadWrite(Data, Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true); + let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0]; + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + match mem_read(SSReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(loaded) => { + match mem_write_value(addr, width_bytes, sign_extend(rs2_val), aq & rl, rl, true) { + MemValue(true) => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS }, + MemValue(false) => { internal_error(__FILE__, __LINE__, "SSAMOSWAP got false from mem_write_value") }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + } + } + } + } + } + } + } + } + } + } +} From 161506364fe6d548ef7c9af8caa66e19a7eab890 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Wed, 7 Feb 2024 14:42:09 -0600 Subject: [PATCH 10/10] update to new bitfield syntax --- model/riscv_insts_zicfiss.sail | 2 +- model/riscv_sys_regs.sail | 2 +- model/riscv_zicfiss_control.sail | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/model/riscv_insts_zicfiss.sail b/model/riscv_insts_zicfiss.sail index 32a0e32f5..60bd7ee78 100644 --- a/model/riscv_insts_zicfiss.sail +++ b/model/riscv_insts_zicfiss.sail @@ -90,7 +90,7 @@ function zicfiss_xSSE(priv : Privilege) -> bool = { else if priv == Supervisor then menvcfg[SSE] == 0b1 else if haveSupMode() - then senvcfg.SSE() == 0b1 + then senvcfg[SSE] == 0b1 else false } diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 3addb2d20..ad467386c 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -860,7 +860,7 @@ function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = { let v = Mk_SEnvcfg(v); let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; // Zicfiss - SSE: shadow stack enable - is ROZ in senvcfg if menvcfg.SSE is 0 - let o = update_SSE(o, if haveZicfiss() & menvcfg.SSE() == 0b1 then v.SSE() else 0b0); + let o = [o with SSE = if haveZicfiss() & menvcfg[SSE] == 0b1 then v[SSE] else 0b0]; // Other extensions are not implemented yet so all other fields are read only zero. o } diff --git a/model/riscv_zicfiss_control.sail b/model/riscv_zicfiss_control.sail index 6baae058d..f153391ea 100644 --- a/model/riscv_zicfiss_control.sail +++ b/model/riscv_zicfiss_control.sail @@ -90,7 +90,7 @@ function clause ext_is_CSR_defined(0x011, priv) = { // ssp else if priv == Supervisor then menvcfg[SSE] == 0b1 else if haveSupMode() - then senvcfg.SSE() == 0b1 + then senvcfg[SSE] == 0b1 else false } function clause ext_read_CSR(0x011) = Some(ssp) @@ -101,7 +101,7 @@ function clause ext_write_CSR(0x011, value) = { * Sail model does not support dynamic switching of UXL/SXL so that is * not considered in the following algorithm yet. */ - if ( architecture(misa.MXL()) == Some(RV64) ) then + if ( architecture(misa[MXL]) == Some(RV64) ) then ssp[2 .. 2] = 0b0; Some(ssp); }