From 79760e34ca7f2c33c22c66340964143cf2ab39a9 Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Thu, 19 May 2022 19:18:37 +0200 Subject: [PATCH 1/7] Add empty_ffi calls to incremental compiler --- compiler/backend/README.md | 2 +- compiler/backend/backendScript.sml | 9 +++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/compiler/backend/README.md b/compiler/backend/README.md index 3654f71d96..0aaad74f7d 100644 --- a/compiler/backend/README.md +++ b/compiler/backend/README.md @@ -11,7 +11,7 @@ This directory contains the ARMv7-specific part of the compiler backend. This directory contains the ARMv8-specific part of the compiler backend. [arm8_asl](arm8_asl): -This directory contains the ASL-derived ARMv8-specific part of the +This directory contains proofs for the ASL-derived ARMv8-specific part of the compiler backend. [backendComputeLib.sml](backendComputeLib.sml): diff --git a/compiler/backend/backendScript.sml b/compiler/backend/backendScript.sml index c08bd752db..79c2295803 100644 --- a/compiler/backend/backendScript.sml +++ b/compiler/backend/backendScript.sml @@ -562,17 +562,22 @@ val compile_inc_progs_def = Define` let (env_id,p) = p_tup in let ps = empty_progs with <| env_id := env_id; source_prog := p |> in let (c',p) = source_to_flat$inc_compile env_id c.source_conf p in + let _ = empty_ffi (strlit "finished: source_to_flat") in let ps = ps with <| flat_prog := keep_progs k p |> in let c = c with source_conf := c' in let p = flat_to_clos_inc_compile p in + let _ = empty_ffi (strlit "finished: flat_to_clos") in let ps = ps with <| clos_prog := (keep_progs k ## keep_progs k) p |> in let (c',p) = clos_to_bvl_compile_inc c.clos_conf p in + let _ = empty_ffi (strlit "finished: clos_to_bvl") in let c = c with clos_conf := c' in let ps = ps with <| bvl_prog := keep_progs k p |> in let (c', p) = bvl_to_bvi_compile_inc_all c.bvl_conf p in + let _ = empty_ffi (strlit "finished: bvl_to_bvi") in let c = c with <| bvl_conf := c' |> in let ps = ps with <| bvi_prog := keep_progs k p |> in let p = bvi_to_data_compile_prog p in + let _ = empty_ffi (strlit "finished: bvi_to_data") in let ps = ps with <| data_prog := keep_progs k p |> in let asm_c = c.lab_conf.asm_conf in let dc = ensure_fp_conf_ok asm_c c.data_conf in @@ -580,9 +585,11 @@ val compile_inc_progs_def = Define` let reg_count1 = asm_c.reg_count - (5 + LENGTH asm_c.avoid_regs) in let p = MAP (\p. full_compile_single asm_c.two_reg_arith reg_count1 c.word_to_word_conf.reg_alg asm_c (p, NONE)) p in + let _ = empty_ffi (strlit "finished: data_to_word") in let ps = ps with <| word_prog := keep_progs k p |> in let bm0 = c.word_conf.bitmaps_length in let (p, fs, bm) = compile_word_to_stack reg_count1 p (Nil, bm0) in + let _ = empty_ffi (strlit "finished: word_to_stack") in let cur_bm = append (FST bm) in let c = c with word_conf := (c.word_conf with bitmaps_length := SND bm) in let ps = ps with <| stack_prog := keep_progs k p ; cur_bm := cur_bm |> in @@ -590,8 +597,10 @@ val compile_inc_progs_def = Define` let p = stack_to_lab$compile_no_stubs c.stack_conf.reg_names c.stack_conf.jump asm_c.addr_offset reg_count2 p in + let _ = empty_ffi (strlit "finished: stack_to_lab") in let ps = ps with <| lab_prog := keep_progs k p |> in let target = lab_to_target$compile c.lab_conf (p:'a prog) in + let _ = empty_ffi (strlit "finished: lab_to_target") in let ps = ps with <| target_prog := OPTION_MAP (\(bytes, _). (bytes, cur_bm)) target |> in let c = c with lab_conf updated_by (case target of NONE => I From 2516df622e0f1c98a36f9a669de0ee0a2c50fed8 Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Mon, 23 May 2022 09:05:53 +0200 Subject: [PATCH 2/7] Move inc_compiler empty_ffi calls into the right place --- compiler/backend/backendScript.sml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/compiler/backend/backendScript.sml b/compiler/backend/backendScript.sml index 79c2295803..0caaff804f 100644 --- a/compiler/backend/backendScript.sml +++ b/compiler/backend/backendScript.sml @@ -562,22 +562,17 @@ val compile_inc_progs_def = Define` let (env_id,p) = p_tup in let ps = empty_progs with <| env_id := env_id; source_prog := p |> in let (c',p) = source_to_flat$inc_compile env_id c.source_conf p in - let _ = empty_ffi (strlit "finished: source_to_flat") in let ps = ps with <| flat_prog := keep_progs k p |> in let c = c with source_conf := c' in let p = flat_to_clos_inc_compile p in - let _ = empty_ffi (strlit "finished: flat_to_clos") in let ps = ps with <| clos_prog := (keep_progs k ## keep_progs k) p |> in let (c',p) = clos_to_bvl_compile_inc c.clos_conf p in - let _ = empty_ffi (strlit "finished: clos_to_bvl") in let c = c with clos_conf := c' in let ps = ps with <| bvl_prog := keep_progs k p |> in let (c', p) = bvl_to_bvi_compile_inc_all c.bvl_conf p in - let _ = empty_ffi (strlit "finished: bvl_to_bvi") in let c = c with <| bvl_conf := c' |> in let ps = ps with <| bvi_prog := keep_progs k p |> in let p = bvi_to_data_compile_prog p in - let _ = empty_ffi (strlit "finished: bvi_to_data") in let ps = ps with <| data_prog := keep_progs k p |> in let asm_c = c.lab_conf.asm_conf in let dc = ensure_fp_conf_ok asm_c c.data_conf in @@ -585,11 +580,9 @@ val compile_inc_progs_def = Define` let reg_count1 = asm_c.reg_count - (5 + LENGTH asm_c.avoid_regs) in let p = MAP (\p. full_compile_single asm_c.two_reg_arith reg_count1 c.word_to_word_conf.reg_alg asm_c (p, NONE)) p in - let _ = empty_ffi (strlit "finished: data_to_word") in let ps = ps with <| word_prog := keep_progs k p |> in let bm0 = c.word_conf.bitmaps_length in let (p, fs, bm) = compile_word_to_stack reg_count1 p (Nil, bm0) in - let _ = empty_ffi (strlit "finished: word_to_stack") in let cur_bm = append (FST bm) in let c = c with word_conf := (c.word_conf with bitmaps_length := SND bm) in let ps = ps with <| stack_prog := keep_progs k p ; cur_bm := cur_bm |> in @@ -597,10 +590,8 @@ val compile_inc_progs_def = Define` let p = stack_to_lab$compile_no_stubs c.stack_conf.reg_names c.stack_conf.jump asm_c.addr_offset reg_count2 p in - let _ = empty_ffi (strlit "finished: stack_to_lab") in let ps = ps with <| lab_prog := keep_progs k p |> in let target = lab_to_target$compile c.lab_conf (p:'a prog) in - let _ = empty_ffi (strlit "finished: lab_to_target") in let ps = ps with <| target_prog := OPTION_MAP (\(bytes, _). (bytes, cur_bm)) target |> in let c = c with lab_conf updated_by (case target of NONE => I @@ -727,28 +718,37 @@ Theorem compile_inc_progs_for_eval_eq: compile_inc_progs_for_eval asm_c' (env_id,inc_c,p) = let c = inc_config_to_config asm_c' inc_c in let (c',p) = source_to_flat$inc_compile env_id c.source_conf p in + let _ = empty_ffi (strlit "finished: source_to_flat") in let c = c with source_conf := c' in let p = flat_to_clos_inc_compile p in + let _ = empty_ffi (strlit "finished: flat_to_clos") in let (c',p) = clos_to_bvl_compile_inc c.clos_conf p in + let _ = empty_ffi (strlit "finished: clos_to_bvl") in let c = c with clos_conf := c' in let (c', p) = bvl_to_bvi_compile_inc_all c.bvl_conf p in + let _ = empty_ffi (strlit "finished: bvl_to_bvi") in let c = c with <| bvl_conf := c' |> in let p = bvi_to_data_compile_prog p in + let _ = empty_ffi (strlit "finished: bvi_to_data") in let asm_c = c.lab_conf.asm_conf in let dc = ensure_fp_conf_ok asm_c' c.data_conf in let p = MAP (compile_part dc) p in let reg_count1 = asm_c'.reg_count - (5 + LENGTH asm_c'.avoid_regs) in let p = MAP (\p. full_compile_single asm_c'.two_reg_arith reg_count1 c.word_to_word_conf.reg_alg asm_c' (p, NONE)) p in + let _ = empty_ffi (strlit "finished: data_to_word") in let bm0 = c.word_conf.bitmaps_length in let (p, fs, bm) = compile_word_to_stack reg_count1 p (Nil, bm0) in + let _ = empty_ffi (strlit "finished: word_to_stack") in let cur_bm = append (FST bm) in let c = c with word_conf := (c.word_conf with bitmaps_length := SND bm) in let reg_count2 = asm_c'.reg_count - (3 + LENGTH asm_c'.avoid_regs) in let p = stack_to_lab$compile_no_stubs c.stack_conf.reg_names c.stack_conf.jump asm_c'.addr_offset reg_count2 p in + let _ = empty_ffi (strlit "finished: stack_to_lab") in let target = lab_to_target$compile c.lab_conf (p:'a prog) in + let _ = empty_ffi (strlit "finished: lab_to_target") in let c = c with lab_conf updated_by (case target of NONE => I | SOME (_, c') => K c') in OPTION_MAP (λx. (config_to_inc_config c,FST x,MAP upper_w2w cur_bm)) target From 3ce09b70bd360f9c5ae139256671daa1cff40330 Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Mon, 23 May 2022 12:49:49 +0200 Subject: [PATCH 3/7] Make chatty copy of incremental word2word compiler --- compiler/backend/backendScript.sml | 4 ++-- compiler/backend/word_to_wordScript.sml | 30 +++++++++++++++++++++++++ 2 files changed, 32 insertions(+), 2 deletions(-) diff --git a/compiler/backend/backendScript.sml b/compiler/backend/backendScript.sml index 0caaff804f..335beced85 100644 --- a/compiler/backend/backendScript.sml +++ b/compiler/backend/backendScript.sml @@ -734,7 +734,7 @@ Theorem compile_inc_progs_for_eval_eq: let dc = ensure_fp_conf_ok asm_c' c.data_conf in let p = MAP (compile_part dc) p in let reg_count1 = asm_c'.reg_count - (5 + LENGTH asm_c'.avoid_regs) in - let p = MAP (\p. full_compile_single asm_c'.two_reg_arith reg_count1 + let p = MAP (\p. full_compile_single_for_eval asm_c'.two_reg_arith reg_count1 c.word_to_word_conf.reg_alg asm_c' (p, NONE)) p in let _ = empty_ffi (strlit "finished: data_to_word") in let bm0 = c.word_conf.bitmaps_length in @@ -753,7 +753,7 @@ Theorem compile_inc_progs_for_eval_eq: | SOME (_, c') => K c') in OPTION_MAP (λx. (config_to_inc_config c,FST x,MAP upper_w2w cur_bm)) target Proof - fs [compile_inc_progs_for_eval_def,compile_inc_progs_def] + fs [compile_inc_progs_for_eval_def,compile_inc_progs_def, full_compile_single_for_eval_eq] \\ rpt (pairarg_tac \\ gvs [EVAL “(inc_config_to_config asm_c' inc_c).lab_conf.asm_conf”]) \\ fs [optionTheory.OPTION_MAP_COMPOSE] \\ AP_THM_TAC diff --git a/compiler/backend/word_to_wordScript.sml b/compiler/backend/word_to_wordScript.sml index fa4d089d81..380925bf27 100644 --- a/compiler/backend/word_to_wordScript.sml +++ b/compiler/backend/word_to_wordScript.sml @@ -50,6 +50,36 @@ val compile_def = Define ` let progs = ZIP (progs,n_oracles) in (col,MAP (full_compile_single two_reg_arith reg_count word_conf.reg_alg asm_conf) progs)` +Definition full_compile_single_for_eval_def: + full_compile_single_for_eval two_reg_arith reg_count alg c p = + let ((name_num,arg_count,prog),col_opt) = p in + let prog = word_simp$compile_exp prog in + let _ = empty_ffi (strlit "finished: word_simp") in + let maxv = max_var prog + 1 in + let inst_prog = inst_select c maxv prog in + let _ = empty_ffi (strlit "finished: word_inst") in + let ssa_prog = full_ssa_cc_trans arg_count inst_prog in + let _ = empty_ffi (strlit "finished: word_ssa") in + let rm_prog = FST(remove_dead ssa_prog LN) in + let _ = empty_ffi (strlit "finished: word_remove_dead") in + let prog = if two_reg_arith then three_to_two_reg rm_prog + else rm_prog in + let _ = empty_ffi (strlit "finished: word_two_reg") in + let reg_prog = word_alloc name_num c alg reg_count prog col_opt in + let _ = empty_ffi (strlit "finished: word_alloc") in + let rmt_prog = remove_must_terminate reg_prog in + let _ = empty_ffi (strlit "finished: word_remove") in + (name_num,arg_count,rmt_prog) +End + +Theorem full_compile_single_for_eval_eq: + full_compile_single two_reg_arith reg_count alg c p = + full_compile_single_for_eval two_reg_arith reg_count alg c p +Proof + rw [full_compile_single_for_eval_def, full_compile_single_def] + \\ PairCases_on ‘p’ \\ simp [compile_single_def] +QED + Theorem compile_alt: compile word_conf (asm_conf:'a asm_config) progs = let (two_reg_arith,reg_count) = (asm_conf.two_reg_arith, asm_conf.reg_count - (5+LENGTH asm_conf.avoid_regs)) in From ca98576aa8b2f03348c43f8896db84a888a41178 Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Mon, 23 May 2022 13:37:18 +0200 Subject: [PATCH 4/7] Enable call_empty_ffi by default --- compiler/backend/x64/x64_configScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/backend/x64/x64_configScript.sml b/compiler/backend/x64/x64_configScript.sml index affd3fb5c2..44e1e9f179 100644 --- a/compiler/backend/x64/x64_configScript.sml +++ b/compiler/backend/x64/x64_configScript.sml @@ -39,7 +39,7 @@ val clos_conf = rconc (EVAL ``clos_to_bvl$default_config``) val bvl_conf = rconc (EVAL``bvl_to_bvi$default_config``) val word_to_word_conf = ``<| reg_alg:=2; col_oracle := [] |>`` -val x64_data_conf = ``<| tag_bits:=4; len_bits:=4; pad_bits:=2; len_size:=32; has_div:=F; has_longdiv:=T; has_fp_ops:=T; has_fp_tern:=F; call_empty_ffi:=F; gc_kind:=Simple|>`` +val x64_data_conf = ``<| tag_bits:=4; len_bits:=4; pad_bits:=2; len_size:=32; has_div:=F; has_longdiv:=T; has_fp_ops:=T; has_fp_tern:=F; call_empty_ffi:=T; gc_kind:=Simple|>`` val x64_word_conf = ``<| bitmaps_length := 0; stack_frame_size := LN |>`` val x64_stack_conf = ``<|jump:=T;reg_names:=x64_names|>`` val x64_lab_conf = ``<|pos:=0;ffi_names:=NONE;labels:=LN;sec_pos_len:=[];asm_conf:=x64_config;init_clock:=5;hash_size:=104729n|>`` From 9bbbc5a8985fb4e9e7ba3452b541b7893304d783 Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Tue, 24 May 2022 09:05:56 +0200 Subject: [PATCH 5/7] Translate full_compile_single_for_eval with spec64 --- compiler/bootstrap/translation/compiler64ProgScript.sml | 1 + 1 file changed, 1 insertion(+) diff --git a/compiler/bootstrap/translation/compiler64ProgScript.sml b/compiler/bootstrap/translation/compiler64ProgScript.sml index 2be0d3340f..b51e6b3a3e 100644 --- a/compiler/bootstrap/translation/compiler64ProgScript.sml +++ b/compiler/bootstrap/translation/compiler64ProgScript.sml @@ -309,6 +309,7 @@ val r = translate (backendTheory.inc_config_to_config_def |> spec64); val r = translate (backendTheory.config_to_inc_config_def |> spec64); val r = translate (word_to_wordTheory.compile_single_def |> spec64); val r = translate (word_to_wordTheory.full_compile_single_def |> spec64); +val r = translate (word_to_wordTheory.full_compile_single_for_eval_def |> spec64); val _ = (next_ml_names := ["compiler_for_eval"]); val r = translate compiler_for_eval_alt; From 2d27068c7eff6aa2b16a505c8a830fbfb011e202 Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Sat, 28 May 2022 11:21:56 +0200 Subject: [PATCH 6/7] Revert "Enable call_empty_ffi by default" This reverts commit ca98576aa8b2f03348c43f8896db84a888a41178. --- compiler/backend/x64/x64_configScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/backend/x64/x64_configScript.sml b/compiler/backend/x64/x64_configScript.sml index 44e1e9f179..affd3fb5c2 100644 --- a/compiler/backend/x64/x64_configScript.sml +++ b/compiler/backend/x64/x64_configScript.sml @@ -39,7 +39,7 @@ val clos_conf = rconc (EVAL ``clos_to_bvl$default_config``) val bvl_conf = rconc (EVAL``bvl_to_bvi$default_config``) val word_to_word_conf = ``<| reg_alg:=2; col_oracle := [] |>`` -val x64_data_conf = ``<| tag_bits:=4; len_bits:=4; pad_bits:=2; len_size:=32; has_div:=F; has_longdiv:=T; has_fp_ops:=T; has_fp_tern:=F; call_empty_ffi:=T; gc_kind:=Simple|>`` +val x64_data_conf = ``<| tag_bits:=4; len_bits:=4; pad_bits:=2; len_size:=32; has_div:=F; has_longdiv:=T; has_fp_ops:=T; has_fp_tern:=F; call_empty_ffi:=F; gc_kind:=Simple|>`` val x64_word_conf = ``<| bitmaps_length := 0; stack_frame_size := LN |>`` val x64_stack_conf = ``<|jump:=T;reg_names:=x64_names|>`` val x64_lab_conf = ``<|pos:=0;ffi_names:=NONE;labels:=LN;sec_pos_len:=[];asm_conf:=x64_config;init_clock:=5;hash_size:=104729n|>`` From e4fb78d3df72f1175c1fb1876360fe22904b639c Mon Sep 17 00:00:00 2001 From: Oskar Abrahamsson Date: Sat, 28 May 2022 11:25:24 +0200 Subject: [PATCH 7/7] Make REPL use linear scan allocator by default --- compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml b/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml index 246345e9da..a630675701 100644 --- a/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml +++ b/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml @@ -11,7 +11,8 @@ val confs = LIST_CONJ to_dataBootstrapTheory.bvi_conf_def] val encode_backend_config_cake_config_lemma = - “encode_backend_config (config_to_inc_config cake_config)” + “encode_backend_config $ config_to_inc_config $ cake_config with <| + word_to_word_conf := (cake_config.word_to_word_conf with reg_alg := 4) |>” |> (SIMP_CONV (srw_ss()) [cake_config_def,confs,encode_backend_config_def] THENC EVAL); Definition config_enc_str_def: