From 24851e5d3cf5639be57c2e989ce438709aa02837 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Mon, 27 Nov 2023 19:39:28 -0600 Subject: [PATCH 1/5] Update CSRs infrastructure - Add machine security configuration register - mseccfg - Legalize menvcfg and senvcfg separately. Some fields of senvcfg are modulated by menvcfg. - Make mstatush writeable and add a legalizer function for it. --- model/riscv_csr_map.sail | 2 ++ model/riscv_insts_zicsr.sail | 12 ++++++++++-- model/riscv_sys_control.sail | 3 +++ model/riscv_sys_regs.sail | 29 +++++++++++++++++++++++++++++ 4 files changed, 44 insertions(+), 2 deletions(-) diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 22cffd5a6..aed6e8d26 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -162,6 +162,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_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index f2980fb9e..484450400 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -56,6 +56,10 @@ function readCSR csr : csreg -> xlenbits = { (0x3D @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b10 @ idx)), (0x3E @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b11 @ idx)), + /* Machine security configuration register */ + (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], @@ -81,7 +85,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, @@ -146,6 +150,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x3D @ idx : bits(4), _) => { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, (0x3E @ idx : bits(4), _) => { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, + /* Machine security configuration register */ + (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) }, @@ -162,7 +170,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_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) }, + (0x10A, _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(get_senvcfg()[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_sys_control.sail b/model/riscv_sys_control.sail index 95ed4d6a5..1497382cc 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -58,6 +58,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 65d141923..ac857a8ea 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -262,6 +262,12 @@ function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { } } +function legalize_mstatush(o : Mstatush, v : bits(32)) -> Mstatush = { + let v : Mstatush = Mk_Mstatush(v); + o + /* MBE and SBE writes are ignored - dynamic XLEN not supported */ +} + function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { /* * Populate all defined fields using the bits of v, stripping anything @@ -848,6 +854,11 @@ function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = { 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. @@ -942,3 +953,21 @@ function get_vtype_vma() = decode_agtype(vtype[vma]) val get_vtype_vta : unit -> agtype function get_vtype_vta() = decode_agtype(vtype[vta]) + +bitfield MSecCfg : bits(64) = { + MLPE : 10 +} + +/* Machine security configuration register */ +register mseccfg : MSecCfg + +function legalize_mseccfg_high(o : MSecCfg, v : xlenbits) -> MSecCfg = { + o +} + +function legalize_mseccfg(o : MSecCfg, v : xlenbits) -> MSecCfg = { + let m = Mk_MSecCfg(zero_extend(v)); + /* Hardwired to zero in the absence of Zicfilp */ + let m = if haveZicfilp() then m else [m with MLPE = 0b0]; + m +} From 15be4458a46dd64b7749d0ce025e0c68055ae850 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Mon, 27 Nov 2023 20:04:28 -0600 Subject: [PATCH 2/5] Add fields introduced by Zicfilp in existing CSRs - mstatus : MPELP, SPELP - menvcfg : LPE - senvcfg : LPE --- model/riscv_sys_regs.sail | 42 +++++++++++++++++++++++++++++++-------- 1 file changed, 34 insertions(+), 8 deletions(-) diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index ac857a8ea..267046fc9 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -184,6 +184,7 @@ function have_privLevel(priv : priv_level) -> bool = } bitfield Mstatush : bits(32) = { + MPELP: 9, MBE : 5, SBE : 4 } @@ -192,9 +193,10 @@ register mstatush : Mstatush bitfield Mstatus : xlenbits = { 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 @@ -203,6 +205,7 @@ bitfield Mstatus : xlenbits = { // SXL : 35 .. 34, // UXL : 33 .. 32, + SPELP: 23, TSR : 22, TW : 21, TVM : 20, @@ -264,9 +267,12 @@ function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { function legalize_mstatush(o : Mstatush, v : bits(32)) -> Mstatush = { let v : Mstatush = Mk_Mstatush(v); - o + let m = if haveZicfilp() then [o with MPELP = v[MPELP]] else o; + m /* 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 = { /* @@ -274,7 +280,11 @@ 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 [m with SPELP = 0b0] else m; + /* Update MPELP if Zicfilp supported and xlen is 64; for xlen 32 MPELP is in mstatush */ + let m = if haveZicfilp() & sizeof(xlen) == 64 then update_mstatus_MPELP(m, v[41..41]) else m; /* Legalize MPP */ let m = [m with MPP = if have_privLevel(m[MPP]) then m[MPP] @@ -558,6 +568,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, @@ -586,6 +597,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = { let s = Mk_Sstatus(zero_extend(0b0)); let s = [s with SD = m[SD]]; let s = set_sstatus_UXL(s, get_mstatus_UXL(m)); + let s = [s with SPELP = m[SPELP]]; let s = [s with MXR = m[MXR]]; let s = [s with SUM = m[SUM]]; let s = [s with XS = m[XS]]; @@ -603,6 +615,8 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { let m = [m with MXR = s[MXR]]; let m = [m with SUM = s[SUM]]; + let m = if not(haveZicfilp()) then m else [m with SPELP = s[SPELP]]; + let m = [m with XS = s[XS]]; // See comment for mstatus.FS. let m = [m with FS = s[FS]]; @@ -811,7 +825,7 @@ bitfield MEnvcfg : 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 @@ -819,7 +833,11 @@ bitfield MEnvcfg : 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, } @@ -832,7 +850,11 @@ bitfield SEnvcfg : xlenbits = { // 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, } @@ -843,6 +865,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]; + /* If Zicfilp supported then update LPE field */ + let o = [o with LPE = if haveZicfilp() then v[LPE] else 0b0]; // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -850,12 +874,14 @@ 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]; + /* If Zicfilp supported then update LPE field */ + let o = [o with LPE = 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; +function get_senvcfg() -> xlenbits = { + let o : SEnvcfg = senvcfg; o.bits() } From 12b25e3f06b1c7b8e6c2daf47dfc2c8bd2559a49 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Mon, 27 Nov 2023 20:07:23 -0600 Subject: [PATCH 3/5] add software check exception --- 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 1497382cc..ebe5c44f5 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -465,6 +465,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..ae8f72c4d 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 = {LANDING_PAD_FAULT} + +function sw_check_code_to_bits (c : SWCheckCodes) -> xlenbits = + match (c) { + LANDING_PAD_FAULT => zero_extend(0b010), + } + /* trap modes */ type tv_mode = bits(2) From 46abcd753a5546f1cf2c1accc27226b46ecbf9d8 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Mon, 27 Nov 2023 20:13:30 -0600 Subject: [PATCH 4/5] Expected Landing Pad (ELP) state management - JALR updates ELP to LP expected on indirect call/jump - Traps preserve ELP state in mstatus.xPELP on trap delivery priv x - xRET restores ELP from mstatus.xPELP - If instruction fetched not LPAD when ELP is LP_EXPECTED cause SW check fault --- model/riscv_jalr_rmem.sail | 5 +++++ model/riscv_jalr_seq.sail | 5 +++++ model/riscv_step.sail | 28 ++++++++++++++++++++-------- model/riscv_sys_control.sail | 15 +++++++++++++++ 4 files changed, 45 insertions(+), 8 deletions(-) diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail index d628630af..a58687fdc 100644 --- a/model/riscv_jalr_rmem.sail +++ b/model/riscv_jalr_rmem.sail @@ -6,6 +6,9 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +/* Zicfilp : Update ELP state */ +val zicfilp_update_elp : (regidx) -> unit + /* The definition for the memory model. */ function clause execute (RISCV_JALR(imm, rs1, rd)) = { @@ -14,5 +17,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */ let newPC : xlenbits = X(rs1) + sign_extend(imm); nextPC = [newPC with 0 = bitzero]; /* Clear newPC[0] */ + /* update ELP if Zicfilp is active */ + zicfilp_update_elp(rs1); RETIRE_SUCCESS } diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index 497a44178..25dedfa76 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -6,6 +6,9 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +/* Zicfilp : Update ELP state */ +val zicfilp_update_elp : (regidx) -> unit + /* The definition for the sequential model. */ function clause execute (RISCV_JALR(imm, rs1, rd)) = { @@ -30,6 +33,8 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { } else { X(rd) = get_next_pc(); set_next_pc(target); + /* update ELP if Zicfilp is active */ + zicfilp_update_elp(rs1); RETIRE_SUCCESS } } diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 5ff7e4bc0..6ba14cb23 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -53,13 +53,19 @@ function step(step_no : int) -> bool = { then { print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast)); }; - /* check for RVC once here instead of every RVC execute clause. */ - if haveRVC() then { - nextPC = PC + 2; - (execute(ast), true) - } else { - handle_illegal(); + /* Zicfilp requires a landing pad (a base inst) if ELP is LP_EXPECTED */ + if elp == ElpState_to_bits(LP_EXPECTED) then { + handle_sw_check_exception(LANDING_PAD_FAULT); (RETIRE_FAIL, true) + } else { + /* check for RVC once here instead of every RVC execute clause. */ + if haveRVC() then { + nextPC = PC + 2; + (execute(ast), true) + } else { + handle_illegal(); + (RETIRE_FAIL, true) + } } }, F_Base(w) => { @@ -70,8 +76,14 @@ function step(step_no : int) -> bool = { then { print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); }; - nextPC = PC + 4; - (execute(ast), true) + /* Zicfilp requires a aligned lpad if elp is LP_EXPECTED */ + if zicfilp_is_elp_violated() then { + handle_sw_check_exception(LANDING_PAD_FAULT); + (RETIRE_FAIL, true) + } else { + nextPC = PC + 4; + (execute(ast), true) + } } } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index ebe5c44f5..927bdb697 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -316,6 +316,8 @@ val rvfi_trap : unit -> unit function rvfi_trap () = () $endif +val zicfilp_preserve_elp : (Privilege) -> unit + /* handle exceptional ctl flow by updating nextPC and operating privilege */ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception)) @@ -341,6 +343,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen cur_privilege = del_priv; + zicfilp_preserve_elp(del_priv); handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() @@ -366,6 +369,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen cur_privilege = del_priv; + zicfilp_preserve_elp(del_priv); handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() @@ -386,6 +390,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen cur_privilege = del_priv; + zicfilp_preserve_elp(del_priv); handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() @@ -396,6 +401,10 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen }; } +/* Zicfilp : extension to restore elp */ +val zicfilp_set_elp_to_mpelp : (unit) -> unit +val zicfilp_set_elp_to_spelp : (unit) -> unit + function exception_handler(cur_priv : Privilege, ctl : ctl_result, pc: xlenbits) -> xlenbits = { match (cur_priv, ctl) { @@ -415,6 +424,9 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; + /* Zicfilp: extension to restore ELP */ + zicfilp_set_elp_to_mpelp(); + if get_config_print_reg() then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform() @@ -432,6 +444,9 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; + /* Zicfilp: extension to restore ELP */ + zicfilp_set_elp_to_spelp(); + if get_config_print_reg() then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform() From 1056a62475450a801b754facae36420f0fae9431 Mon Sep 17 00:00:00 2001 From: Ved Shanbhogue Date: Mon, 27 Nov 2023 20:19:45 -0600 Subject: [PATCH 5/5] Add Zicfilp register state and flows - Add elp state register and its initialization - xLPE to track if landing pads enabled at priv x - Functions that implement ELP state management - LPAD instruction --- Makefile | 3 + model/riscv_insts_base.sail | 13 +- model/riscv_insts_zicfilp.sail | 215 +++++++++++++++++++++++++++++++++ model/riscv_sys_control.sail | 3 + model/riscv_sys_regs.sail | 3 + model/riscv_zicfilp_regs.sail | 102 ++++++++++++++++ 6 files changed, 338 insertions(+), 1 deletion(-) create mode 100644 model/riscv_insts_zicfilp.sail create mode 100644 model/riscv_zicfilp_regs.sail diff --git a/Makefile b/Makefile index af355efc1..ba3d61122 100644 --- a/Makefile +++ b/Makefile @@ -49,6 +49,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 diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 26915f22c..802d4e125 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -12,14 +12,22 @@ /* ****************************************************************** */ union clause ast = UTYPE : (bits(20), regidx, uop) +union clause ast = zicfilp_lpad : (bits(20)) mapping encdec_uop : uop <-> bits(7) = { RISCV_LUI <-> 0b0110111, RISCV_AUIPC <-> 0b0010111 } +/* Zicfilp landing pad lpad is auipc x0, imm */ +function is_lpad(op : uop, rd : regidx) -> bool = + haveZicfilp() & rd == zreg & op == RISCV_AUIPC + mapping clause encdec = UTYPE(imm, rd, op) - <-> imm @ rd @ encdec_uop(op) + <-> imm @ rd @ encdec_uop(op) if not(is_lpad(op, rd)) + +mapping clause encdec = zicfilp_lpad(imm) + <-> imm @ 0b00000 @ 0b0010111 function clause execute UTYPE(imm, rd, op) = { let off : xlenbits = sign_extend(imm @ 0x000); @@ -39,6 +47,9 @@ mapping utype_mnemonic : uop <-> string = { mapping clause assembly = UTYPE(imm, rd, op) <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_20(imm) +mapping clause assembly = zicfilp_lpad(imm) + <-> "lpad" ^ spc() ^ hex_bits_20(imm) + /* ****************************************************************** */ union clause ast = RISCV_JAL : (bits(21), regidx) diff --git a/model/riscv_insts_zicfilp.sail b/model/riscv_insts_zicfilp.sail new file mode 100644 index 000000000..8c238e752 --- /dev/null +++ b/model/riscv_insts_zicfilp.sail @@ -0,0 +1,215 @@ +/*=======================================================================================*/ +/* 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 */ +val get_MPELP : (unit) -> elp_state +/* 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) -> 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); + + print("jalr: elp= " ^ BitStr(elp) ^ " is_lp_expected=" ^ BitStr(bool_to_bits(is_lp_expected))); +} +/* AUIPC with rd=x0 is a lpad instruction when zicfilp is active else a no-op */ +function clause execute zicfilp_lpad( lpl ) = { + /* expected label is in x7 bits 31:12 */ + let exp_lbl : bits(20) = x7[31..12]; + + print("lpad:elp= " ^ BitStr(elp) ^ " lpl= " ^ BitStr(lpl) ^ " x7_31_12= " ^ BitStr(exp_lbl)); + + 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_preserve_elp(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)); + } +} +/* Check if fetch violates ELP */ +function zicfilp_is_elp_violated() -> bool = { + /* 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 + */ + if not(zicfilp_xLPE()) + then false + else if elp != ElpState_to_bits(LP_EXPECTED) + then false + else if ( (PC[1 .. 0] != 0b00) | (instbits[6..0] != 0b0010111) | (instbits[11..7] != 0b00000) ) + then true + else false +} + +/* helper to update MPELP in mstatus */ +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 + +/* helpers to get MPELP from mstatus/mstatush */ +function get_MPELP() -> elp_state = + if sizeof(xlen) == 64 + then mstatus.bits()[41..41] + else mstatush.MPELP() diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 927bdb697..86a8e34c5 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -497,6 +497,7 @@ function handle_exception(e: ExceptionType) -> unit = { function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit = set_next_pc(trap_handler(del_priv, true, interruptType_to_bits(i), PC, None(), None())) +val init_zicfilp_regs : unit -> unit /* state state initialization */ function init_sys() -> unit = { @@ -577,6 +578,8 @@ function init_sys() -> unit = { // PMP's L and A fields are set to 0 on reset. init_pmp(); + init_zicfilp_regs(); + // log compatibility with spike if get_config_print_reg() then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")") diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 267046fc9..65f88bd1e 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -168,6 +168,9 @@ function haveZalrsc() -> bool = haveAtomics() /* Zicond extension support */ function haveZicond() -> bool = true +/* Zicfilp extension support */ +function haveZicfilp() -> 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. diff --git a/model/riscv_zicfilp_regs.sail b/model/riscv_zicfilp_regs.sail new file mode 100644 index 000000000..de304aa84 --- /dev/null +++ b/model/riscv_zicfilp_regs.sail @@ -0,0 +1,102 @@ +/*=======================================================================================*/ +/* 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); +}