Improve SSA

compiler/backend/README.md

@@ -341,6 +341,9 @@ The bignum library used by the CakeML compiler. Note that the
 implementation is automatically generated from a shallow embedding
 that is part of the HOL distribution in mc_multiwordTheory.
 
+[word_copyScript.sml](word_copyScript.sml):
+This compilation pass performs a copy propagation phase.
+
 [word_cseScript.sml](word_cseScript.sml):
 Defines a common sub-expression elimination pass on a wordLang program.
 This pass is to run immeidately atfer the SSA-like renaming.
@@ -384,5 +387,8 @@ This compiler phase composes the phases internal to wordLang:
     5) reg_alloc;
     6) word_to_stack.
 
+[word_unreachScript.sml](word_unreachScript.sml):
+This compilation pass removes trivially unreachable code.
+
 [x64](x64):
 This directory contains the x64-specific part of the compiler backend.

compiler/backend/backendComputeLib.sml

@@ -284,6 +284,7 @@ val add_backend_compset = computeLib.extend_compset
     ,bvl_handleTheory.handle_simp_def
     ,bvl_handleTheory.LetLet_def
     ,bvl_handleTheory.SmartLet_def
+    ,bvl_handleTheory.LetLet_def
     ,bvl_handleTheory.OptionalLetLet_def
     ,bvl_handleTheory.compile_def
     ,bvl_handleTheory.compile_exp_def
@@ -717,6 +718,7 @@ val add_backend_compset = computeLib.extend_compset
     ,word_allocTheory.apply_colour_exp_def
     ,word_allocTheory.ssa_cc_trans_exp_def
     ,word_allocTheory.list_next_var_rename_move_def
+    ,word_allocTheory.force_rename_def
     ,word_allocTheory.ssa_cc_trans_inst_def
     ,word_allocTheory.fix_inconsistencies_def
     ,word_allocTheory.fake_moves_def

compiler/backend/backendScript.sml

@@ -303,10 +303,12 @@ val to_livesets_def = Define`
     let inst_prog = inst_select asm_conf maxv prog in
     let ssa_prog = full_ssa_cc_trans arg_count inst_prog in
     let cse_prog = word_common_subexp_elim ssa_prog in
-    let rm_prog = FST(remove_dead cse_prog LN) in
-    let prog = if two_reg_arith then three_to_two_reg rm_prog
-                                else rm_prog in
-     (name_num,arg_count,prog)) p in
+    let cp_prog = copy_prop cse_prog in
+    let two_prog = if two_reg_arith then three_to_two_reg cp_prog
+                                else cp_prog in
+    let unreach_prog = remove_unreach two_prog in
+    let rm_prog = FST(remove_dead unreach_prog LN) in
+     (name_num,arg_count,rm_prog)) p in
   let data = MAP (\(name_num,arg_count,prog).
     let (heu_moves,spillcosts) = get_heuristics alg name_num prog in
     (get_clash_tree prog,heu_moves,spillcosts,get_forced c.lab_conf.asm_conf prog [])) p
@@ -325,10 +327,12 @@ val to_livesets_0_def = Define`
     let inst_prog = inst_select asm_conf maxv prog in
     let ssa_prog = full_ssa_cc_trans arg_count inst_prog in
     let cse_prog = word_common_subexp_elim ssa_prog in
-    let rm_prog = FST(remove_dead cse_prog LN) in
-    let prog = if two_reg_arith then three_to_two_reg rm_prog
-                                else rm_prog in
-     (name_num,arg_count,prog)) p in
+    let cp_prog = copy_prop cse_prog in
+    let two_prog = if two_reg_arith then three_to_two_reg cp_prog
+                                else cp_prog in
+    let unreach_prog = remove_unreach two_prog in
+    let rm_prog = FST(remove_dead unreach_prog LN) in
+     (name_num,arg_count,rm_prog)) p in
   let data = MAP (\(name_num,arg_count,prog).
     let (heu_moves,spillcosts) = get_heuristics alg name_num prog in
     (get_clash_tree prog,heu_moves,spillcosts,get_forced c.lab_conf.asm_conf prog [])) p

compiler/backend/backend_passesScript.sml

@@ -213,12 +213,18 @@ Definition to_word_all_def:
                   ((name_num,arg_count,word_common_subexp_elim prog),col_opt)) p in
     let ps = ps ++ [(strlit "after word_cse",Word (MAP FST p) names)] in
     let p = MAP (λ((name_num,arg_count,prog),col_opt).
-                  ((name_num,arg_count,FST (remove_dead prog LN)),col_opt)) p in
-    let ps = ps ++ [(strlit "after remove_dead in word_alloc",Word (MAP FST p) names)] in
+                  ((name_num,arg_count,copy_prop prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_copy",Word (MAP FST p) names)] in
     let p = MAP (λ((name_num,arg_count,prog),col_opt).
                   ((name_num,arg_count,
                    if two_reg_arith then three_to_two_reg prog else prog),col_opt)) p in
     let ps = ps ++ [(strlit "after three_to_two_reg from word_inst",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,remove_unreach prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_unreach",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,FST (remove_dead prog LN)),col_opt)) p in
+    let ps = ps ++ [(strlit "after remove_dead in word_alloc",Word (MAP FST p) names)] in
     let p = MAP (λ((name_num,arg_count,prog),col_opt).
                   ((name_num,arg_count,
                    remove_must_terminate
@@ -385,12 +391,18 @@ Definition from_word_0_all_def:
                   ((name_num,arg_count,word_common_subexp_elim prog),col_opt)) p in
     let ps = ps ++ [(strlit "after word_cse",Word (MAP FST p) names)] in
     let p = MAP (λ((name_num,arg_count,prog),col_opt).
-                  ((name_num,arg_count,FST (remove_dead prog LN)),col_opt)) p in
-    let ps = ps ++ [(strlit "after remove_dead in word_alloc",Word (MAP FST p) names)] in
+                  ((name_num,arg_count,copy_prop prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_copy",Word (MAP FST p) names)] in
     let p = MAP (λ((name_num,arg_count,prog),col_opt).
                   ((name_num,arg_count,
                    if two_reg_arith then three_to_two_reg prog else prog),col_opt)) p in
     let ps = ps ++ [(strlit "after three_to_two_reg from word_inst",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,remove_unreach prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_unreach",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,FST (remove_dead prog LN)),col_opt)) p in
+    let ps = ps ++ [(strlit "after remove_dead in word_alloc",Word (MAP FST p) names)] in
     let p = MAP (λ((name_num,arg_count,prog),col_opt).
                   ((name_num,arg_count,
                    remove_must_terminate
@@ -457,7 +469,7 @@ Proof
 QED
 
 Theorem number_of_passes:
-  LENGTH (FST (to_target_all c p)) = 36
+  LENGTH (FST (to_target_all c p)) = 38
 Proof
   fs [to_target_all_def] \\ rpt (pairarg_tac \\ gvs [])
   \\ fs [to_lab_all_def] \\ rpt (pairarg_tac \\ gvs [])

compiler/backend/cv_compute/backend_asmLib.sml

@@ -93,6 +93,11 @@ fun define_target_specific_backend asm_config_def = let
   val th = compile_cake_def |> asm_spec
   val th = ISPEC asm_conf compile_cake_thm |> REWRITE_RULE [th]
   val res = save_thm ("compile_cake_" ^ name ^ "_thm", th)
+  (* explorer *)
+  val th = to_word_all_def |> asm_spec
+  val th = to_stack_all_def |> REWRITE_RULE [word_to_stackTheory.compile_def] |> asm_spec
+  val th = to_lab_all_def |> asm_spec
+  val th = compile_cake_explore_def |> asm_spec
   in th end
 
 end

compiler/backend/cv_compute/backend_asmScript.sml

@@ -4,6 +4,7 @@
 *)
 
 open preamble backendTheory lab_to_targetTheory backend_enc_decTheory;
+open backend_passesTheory;
 
 val _ = new_theory "backend_asm";
 
@@ -73,12 +74,15 @@ Definition to_livesets_0_def:
     let inst_prog = inst_select asm_conf maxv prog in
     let ssa_prog = full_ssa_cc_trans arg_count inst_prog in
     let cse_prog = word_common_subexp_elim ssa_prog in
-    let rm_prog = FST(remove_dead cse_prog LN) in
+    let cp_prog = copy_prop cse_prog in
+    let two_prog =
       if asm_conf.two_reg_arith then
-        let prog = three_to_two_reg rm_prog in
-          (name_num,arg_count,prog)
-      else (name_num,arg_count,rm_prog)) p in
-  let data = MAP (\(name_num,arg_count,prog).
+        three_to_two_reg cp_prog else cp_prog in
+    let unreach_prog = remove_unreach two_prog in
+    let rm_prog = FST(remove_dead unreach_prog LN) in
+        (name_num,arg_count,rm_prog))
+      p in
+    let data = MAP (\(name_num,arg_count,prog).
     let (heu_moves,spillcosts) = get_heuristics alg name_num prog in
     (get_clash_tree prog,heu_moves,spillcosts,get_forced asm_conf prog [])) p
   in
@@ -266,11 +270,12 @@ Definition each_inlogic_def:
        inst_prog = inst_select asm_conf maxv prog;
        ssa_prog = full_ssa_cc_trans arg_count inst_prog;
        cse_prog = word_common_subexp_elim ssa_prog;
-       rm_prog = FST (remove_dead cse_prog LN);
+       cp_prog = copy_prop cse_prog;
+       two_prog = if asm_conf.two_reg_arith then three_to_two_reg cp_prog else cp_prog;
+       unreach_prog = remove_unreach two_prog;
+       rm_prog = FST (remove_dead unreach_prog LN);
    in
-     case word_alloc_inlogic asm_conf
-            (if asm_conf.two_reg_arith then three_to_two_reg rm_prog else rm_prog)
-            col_opt
+     case word_alloc_inlogic asm_conf rm_prog col_opt
      of NONE => NONE
       | SOME reg_prog =>
         case each_inlogic asm_conf rest of
@@ -512,6 +517,212 @@ Proof
   \\ rw [] \\ gvs []
 QED
 
+(*----------------------------------------------------------------*
+   Explorer for in-logic evaluation of it
+ *----------------------------------------------------------------*)
+
+Definition to_flat_all_def:
+  to_flat_all (c:inc_config) p =
+    let ps = [] in
+    let ps = ps ++ [(strlit "original source code",Source p)] in
+    let p = source_let$compile_decs p in
+    let ps = ps ++ [(strlit "after source_let",Source p)] in
+    let (c',p) = source_to_flat$compile_prog c.inc_source_conf p in
+    let ps = ps ++ [(strlit "after source_to_flat",Flat p)] in
+    let p = flat_elim$remove_flat_prog p in
+    let ps = ps ++ [(strlit "after remove_flat",Flat p)] in
+    let p = MAP (flat_pattern$compile_dec c'.pattern_cfg) p in
+    let ps = ps ++ [(strlit "after flat_pattern",Flat p)] in
+    let c = c with inc_source_conf := c' in
+      ((ps: (mlstring # 'a any_prog) list),c,p)
+End
+
+Definition to_clos_all_def:
+  to_clos_all (c:inc_config) p =
+    let (ps,c,p) = to_flat_all c p in
+    let p = flat_to_clos$compile_prog p in
+    let ps = ps ++ [(strlit "after flat_to_clos",Clos p [])] in
+      ((ps: (mlstring # 'a any_prog) list),c,p)
+End
+
+Definition to_bvl_all_def:
+  to_bvl_all (c:inc_config) p =
+    let (ps,c,es0) = to_clos_all c p in
+    let c0 = c.inc_clos_conf in
+    let es = clos_mti$compile c0.do_mti c0.max_app es0 in
+    let ps = ps ++ [(strlit "after clos_mti",Clos es [])] in
+    let loc = c0.next_loc + MAX 1 (LENGTH es) in
+    let loc = if loc MOD 2 = 0 then loc else loc + 1 in
+    let (n,es) = clos_number$renumber_code_locs_list loc es in
+    let ps = ps ++ [(strlit "after clos_number",Clos es [])] in
+    let (kc,es) = clos_known$compile c0.known_conf es in
+    let ps = ps ++ [(strlit "after clos_known",Clos es [])] in
+    let (es,g,aux) = clos_call$compile c0.do_call es in
+    let ps = ps ++ [(strlit "after clos_call",Clos es aux)] in
+    let prog = chain_exps c0.next_loc es ++ aux in
+    let prog = clos_annotate$compile prog in
+    let ps = ps ++ [(strlit "after clos_annotate",Clos [] prog)] in
+    let c1 = c0 with
+         <|start := c0.next_loc; next_loc := n; known_conf := kc;
+           call_state := (g,aux)|> in
+    let init_stubs = toAList (init_code c1.max_app) in
+    let init_globs =
+            [(num_stubs c1.max_app − 1,0,
+              init_globals c1.max_app (num_stubs c1.max_app + c1.start))] in
+    let comp_progs = clos_to_bvl$compile_prog c1.max_app prog in
+    let prog' = init_stubs ++ init_globs ++ comp_progs in
+    let func_names =
+            make_name_alist (MAP FST prog') prog (num_stubs c1.max_app)
+              c0.next_loc (LENGTH es0) in
+    let ps = ps ++ [(strlit "after clos_to_bvl",Bvl prog' func_names)] in
+    let c2 = c1 with start := num_stubs c1.max_app − 1 in
+    let p = code_sort prog' in
+    let c = c with inc_clos_conf := c2 in
+      ((ps: (mlstring # 'a any_prog) list),c,p,func_names)
+End
+
+Definition to_bvi_all_def:
+  to_bvi_all (c:inc_config) p =
+    let (ps,c,p,names) = to_bvl_all c p in
+    let start = c.inc_clos_conf.start in
+    let c0 = c.inc_bvl_conf in
+    let limit = c0.inline_size_limit in
+    let split_seq = c0.split_main_at_seq in
+    let cut_size = c0.exp_cut in
+    let (inlines,prog1) = bvl_inline$tick_compile_prog limit LN p in
+    let prog = MAP (λ(name,arity,exp). (name,arity, HD (remove_ticks [exp]))) prog1 in
+    let ps = ps ++ [(strlit "after bvl_inline and remove_ticks",Bvl prog names)] in
+    let prog = MAP (λ(name,arity,exp). (name,arity, let_op_sing exp)) prog in
+    let ps = ps ++ [(strlit "after let_op_sing",Bvl prog names)] in
+    let prog = MAP (λ(name,arity,exp). (name,arity,
+                       bvl_handle$compile_any split_seq cut_size arity exp)) prog in
+    let ps = ps ++ [(strlit "after bvl_handle",Bvl prog names)] in
+    let (loc,code,n1) = bvl_to_bvi$compile_prog start 0 prog in
+    let (n2,code') = bvi_tailrec$compile_prog (bvl_num_stubs + 2) code in
+    let (s,p,l,n1,n2,names) = (loc,code',inlines,n1,n2,get_names (MAP FST code') names) in
+    let names = sptree$union (sptree$fromAList $ (data_to_word$stub_names () ++
+      word_to_stack$stub_names () ++ stack_alloc$stub_names () ++
+      stack_remove$stub_names ())) names in
+    let ps = ps ++ [(strlit "after bvl_to_bvi",Bvi code names)] in
+    let ps = ps ++ [(strlit "after bvi_tailrec",Bvi code' names)] in
+    let c = c with inc_clos_conf updated_by (λc. c with start := s) in
+    let c = c with inc_bvl_conf updated_by
+      (λc. c with <| inlines := l; next_name1 := n1; next_name2 := n2 |>) in
+     ((ps: (mlstring # 'a any_prog) list),c,p,names)
+End
+
+Definition to_data_all_def:
+  to_data_all (c:inc_config) p =
+    let (ps,c,p,names) = to_bvi_all c p in
+    let p = MAP (λ(a,n,e). (a,n,FST (compile n (COUNT_LIST n) T [] [e]))) p in
+    let ps = ps ++ [(strlit "after bvi_to_data",Data p names)] in
+    let p = MAP (λ(a,n,e). (a,n,FST (data_live$compile e LN))) p in
+    let ps = ps ++ [(strlit "after data_live",Data p names)] in
+    let p = MAP (λ(a,n,e). (a,n,data_simp$simp e Skip)) p in
+    let ps = ps ++ [(strlit "after data_simp",Data p names)] in
+    let p = MAP (λ(a,n,e). (a,n,data_space$compile e)) p in
+    let ps = ps ++ [(strlit "after data_space",Data p names)] in
+      ((ps: (mlstring # 'a any_prog) list),c,p,names)
+End
+
+Definition to_word_all_def:
+  to_word_all asm_conf (c:inc_config) p =
+    let (ps,c,p,names) = to_data_all c p in
+    let data_conf = c.inc_data_conf in
+    let word_conf = c.inc_word_to_word_conf in
+    let data_conf =
+            data_conf with
+            <|has_fp_ops := (1 < asm_conf.fp_reg_count);
+              has_fp_tern :=
+                (asm_conf.ISA = ARMv7 ∧ 2 < asm_conf.fp_reg_count)|> in
+    let p = stubs (:α) data_conf ++ MAP (compile_part data_conf) p in
+    let ps = ps ++ [(strlit "after data_to_word",Word p names)] in
+    let (two_reg_arith,reg_count) =
+            (asm_conf.two_reg_arith,
+             asm_conf.reg_count − (5 + LENGTH asm_conf.avoid_regs)) in
+    let (n_oracles,col) = next_n_oracle (LENGTH p) word_conf.col_oracle in
+    let p = ZIP (p,n_oracles) in
+    let alg = word_conf.reg_alg in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,word_simp$compile_exp prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_simp",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,
+                     inst_select asm_conf (max_var prog + 1) prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_inst",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,full_ssa_cc_trans arg_count prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_ssa",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,word_common_subexp_elim prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_cse",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,copy_prop prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_copy",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,
+                   if two_reg_arith then three_to_two_reg prog else prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after three_to_two_reg from word_inst",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,remove_unreach prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_unreach",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,FST (remove_dead prog LN)),col_opt)) p in
+    let ps = ps ++ [(strlit "after remove_dead in word_alloc",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,
+                   remove_must_terminate
+                     (case word_alloc_inlogic asm_conf prog col_opt of
+                      | NONE => Skip
+                      | SOME x => x)))) p in
+    let ps = ps ++ [(strlit "after word_alloc (and remove_must_terminate)",Word p names)] in
+    let c = c with inc_word_to_word_conf updated_by (λc. c with col_oracle := col) in
+      ((ps: (mlstring # 'a any_prog) list),c,p,names)
+End
+
+Definition to_stack_all_def:
+  to_stack_all asm_conf (c:inc_config) p =
+    let (ps,c,p,names) = to_word_all asm_conf c p in
+    let (bm,c',fs,p) = word_to_stack$compile asm_conf p in
+    let ps = ps ++ [(strlit "after word_to_stack",Stack p names)] in
+    let c = c with inc_word_conf := c' in
+      ((ps: (mlstring # 'a any_prog) list),bm,c,p,names)
+End
+
+Definition to_lab_all_def:
+  to_lab_all (asm_conf:'a asm_config) (c:inc_config) p =
+    let (ps,bm,c,p,names) = to_stack_all asm_conf c p in
+    let stack_conf = c.inc_stack_conf in
+    let data_conf = c.inc_data_conf in
+    let max_heap = 2 * max_heap_limit (:'a) c.inc_data_conf - 1 in
+    let sp = asm_conf.reg_count - (LENGTH asm_conf.avoid_regs + 3) in
+    let offset = asm_conf.addr_offset in
+    let prog = stack_rawcall$compile p in
+    let ps = ps ++ [(strlit "after stack_rawcall",Stack prog names)] in
+    let prog = stack_alloc$compile data_conf prog in
+    let ps = ps ++ [(strlit "after stack_alloc",Stack prog names)] in
+    let prog = stack_remove$compile stack_conf.jump offset (is_gen_gc data_conf.gc_kind)
+                 max_heap sp InitGlobals_location prog in
+    let ps = ps ++ [(strlit "after stack_remove",Stack prog names)] in
+    let prog = stack_names$compile stack_conf.reg_names prog in
+    let ps = ps ++ [(strlit "after stack_names",Stack prog names)] in
+    let p = MAP prog_to_section prog in
+    let ps = ps ++ [(strlit "after stack_to_lab",Lab p names)] in
+      ((ps: (mlstring # 'a any_prog) list),bm:'a word list,c,p,names)
+End
+
+Definition compile_cake_explore_def:
+  compile_cake_explore (asm_conf :'a asm_config) (c :inc_config) p =
+    let (ps,bm,c,p,names) = to_lab_all asm_conf c p in
+    let p = filter_skip p in
+    let ps = ps ++ [(«after filter_skip»,Lab p names)] in
+      concat (append (FOLDR (pp_with_title any_prog_pp) Nil ps))
+End
+
+(*----------------------------------------------------------------*
+   Misc
+ *----------------------------------------------------------------*)
+
 Theorem exists_oracle:
   P x ⇒ ∃oracle. P oracle
 Proof