Merge pull request #908 from CakeML/common-sub-exp-elim

Add new common subexpression elimination pass to wordLang

compiler/backend/README.md

@@ -257,12 +257,15 @@ Proofs and automation for serialising HOL values.
 
 [source_letScript.sml](source_letScript.sml):
 This is a source-to-source transformation that lifts Let/Letrec expressions
-out of Dlet/Dletrecs when they are independent of function arguments.
+that sit at the top of Dlet:s into their own Dlet/Dletrec:s.
 
 [source_to_flatScript.sml](source_to_flatScript.sml):
 This is the compiler phase that translates the CakeML source
 language into flatLang.
 
+[source_to_sourceScript.sml](source_to_sourceScript.sml):
+This phase collects all source-to-source transformations.
+
 [stackLangScript.sml](stackLangScript.sml):
 The stackLang intermediate language is a structured programming
 language with function calls, while loops, if statements, etc. All
@@ -318,6 +321,10 @@ 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_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.
+
 [word_depthScript.sml](word_depthScript.sml):
 Computes the call graph for wordLang program with an acyclic call
 graph. This graph is in turn used to compute the max stack depth

compiler/backend/backendComputeLib.sml

@@ -116,6 +116,15 @@ val add_backend_compset = computeLib.extend_compset
 
   ,computeLib.Defs (theory_computes "flat_to_clos")
 
+  ,computeLib.Defs (theory_computes "word_cse")
+  ,computeLib.Tys [``:word_cse$knowledge``]
+
+  ,computeLib.Defs (theory_computes "mlmap")
+  ,computeLib.Tys [``:('k,'v) mlmap$map``]
+  ,computeLib.Defs (theory_computes "balanced_map")
+  ,computeLib.Tys [``:('k,'v) balanced_map$balanced_map``,
+                   ``:ternaryComparisons$ordering``]
+
   ,computeLib.Tys
     [``:closLang$exp``
     ,``:closLang$op``

compiler/backend/backendScript.sml

@@ -309,7 +309,8 @@ val to_livesets_def = Define`
     let maxv = max_var prog + 1 in
     let inst_prog = inst_select asm_conf maxv prog in
     let ssa_prog = full_ssa_cc_trans arg_count inst_prog in
-    let rm_prog = FST(remove_dead ssa_prog LN) 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
@@ -330,7 +331,8 @@ val to_livesets_0_def = Define`
     let maxv = max_var prog + 1 in
     let inst_prog = inst_select asm_conf maxv prog in
     let ssa_prog = full_ssa_cc_trans arg_count inst_prog in
-    let rm_prog = FST(remove_dead ssa_prog LN) 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

compiler/backend/data_to_wordScript.sml

@@ -1167,7 +1167,7 @@ End
 
 Definition lookup_mem_def:
   lookup_mem m a =
-    dtcase lookup a m of
+    dtcase sptree$lookup a m of
     | NONE => (F,Word (0w:'a word))
     | SOME x => x
 End
@@ -1224,7 +1224,7 @@ Definition part_to_words_def:
             | NONE => NONE
             | SOME hd => SOME ((T,(make_ptr c offset (0w:'a word) (LENGTH ws))),
                                MAP (λw. (F,Word w)) (hd::ws))) ∧
-  part_to_words c m (Con t ns) (offset:'a word) =
+  part_to_words c m (closLang$Con t ns) (offset:'a word) =
     (if NULL ns then
        if t < dimword (:'a) DIV 16
        then SOME ((F,Word (n2w (16 * t + 2))),[]) else NONE

compiler/backend/proofs/README.md

@@ -147,6 +147,9 @@ Correctness proof for word_alloc
 [word_bignumProofScript.sml](word_bignumProofScript.sml):
 Correctness proof for word_bignum
 
+[word_cseProofScript.sml](word_cseProofScript.sml):
+Correctness proof for word_cse
+
 [word_depthProofScript.sml](word_depthProofScript.sml):
 Proves correctness of the max_depth applied to the call graph of a
 wordLang program as produced by the word_depth$call_graph function.

compiler/backend/proofs/data_to_wordProofScript.sml

@@ -2070,11 +2070,12 @@ Proof
   simp[COND_RAND]>>
   fs[word_good_handlers_three_to_two_reg]>>
   match_mp_tac word_good_handlers_remove_dead>>
+  match_mp_tac word_cseProofTheory.word_good_handlers_word_common_subexp_elim >>
   simp[word_good_handlers_full_ssa_cc_trans,word_good_handlers_inst_select]>>
   match_mp_tac word_good_handlers_word_simp>>
   fs[FORALL_PROD]>>
   metis_tac[EL_MEM]
-QED;
+QED
 
 Theorem word_get_code_labels_word_to_word_incr_helper:
   ∀oracles.
@@ -2097,7 +2098,8 @@ Proof
     fs[COND_RAND]>>
     fs[word_get_code_labels_three_to_two_reg]>>
     old_drule (word_get_code_labels_remove_dead|>SIMP_RULE std_ss [SUBSET_DEF])>>
-    simp[word_get_code_labels_full_ssa_cc_trans,word_get_code_labels_inst_select]>>
+    simp[word_get_code_labels_full_ssa_cc_trans,word_get_code_labels_inst_select,
+         word_cseProofTheory.word_get_code_labels_word_common_subexp_elim]>>
     strip_tac>>
     old_drule (word_get_code_labels_word_simp|>SIMP_RULE std_ss [SUBSET_DEF])>>
     rw[]>>fs[FORALL_PROD,EXISTS_PROD,PULL_EXISTS,EVERY_MEM]>>
@@ -2170,7 +2172,7 @@ val word_get_code_labels_MemEqList = Q.prove(`
 Triviality part_to_words_isWord:
   ∀h c m i w ws.
     part_to_words c m h i = SOME (w,ws) ∧
-    (∀n v. lookup n m = SOME v ⇒ isWord (SND v)) ⇒
+    (∀n v. sptree$lookup n m = SOME v ⇒ isWord (SND v)) ⇒
     EVERY isWord (MAP SND ws) ∧ isWord (SND w)
 Proof
   Cases_on ‘h’ \\ fs [part_to_words_def] \\ rw []
@@ -2187,7 +2189,7 @@ QED
 Triviality parts_to_words_isWord:
   ∀ps c w ws m n i.
     parts_to_words c m n ps i = SOME (w,ws) ∧
-    (∀n v. lookup n m = SOME v ⇒ isWord (SND v)) ⇒
+    (∀n v. sptree$lookup n m = SOME v ⇒ isWord (SND v)) ⇒
     EVERY isWord (MAP SND ws) ∧ isWord (SND w)
 Proof
   Induct

compiler/backend/proofs/data_to_word_assignProofScript.sml

@@ -33,6 +33,8 @@ val shift_def = backend_commonTheory.word_shift_def
 val isWord_def = wordSemTheory.isWord_def
 val theWord_def = wordSemTheory.theWord_def
 
+Overload lookup[local] = “sptree$lookup”;
+
 val assign_def =
   data_to_wordTheory.assign_def
   |> REWRITE_RULE [arg1_def, arg2_def, arg3_def, arg4_def, all_assign_defs];
@@ -13221,7 +13223,7 @@ Proof
             >- (
               first_x_assum (mp_tac o GSYM)
               \\ simp[DROP_LENGTH_NIL_rwt,wordSemTheory.write_bytearray_def]
-              \\ qpat_abbrev_tac`refs = insert _ _ x.refs`
+              \\ qpat_abbrev_tac`refs = sptree$insert _ _ x.refs`
               \\ `refs = x.refs` by simp[Abbr`refs`,insert_unchanged]
               \\ rw[]
               >- (qpat_x_assum `memory_rel _ _ _ _ _ _ _ _ (_ :: _ :: _)` mp_tac

compiler/backend/proofs/data_to_word_bignumProofScript.sml

@@ -5,7 +5,7 @@ open preamble dataSemTheory dataPropsTheory
      copying_gcTheory int_bitwiseTheory finite_mapTheory
      data_to_word_memoryProofTheory data_to_word_gcProofTheory
      data_to_wordTheory wordPropsTheory labPropsTheory
-     set_sepTheory semanticsPropsTheory word_to_wordProofTheory
+     set_sepTheory semanticsPropsTheory
      helperLib alignmentTheory blastLib word_bignumTheory
      wordLangTheory word_bignumProofTheory gen_gc_partialTheory
      gc_sharedTheory word_gcFunctionsTheory word_depthProofTheory;

compiler/backend/proofs/data_to_word_gcProofScript.sml

@@ -4,7 +4,7 @@
 open preamble dataSemTheory dataPropsTheory copying_gcTheory
      int_bitwiseTheory data_to_word_memoryProofTheory finite_mapTheory
      data_to_wordTheory wordPropsTheory labPropsTheory whileTheory
-     set_sepTheory semanticsPropsTheory word_to_wordProofTheory
+     set_sepTheory semanticsPropsTheory
      helperLib alignmentTheory blastLib word_bignumTheory wordLangTheory
      word_bignumProofTheory gen_gc_partialTheory gc_sharedTheory
      word_gcFunctionsTheory backendPropsTheory
@@ -27,6 +27,8 @@ val isWord_def = wordSemTheory.isWord_def
 val theWord_def = wordSemTheory.theWord_def
 val is_fwd_ptr_def = wordSemTheory.is_fwd_ptr_def
 
+Overload lookup[local] = “sptree$lookup”;
+
 val _ = hide "next";
 
 val drule = old_drule

compiler/backend/proofs/data_to_word_memoryProofScript.sml

@@ -252,7 +252,7 @@ val v_all_ts_def = tDefine"v_all_ts" `
 (* TODO: MOVE *)
 val all_ts_def = Define`
   all_ts refs stack =
-    let refs_v = {x | ∃n l. lookup n refs = SOME (ValueArray l) ∧ MEM x l}
+    let refs_v = {x | ∃n l. sptree$lookup n refs = SOME (ValueArray l) ∧ MEM x l}
     in {ts | ∃x. (x ∈ refs_v ∨ MEM x stack) ∧ MEM ts (v_all_ts x)}
 `
 

compiler/backend/proofs/stack_allocProofScript.sml

@@ -5035,7 +5035,7 @@ val alloc_correct = Q.prove(
 
 val find_code_IMP_lookup = Q.prove(
   `find_code dest regs (s:'a num_map) = SOME x ==>
-    ?k. lookup k s = SOME x /\
+    ?k. sptree$lookup k s = SOME x /\
         (find_code dest regs = ((lookup k):'a num_map -> 'a option))`,
   Cases_on `dest` \\ full_simp_tac(srw_ss())[find_code_def,FUN_EQ_THM]
   \\ every_case_tac \\ full_simp_tac(srw_ss())[] \\ metis_tac []);

compiler/backend/proofs/stack_rawcallProofScript.sml

@@ -21,8 +21,8 @@ Type prog[pp] = “:α stackLang$prog”
 Definition state_ok_def:
   state_ok i code <=>
     !n v.
-      lookup n i = SOME v ==>
-      ?p. lookup n code = SOME (Seq (StackAlloc v) p)
+      sptree$lookup n i = SOME v ==>
+      ?p. sptree$lookup n code = SOME (Seq (StackAlloc v) p)
 End
 
 Definition state_rel_def:
@@ -36,7 +36,7 @@ Definition state_rel_def:
       t.compile_oracle = (I ## compile ## I) o s.compile_oracle /\ *)
       state_ok i s.code /\
       !n b.
-        lookup n s.code = SOME b ==>
+        sptree$lookup n s.code = SOME b ==>
         ?i. state_ok i s.code /\
             lookup n c = SOME (comp_top i b)
 End