From 748282ee2f2ad02ee968922707f9a1745699a652 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Sun, 19 Nov 2023 16:49:42 -0600 Subject: [PATCH] add zicfilp extensions --- Makefile | 5 + model/riscv_csr_map.sail | 2 + model/riscv_ext_regs.sail | 5 +- model/riscv_insts_zicfilp.sail | 179 +++++++++++++++++++++++++++++++++ model/riscv_insts_zicsr.sail | 18 ++-- model/riscv_step_ext.sail | 7 +- model/riscv_step_rvfi.sail | 7 +- model/riscv_step_zicfilp.sail | 117 +++++++++++++++++++++ model/riscv_sys_control.sail | 3 + model/riscv_sys_regs.sail | 83 ++++++++++++++- model/riscv_zicfilp_regs.sail | 111 ++++++++++++++++++++ 11 files changed, 523 insertions(+), 14 deletions(-) create mode 100644 model/riscv_insts_zicfilp.sail create mode 100644 model/riscv_step_zicfilp.sail create mode 100644 model/riscv_zicfilp_regs.sail diff --git a/Makefile b/Makefile index 9140065bd..32cb03206 100644 --- a/Makefile +++ b/Makefile @@ -42,6 +42,9 @@ SAIL_DEFAULT_INST += riscv_insts_zbkx.sail SAIL_DEFAULT_INST += riscv_insts_zicond.sail +SAIL_DEFAULT_INST += riscv_zicfilp_regs.sail # Zicfilp state +SAIL_DEFAULT_INST += riscv_insts_zicfilp.sail # Zicfilp instructions + SAIL_DEFAULT_INST += riscv_insts_vext_utils.sail SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail SAIL_DEFAULT_INST += riscv_insts_vext_arith.sail @@ -95,6 +98,8 @@ SAIL_ARCH_SRCS += riscv_types_kext.sail # Shared/common code for the cryptogr SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail +SAIL_STEP_SRCS += riscv_step_zicfilp.sail +RVFI_STEP_SRCS += riscv_step_zicfilp.sail # Control inclusion of 64-bit only riscv_analysis ifeq ($(ARCH),RV32) diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index da68556f0..0abd5eae3 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -159,6 +159,8 @@ mapping clause csr_name_map = 0xB00 <-> "mcycle" mapping clause csr_name_map = 0xB02 <-> "minstret" mapping clause csr_name_map = 0xB80 <-> "mcycleh" mapping clause csr_name_map = 0xB82 <-> "minstreth" +/* machine security configuration */ +mapping clause csr_name_map = 0x747 <-> "mseccfg" /* TODO: other hpm counters and events */ /* trigger/debug */ mapping clause csr_name_map = 0x7a0 <-> "tselect" diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail index 8568e6a39..1452e3698 100644 --- a/model/riscv_ext_regs.sail +++ b/model/riscv_ext_regs.sail @@ -80,9 +80,12 @@ This function is called after above when running rvfi and allows the model to be initialised differently (e.g. CHERI cap regs are initialised to omnipotent instead of null). */ +val init_zicfilp_regs : unit -> unit val ext_rvfi_init : unit -> unit function ext_rvfi_init () = { - x1 = x1 // to avoid hook being optimized out + x1 = x1; // to avoid hook being optimized out + /* Zicfilp register state */ + init_zicfilp_regs(); } diff --git a/model/riscv_insts_zicfilp.sail b/model/riscv_insts_zicfilp.sail new file mode 100644 index 000000000..35b5bbad9 --- /dev/null +++ b/model/riscv_insts_zicfilp.sail @@ -0,0 +1,179 @@ +/*=======================================================================================*/ +/* 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 */ +/* Ved Shanbhogue */ +/* */ +/* 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 'Zicfilp' extension. */ +/* ****************************************************************** */ +/* Forward-edge CFI: Landing pads */ +/* Sail does not yet support H extension - this needs to be updated to + support henvcfg for VS when H extension support is included */ +function zicfilp_xLPE() -> bool = { + /* When S-mode is implemented + * Priv xLPE + * M mseccfg.MLPE + * S/HS menvcfg.LPE + * VS henvcfg.LPE + * U/VU senvcfg.LPE + * When S-mode is not implemented + * Priv xLPE + * M mseccfg.MLPE + * U menvcfg.LPE + */ + if not(haveZicfilp()) + then false + else if cur_privilege == Machine + then mseccfg.MLPE() == 0b1 + else if cur_privilege == Supervisor + then menvcfg.LPE() == 0b1 + else if not(haveSupMode()) + then menvcfg.LPE() == 0b1 + else senvcfg.LPE() == 0b1 +} +/* extension to jalr */ +function zicfilp_update_elp(rs1_reg : regidx, rd_reg : regidx) -> unit = { + /* + * An indirect branch using JALR, C.JALR, or C.JR with rs1 as x7 is termed + * a software guarded branch. Such branches do not need to land on a LPAD + * instruction and thus do not set ELP to LP_EXPECTED. JALR/C.JR/C.JALR + * using x1/x5 as source are returns; they do not set ELP to LP_EXPECTED. + * + * is_lp_expected = ( (JALR || C.JR || C.JALR) && + * (rs1 != x1) && (rs1 != x5) && (rs1 != x7) ) ? 1 : 0; + */ + let is_lp_expected : bool = ((rs1_reg != 0b00001) & (rs1_reg != 0b00101) & + (rs1_reg != 0b00111)); + if is_lp_expected == true & zicfilp_xLPE() + then elp = ElpState_to_bits(LP_EXPECTED); + +} +/* AUIPC with rd=x0 is a lpad instruction when zicfilp is active else a no-op */ +function zicfilp_lpad( lpl : bits(20) ) -> Retired = { + /* expected label is in x7 bits 31:12 */ + let exp_lbl : bits(20) = x7[31..12]; + + if zicfilp_xLPE() & (elp == ElpState_to_bits(LP_EXPECTED)) then { + if ( (lpl != exp_lbl) & (lpl != 0b00000000000000000000) ) + then { handle_sw_check_exception(LANDING_PAD_FAULT); RETIRE_FAIL } + else {elp = ElpState_to_bits(NO_LP_EXPECTED); RETIRE_SUCCESS }; + } else { + RETIRE_SUCCESS + } +} +/* trap delivery extension */ +function zicfilp_trap_extension(del_priv : Privilege) -> unit = { + /* When a trap is taken into privilege mode x, the xPELP is set + to ELP and ELP is set to NO_LP_EXPECTED. */ + /* Sail does not have support for Debug mode - this needs to be + updated when Debug mode support is added */ + if haveZicfilp() then { + match (del_priv, sizeof(xlen)) { + (Machine, 32 ) => {mstatush = update_MPELP(mstatush, elp)}, + (Machine, _ ) => {mstatus = update_mstatus_MPELP(mstatus, elp)}, + ( _, _ ) => {mstatus = update_SPELP(mstatus, elp)}, + }; + elp = ElpState_to_bits(NO_LP_EXPECTED); + } +} +/* extension to MRET */ +function zicfilp_set_elp_to_mpelp() -> unit = { + /* An MRET or SRET instruction is used to return from a trap in M-mode + * or S-mode, respectively. When executing an xRET instruction, if xPP + * holds the value y, then ELP is set to the value of xPELP if yLPE is + * 1; otherwise, it is set to NO_LP_EXPECTED; xPELP is set to + * NO_LP_EXPECTED. + */ + if haveZicfilp() then { + match zicfilp_xLPE() { + true => { elp = get_MPELP() }, + false => { elp = ElpState_to_bits(NO_LP_EXPECTED) } + }; + match (sizeof(xlen)) { + 32 => {mstatush = update_MPELP(mstatush, ElpState_to_bits(NO_LP_EXPECTED))}, + _ => {mstatus = update_mstatus_MPELP(mstatus, ElpState_to_bits(NO_LP_EXPECTED))} + }; + } +} +/* extension to SRET */ +function zicfilp_set_elp_to_spelp() -> unit = { + /* An MRET or SRET instruction is used to return from a trap in M-mode + * or S-mode, respectively. When executing an xRET instruction, if xPP + * holds the value y, then ELP is set to the value of xPELP if yLPE is + * 1; otherwise, it is set to NO_LP_EXPECTED; xPELP is set to + * NO_LP_EXPECTED. + */ + if haveZicfilp() then { + match zicfilp_xLPE() { + true => { elp = mstatus.SPELP() }, + false => { elp = ElpState_to_bits(NO_LP_EXPECTED) } + }; + mstatus = update_SPELP(mstatus, ElpState_to_bits(NO_LP_EXPECTED)); + } +} diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 8953ad4b3..9b2c488f0 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -131,6 +131,9 @@ function readCSR csr : csreg -> xlenbits = { (0x3BE, _) => pmpaddr14, (0x3BF, _) => pmpaddr15, + (0x747, _) => mseccfg.bits()[(sizeof(xlen) - 1) .. 0], // mseccfg + (0x757, 32) => mseccfg.bits()[63 .. 32], // mseccfgh + /* machine mode counters */ (0xB00, _) => mcycle[(sizeof(xlen) - 1) .. 0], (0xB02, _) => minstret[(sizeof(xlen) - 1) .. 0], @@ -156,7 +159,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(), @@ -198,10 +201,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) }, (0x305, _) => { Some(set_mtvec(value)) }, (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits())) }, - (0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) }, - (0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits()) }, - (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now - (0x31A, 32) => { menvcfg = legalize_envcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) }, + (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) }, + (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits()) }, + (0x310, 32) => { mstatush = legalize_mstatush(mstatush, value); Some(mstatush.bits())}, + (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) }, (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits())) }, (0x340, _) => { mscratch = value; Some(mscratch) }, (0x341, _) => { Some(set_xret_target(Machine, value)) }, @@ -232,6 +235,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x3BE, _) => { pmpaddr14 = pmpWriteAddr(pmpLocked(pmp14cfg), pmpTORLocked(pmp15cfg), pmpaddr14, value); Some(pmpaddr14) }, (0x3BF, _) => { pmpaddr15 = pmpWriteAddr(pmpLocked(pmp15cfg), false, pmpaddr15, value); Some(pmpaddr15) }, + (0x747, _) => { mseccfg = legalize_mseccfg(mseccfg, value); Some(mseccfg.bits()[sizeof(xlen) - 1 .. 0]) }, + (0x757, 32) => { mseccfg = legalize_mseccfg_high(mseccfg, value); Some(mseccfg.bits()[63 .. 32]) }, + /* machine mode counters */ (0xB00, _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) }, (0xB02, _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_increment = false; Some(value) }, @@ -248,7 +254,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, (0x105, _) => { Some(set_stvec(value)) }, (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits())) }, - (0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) }, + (0x10A, _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) }, (0x140, _) => { sscratch = value; Some(sscratch) }, (0x141, _) => { Some(set_xret_target(Supervisor, value)) }, (0x142, _) => { scause->bits() = value; Some(scause.bits()) }, diff --git a/model/riscv_step_ext.sail b/model/riscv_step_ext.sail index 2232c72b7..8fc93e4c8 100644 --- a/model/riscv_step_ext.sail +++ b/model/riscv_step_ext.sail @@ -70,9 +70,14 @@ /* The default implementation of hooks for the step() and main() functions. */ +/* Zicfilp extension to fetch */ +val zicfilp_check_if_lpad : (FetchResult) -> FetchResult + function ext_init() -> unit = () -function ext_fetch_hook(f : FetchResult) -> FetchResult = f +function ext_fetch_hook(f : FetchResult) -> FetchResult = { + zicfilp_check_if_lpad(f) +} function ext_pre_step_hook() -> unit = () function ext_post_step_hook() -> unit = () diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail index d23a679d7..b46de8522 100644 --- a/model/riscv_step_rvfi.sail +++ b/model/riscv_step_rvfi.sail @@ -68,9 +68,14 @@ /* SUCH DAMAGE. */ /*=======================================================================================*/ +/* Zicfilp extension to fetch */ +val zicfilp_check_if_lpad : (FetchResult) -> FetchResult + /* Step hooks for rvfi. */ -function ext_fetch_hook(f : FetchResult) -> FetchResult = f +function ext_fetch_hook(f : FetchResult) -> FetchResult = { + zicfilp_check_if_lpad(f) +} function ext_pre_step_hook() -> unit = () diff --git a/model/riscv_step_zicfilp.sail b/model/riscv_step_zicfilp.sail new file mode 100644 index 000000000..970a26f27 --- /dev/null +++ b/model/riscv_step_zicfilp.sail @@ -0,0 +1,117 @@ +/*=======================================================================================*/ +/* 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 fetch extension in the 'Zicfilp' extension.*/ +/* ****************************************************************** */ +/* Forward-edge CFI: Landing pads */ +val zicfilp_xLPE : (unit) -> bool +function zicfilp_check_if_lpad(f : FetchResult) -> FetchResult = { + if not(zicfilp_xLPE()) + then f + else { + /* landing pad is a AUIPC with rd=x0 */ + /* When ELP is set to LP_EXPECTED, if the next instruction in + * the instruction stream is not 4-byte aligned, or is not LPAD, or + * if the landing pad label encoded in LPAD is not zero and does not + * match the expected landing pad label in bits 31:12 of the x7 + * register, then a software-check exception (cause=18) with xtval + * set to "landing pad fault (code=2)" is raised else the ELP is + * updated to NO_LP_EXPECTED. The label check is performed in + * riscv_insts_zicfilp:zicfilp_lpad + */ + match f { + F_Base(f) => { + let inst : word = zero_extend(f); + let lpad_op : bits(7) = inst[6 .. 0]; + let rd_reg : regidx = inst[11.. 7]; + if elp != ElpState_to_bits(LP_EXPECTED) + then F_Base(f) + else if PC[1 .. 0] != 0b00 + then F_Error(E_SW_Check_Fault(), zero_extend(sw_check_code_to_bits(LANDING_PAD_FAULT))) + else if ((lpad_op != 0b0010111) | (rd_reg != 0b00000)) + then F_Error(E_SW_Check_Fault(), zero_extend(sw_check_code_to_bits(LANDING_PAD_FAULT))) + else F_Base(f) + }, + F_RVC(f) => { + if (elp != ElpState_to_bits(LP_EXPECTED)) + then F_RVC(f) + else F_Error(E_SW_Check_Fault(), zero_extend(sw_check_code_to_bits(LANDING_PAD_FAULT))) + }, + F_Ext_Error(e) => { + f + }, + F_Error(e, addr) => { + f + } + } + } +} diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index b33d3ea5f..c5617fc11 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -134,6 +134,9 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = /* disabled trigger/debug module */ 0x7a0 => p == Machine, + /* Machine security configuration */ + 0x747 => p == Machine, + /* supervisor mode: trap setup */ 0x100 => haveSupMode() & (p == Machine | p == Supervisor), // sstatus 0x102 => haveSupMode() & haveNExt() & (p == Machine | p == Supervisor), // sedeleg diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index f472ca2b8..fbdc81b9b 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -215,18 +215,24 @@ function haveZmmul() -> bool = true /* Zicond extension support */ function haveZicond() -> bool = true +/* Zicfilp extension support */ +function haveZicfilp() -> bool = true + bitfield Mstatush : bits(32) = { + MPELP: 9, MBE : 5, SBE : 4 } register mstatush : Mstatush bitfield Mstatus : xlenbits = { + // The SD field does not exist in RV32 and is fixed to 0 SD : xlen - 1, - // The MBE and SBE fields are in mstatus in RV64 and absent in RV32. + // The MPELP, MBE and SBE fields are in mstatus in RV64 and absent in RV32. // On RV32, they are in mstatush, which doesn't exist in RV64. For now, // they are handled in an ad-hoc way. + // MPELP: 41, // MBE : 37 // SBE : 36 @@ -235,6 +241,7 @@ bitfield Mstatus : xlenbits = { // SXL : 35 .. 34, // UXL : 33 .. 32, + SPELP: 23, TSR : 22, TW : 21, TVM : 20, @@ -293,6 +300,17 @@ function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { Mk_Mstatus(m) } } +function legalize_mstatush(o : Mstatush, v : bits(32)) -> Mstatush = { + let v : Mstatush = Mk_Mstatush(v); + if haveZicfilp() then { + let mh = update_MPELP(o, v.MPELP()); + mh + } else o; + /* MBE and SBE writes are ignored - dynamic XLEN not supported */ +} + +/* function to update MPELP field in mstatus */ +val update_mstatus_MPELP : (Mstatus, bits(1)) -> Mstatus function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { /* @@ -300,7 +318,17 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { * that does not have a matching bitfield entry. All bits above 32 are handled * explicitly later. */ - let m : Mstatus = Mk_Mstatus(zero_extend(v[22 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0])); + let m : Mstatus = Mk_Mstatus(zero_extend(v[23 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0])); + + let m = if not(haveZicfilp()) then { + let m = update_SPELP(m, 0b0); + m + } else m; + /* Update MPELP if Zicfilp supported */ + let m = if haveZicfilp() & sizeof(xlen) == 64 then { + let m = update_mstatus_MPELP(m, v[41..41]); + m + } else m; /* We don't have any extension context yet. */ let m = update_XS(m, extStatus_to_bits(Off)); @@ -594,6 +622,7 @@ bitfield Sstatus : xlenbits = { // The UXL field does not exist on RV32, so we define an explicit // getter and setter below. // UXL : 30 .. 29, + SPELP: 23, MXR : 19, SUM : 18, XS : 16 .. 15, @@ -622,6 +651,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = { let s = Mk_Sstatus(zero_extend(0b0)); let s = update_SD(s, m.SD()); let s = set_sstatus_UXL(s, get_mstatus_UXL(m)); + let s = update_SPELP(s, m.SPELP()); let s = update_MXR(s, m.MXR()); let s = update_SUM(s, m.SUM()); let s = update_XS(s, m.XS()); @@ -636,6 +666,10 @@ function lower_mstatus(m : Mstatus) -> Sstatus = { } function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { + let m = if haveZicfilp() then { + let m = update_SPELP(m, s.SPELP()); + m + } else m; let m = update_MXR(m, s.MXR()); let m = update_SUM(m, s.SUM()); @@ -849,7 +883,7 @@ bitfield Envcfg : bits(64) = { // Page Based Memory Types Extension PBMTE : 62, // Reserved WPRI bits. - wpri_1 : 61 .. 8, + wpri_2 : 61 .. 8, // Cache Block Zero instruction Enable CBZE : 7, // Cache Block Clean and Flush instruction Enable @@ -857,7 +891,11 @@ bitfield Envcfg : bits(64) = { // Cache Block Invalidate instruction Enable CBIE : 5 .. 4, // Reserved WPRI bits. - wpri_0 : 3 .. 1, + wpri_1 : 3 .. 3, + // Landing-pad enable + LPE : 2 .. 2, + // Reserved WPRI bits. + wpri_0 : 1 .. 1, // Fence of I/O implies Memory FIOM : 0, } @@ -865,12 +903,26 @@ bitfield Envcfg : bits(64) = { register menvcfg : Envcfg register senvcfg : Envcfg -function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = { +function legalize_menvcfg(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); + /* If Zicfilp supported then update LPE field */ + let o = update_LPE(o, if haveZicfilp() then v.LPE() 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); + /* If Zicfilp supported then update LPE field */ + let o = update_LPE(o, if haveZicfilp() then v.LPE() 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 @@ -964,3 +1016,24 @@ function get_vtype_vma() = decode_agtype(vtype.vma()) val get_vtype_vta : unit -> agtype effect {rreg} function get_vtype_vta() = decode_agtype(vtype.vta()) + +bitfield MSecCfg : bits(64) = { + MLPE : 10 +} + +register mseccfg : MSecCfg + +function legalize_mseccfg_high(c : MSecCfg, value : xlenbits) -> MSecCfg = { + c +} + +function legalize_mseccfg(c : MSecCfg, value : xlenbits) -> MSecCfg = { + let m = Mk_MSecCfg(zero_extend(value)); + /* Hardwired to zero in the absence of Zicfilp */ + let m = if not(haveZicfilp()) then { + let m = update_MLPE(m, 0b0); + m + } else m; + m +} + diff --git a/model/riscv_zicfilp_regs.sail b/model/riscv_zicfilp_regs.sail new file mode 100644 index 000000000..391e57186 --- /dev/null +++ b/model/riscv_zicfilp_regs.sail @@ -0,0 +1,111 @@ +/*=======================================================================================*/ +/* 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. */ +/*=======================================================================================*/ + +/* Architectural state for the Zicfilp extension. */ +type elp_state = bits(1) + +enum ElpState = {NO_LP_EXPECTED, LP_EXPECTED} + +function ElpState_to_bits (e : ElpState) -> elp_state = + match (e) { + NO_LP_EXPECTED => 0b0, + LP_EXPECTED => 0b1 + } + +function ElpState_of_bits (e : elp_state) -> ElpState = + match (e) { + 0b0 => NO_LP_EXPECTED, + 0b1 => LP_EXPECTED + } + +function ElpState_to_str (e : ElpState) -> string = + match (e) { + NO_LP_EXPECTED => "NO_LP_EXPECTED", + LP_EXPECTED => "LP_EXPECTED" + } + +overload to_str = {ElpState_to_str} + +register elp : elp_state + +val init_zicfilp_regs : unit -> unit +function init_zicfilp_regs () = { + elp = ElpState_to_bits(NO_LP_EXPECTED); +} +function update_mstatus_MPELP(o : Mstatus, e : elp_state) -> Mstatus = + if sizeof(xlen) == 64 + then Mk_Mstatus([o.bits() with 41 .. 41 = e]) + else o + +function get_MPELP() -> elp_state = + if sizeof(xlen) == 64 + then mstatus.bits()[41..41] + else mstatush.MPELP()