Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for CSR instructions and registers in RISC-V lifter and backlifter #196

Merged
merged 11 commits into from
Dec 5, 2024
Merged

Support for CSR instructions and registers in RISC-V lifter and backlifter #196

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
55521e9
Small fix to tutorial Makefile
didriklundberg Nov 22, 2024
72c6787
Merge pull request #194 from kth-step/dev_tutorial_fix
didriklundberg Nov 23, 2024
26c5108
Changed installation script to install branch from kth-step fork instead
didriklundberg Oct 21, 2020
d7eca9e
Bugfix for alternate branch-specific HOL4, small changes in RISC-V se…
didriklundberg Oct 27, 2020
41a1c37
Small changes to selftests, some work on CSR instruction lifting
didriklundberg Oct 28, 2020
4d178e4
CSRRW, CSRRS, CSRRC, CSRRWI, CSRRSI and CSRRCI instructions now lifti…
didriklundberg Oct 28, 2020
10ace80
Typos
didriklundberg Oct 28, 2020
cae4f3e
Fixing rebase typo
didriklundberg Dec 2, 2024
f922ca7
Typo fix + backlifter fix for latest RISC-V L3 model
didriklundberg Dec 2, 2024
9a76df9
Added support for more CSR registers in RISC-V lifter and backlifter
didriklundberg Dec 5, 2024
b99b4f4
use Holmakefile path relative to HOLBADIR
palmskog Dec 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions examples/tutorial/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@

MAKEFILE_DIRS=1-code 3-exec 8-symbexec
HOLMAKEFILE_DIRS=2-lift 4-bir-to-arm 5-wp 6-smt 7-composition support support2
HOLMAKEFILE_DIRS=2-lift 4-bir-to-arm 5-wp 6-smt 7-composition

##########################################################

.DEFAULT_GOAL := all
all: 7-composition support2
all: 7-composition

##########################################################

Expand Down
1 change: 0 additions & 1 deletion scripts/setup/install_hol4.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,4 +117,3 @@ do
cd "${HOL4_DIR}/${dir}"
${HOL4_DIR}/bin/Holmake
done

160 changes: 155 additions & 5 deletions src/theory/tools/backlifter/bir_riscv_backlifterScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -408,15 +408,41 @@ Definition default_riscv_bir_env_GPRS_tmp_def:
env_map)))))))))))))))))))))))))))))))
End

Definition default_riscv_bir_env_CSRS_def:
default_riscv_bir_env_CSRS ms env_map =
("mhartid" =+ SOME (BVal_Imm (Imm64 ( ((ms.c_MCSR ms.procID).mhartid) ))))
(("MPRV" =+ SOME (BVal_Imm (Imm8 ( w2w((ms.c_MCSR ms.procID).mstatus.MPRV) ))))
(("mscratch" =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mscratch ))))
(("mepc" =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mepc ))))
(("mcause" =+ SOME (BVal_Imm (Imm64 ( reg'mcause $ (ms.c_MCSR ms.procID).mcause ))))
(("mtval" =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mtval ))))
(("mip" =+ SOME (BVal_Imm (Imm64 ( reg'mip $ (ms.c_MCSR ms.procID).mip ))))
env_map))))))
End

Definition default_riscv_bir_env_CSRS_tmp_def:
default_riscv_bir_env_CSRS_tmp ms env_map =
("tmp_mhartid" =+ SOME (BVal_Imm (Imm64 ( ((ms.c_MCSR ms.procID).mhartid) ))))
(("tmp_MPRV" =+ SOME (BVal_Imm (Imm8 ( w2w((ms.c_MCSR ms.procID).mstatus.MPRV) ))))
(("tmp_mscratch" =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mscratch ))))
(("tmp_mepc" =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mepc ))))
(("tmp_mcause" =+ SOME (BVal_Imm (Imm64 ( reg'mcause $ (ms.c_MCSR ms.procID).mcause ))))
(("tmp_mtval" =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mtval ))))
(("tmp_mip" =+ SOME (BVal_Imm (Imm64 ( reg'mip $ (ms.c_MCSR ms.procID).mip ))))
env_map))))))
End

Definition default_riscv_bir_state_def:
default_riscv_bir_state ms =
<| bst_pc := bir_block_pc (BL_Address (Imm64 (ms.c_PC ms.procID))) ;
bst_environ := BEnv
(default_riscv_bir_env_GPRS ms
(default_riscv_bir_env_GPRS_tmp ms
(default_riscv_bir_env_FPRS ms
(default_riscv_bir_env_FPRS_tmp ms
(default_riscv_bir_env_basic ms bir_env_map_empty)))));
(default_riscv_bir_env_CSRS ms
(default_riscv_bir_env_CSRS_tmp ms
(default_riscv_bir_env_GPRS ms
(default_riscv_bir_env_GPRS_tmp ms
(default_riscv_bir_env_FPRS ms
(default_riscv_bir_env_FPRS_tmp ms
(default_riscv_bir_env_basic ms bir_env_map_empty)))))));
bst_status := BST_Running
|>
End
Expand Down Expand Up @@ -489,6 +515,8 @@ Theorem default_riscv_bir_state_GPRS_read[local]:
SOME (BVal_Imm (Imm64 (ms.c_gpr ms.procID 31w)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
bir_envTheory.bir_env_read_UPDATE,
bir_envTheory.bir_var_name_def,
Expand Down Expand Up @@ -567,6 +595,8 @@ Theorem default_riscv_bir_state_GPRS_read_tmp[local]:
SOME (BVal_Imm (Imm64 (ms.c_gpr ms.procID 31w)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
bir_envTheory.bir_env_read_UPDATE,
Expand Down Expand Up @@ -646,6 +676,8 @@ Theorem default_riscv_bir_state_GPRS_lookup_type[local]:
SOME (bir_var_type (BVar "x31" (BType_Imm Bit64)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
bir_env_oldTheory.bir_env_var_is_declared_def,
bir_envTheory.bir_var_name_def,
Expand Down Expand Up @@ -726,6 +758,8 @@ Theorem default_riscv_bir_state_GPRS_lookup_type_tmp[local]:
SOME (bir_var_type (BVar "tmp_x31" (BType_Imm Bit64)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
bir_env_oldTheory.bir_env_var_is_declared_def,
Expand Down Expand Up @@ -807,6 +841,8 @@ Theorem default_riscv_bir_state_FPRS_read[local]:
SOME (BVal_Imm (Imm64 (ms.c_fpr ms.procID 31w)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
default_riscv_bir_env_FPRS_def,
Expand Down Expand Up @@ -887,6 +923,8 @@ Theorem default_riscv_bir_state_FPRS_read_tmp[local]:
SOME (BVal_Imm (Imm64 (ms.c_fpr ms.procID 31w)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
default_riscv_bir_env_FPRS_def,
Expand Down Expand Up @@ -968,6 +1006,8 @@ Theorem default_riscv_bir_state_FPRS_lookup_type[local]:
SOME (bir_var_type (BVar "f31" (BType_Imm Bit64)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
default_riscv_bir_env_FPRS_def,
Expand Down Expand Up @@ -1050,6 +1090,8 @@ Theorem default_riscv_bir_state_FPRS_lookup_type_tmp[local]:
SOME (bir_var_type (BVar "tmp_f31" (BType_Imm Bit64)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
default_riscv_bir_env_FPRS_def,
Expand All @@ -1065,12 +1107,115 @@ Proof
type_of_bir_imm_def]
QED

Theorem default_riscv_bir_state_MCSRS_read[local]:
!ms.
bir_env_read (BVar "mhartid" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mhartid)) /\
bir_env_read (BVar "MPRV" (BType_Imm Bit8)) (default_riscv_bir_state ms).bst_environ =
SOME (BVal_Imm (Imm8 (w2w (ms.c_MCSR ms.procID).mstatus.MPRV))) /\
bir_env_read (BVar "mscratch" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mscratch)) /\
bir_env_read (BVar "mepc" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mepc)) /\
bir_env_read (BVar "mcause" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
SOME (BVal_Imm (Imm64 $ reg'mcause (ms.c_MCSR ms.procID).mcause)) /\
bir_env_read (BVar "mtval" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mtval)) /\
bir_env_read (BVar "mip" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
SOME (BVal_Imm (Imm64 $ reg'mip (ms.c_MCSR ms.procID).mip))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
default_riscv_bir_env_FPRS_def,
bir_envTheory.bir_env_read_UPDATE,
bir_envTheory.bir_var_name_def,
bir_envTheory.bir_env_lookup_UPDATE,
bir_envTheory.bir_var_type_def,
bir_valuesTheory.type_of_bir_val_def,
type_of_bir_imm_def,
bir_immTheory.type_of_bool2b]
QED

Theorem default_riscv_bir_state_MCSRS_lookup_type[local]:
!ms.
bir_env_lookup_type "mhartid" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "mhartid" (BType_Imm Bit64))) /\
bir_env_lookup_type "MPRV" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "MPRV" (BType_Imm Bit8))) /\
bir_env_lookup_type "mscratch" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "mscratch" (BType_Imm Bit64))) /\
bir_env_lookup_type "mepc" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "mepc" (BType_Imm Bit64))) /\
bir_env_lookup_type "mcause" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "mcause" (BType_Imm Bit64))) /\
bir_env_lookup_type "mtval" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "mtval" (BType_Imm Bit64))) /\
bir_env_lookup_type "mip" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "mip" (BType_Imm Bit64)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
default_riscv_bir_env_FPRS_def,
bir_env_oldTheory.bir_env_var_is_declared_def,
bir_envTheory.bir_var_name_def,
bir_envTheory.bir_env_read_UPDATE,
bir_envTheory.bir_var_name_def,
bir_envTheory.bir_env_lookup_UPDATE,
bir_envTheory.bir_var_type_def,
bir_envTheory.bir_env_lookup_type_def,
bir_valuesTheory.type_of_bir_val_def,
type_of_bir_imm_def]
QED

Theorem default_riscv_bir_state_MCSRS_lookup_type_tmp[local]:
!ms.
bir_env_lookup_type "tmp_mhartid" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "tmp_mhartid" (BType_Imm Bit64))) /\
bir_env_lookup_type "tmp_MPRV" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "tmp_MPRV" (BType_Imm Bit8))) /\
bir_env_lookup_type "tmp_mscratch" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "tmp_mscratch" (BType_Imm Bit64))) /\
bir_env_lookup_type "tmp_mepc" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "tmp_mepc" (BType_Imm Bit64))) /\
bir_env_lookup_type "tmp_mcause" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "tmp_mcause" (BType_Imm Bit64))) /\
bir_env_lookup_type "tmp_mtval" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "tmp_mtval" (BType_Imm Bit64))) /\
bir_env_lookup_type "tmp_mip" (default_riscv_bir_state ms).bst_environ =
SOME (bir_var_type (BVar "tmp_mip" (BType_Imm Bit64)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
default_riscv_bir_env_FPRS_def,
bir_env_oldTheory.bir_env_var_is_declared_def,
bir_envTheory.bir_var_name_def,
bir_envTheory.bir_env_read_UPDATE,
bir_envTheory.bir_var_name_def,
bir_envTheory.bir_env_lookup_UPDATE,
bir_envTheory.bir_var_type_def,
bir_envTheory.bir_env_lookup_type_def,
bir_valuesTheory.type_of_bir_val_def,
type_of_bir_imm_def]
QED


Theorem default_riscv_bir_state_basic_env_read[local]:
!ms.
bir_env_read (BVar "MEM8" (BType_Mem Bit64 Bit8)) (default_riscv_bir_state ms).bst_environ =
SOME (BVal_Mem Bit64 Bit8 (bir_mmap_w_w2n (bir_mf2mm ms.MEM8)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
default_riscv_bir_env_FPRS_def,
Expand All @@ -1095,6 +1240,8 @@ Theorem default_riscv_bir_state_basic_lookup_type[local]:
SOME (bir_var_type (BVar "tmp_COND" (BType_Imm Bit1)))
Proof
rw [default_riscv_bir_state_def,
default_riscv_bir_env_CSRS_def,
default_riscv_bir_env_CSRS_tmp_def,
default_riscv_bir_env_GPRS_def,
default_riscv_bir_env_GPRS_tmp_def,
default_riscv_bir_env_FPRS_def,
Expand All @@ -1119,6 +1266,9 @@ strip_tac >> strip_tac >>
FULL_SIMP_TAC std_ss [bir_lifting_machinesTheory.riscv_bmr_rel_EVAL,
bir_env_oldTheory.bir_env_var_is_declared_def,bir_envTheory.bir_var_name_def] >>
fs [
default_riscv_bir_state_MCSRS_read,
default_riscv_bir_state_MCSRS_lookup_type,
default_riscv_bir_state_MCSRS_lookup_type_tmp,
default_riscv_bir_state_GPRS_read,
default_riscv_bir_state_GPRS_read_tmp,
default_riscv_bir_state_GPRS_lookup_type,
Expand Down
73 changes: 65 additions & 8 deletions src/theory/tools/lifter/bir_lifting_machinesScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -607,13 +607,30 @@ Definition arm8_lifted_pc_def:
(\ms:arm8_state. Imm64 (ms.PC))
End

(* Well defined state *)
(* Well-defined state *)
(* https://static.docs.arm.com/100878/0100/fundamentals_of_armv8_a_100878_0100_en.pdf
* tells us that
* ELn: Exception level n. EL0 is user, EL1 kernel, EL2 Hypervisor, EL3 firmware (p. 4 of PDF).
* SCTLR: System control register; for EL1, EL2 and EL3 (p. 24 of PDF).
* PSTATE: Processor state flags, accessed through special-purpose registers. (p. 16 of PDF)
* TCR: Translation Control Register; for EL1, EL2 and EL3. Determines
* Translation Table Base Register. *)
Definition arm8_state_is_OK_def:
arm8_state_is_OK (ms:arm8_state) <=> (
~ms.SCTLR_EL1.E0E ∧ (ms.PSTATE.EL = 0w) ∧ (ms.exception = NoException) /\
arm8_state_is_OK (ms:arm8_state) <=>
(* Explicit data accesses at EL0 MUST be little-endian. *)
~ms.SCTLR_EL1.E0E /\
(* Exception level must be 0 (user) *)
(ms.PSTATE.EL = 0w) /\
(* Exception must be NoException (as opposed to ALIGNMENT_FAULT,
* UNDEFINED_FAULT and ASSERT).*)
(ms.exception = NoException) /\
(* Stack Alignment Check MUST NOT be enabled for EL0. *)
~ms.SCTLR_EL1.SA0 /\
(* Translation control register for EL1 must not be TBI0 or TBI1,
* meaning it must be "tcr_el1'rst", which is a 62-bit field.
* TODO: What is TBI0 and TBI1? *)
~ms.TCR_EL1.TBI0 /\
~ms.TCR_EL1.TBI1)
~ms.TCR_EL1.TBI1
End

Definition arm8_bmr_def:
Expand Down Expand Up @@ -759,10 +776,16 @@ Definition m0_lifted_pc_def:
(\ms:m0_state. Imm32 (ms.REG RName_PC))
End

(* AIRCR: Application Interrupt and Reset Control Register.
* CONTROL: Special register in Cortex-M processor. Can be accessed using MSR and MRS. *)
Definition m0_state_is_OK_def:
m0_state_is_OK (ef, sel) (s:m0_state) =
((s.AIRCR.ENDIANNESS <=> ef) /\ (s.CONTROL.SPSEL <=> sel) /\
(s.exception = NoException))
(* Endianness must match argument ef. *)
((s.AIRCR.ENDIANNESS <=> ef) /\
(* Stack pointer selection bit in the control register must match argument sel. *)
(s.CONTROL.SPSEL <=> sel) /\
(* Exception must be NoException. *)
(s.exception = NoException))
End

(* Just a dummy for now *)
Expand Down Expand Up @@ -1001,6 +1024,39 @@ Definition riscv_FPRS_lifted_imms_LIST_def:
End
Theorem riscv_FPRS_lifted_imms_LIST_EVAL = EVAL ``riscv_FPRS_lifted_imms_LIST``

(* NOTE: Since the L3 model uses separate immediate values for the fields
* of a single system register (instead of letting the entire system register
* be represented as one immediate), we do so here as well. *)
val riscv_sysregs_lifted_imms_LIST_def = Define `
riscv_sysregs_lifted_imms_LIST = [
(BMLI (BVar "mhartid" (BType_Imm Bit64))
(\ms:riscv_state. Imm64 ((ms.c_MCSR ms.procID).mhartid))
);
(* MPRV (from the mstatus register) is really a 2-bit value,
* but is represented as an 8-bit immediate *)
(BMLI (BVar "MPRV" (BType_Imm Bit8))
(\ms:riscv_state. Imm8 (w2w((ms.c_MCSR ms.procID).mstatus.MPRV)))
);
(BMLI (BVar "mscratch" (BType_Imm Bit64))
(\ms:riscv_state. Imm64 ((ms.c_MCSR ms.procID).mscratch))
);
(BMLI (BVar "mepc" (BType_Imm Bit64))
(\ms:riscv_state. Imm64 ((ms.c_MCSR ms.procID).mepc))
);
(BMLI (BVar "mcause" (BType_Imm Bit64))
(\ms:riscv_state. Imm64 $ reg'mcause ((ms.c_MCSR ms.procID).mcause))
);
(BMLI (BVar "mtval" (BType_Imm Bit64))
(\ms:riscv_state. Imm64 ((ms.c_MCSR ms.procID).mtval))
);
(BMLI (BVar "mip" (BType_Imm Bit64))
(\ms:riscv_state. Imm64 $ reg'mip ((ms.c_MCSR ms.procID).mip))
)
]
`;
val riscv_sysregs_lifted_imms_LIST_EVAL = save_thm("riscv_sysregs_lifted_imms_LIST_EVAL",
EVAL ``riscv_sysregs_lifted_imms_LIST``
);

(* Note: For some reason, MEM is named MEM8 in the RISC-V state.
* Since memory is shared between processes, this does not require
Expand Down Expand Up @@ -1028,8 +1084,8 @@ Definition riscv_bmr_def:
* OK state is now minimal. *)
bmr_extra := \ms. riscv_state_is_OK ms;
(* Registers are the 32 general-purpose registers as well as the
* 32 fprs (fpr = floating point register?). *)
bmr_imms := (riscv_GPRS_lifted_imms_LIST++riscv_FPRS_lifted_imms_LIST);
* 32 floating-point registers. *)
bmr_imms := (riscv_GPRS_lifted_imms_LIST++riscv_FPRS_lifted_imms_LIST++riscv_sysregs_lifted_imms_LIST);
(* Done! *)
bmr_mem := riscv_lifted_mem;
(* Done! *)
Expand All @@ -1042,6 +1098,7 @@ End
(* Evaluation theorem of RISC-V BMR. *)
Theorem riscv_bmr_EVAL = SIMP_CONV list_ss [riscv_bmr_def, riscv_state_is_OK_def,
riscv_GPRS_lifted_imms_LIST_EVAL, riscv_FPRS_lifted_imms_LIST_EVAL,
riscv_sysregs_lifted_imms_LIST_EVAL,
riscv_lifted_mem_def,
riscv_lifted_pc_def, bir_temp_var_name_def]
``riscv_bmr``
Expand Down
Loading
Loading