From 73428463f488921bbfb588384f85adec7aaa1cca Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Thu, 9 Jan 2025 15:22:11 +0100 Subject: [PATCH 1/2] Fixed typo in RISC-V step theory, updates to RISC-V selftest --- .../riscv/step/riscv_stepScript.sml | 7 +++-- src/tools/lifter/selftest_riscv.log | 30 ++++++++++++++++++- src/tools/lifter/selftest_riscv.sml | 12 ++------ 3 files changed, 36 insertions(+), 13 deletions(-) diff --git a/src/shared/l3-machine-code/riscv/step/riscv_stepScript.sml b/src/shared/l3-machine-code/riscv/step/riscv_stepScript.sml index 758626c60..af00a5786 100644 --- a/src/shared/l3-machine-code/riscv/step/riscv_stepScript.sml +++ b/src/shared/l3-machine-code/riscv/step/riscv_stepScript.sml @@ -835,6 +835,7 @@ in val () = utilsLib.reset_thms() fun class args avoid n = let + val is_csr = Lib.mem n ["CSRRW", "CSRRS", "CSRRC", "CSRRWI", "CSRRSI", "CSRRCI"] val name = "dfn'" ^ n val read = if Lib.mem n ["LD"] then [address_aligned3] else [] val (write, n) = @@ -844,7 +845,7 @@ in ([write'GPR], n) (* These rewrites should be done for all CSR instructions *) val csr = - if Lib.mem n ["CSRRW", "CSRRS", "CSRRC", "CSRRWI", "CSRRSI", "CSRRCI"] + if is_csr then [checkCSROp, check_CSR_access, CSR, privLevel, csrRW, csrPR] else [] val thms = DB.fetch "riscv" (name ^ "_def") :: write @ read @ csr @@ -948,14 +949,14 @@ val SW = store [] "SW" val SH = store [] "SH" val SB = store [] "SB" -val csrinst = class `(rd, rs1, csr)` +val csrinst = class_rd0 `(rd, rs1, csr)` (* TODO: How to handle privilege level? Currently, machine mode is always assumed *) val CSRRW_M = csrinst [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRW" val CSRRS_M = csrinst [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRS" val CSRRC_M = csrinst [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRC" -val csrinsti = class `(rd, imm, csr)` +val csrinsti = class_rd0 `(rd, imm, csr)` val CSRRWI_M = csrinsti [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRWI" val CSRRSI_M = csrinsti [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRSI" diff --git a/src/tools/lifter/selftest_riscv.log b/src/tools/lifter/selftest_riscv.log index 1f1e23d22..8f4b54805 100644 --- a/src/tools/lifter/selftest_riscv.log +++ b/src/tools/lifter/selftest_riscv.log @@ -945,6 +945,34 @@ CSRRW x1, mscratch(0x340), x2: 340110F3 @ 0x10030 - OK bb_last_statement := BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>]) +CSRW mie(0x304), 0: 30405073 @ 0x10030 - OK + [] +|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w) + (0x10030w,[115w; 80w; 64w; 48w]) + (BirProgram + [<|bb_label := BL_Address_HC (Imm64 0x10030w) "30405073"; + bb_statements := + [BStmt_Assert + (BExp_BinPred BIExp_Equal + (BExp_Den (BVar "MPRV" (BType_Imm Bit8))) + (BExp_Const (Imm8 3w)))]; + bb_last_statement := + BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>]) + +CSRW mstatus(0x300), 0: 30005073 @ 0x10030 - OK + [] +|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w) + (0x10030w,[115w; 80w; 0w; 48w]) + (BirProgram + [<|bb_label := BL_Address_HC (Imm64 0x10030w) "30005073"; + bb_statements := + [BStmt_Assert + (BExp_BinPred BIExp_Equal + (BExp_Den (BVar "MPRV" (BType_Imm Bit8))) + (BExp_Const (Imm8 3w)))]; + bb_last_statement := + BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>]) + CSRRS x1, mscratch(0x340), x2: 340120F3 @ 0x10030 - OK [] |- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w) @@ -1474,7 +1502,7 @@ REMUW x5, x6, x7: 027372BB @ 0x10030 - OK SUMMARY FAILING HEXCODES RISC-V -Instructions FAILED: 4/82 +Instructions FAILED: 4/84 "0881008F" (* bmr_step_hex failed *), "00000073" (* bmr_step_hex failed *), diff --git a/src/tools/lifter/selftest_riscv.sml b/src/tools/lifter/selftest_riscv.sml index 8f09521b0..636c17a49 100644 --- a/src/tools/lifter/selftest_riscv.sml +++ b/src/tools/lifter/selftest_riscv.sml @@ -311,6 +311,9 @@ val _ = print_msg "\n\n"; * (see bottom of riscv_stepScript.sml) *) (* CSRRW x1, mscratch(0x340), x2 : 001101000000 00010 001000011110011 *) val _ = riscv_test_hex_print_asm "CSRRW x1, mscratch(0x340), x2" "340110F3"; +val _ = riscv_test_hex_print_asm "CSRW mie(0x304), 0" "30405073"; +val _ = riscv_test_hex_print_asm "CSRW mstatus(0x300), 0" "30005073"; + (* CSRRS x1, mscratch(0x340), x2 : 001101000000 00010 010000011110011 *) val _ = riscv_test_hex_print_asm "CSRRS x1, mscratch(0x340), x2" "340120F3"; (* CSRRC x1, mscratch(0x340), x2 : 001101000000 00010 011000011110011 *) @@ -332,15 +335,6 @@ val _ = riscv_test_hex_print_asm "CSRR a5, mtval(0x343)" "343027F3"; val _ = riscv_test_hex_print_asm "CSRR a5, mip(0x344)" "344027F3"; -(* TODO: These fail in riscv_stepLib for some reason... - -val _ = riscv_test_hex_print_asm "CSRW mie(0x304), 0" "30405073"; -val _ = riscv_test_hex_print_asm "CSRW mstatus(0x300), 0" "30005073"; - -open riscv_stepLib; -val _ = riscv_step_hex "30405073"; - -*) val _ = print_msg "\n"; val _ = print_header "RV64M Standard Extension (instructions inherited from RV32M)"; From 26593a6a2ad42ea732cf9dddfb5b01f5ac9660e6 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Mon, 20 Jan 2025 11:55:28 +0100 Subject: [PATCH 2/2] remove superfluous kernel example --- examples/riscv/kernel-trap-entry/Holmakefile | 30 ----------- examples/riscv/kernel-trap-entry/kernel.da | 52 ------------------- .../riscv/kernel-trap-entry/kernelScript.sml | 21 -------- 3 files changed, 103 deletions(-) delete mode 100644 examples/riscv/kernel-trap-entry/Holmakefile delete mode 100644 examples/riscv/kernel-trap-entry/kernel.da delete mode 100644 examples/riscv/kernel-trap-entry/kernelScript.sml diff --git a/examples/riscv/kernel-trap-entry/Holmakefile b/examples/riscv/kernel-trap-entry/Holmakefile deleted file mode 100644 index d79e4e0a2..000000000 --- a/examples/riscv/kernel-trap-entry/Holmakefile +++ /dev/null @@ -1,30 +0,0 @@ -INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \ - $(HOLDIR)/examples/l3-machine-code/arm8/model \ - $(HOLDIR)/examples/l3-machine-code/arm8/step \ - $(HOLDIR)/examples/l3-machine-code/m0/model \ - $(HOLDIR)/examples/l3-machine-code/m0/step \ - $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \ - $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \ - $(HOLBADIR)/src/theory/bir \ - $(HOLBADIR)/src/theory/bir-support \ - $(HOLBADIR)/src/theory/program_logic \ - $(HOLBADIR)/src/theory/tools/lifter \ - $(HOLBADIR)/src/theory/tools/backlifter \ - $(HOLBADIR)/src/tools/lifter \ - $(HOLBADIR)/src/tools/backlifter \ - $(HOLBADIR)/src/tools/exec \ - $(HOLBADIR)/src/tools/comp \ - $(HOLBADIR)/src/tools/wp \ - $(HOLBADIR)/src/tools/backlifter \ - $(HOLBADIR)/src/tools/symbexec \ - $(HOLBADIR)/src/tools/symbexec/examples/common \ - $(HOLBADIR)/src - -all: $(DEFAULT_TARGETS) -.PHONY: all - -ifdef POLY -ifndef HOLBA_POLYML_HEAPLESS -HOLHEAP = $(HOLBADIR)/src/holba-heap -endif -endif diff --git a/examples/riscv/kernel-trap-entry/kernel.da b/examples/riscv/kernel-trap-entry/kernel.da deleted file mode 100644 index 51405f6dd..000000000 --- a/examples/riscv/kernel-trap-entry/kernel.da +++ /dev/null @@ -1,52 +0,0 @@ - -build/qemu_virt_norvc/kernel.elf: file format elf64-littleriscv - - -Disassembly of section .text: - -00000000800000e0 : - 800000e0: 34051573 csrrw a0,mscratch,a0 - 800000e4: 00153823 sd ra,16(a0) - 800000e8: 00253c23 sd sp,24(a0) - 800000ec: 02353023 sd gp,32(a0) - 800000f0: 02453423 sd tp,40(a0) - 800000f4: 02553823 sd t0,48(a0) - 800000f8: 02653c23 sd t1,56(a0) - 800000fc: 04753023 sd t2,64(a0) - 80000100: 04853423 sd s0,72(a0) - 80000104: 04953823 sd s1,80(a0) - 80000108: 06b53023 sd a1,96(a0) - 8000010c: 06c53423 sd a2,104(a0) - 80000110: 06d53823 sd a3,112(a0) - 80000114: 06e53c23 sd a4,120(a0) - 80000118: 08f53023 sd a5,128(a0) - 8000011c: 09053423 sd a6,136(a0) - 80000120: 09153823 sd a7,144(a0) - 80000124: 09253c23 sd s2,152(a0) - 80000128: 0b353023 sd s3,160(a0) - 8000012c: 0b453423 sd s4,168(a0) - 80000130: 0b553823 sd s5,176(a0) - 80000134: 0b653c23 sd s6,184(a0) - 80000138: 0d753023 sd s7,192(a0) - 8000013c: 0d853423 sd s8,200(a0) - 80000140: 0d953823 sd s9,208(a0) - 80000144: 0da53c23 sd s10,216(a0) - 80000148: 0fb53023 sd s11,224(a0) - 8000014c: 0fc53423 sd t3,232(a0) - 80000150: 0fd53823 sd t4,240(a0) - 80000154: 0fe53c23 sd t5,248(a0) - 80000158: 11f53023 sd t6,256(a0) - 8000015c: 34102373 csrr t1,mepc - 80000160: 340023f3 csrr t2,mscratch - 80000164: 00653423 sd t1,8(a0) - 80000168: 04753c23 sd t2,88(a0) - 8000016c: 00005197 auipc gp,0x5 - 80000170: 69818193 addi gp,gp,1688 # 80005804 <__global_pointer$> - 80000174: 00006117 auipc sp,0x6 - 80000178: 28c10113 addi sp,sp,652 # 80006400 - 8000017c: f14022f3 csrr t0,mhartid - 80000180: 00a29293 slli t0,t0,0xa - 80000184: 40510133 sub sp,sp,t0 - 80000188: 342025f3 csrr a1,mcause - 8000018c: 34302673 csrr a2,mtval - 80000190: 238040ef jal 800043c8 diff --git a/examples/riscv/kernel-trap-entry/kernelScript.sml b/examples/riscv/kernel-trap-entry/kernelScript.sml deleted file mode 100644 index aa96c12a8..000000000 --- a/examples/riscv/kernel-trap-entry/kernelScript.sml +++ /dev/null @@ -1,21 +0,0 @@ -open HolKernel Parse; - -open bir_lifter_interfaceLib; -open birs_auxLib; - -val _ = Parse.current_backend := PPBackEnd.vt100_terminal; -val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2; - -val _ = new_theory "kernel"; - -val _ = lift_da_and_store "kernel" "kernel.da" da_riscv - ((Arbnum.fromInt 0x800000e0), (Arbnum.fromInt 0x80000194)); - -(* ----------------------------------------- *) -(* Program variable definitions and theorems *) -(* ----------------------------------------- *) - -val bir_prog_def = DB.fetch "-" "bir_kernel_prog_def"; -val _ = gen_prog_vars_birenvtyl_defthms "kernel" bir_prog_def; - -val _ = export_theory ();