1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96

// =======================================================================================
// This Sail RISC-V architecture model, comprising all files and
// directories except where otherwise noted is subject the BSD
// two-clause license in the LICENSE file.
//
// SPDX-License-Identifier: BSD-2-Clause
// =======================================================================================

function get_xLPE(p : Privilege) -> 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
  //
  match p {
    Machine           => bool_bits(mseccfg[MLPE]),
    Supervisor        => bool_bits(menvcfg[LPE]),
    User              => if   currentlyEnabled(Ext_S)
                         then bool_bits(senvcfg[LPE])
                         else bool_bits(menvcfg[LPE]),
    // TODO: check henvcfg for VS mode
    VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
    VirtualUser       => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
  }

function clause currentlyEnabled(Ext_Zicfilp) =
  currentlyEnabled(Ext_Zicsr) & hartSupports(Ext_Zicfilp) & get_xLPE(cur_privilege)

/// Architectural state for the Zicfilp extension.

enum landing_pad_expectation = { NO_LP_EXPECTED, LP_EXPECTED }

// Expected Landing Pad
register elp : bits(1)

mapping landing_pad_bits : bits(1) <-> landing_pad_expectation = {
  0b0 <-> NO_LP_EXPECTED,
  0b1 <-> LP_EXPECTED,
}

function update_elp_state(rs1 : regidx) -> unit =
  if currentlyEnabled(Ext_Zicfilp) then {
    let is_software_guarded_branch = rs1 == Regidx(zero_extend(0x7));
    let is_return = rs1 == Regidx(zero_extend(0x1)) | rs1 == Regidx(zero_extend(0x5));
    elp = bool_to_bits(not(is_software_guarded_branch) & not(is_return))
  }

function is_landing_pad_expected() -> bool =
  elp == landing_pad_bits(LP_EXPECTED)

function reset_elp() -> unit =
  elp = landing_pad_bits(NO_LP_EXPECTED)

/// Interaction with system registers.

// When a trap is taken into privilege mode x, the xPELP is set
// to ELP and ELP is set to NO_LP_EXPECTED.
function zicfilp_preserve_elp_on_trap(x : Privilege) -> unit = {
  // When Sdext is added, ELP will need to be preserved there as well.
  match x {
    Machine           => { mstatus[MPELP] = elp; },
    Supervisor        => { mstatus[SPELP] = elp; },
    User              => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
    VirtualSupervisor => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
    VirtualUser       => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
};
  reset_elp();
}

// When executing an xRET instruction, if the new privilege mode is 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.
function zicfilp_restore_elp_on_xret(xret : xRET_type, y : Privilege) -> unit = {
  let pelp : bits(1) = match xret {
    mRET => {
      let pelp = mstatus[MPELP];
      mstatus[MPELP] = landing_pad_bits(NO_LP_EXPECTED);
      pelp
    },
    sRET => {
      let pelp = mstatus[SPELP];
      mstatus[SPELP] = landing_pad_bits(NO_LP_EXPECTED);
      pelp
    },
  };
  elp = if get_xLPE(y) then pelp else landing_pad_bits(NO_LP_EXPECTED);
}