kernel trap entry subroutine lifts fully

kth-step · Dec 17, 2024 · 61e2074 · 61e2074
1 parent 4f885f2
commit 61e2074
Show file tree

Hide file tree

Showing 3 changed files with 103 additions and 0 deletions.
diff --git a/examples/riscv/kernel-trap-entry/Holmakefile b/examples/riscv/kernel-trap-entry/Holmakefile
@@ -0,0 +1,30 @@
+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
@@ -0,0 +1,52 @@
+
+build/qemu_virt_norvc/kernel.elf:     file format elf64-littleriscv
+
+
+Disassembly of section .text:
+
+00000000800000e0 <trap_entry>:
+    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 <slots>
+    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 <trap_handler>
diff --git a/examples/riscv/kernel-trap-entry/kernelScript.sml b/examples/riscv/kernel-trap-entry/kernelScript.sml
@@ -0,0 +1,21 @@
+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 ();