From 0743bb140ae8510cb2b5848a46dc8a1468b1f653 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Wed, 21 Feb 2024 23:57:36 +0100 Subject: [PATCH] mod2 riscv example --- examples/riscv/Holmakefile | 14 ++++++++ examples/riscv/mod2/Holmakefile | 14 ++++++++ examples/riscv/mod2/mod2.c | 7 ++++ examples/riscv/mod2/mod2.da | 10 ++++++ examples/riscv/mod2/mod2Script.sml | 15 +++++++++ .../riscv/mod2/mod2_backliftingScript.sml | 23 +++++++++++++ examples/riscv/mod2/mod2_propScript.sml | 28 ++++++++++++++++ examples/riscv/test-riscv.sml | 33 +++++++++++++++++++ 8 files changed, 144 insertions(+) create mode 100644 examples/riscv/Holmakefile create mode 100644 examples/riscv/mod2/Holmakefile create mode 100644 examples/riscv/mod2/mod2.c create mode 100644 examples/riscv/mod2/mod2.da create mode 100644 examples/riscv/mod2/mod2Script.sml create mode 100644 examples/riscv/mod2/mod2_backliftingScript.sml create mode 100644 examples/riscv/mod2/mod2_propScript.sml create mode 100644 examples/riscv/test-riscv.sml diff --git a/examples/riscv/Holmakefile b/examples/riscv/Holmakefile new file mode 100644 index 000000000..f750e3ab1 --- /dev/null +++ b/examples/riscv/Holmakefile @@ -0,0 +1,14 @@ +INCLUDES = $(HOLBADIR)/examples/riscv/swap \ + $(HOLBADIR)/examples/riscv/isqrt \ + $(HOLBADIR)/examples/riscv/mod2 + +all: $(DEFAULT_TARGETS) test-riscv.exe +.PHONY: all + +test-riscv.exe: test-riscv.uo + $(HOLMOSMLC) -o $@ $< + +test: test-riscv.exe + ./test-riscv.exe + +EXTRA_CLEANS = test-riscv.exe diff --git a/examples/riscv/mod2/Holmakefile b/examples/riscv/mod2/Holmakefile new file mode 100644 index 000000000..2e1adef05 --- /dev/null +++ b/examples/riscv/mod2/Holmakefile @@ -0,0 +1,14 @@ +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 \ + $(HOLDIR)/examples/l3-machine-code/riscv/model \ + $(HOLDIR)/examples/l3-machine-code/riscv/step \ + $(HOLBADIR)/src/theory/bir \ + $(HOLBADIR)/src/theory/bir-support \ + $(HOLBADIR)/src/tools/lifter \ + $(HOLBADIR)/src/tools/backlifter + +all: $(DEFAULT_TARGETS) +.PHONY: all diff --git a/examples/riscv/mod2/mod2.c b/examples/riscv/mod2/mod2.c new file mode 100644 index 000000000..0784cb2e5 --- /dev/null +++ b/examples/riscv/mod2/mod2.c @@ -0,0 +1,7 @@ +#include + +uint64_t mod2(uint64_t * i) { + uint64_t j; + j = * i % 2; + return j; +} diff --git a/examples/riscv/mod2/mod2.da b/examples/riscv/mod2/mod2.da new file mode 100644 index 000000000..88e58dd47 --- /dev/null +++ b/examples/riscv/mod2/mod2.da @@ -0,0 +1,10 @@ + +mod2.o: file format elf64-littleriscv + + +Disassembly of section .text: + +0000000000000000 : + 0: 00053503 ld a0,0(a0) + 4: 00157513 andi a0,a0,1 + 8: 00008067 ret diff --git a/examples/riscv/mod2/mod2Script.sml b/examples/riscv/mod2/mod2Script.sml new file mode 100644 index 000000000..84122e56c --- /dev/null +++ b/examples/riscv/mod2/mod2Script.sml @@ -0,0 +1,15 @@ +open HolKernel Parse; + +(* FIXME: needed to avoid quse errors *) +open m0_stepLib; + +open bir_lifter_interfaceLib; + +val _ = Parse.current_backend := PPBackEnd.vt100_terminal; +val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2; + +val _ = new_theory "mod2"; + +val _ = lift_da_and_store "mod2" "mod2.da" da_riscv ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000)); + +val _ = export_theory (); diff --git a/examples/riscv/mod2/mod2_backliftingScript.sml b/examples/riscv/mod2/mod2_backliftingScript.sml new file mode 100644 index 000000000..945eec5b9 --- /dev/null +++ b/examples/riscv/mod2/mod2_backliftingScript.sml @@ -0,0 +1,23 @@ +open HolKernel Parse boolLib bossLib; + +(* FIXME: needed to avoid quse errors *) +open m0_stepLib; + +open bir_backlifterLib; + +val _ = new_theory "mod2_backlifting"; + +(* +val arm_add_reg_contract_thm = + save_thm("arm_add_reg_contract_thm", + get_arm8_contract_sing bir_add_reg_ct ``bir_add_reg_progbin`` ``arm8_add_reg_pre`` + ``arm8_add_reg_post`` bir_add_reg_prog_def + [bir_add_reg_contract_1_pre_def, bir_add_reg_pre_def] + bir_add_reg_contract_1_pre_def arm8_pre_imp_bir_pre_thm + [bir_add_reg_contract_4_post_def] arm8_post_imp_bir_post_thm + bir_prog_add_regTheory.bir_add_reg_arm8_lift_THM); + +|- arm8_cont bir_add_reg_progbin 28w {72w} arm8_add_reg_pre arm8_add_reg_post +*) + +val _ = export_theory (); diff --git a/examples/riscv/mod2/mod2_propScript.sml b/examples/riscv/mod2/mod2_propScript.sml new file mode 100644 index 000000000..9d2aef3d0 --- /dev/null +++ b/examples/riscv/mod2/mod2_propScript.sml @@ -0,0 +1,28 @@ +open HolKernel boolLib Parse bossLib; + +open BasicProvers simpLib metisLib; + +open numTheory arithmeticTheory int_bitwiseTheory pairTheory combinTheory wordsTheory; + +(* FIXME: needed to avoid quse errors *) +open m0_stepLib; + +open bir_inst_liftingTheory; +open bir_lifting_machinesTheory; +open bir_lifting_machinesLib bir_lifting_machinesLib_instances; + +open bir_programSyntax bir_program_labelsTheory bir_immTheory; + +open mod2Theory; + +val _ = new_theory "mod2_prop"; + +(* top-level relation between pre and post RISC-V states *) +Definition mod2_spec_def: + mod2_spec_def ms ms' : bool = + let input = ms.c_gpr ms.procID 0w in + let output = ms'.c_gpr ms'.procID 0w in + (w2n output) = (w2n input) MOD 2 +End + +val _ = export_theory (); diff --git a/examples/riscv/test-riscv.sml b/examples/riscv/test-riscv.sml new file mode 100644 index 000000000..aa63856d7 --- /dev/null +++ b/examples/riscv/test-riscv.sml @@ -0,0 +1,33 @@ +open HolKernel Parse boolLib bossLib; + +val _ = Parse.current_backend := PPBackEnd.vt100_terminal; +val _ = Globals.show_tags := true; + +open wordsTheory; + +open bir_programSyntax bir_program_labelsTheory bir_immTheory; + +open swapTheory swap_propTheory; +open isqrtTheory isqrt_propTheory; +open mod2Theory mod2_propTheory; + +fun print_and_check_thm name thm t_concl = + let + val _ = print (name ^ ":\n"); + val _ = print "===============================\n"; + val _ = (Hol_pp.print_thm thm; print "\n"); + val _ = if identical (concl thm) t_concl then () else + raise Fail "print_and_check_thm::conclusion is not as expected" + val _ = print "\n\n"; + in + () + end; + +val _ = print_and_check_thm + "swap RISC-V lift theorem" + bir_swap_riscv_lift_THM + `` + bir_is_lifted_prog riscv_bmr (WI_end (0w : word64) (0x1000000w : word64)) + bir_swap_progbin + (bir_swap_prog : 'observation_type bir_program_t) + ``;