RISC-V backlifting and examples

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/swap/Holmakefile

@@ -8,7 +8,12 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/tools/lifter \
-           $(HOLBADIR)/src/tools/exec
+           $(HOLBADIR)/src/tools/exec \
+           $(HOLBADIR)/src/theory/tools/backlifter \
+           $(HOLBADIR)/src/tools/comp \
+           $(HOLBADIR)/src/tools/wp \
+           $(HOLBADIR)/src/tools/backlifter \
+           $(HOLBADIR)/examples/tutorial/support
 
 all: $(DEFAULT_TARGETS)
 .PHONY: all

examples/riscv/swap/swap_propScript.sml

@@ -1,25 +1,33 @@
 open HolKernel boolLib Parse bossLib;
 
-open bir_programSyntax bir_program_labelsTheory bir_immTheory;
+(* FIXME: needed to avoid quse errors *)
+open m0_stepLib;
 
-open swapTheory;
+open bir_programSyntax bir_program_labelsTheory;
+open bir_immTheory bir_valuesTheory bir_expTheory;
+open bir_tsTheory bir_bool_expTheory;
 
-val _ = new_theory "swap_prop";
+open bir_riscv_backlifterTheory;
+open bir_backlifterLib;
+open bir_compositionLib;
+
+open bir_wpLib bir_wp_expLib;
+open bir_wpTheory bir_htTheory;
+open bir_wp_interfaceLib;
 
-val blocks = (fst o listSyntax.dest_list o dest_BirProgram o snd o dest_eq o concl o EVAL) ``bir_swap_prog``;
+open tutorial_smtSupportLib;
 
-(el 1)blocks;
-(el 2)blocks;
+open swapTheory;
 
-bir_swap_riscv_lift_THM;
+val _ = new_theory "swap_prop";
 
 Definition swap_mem_spec_def:
  swap_mem_spec ms =
- let ms'_mem8 = (riscv_mem_store_word (ms.c_gpr ms.procID 0w)
-   (riscv_mem_load_word ms.MEM8 (ms.c_gpr ms.procID 1w)) ms.MEM8)
+ let ms'_mem8 = (riscv_mem_store_dword (ms.c_gpr ms.procID 0w)
+   (riscv_mem_load_dword ms.MEM8 (ms.c_gpr ms.procID 1w)) ms.MEM8)
  in
-   (riscv_mem_store_word (ms.c_gpr ms.procID 1w)
-    (riscv_mem_load_word ms.MEM8 (ms.c_gpr ms.procID 0w)) ms'_mem8)
+   (riscv_mem_store_dword (ms.c_gpr ms.procID 1w)
+    (riscv_mem_load_dword ms.MEM8 (ms.c_gpr ms.procID 0w)) ms'_mem8)
 End
 
 Definition swap_spec_output_def:
@@ -30,7 +38,85 @@ Definition swap_spec_def:
  swap_spec ms ms' : bool = (ms'.MEM8 = swap_mem_spec ms)
 End
 
-(* run symbolic execution of BIR to get two symbolic states  *)
-(* connect this back to the riscv state via the lifting theorem *)
+Definition riscv_swap_pre_def:
+ riscv_swap_pre (m : riscv_state) = F
+End
+
+Definition riscv_swap_post_def:
+ riscv_swap_post (m : riscv_state) = T
+End
+
+Definition bir_swap_pre_def:
+  bir_swap_pre : bir_exp_t = bir_exp_false
+End
+
+Definition bir_swap_post_def:
+ bir_swap_post : bir_exp_t = bir_exp_true
+End
+
+Theorem swap_riscv_pre_imp_bir_pre_thm:
+ bir_pre_riscv_to_bir riscv_swap_pre bir_swap_pre
+Proof
+ EVAL_TAC >> rw []
+QED
+
+Theorem swap_riscv_post_imp_bir_post_thm:
+ !ls. bir_post_bir_to_riscv riscv_swap_post (\l. bir_swap_post) ls
+Proof
+ EVAL_TAC >> rw []
+QED
+
+val prog_tm = (lhs o concl) bir_swap_prog_def;
+val prefix = "swap_entry_";
+val first_block_label_tm = ``BL_Address (Imm64 0w)``;
+val ending_set = ``{BL_Address (Imm64 20w)}``;
+val postcond_tm = ``\l : bir_label_t . if l = BL_Address (Imm64 20w) then bir_swap_post else bir_exp_false``;
+val defs = [bir_swap_prog_def, bir_swap_post_def, bir_swap_pre_def, type_of_bir_exp_def,
+            bir_exp_false_def, bir_exp_true_def, BType_Bool_def,bir_is_bool_exp_def,
+            type_of_bir_imm_def];
+
+val (bir_swap_entry_ht, bir_swap_entry_wp_tm) =
+  bir_obtain_ht prog_tm first_block_label_tm
+                ending_set ending_set_to_sml_list
+                postcond_tm postcond_exp_from_label
+                prefix defs;
+
+Definition bir_swap_entry_wp_def:
+ bir_swap_entry_wp = ^bir_swap_entry_wp_tm
+End
+val _ = save_thm("bir_swap_entry_ht", bir_swap_entry_ht);
+
+val bir_swap_pre_tm = (lhs o concl) bir_swap_pre_def;
+val bir_swap_pre_imp = bimp (bir_swap_pre_tm, bir_swap_entry_wp_tm);
+val bir_swap_pre_imp_taut_thm = prove_exp_is_taut bir_swap_pre_imp;
+
+val bir_cont_swap =
+  bir_exec_to_labels_triple_to_bir_cont_predset bir_swap_entry_ht bir_swap_pre_imp_taut_thm;
+val _= save_thm ("bir_cont_swap", bir_cont_swap);
+
+(* For debugging:
+
+val bir_ct = bir_cont_swap;
+val prog_bin = ``bir_swap_progbin``;
+val riscv_pre = ``riscv_swap_pre``;
+val riscv_post = ``riscv_swap_post``;
+val bir_prog_def = bir_swap_prog_def;
+val bir_pre_defs = [bir_swap_pre_def]
+val bir_pre1_def = bir_swap_pre_def;
+val riscv_pre_imp_bir_pre_thm = swap_riscv_pre_imp_bir_pre_thm;
+val bir_post_defs = [bir_swap_post_def];
+val riscv_post_imp_bir_post_thm = swap_riscv_post_imp_bir_post_thm;
+val bir_is_lifted_prog_thm = bir_swap_riscv_lift_THM;
+*)
+
+val riscv_swap_contract_thm = save_thm("riscv_swap_contract_thm",
+ get_riscv_contract_sing
+  bir_cont_swap
+  ``bir_swap_progbin``
+  ``riscv_swap_pre`` ``riscv_swap_post`` bir_swap_prog_def
+  [bir_swap_pre_def]
+  bir_swap_pre_def swap_riscv_pre_imp_bir_pre_thm
+  [bir_swap_post_def] swap_riscv_post_imp_bir_post_thm
+  bir_swap_riscv_lift_THM);
 
 val _ = export_theory ();

examples/riscv/test-riscv.sml

@@ -0,0 +1,41 @@
+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)
+  ``;
+
+val _ = print_and_check_thm
+  "swap RISC-V backlifted theorem"
+  riscv_swap_contract_thm
+  ``riscv_cont
+     bir_swap_progbin
+     0w {20w}
+     riscv_swap_pre riscv_swap_post``;

examples/tutorial/4-bir-to-arm/tutorial_bir_to_armScript.sml

@@ -25,7 +25,7 @@ open bir_inst_liftingHelpersLib;
 
 (* Code specific for the example *)
 open HolBASimps;
-open bir_backlifterTheory;
+open bir_arm8_backlifterTheory;
 open bslSyntax;
 
 val _ = new_theory "tutorial_bir_to_arm";