mod2 riscv example

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

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

examples/riscv/mod2/mod2.c

@@ -0,0 +1,7 @@
+#include <stdint.h>
+
+uint64_t mod2(uint64_t * i) {
+  uint64_t j;
+  j =  * i % 2;
+  return j;
+}

examples/riscv/mod2/mod2.da

@@ -0,0 +1,10 @@
+
+mod2.o:     file format elf64-littleriscv
+
+
+Disassembly of section .text:
+
+0000000000000000 <mod2>:
+   0:	00053503          	ld	a0,0(a0)
+   4:	00157513          	andi	a0,a0,1
+   8:	00008067          	ret

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 ();

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 ();

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 ();

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)
+  ``;