Merge pull request #887 from CakeML/inc-compiler-emptyffi

Enable empty_ffi and linear scan allocator for REPL

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):

compiler/backend/backendScript.sml

@@ -718,33 +718,42 @@ 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
+    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
     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
 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

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

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:

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;