Add arm8 bootstrap

Support for bootstrapping on arm8 has been added. It is nearly identical
to the bootstrap scripts for x64, with the exception that "x64" has been
replaced with "arm8". Currently the REPL is only supported on x64, so
the `EVAL` flag is always disabled for arm8, even on Linux.

.gitignore

@@ -16,6 +16,7 @@
 *.S
 
 # Generated tarball
+cake-arm-64.tar.gz
 cake-x64-64.tar.gz
 config_enc_str.txt
 

Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = developers compiler/bootstrap/compilation/x64/64/proofs
+INCLUDES = developers compiler/bootstrap/compilation/x64/64/proofs compiler/bootstrap/compilation/arm8/64/proofs
 
 all: $(DEFAULT_TARGETS) README.md cake-x64-64.tar.gz
 .PHONY: all
@@ -10,3 +10,6 @@ README.md: developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)
 
 cake-x64-64.tar.gz: compiler/bootstrap/compilation/x64/64/cake-x64-64.tar.gz
  $(CP) $< $@
+
+cake-arm8-64.tar.gz: compiler/bootstrap/compilation/arm8/64/cake-arm8-64.tar.gz
+ $(CP) $< $@

compiler/bootstrap/compilation/arm8/64/Holmakefile

@@ -0,0 +1,23 @@
+ARCH = arm8
+WORD_SIZE = 64
+INCLUDES = $(CAKEMLDIR)/semantics $(CAKEMLDIR)/basis ../../../.. $(CAKEMLDIR)/unverified/sexpr-bootstrap \
+ ../../../../encoders/asm ../../../../encoders/$(ARCH)\
+ ../../../../backend/$(ARCH) ../../../../backend/serialiser ../../../translation
+
+all: $(DEFAULT_TARGETS) README.md cake-$(ARCH)-$(WORD_SIZE).tar.gz
+.PHONY: all
+
+README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
+DIRS = $(wildcard */)
+README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
+ $(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
+
+cake.S: *$(ARCH)BootstrapScript.sml
+config_enc_str.txt: *$(ARCH)_config_encScript.sml
+
+cake-sexpr-64: *sexprBootstrap64Script.sml
+
+cake-$(ARCH)-$(WORD_SIZE).tar.gz: cake.S basis_ffi.c Makefile hello.cml how-to.md cake-sexpr-64 config_enc_str.txt candle_boot.ml repl_boot.cml
+ tar -chzf $@ --transform='s|^|cake-$(ARCH)-$(WORD_SIZE)/|' cake.S basis_ffi.c Makefile hello.cml how-to.md cake-sexpr-64 config_enc_str.txt candle_boot.ml repl_boot.cml
+
+EXTRA_CLEANS = cake.S cake-$(ARCH)-$(WORD_SIZE).tar.gz cake test-hello.cake output expected_output

compiler/bootstrap/compilation/arm8/64/Makefile

@@ -0,0 +1 @@
+../Makefile

compiler/bootstrap/compilation/arm8/64/README.md

@@ -0,0 +1,45 @@
+This directory contains scripts that compile the CakeML compiler
+inside the logic to produce the verified machine code version of the
+64-bit compiler.
+
+[basis_ffi.c](basis_ffi.c):
+Implements the foreign function interface (FFI) used in the CakeML basis
+library, as a thin wrapper around the relevant system calls.
+
+[hello.cml](hello.cml):
+A simple hello world program in CakeML
+
+[proofs](proofs):
+This directory contains the end-to-end correctness theorem for the
+64-bit version of the CakeML compiler.
+
+[repl_boot.cml](repl_boot.cml):
+This file gives the CakeML REPL multi-line input and file loading
+capabilities.
+
+[sexprBootstrap32Script.sml](sexprBootstrap32Script.sml):
+Produces an sexp print-out of the bootstrap translated compiler
+definition for the 32-bit version of the compiler.
+
+[sexprBootstrap64Script.sml](sexprBootstrap64Script.sml):
+Produces an sexp print-out of the bootstrap translated compiler
+definition for the 64-bit version of the compiler.
+
+[test-hello.cml](test-hello.cml):
+A hello world program used for testing that the bootstrapped
+compiler was built succesfully.
+
+[to_dataBootstrapScript.sml](to_dataBootstrapScript.sml):
+Evaluate the 32-bit version of the compiler down to a DataLang
+program.
+
+[to_lab_arm8BootstrapScript.sml](to_lab_arm8BootstrapScript.sml):
+Evaluate the 64-bit version of the compiler down to a LabLang
+program (an assembly program).
+
+[arm8BootstrapScript.sml](arm8BootstrapScript.sml):
+Evaluate the final part of the 64-bit version of the compiler
+into machine code for arm8.
+
+[arm8_config_encScript.sml](arm8_config_encScript.sml):
+Encoding of compiler state

compiler/bootstrap/compilation/arm8/64/arm8BootstrapScript.sml

@@ -0,0 +1,292 @@
+(*
+ Evaluate the final part of the 64-bit version of the compiler
+ into machine code for arm8.
+*)
+open preamble to_lab_arm8BootstrapTheory compilationLib
+
+val _ = new_theory "arm8Bootstrap";
+
+val () = ml_translatorLib.reset_translation();
+
+(*
+ val lab_prog_def =
+ let
+ val (ls,ty) = to_lab_arm8BootstrapTheory.lab_prog_def |> rconc |> listSyntax.dest_list
+ val ls' = listSyntax.mk_list(List.take(List.drop(ls,2000),40),ty)
+ in mk_thm([],``lab_prog = ^ls'``) end
+*)
+
+val filename = "cake.S"
+
+val bootstrap_thm =
+ compilationLib.cbv_to_bytes_arm8
+ stack_to_lab_thm lab_prog_def
+ "cake_code" "cake_data" "cake_config" filename;
+
+val cake_compiled = save_thm("cake_compiled", bootstrap_thm);
+
+(* avoid saving the long list of bytes in the Theory.sml file
+ they can only be found in the exported cake.S file *)
+val _ = Theory.delete_binding "cake_code_def";
+
+val _ = export_theory();
+
+(*
+val Label_tm = ela2 |> SPEC_ALL |> concl |> lhs |> rator |> rand |> rator |> rand |> repeat rator;
+val Asm_tm = ela3 |> SPEC_ALL |> concl |> lhs |> rator |> rand |> rator |> rand |> repeat rator;
+val LabAsm_tm = ela4 |> SPEC_ALL |> concl |> lhs |> rator |> rand |> rator |> rand |> repeat rator;
+
+fun enc_lines_again_rule labs_def =
+let
+ fun f th = let
+ val ls = th |> rconc |> rator |> rand
+ in if listSyntax.is_nil ls then
+ CONV_RULE(RAND_CONV (REWR_CONV ela1 THENC RATOR_CONV(RAND_CONV eval))) th
+ else let
+ val tm = listSyntax.dest_cons ls |> #1 |> repeat rator
+ val th =
+ if same_const Label_tm tm then
+ CONV_RULE(RAND_CONV (REWR_CONV ela2 THENC add_pos_conv)) th
+ else if same_const Asm_tm tm then
+ CONV_RULE(RAND_CONV (REWR_CONV ela3 THENC add_pos_conv)) th
+ else
+ let
+ val _ = assert (same_const LabAsm_tm) tm
+ val th = CONV_RULE(RAND_CONV (
+ REWR_CONV ela4 THENC
+ RAND_CONV (RATOR_CONV(RAND_CONV(REWR_CONV labs_def)) THENC eval) THENC
+ REWR_CONV LET_THM THENC BETA_CONV THENC
+ RATOR_CONV(RATOR_CONV(RAND_CONV eval)))) th
+ val tm = th |> rconc |> rator |> rator |> rand
+ in
+ if same_const T tm then
+ CONV_RULE(RAND_CONV (REWR_CONV COND_T THENC add_pos_conv)) th
+ else (assert (same_const F) tm;
+ CONV_RULE(RAND_CONV (REWR_CONV COND_F THENC
+ RAND_CONV eval THENC REWR_CONV LET_THM THENC BETA_CONV THENC
+ RAND_CONV eval THENC REWR_CONV LET_THM THENC BETA_CONV THENC
+ add_pos_conv THENC
+ RAND_CONV(RAND_CONV(RAND_CONV eval THENC REWR_CONV AND_T)))) th)
+ end
+ in
+ f th
+ end
+ end
+in f end
+*)
+
+(*
+fun enc_lines_again_rule labs_def =
+let
+ fun f th =
+ let
+ val (th,b) =
+ (* Asm *)
+ (CONV_RULE(RAND_CONV (REWR_CONV ela3 THENC add_pos_conv)) th,true)
+ handle HOL_ERR _ =>
+ (* Label *)
+ (CONV_RULE(RAND_CONV (REWR_CONV ela2 THENC add_pos_conv)) th,true)
+ handle HOL_ERR _ =>
+ (* LabAsm *)
+ let
+ val th = CONV_RULE(RAND_CONV (
+ REWR_CONV ela4 THENC
+ RAND_CONV (RATOR_CONV(RAND_CONV(REWR_CONV labs_def)) THENC eval) THENC
+ let_CONV THENC
+ RATOR_CONV(RATOR_CONV(RAND_CONV eval)))) th
+ in
+ (* no offset update *)
+ (CONV_RULE(RAND_CONV (REWR_CONV COND_T THENC add_pos_conv)) th,true)
+ handle HOL_ERR _ =>
+ (* offset update *)
+ (CONV_RULE(RAND_CONV (REWR_CONV COND_F THENC
+ RAND_CONV eval THENC let_CONV THENC
+ RAND_CONV eval THENC let_CONV THENC
+ add_pos_conv THENC
+ RAND_CONV(RAND_CONV(RAND_CONV eval THENC REWR_CONV AND_T)))) th,true)
+ end
+ handle HOL_ERR _ =>
+ (* nil *)
+ (CONV_RULE(RAND_CONV (REWR_CONV ela1 THENC RATOR_CONV(RAND_CONV eval))) th,false)
+ in if b then f th else th end
+in f end
+
+fun enc_lines_again_conv labs_def = enc_lines_again_rule labs_def o REFL
+*)
+
+(*
+fun enc_lines_again_conv labs_def tm = tm |> (
+ IFC
+ ((REWR_CONV ela3 THENC add_pos_conv) ORELSEC
+ (REWR_CONV ela2 THENC add_pos_conv) ORELSEC
+ (REWR_CONV ela4 THENC
+ RAND_CONV (RATOR_CONV(RAND_CONV(REWR_CONV labs_def)) THENC eval) THENC
+ let_CONV THENC
+ RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
+ ((REWR_CONV COND_T THENC add_pos_conv) ORELSEC
+ (REWR_CONV COND_F THENC
+ RAND_CONV eval THENC let_CONV THENC
+ RAND_CONV eval THENC let_CONV THENC
+ add_pos_conv THENC
+ RAND_CONV(RAND_CONV(RAND_CONV eval THENC REWR_CONV AND_T))))))
+ (enc_lines_again_conv labs_def)
+ (REWR_CONV ela1 THENC RATOR_CONV(RAND_CONV eval)))
+*)
+
+(*
+fun enc_lines_again_conv labs_def tm = tm |> (
+ IFC
+ ((REWR_CONV ela3) ORELSEC
+ (REWR_CONV ela2) ORELSEC
+ (REWR_CONV ela4 THENC
+ RAND_CONV (RATOR_CONV(RAND_CONV(REWR_CONV labs_def)) THENC eval) THENC
+ let_CONV THENC
+ RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
+ ((REWR_CONV COND_T) ORELSEC
+ (REWR_CONV COND_F THENC
+ RAND_CONV eval THENC let_CONV THENC
+ RAND_CONV eval THENC let_CONV))))
+ (enc_lines_again_conv labs_def)
+ (REWR_CONV ela1 THENC eval))
+*)
+
+(*
+fun enc_lines_again_conv tm = tm |> (
+ IFC
+ ((REWR_CONV ela3) ORELSEC
+ (REWR_CONV ela2) ORELSEC
+ (REWR_CONV ela4 THENC
+ RAND_CONV eval THENC let_CONV THENC
+ RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
+ ((REWR_CONV COND_T) ORELSEC
+ (REWR_CONV COND_F THENC
+ RAND_CONV eval THENC let_CONV THENC
+ RAND_CONV eval THENC let_CONV))))
+ (enc_lines_again_conv)
+ (REWR_CONV ela1 THENC eval))
+*)
+
+(*
+fun enc_lines_again_conv tm = tm |> (
+ IFC
+ ((REWR_CONV ela3) ORELSEC
+ (REWR_CONV ela2) ORELSEC
+ (REWR_CONV ela4 THENC
+ RAND_CONV eval THENC let_CONV THENC
+ RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
+ COND_CONV THENC
+ TRY_CONV
+ (RAND_CONV eval THENC let_CONV THENC
+ RAND_CONV eval THENC let_CONV)))
+ (enc_lines_again_conv)
+ (REWR_CONV ela1 THENC eval))
+*)
+
+(*
+fun enc_lines_again_conv tm = tm |> (
+ IFC
+ ((REWR_CONV ela3) ORELSEC
+ (REWR_CONV ela2) ORELSEC
+ (REWR_CONV ela4 THENC
+ RAND_CONV eval THENC let_CONV THENC
+ RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
+ COND_CONV THENC REPEATC let_CONV))
+ (enc_lines_again_conv)
+ (REWR_CONV ela1 THENC eval))
+*)
+
+(*
+val encoded_prog_thm_prefix =
+ let
+ val (car,cdr) = dest_comb (concl encoded_prog_thm)
+ val (ls,ty) = listSyntax.dest_list cdr
+ val ls' = List.take(ls,10)
+ in mk_thm([],mk_comb(car,listSyntax.mk_list(ls',ty))) end
+val encoded_prog_defs_prefix =
+ List.take(List.rev encoded_prog_defs,10)
+
+(* rule using exceptions *)
+val enc_secs_again_thm =
+ tm13 |> timez "enc_secs_again" (
+ RAND_CONV(REWR_CONV encoded_prog_thm_prefix) THENC
+ enc_secs_again_conv
+ "enc_again_" (enc_lines_again_conv computed_labs_def) 0
+ encoded_prog_defs_prefix)
+2m15s
+
+(* custom conv *)
+val enc_secs_again_thm =
+ tm13 |> timez "enc_secs_again" (
+ RAND_CONV(REWR_CONV encoded_prog_thm_prefix) THENC
+ enc_secs_again_conv
+ "enc_again_" (enc_lines_again_conv computed_labs_def) 0
+ encoded_prog_defs_prefix)
+2m17s
+
+(* custom conv with IFC *)
+val enc_secs_again_thm =
+ tm13 |> timez "enc_secs_again" (
+ RAND_CONV(REWR_CONV encoded_prog_thm_prefix) THENC
+ enc_secs_again_conv
+ "enc_again_" (enc_lines_again_conv computed_labs_def) 0
+ encoded_prog_defs_prefix)
+2m18s
+
+val enc_secs_again_thm =
+ tm13 |> timez "enc_secs_again" (
+ RAND_CONV(REWR_CONV encoded_prog_thm_prefix) THENC
+ enc_secs_again_conv
+ "enc_again_"
+ (PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC eval)
+ 0
+ encoded_prog_defs_prefix)
+14.4s
+
+val (dth::dths) = encoded_prog_defs_prefix
+val tm = tm13 |> RAND_CONV(REWR_CONV encoded_prog_thm_prefix) |> rconc
+val th1 = tm |> (REWR_CONV esc THENC (RAND_CONV(RATOR_CONV(RAND_CONV(REWR_CONV dth)))))
+val tm = th1 |> rconc |> rand
+
+val test1 =
+ time (PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC eval) tm
+1.1s
+
+val th = REFL tm
+
+(* rule with exceptions *)
+val test2 =
+ time (enc_lines_again_conv computed_labs_def) tm
+17.1s
+val check = rconc test1 = rconc test2
+
+(* custom conv with IFC *)
+val test3 =
+ time (enc_lines_again_conv computed_labs_def) tm
+30.6s
+val check = rconc test1 = rconc test3
+
+(* custom conv with IFC and delayed leaves *)
+val test4 =
+ time (enc_lines_again_conv computed_labs_def) tm
+31.3s
+val check = rconc test1 = rconc test4
+
+(* custom conv with labs expanded *)
+val test5 =
+ time (PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC enc_lines_again_conv) tm
+21.2s
+val check = rconc test1 = rconc test5
+
+(* custom conv with labs expanded using COND_CONV *)
+val test6 =
+ time (PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC enc_lines_again_conv) tm
+19.4s
+val check = rconc test1 = rconc test6
+
+(* custom conv with labs expanded using COND_CONV and deferring all computations *)
+val test7 =
+ time (PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC enc_lines_again_conv) tm
+19.6s
+val check = rconc test1 = rconc test7
+
+*)