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
|
/*=======================================================================================*/
/* 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 */
/*=======================================================================================*/
termination_measure n_leading_spaces s = string_length(s)
val compressed_measure : ast -> int
function compressed_measure(instr) =
match instr {
C_ADDI4SPN (rdc,nzimm) => 1,
C_LW (uimm,rsc,rdc) => 1,
C_LD (uimm,rsc,rdc) => 1,
C_SW (uimm,rsc1,rsc2) => 1,
C_SD (uimm,rsc1,rsc2) => 1,
C_ADDI (nzi,rsd) => 1,
C_JAL (imm) => 1,
C_LI (imm,rd) => 1,
C_ADDI16SP (imm) => 1,
C_LUI (imm,rd) => 1,
C_SRLI (shamt,rsd) => 1,
C_SRAI (shamt,rsd) => 1,
C_ANDI (imm,rsd) => 1,
C_SUB (rsd,rs2) => 1,
C_XOR (rsd,rs2) => 1,
C_OR (rsd,rs2) => 1,
C_AND (rsd,rs2) => 1,
C_SUBW (rsd,rs2) => 1,
C_ADDW (rsd,rs2) => 1,
C_J (imm) => 1,
C_BEQZ (imm,rs) => 1,
C_BNEZ (imm,rs) => 1,
C_SLLI (shamt,rsd) => 1,
C_LWSP (uimm,rd) => 1,
C_LDSP (uimm,rd) => 1,
C_SWSP (uimm,rs2) => 1,
C_SDSP (uimm,rs2) => 1,
C_JR (rs1) => 1,
C_JALR (rs1) => 1,
C_MV (rd,rs2) => 1,
C_EBREAK (tt) => 1,
C_ADD (rsd,rs2) => 1,
_ => 0
}
termination_measure execute(i) = compressed_measure(i)
|
