Skip to content

Commit 4d60801

Browse files
LudvikGaloisLudvikGalois
committed
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.
1 parent c2d3143 commit 4d60801

28 files changed

+2360
-1
lines changed

‎.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
*.S
1717

1818
# Generated tarball
19+
cake-arm-64.tar.gz
1920
cake-x64-64.tar.gz
2021
config_enc_str.txt
2122

‎Holmakefile

+4-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
INCLUDES = developers compiler/bootstrap/compilation/x64/64/proofs
1+
INCLUDES = developers compiler/bootstrap/compilation/x64/64/proofs compiler/bootstrap/compilation/arm8/64/proofs
22

33
all: $(DEFAULT_TARGETS) README.md cake-x64-64.tar.gz
44
.PHONY: all
@@ -10,3 +10,6 @@ README.md: developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)
1010

1111
cake-x64-64.tar.gz: compiler/bootstrap/compilation/x64/64/cake-x64-64.tar.gz
1212
$(CP) $< $@
13+
14+
cake-arm8-64.tar.gz: compiler/bootstrap/compilation/arm8/64/cake-arm8-64.tar.gz
15+
$(CP) $< $@

‎compiler/bootstrap/compilation/arm8/64/Holmakefile

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
ARCH = arm8
2+
WORD_SIZE = 64
3+
INCLUDES = $(CAKEMLDIR)/semantics $(CAKEMLDIR)/basis ../../../.. $(CAKEMLDIR)/unverified/sexpr-bootstrap \
4+
../../../../encoders/asm ../../../../encoders/$(ARCH)\
5+
../../../../backend/$(ARCH) ../../../../backend/serialiser ../../../translation
6+
7+
all: $(DEFAULT_TARGETS) README.md cake-$(ARCH)-$(WORD_SIZE).tar.gz
8+
.PHONY: all
9+
10+
README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
11+
DIRS = $(wildcard */)
12+
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
13+
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
14+
15+
cake.S: *$(ARCH)BootstrapScript.sml
16+
config_enc_str.txt: *$(ARCH)_config_encScript.sml
17+
18+
cake-sexpr-64: *sexprBootstrap64Script.sml
19+
20+
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
21+
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
22+
23+
EXTRA_CLEANS = cake.S cake-$(ARCH)-$(WORD_SIZE).tar.gz cake test-hello.cake output expected_output

‎compiler/bootstrap/compilation/arm8/64/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
../Makefile

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

+45
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
This directory contains scripts that compile the CakeML compiler
2+
inside the logic to produce the verified machine code version of the
3+
64-bit compiler.
4+
5+
[basis_ffi.c](basis_ffi.c):
6+
Implements the foreign function interface (FFI) used in the CakeML basis
7+
library, as a thin wrapper around the relevant system calls.
8+
9+
[hello.cml](hello.cml):
10+
A simple hello world program in CakeML
11+
12+
[proofs](proofs):
13+
This directory contains the end-to-end correctness theorem for the
14+
64-bit version of the CakeML compiler.
15+
16+
[repl_boot.cml](repl_boot.cml):
17+
This file gives the CakeML REPL multi-line input and file loading
18+
capabilities.
19+
20+
[sexprBootstrap32Script.sml](sexprBootstrap32Script.sml):
21+
Produces an sexp print-out of the bootstrap translated compiler
22+
definition for the 32-bit version of the compiler.
23+
24+
[sexprBootstrap64Script.sml](sexprBootstrap64Script.sml):
25+
Produces an sexp print-out of the bootstrap translated compiler
26+
definition for the 64-bit version of the compiler.
27+
28+
[test-hello.cml](test-hello.cml):
29+
A hello world program used for testing that the bootstrapped
30+
compiler was built succesfully.
31+
32+
[to_dataBootstrapScript.sml](to_dataBootstrapScript.sml):
33+
Evaluate the 32-bit version of the compiler down to a DataLang
34+
program.
35+
36+
[to_lab_arm8BootstrapScript.sml](to_lab_arm8BootstrapScript.sml):
37+
Evaluate the 64-bit version of the compiler down to a LabLang
38+
program (an assembly program).
39+
40+
[arm8BootstrapScript.sml](arm8BootstrapScript.sml):
41+
Evaluate the final part of the 64-bit version of the compiler
42+
into machine code for arm8.
43+
44+
[arm8_config_encScript.sml](arm8_config_encScript.sml):
45+
Encoding of compiler state

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

+292
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,292 @@
1+
(*
2+
Evaluate the final part of the 64-bit version of the compiler
3+
into machine code for arm8.
4+
*)
5+
open preamble to_lab_arm8BootstrapTheory compilationLib
6+
7+
val _ = new_theory "arm8Bootstrap";
8+
9+
val () = ml_translatorLib.reset_translation();
10+
11+
(*
12+
val lab_prog_def =
13+
let
14+
val (ls,ty) = to_lab_arm8BootstrapTheory.lab_prog_def |> rconc |> listSyntax.dest_list
15+
val ls' = listSyntax.mk_list(List.take(List.drop(ls,2000),40),ty)
16+
in mk_thm([],``lab_prog = ^ls'``) end
17+
*)
18+
19+
val filename = "cake.S"
20+
21+
val bootstrap_thm =
22+
compilationLib.cbv_to_bytes_arm8
23+
stack_to_lab_thm lab_prog_def
24+
"cake_code" "cake_data" "cake_config" filename;
25+
26+
val cake_compiled = save_thm("cake_compiled", bootstrap_thm);
27+
28+
(* avoid saving the long list of bytes in the Theory.sml file
29+
they can only be found in the exported cake.S file *)
30+
val _ = Theory.delete_binding "cake_code_def";
31+
32+
val _ = export_theory();
33+
34+
(*
35+
val Label_tm = ela2 |> SPEC_ALL |> concl |> lhs |> rator |> rand |> rator |> rand |> repeat rator;
36+
val Asm_tm = ela3 |> SPEC_ALL |> concl |> lhs |> rator |> rand |> rator |> rand |> repeat rator;
37+
val LabAsm_tm = ela4 |> SPEC_ALL |> concl |> lhs |> rator |> rand |> rator |> rand |> repeat rator;
38+
39+
fun enc_lines_again_rule labs_def =
40+
let
41+
fun f th = let
42+
val ls = th |> rconc |> rator |> rand
43+
in if listSyntax.is_nil ls then
44+
CONV_RULE(RAND_CONV (REWR_CONV ela1 THENC RATOR_CONV(RAND_CONV eval))) th
45+
else let
46+
val tm = listSyntax.dest_cons ls |> #1 |> repeat rator
47+
val th =
48+
if same_const Label_tm tm then
49+
CONV_RULE(RAND_CONV (REWR_CONV ela2 THENC add_pos_conv)) th
50+
else if same_const Asm_tm tm then
51+
CONV_RULE(RAND_CONV (REWR_CONV ela3 THENC add_pos_conv)) th
52+
else
53+
let
54+
val _ = assert (same_const LabAsm_tm) tm
55+
val th = CONV_RULE(RAND_CONV (
56+
REWR_CONV ela4 THENC
57+
RAND_CONV (RATOR_CONV(RAND_CONV(REWR_CONV labs_def)) THENC eval) THENC
58+
REWR_CONV LET_THM THENC BETA_CONV THENC
59+
RATOR_CONV(RATOR_CONV(RAND_CONV eval)))) th
60+
val tm = th |> rconc |> rator |> rator |> rand
61+
in
62+
if same_const T tm then
63+
CONV_RULE(RAND_CONV (REWR_CONV COND_T THENC add_pos_conv)) th
64+
else (assert (same_const F) tm;
65+
CONV_RULE(RAND_CONV (REWR_CONV COND_F THENC
66+
RAND_CONV eval THENC REWR_CONV LET_THM THENC BETA_CONV THENC
67+
RAND_CONV eval THENC REWR_CONV LET_THM THENC BETA_CONV THENC
68+
add_pos_conv THENC
69+
RAND_CONV(RAND_CONV(RAND_CONV eval THENC REWR_CONV AND_T)))) th)
70+
end
71+
in
72+
f th
73+
end
74+
end
75+
in f end
76+
*)
77+
78+
(*
79+
fun enc_lines_again_rule labs_def =
80+
let
81+
fun f th =
82+
let
83+
val (th,b) =
84+
(* Asm *)
85+
(CONV_RULE(RAND_CONV (REWR_CONV ela3 THENC add_pos_conv)) th,true)
86+
handle HOL_ERR _ =>
87+
(* Label *)
88+
(CONV_RULE(RAND_CONV (REWR_CONV ela2 THENC add_pos_conv)) th,true)
89+
handle HOL_ERR _ =>
90+
(* LabAsm *)
91+
let
92+
val th = CONV_RULE(RAND_CONV (
93+
REWR_CONV ela4 THENC
94+
RAND_CONV (RATOR_CONV(RAND_CONV(REWR_CONV labs_def)) THENC eval) THENC
95+
let_CONV THENC
96+
RATOR_CONV(RATOR_CONV(RAND_CONV eval)))) th
97+
in
98+
(* no offset update *)
99+
(CONV_RULE(RAND_CONV (REWR_CONV COND_T THENC add_pos_conv)) th,true)
100+
handle HOL_ERR _ =>
101+
(* offset update *)
102+
(CONV_RULE(RAND_CONV (REWR_CONV COND_F THENC
103+
RAND_CONV eval THENC let_CONV THENC
104+
RAND_CONV eval THENC let_CONV THENC
105+
add_pos_conv THENC
106+
RAND_CONV(RAND_CONV(RAND_CONV eval THENC REWR_CONV AND_T)))) th,true)
107+
end
108+
handle HOL_ERR _ =>
109+
(* nil *)
110+
(CONV_RULE(RAND_CONV (REWR_CONV ela1 THENC RATOR_CONV(RAND_CONV eval))) th,false)
111+
in if b then f th else th end
112+
in f end
113+
114+
fun enc_lines_again_conv labs_def = enc_lines_again_rule labs_def o REFL
115+
*)
116+
117+
(*
118+
fun enc_lines_again_conv labs_def tm = tm |> (
119+
IFC
120+
((REWR_CONV ela3 THENC add_pos_conv) ORELSEC
121+
(REWR_CONV ela2 THENC add_pos_conv) ORELSEC
122+
(REWR_CONV ela4 THENC
123+
RAND_CONV (RATOR_CONV(RAND_CONV(REWR_CONV labs_def)) THENC eval) THENC
124+
let_CONV THENC
125+
RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
126+
((REWR_CONV COND_T THENC add_pos_conv) ORELSEC
127+
(REWR_CONV COND_F THENC
128+
RAND_CONV eval THENC let_CONV THENC
129+
RAND_CONV eval THENC let_CONV THENC
130+
add_pos_conv THENC
131+
RAND_CONV(RAND_CONV(RAND_CONV eval THENC REWR_CONV AND_T))))))
132+
(enc_lines_again_conv labs_def)
133+
(REWR_CONV ela1 THENC RATOR_CONV(RAND_CONV eval)))
134+
*)
135+
136+
(*
137+
fun enc_lines_again_conv labs_def tm = tm |> (
138+
IFC
139+
((REWR_CONV ela3) ORELSEC
140+
(REWR_CONV ela2) ORELSEC
141+
(REWR_CONV ela4 THENC
142+
RAND_CONV (RATOR_CONV(RAND_CONV(REWR_CONV labs_def)) THENC eval) THENC
143+
let_CONV THENC
144+
RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
145+
((REWR_CONV COND_T) ORELSEC
146+
(REWR_CONV COND_F THENC
147+
RAND_CONV eval THENC let_CONV THENC
148+
RAND_CONV eval THENC let_CONV))))
149+
(enc_lines_again_conv labs_def)
150+
(REWR_CONV ela1 THENC eval))
151+
*)
152+
153+
(*
154+
fun enc_lines_again_conv tm = tm |> (
155+
IFC
156+
((REWR_CONV ela3) ORELSEC
157+
(REWR_CONV ela2) ORELSEC
158+
(REWR_CONV ela4 THENC
159+
RAND_CONV eval THENC let_CONV THENC
160+
RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
161+
((REWR_CONV COND_T) ORELSEC
162+
(REWR_CONV COND_F THENC
163+
RAND_CONV eval THENC let_CONV THENC
164+
RAND_CONV eval THENC let_CONV))))
165+
(enc_lines_again_conv)
166+
(REWR_CONV ela1 THENC eval))
167+
*)
168+
169+
(*
170+
fun enc_lines_again_conv tm = tm |> (
171+
IFC
172+
((REWR_CONV ela3) ORELSEC
173+
(REWR_CONV ela2) ORELSEC
174+
(REWR_CONV ela4 THENC
175+
RAND_CONV eval THENC let_CONV THENC
176+
RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
177+
COND_CONV THENC
178+
TRY_CONV
179+
(RAND_CONV eval THENC let_CONV THENC
180+
RAND_CONV eval THENC let_CONV)))
181+
(enc_lines_again_conv)
182+
(REWR_CONV ela1 THENC eval))
183+
*)
184+
185+
(*
186+
fun enc_lines_again_conv tm = tm |> (
187+
IFC
188+
((REWR_CONV ela3) ORELSEC
189+
(REWR_CONV ela2) ORELSEC
190+
(REWR_CONV ela4 THENC
191+
RAND_CONV eval THENC let_CONV THENC
192+
RATOR_CONV(RATOR_CONV(RAND_CONV eval)) THENC
193+
COND_CONV THENC REPEATC let_CONV))
194+
(enc_lines_again_conv)
195+
(REWR_CONV ela1 THENC eval))
196+
*)
197+
198+
(*
199+
val encoded_prog_thm_prefix =
200+
let
201+
val (car,cdr) = dest_comb (concl encoded_prog_thm)
202+
val (ls,ty) = listSyntax.dest_list cdr
203+
val ls' = List.take(ls,10)
204+
in mk_thm([],mk_comb(car,listSyntax.mk_list(ls',ty))) end
205+
val encoded_prog_defs_prefix =
206+
List.take(List.rev encoded_prog_defs,10)
207+
208+
(* rule using exceptions *)
209+
val enc_secs_again_thm =
210+
tm13 |> timez "enc_secs_again" (
211+
RAND_CONV(REWR_CONV encoded_prog_thm_prefix) THENC
212+
enc_secs_again_conv
213+
"enc_again_" (enc_lines_again_conv computed_labs_def) 0
214+
encoded_prog_defs_prefix)
215+
2m15s
216+
217+
(* custom conv *)
218+
val enc_secs_again_thm =
219+
tm13 |> timez "enc_secs_again" (
220+
RAND_CONV(REWR_CONV encoded_prog_thm_prefix) THENC
221+
enc_secs_again_conv
222+
"enc_again_" (enc_lines_again_conv computed_labs_def) 0
223+
encoded_prog_defs_prefix)
224+
2m17s
225+
226+
(* custom conv with IFC *)
227+
val enc_secs_again_thm =
228+
tm13 |> timez "enc_secs_again" (
229+
RAND_CONV(REWR_CONV encoded_prog_thm_prefix) THENC
230+
enc_secs_again_conv
231+
"enc_again_" (enc_lines_again_conv computed_labs_def) 0
232+
encoded_prog_defs_prefix)
233+
2m18s
234+
235+
val enc_secs_again_thm =
236+
tm13 |> timez "enc_secs_again" (
237+
RAND_CONV(REWR_CONV encoded_prog_thm_prefix) THENC
238+
enc_secs_again_conv
239+
"enc_again_"
240+
(PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC eval)
241+
0
242+
encoded_prog_defs_prefix)
243+
14.4s
244+
245+
val (dth::dths) = encoded_prog_defs_prefix
246+
val tm = tm13 |> RAND_CONV(REWR_CONV encoded_prog_thm_prefix) |> rconc
247+
val th1 = tm |> (REWR_CONV esc THENC (RAND_CONV(RATOR_CONV(RAND_CONV(REWR_CONV dth)))))
248+
val tm = th1 |> rconc |> rand
249+
250+
val test1 =
251+
time (PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC eval) tm
252+
1.1s
253+
254+
val th = REFL tm
255+
256+
(* rule with exceptions *)
257+
val test2 =
258+
time (enc_lines_again_conv computed_labs_def) tm
259+
17.1s
260+
val check = rconc test1 = rconc test2
261+
262+
(* custom conv with IFC *)
263+
val test3 =
264+
time (enc_lines_again_conv computed_labs_def) tm
265+
30.6s
266+
val check = rconc test1 = rconc test3
267+
268+
(* custom conv with IFC and delayed leaves *)
269+
val test4 =
270+
time (enc_lines_again_conv computed_labs_def) tm
271+
31.3s
272+
val check = rconc test1 = rconc test4
273+
274+
(* custom conv with labs expanded *)
275+
val test5 =
276+
time (PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC enc_lines_again_conv) tm
277+
21.2s
278+
val check = rconc test1 = rconc test5
279+
280+
(* custom conv with labs expanded using COND_CONV *)
281+
val test6 =
282+
time (PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC enc_lines_again_conv) tm
283+
19.4s
284+
val check = rconc test1 = rconc test6
285+
286+
(* custom conv with labs expanded using COND_CONV and deferring all computations *)
287+
val test7 =
288+
time (PATH_CONV "llllr" (REWR_CONV computed_labs_def) THENC enc_lines_again_conv) tm
289+
19.6s
290+
val check = rconc test1 = rconc test7
291+
292+
*)

0 commit comments

Comments
 (0)