Add Zicfilp extension

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

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"

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)
 

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()

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) },

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
 }

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
  }
  }

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)
+ }
  }
  }
  }