Add flag to force GC at end of CakeML program

Also greatly streamline a proof.
CakeML · Mar 20, 2023 · 8c4eaa2 · 8c4eaa2
1 parent 93b26ee
commit 8c4eaa2
Show file tree

Hide file tree

Showing 5 changed files with 65 additions and 95 deletions.
diff --git a/compiler/backend/passes/proofs/state_to_cakeProofScript.sml b/compiler/backend/passes/proofs/state_to_cakeProofScript.sml
@@ -637,7 +637,7 @@ Inductive dstep_rel:
   (step_rel (seve, SOME sst, sk) (Estep (cenv,dst.refs,dst.fp_state,ceve,ck)) ∧
    ¬is_halt (seve, SOME sst, sk)
     ⇒ dstep_rel (seve, SOME sst, sk)
-        (Dstep dst (ExpVal cenv ceve ck locs (Pvar "prog")) [CdlocalG lenv genv []])) ∧
+        (Dstep dst (ExpVal cenv ceve ck locs (Pvar "prog")) [CdlocalG lenv genv (final_gc flag)])) ∧
 
   dstep_rel (Val sv, SOME sst, []) Ddone ∧
 
@@ -648,7 +648,7 @@ Inductive dstep_rel:
              (Effi ch ws1 ws2 0 cenv' dst.refs ck)
     ⇒ dstep_rel (Action ch conf, SOME sst, sk)
                 (Dffi dst (ch,ws1,ws2,0,cenv',ck)
-                 locs (Pvar "prog") [CdlocalG lenv genv []]))
+                 locs (Pvar "prog") [CdlocalG lenv genv (final_gc flag)]))
 End
 
 Inductive next_res_rel:
@@ -2290,37 +2290,44 @@ Theorem dstep1_rel:
           ⇒ dget_ffi_array d = SOME ws
 Proof
   reverse $ rw[Once dstep_rel_cases] >> gvs[]
-  >- simp[dstep_rel_cases, sstep, SF SFY_ss]
-  >- simp[dstep_rel_cases, sstep, SF SFY_ss]
-  >- simp[dstep_rel_cases, sstep, SF SFY_ss] >>
+  >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL)
+  >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL)
+  >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL) >>
   drule step1_rel >> simp[] >> strip_tac >> gvs[] >>
   `cstep_n (SUC n) (Estep (cenv,dst.refs,dst.fp_state,ceve,ck)) ≠ Edone` by (
     CCONTR_TAC >> gvs[step_rel_cases]) >>
   qrefine `m + n` >> simp[SUC_ADD_SYM, itree_semanticsPropsTheory.step_n_add] >>
   drule $ SRULE [] cstep_n_to_dstep_n >>
   disch_then $ qspecl_then
-    [`benv`,`locs`,`Pvar "prog"`,`[CdlocalG lenv genv []]`] assume_tac >> gvs[] >>
-  pop_assum kall_tac >>
+    [`benv`,`locs`,`Pvar "prog"`,`[CdlocalG lenv genv (final_gc flag)]`] assume_tac >>
+  gvs[] >> pop_assum kall_tac >>
   reverse $ Cases_on
     `cstep_n (SUC n) (Estep (cenv,dst.refs,dst.fp_state,ceve,ck))` >> gvs[]
   >- fs[Once step_rel_cases]
   >- (
     qpat_x_assum `step_rel _ _` mp_tac >>
-    simp[step_rel_cases, dstep_rel_cases] >> strip_tac >> gvs[SF SFY_ss]
+    simp[step_rel_cases, dstep_rel_cases] >> strip_tac >> gvs[SF SFY_ss] >>
+    irule_at Any EQ_REFL
     ) >>
   PairCases_on `p` >> gvs[] >>
   drule $ iffLR step_rel_cases >> simp[] >> strip_tac >> gvs[]
-  >- (qexists0 >> simp[dstep, dstep_rel_cases])
+  >- (qexists0 >> simp[dstep, dstep_rel_cases] >> irule_at Any EQ_REFL)
   >- (
     reverse $ Cases_on `sk'` >> gvs[]
-    >- (qexists0 >> simp[dstep, dstep_rel_cases]) >>
+    >- (qexists0 >> simp[dstep, dstep_rel_cases] >> irule_at Any EQ_REFL) >>
     gvs[Once cont_rel_cases] >> qrefine `SUC m` >> simp[dstep] >>
     simp[astTheory.pat_bindings_def, pmatch_def] >>
+    reverse $ rw[final_gc_def]
+    >- (ntac 2 (qrefine `SUC m` >> simp[dstep]) >> simp[dstep_rel_cases]) >>
+    ntac 2 (qrefine `SUC m` >> simp[dstep]) >>
+    simp[dstep, astTheory.pat_bindings_def, smallStepTheory.collapse_env_def] >>
+    ntac 6 (qrefine `SUC m` >> simp[cstep, dstep, do_app_def]) >>
+    simp[astTheory.pat_bindings_def, pmatch_def] >>
     ntac 2 (qrefine `SUC m` >> simp[dstep]) >> simp[dstep_rel_cases]
     )
   >- (
     reverse $ Cases_on `sk'` >> gvs[]
-    >- (qexists0 >> simp[dstep, dstep_rel_cases]) >>
+    >- (qexists0 >> simp[dstep, dstep_rel_cases] >> irule_at Any EQ_REFL) >>
     gvs[Once cont_rel_cases] >>
     qrefine `SUC m` >> simp[dstep, dstep_rel_cases, SF SFY_ss]
     )
@@ -2338,9 +2345,9 @@ Proof
   qrefine `SUC (m + k)` >> simp[SUC_ADD_SYM] >>
   once_rewrite_tac[ADD_COMM] >> simp[itree_semanticsPropsTheory.step_n_add] >>
   drule $ iffLR dstep_rel_cases >> reverse strip_tac >> gvs[step_n_alt]
-  >- simp[dstep_rel_cases, sstep, SF SFY_ss]
-  >- simp[dstep_rel_cases, sstep, SF SFY_ss]
-  >- simp[dstep_rel_cases, sstep, SF SFY_ss] >>
+  >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL)
+  >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL)
+  >- (simp[dstep_rel_cases, sstep, SF SFY_ss] >> irule_at Any EQ_REFL) >>
   drule dstep1_rel >> disch_then $ qspec_then `benv` mp_tac >> impl_tac
   >- (rw[] >> last_x_assum $ qspec_then `n' + n` mp_tac >> simp[step_n_add]) >>
   strip_tac >> gvs[] >> goal_assum drule >> simp[]
@@ -2446,87 +2453,35 @@ Proof
   >- (
     qrefine `SUC m` >> simp[dstep] >>
     simp[astTheory.pat_bindings_def, pmatch_def] >>
-    ntac 2 (qrefine `SUC m` >> simp[dstep]) >>
-    simp[dstep_rel_cases] >> gvs[Once cont_rel_cases]
+    reverse $ rw[final_gc_def] >> ntac 2 (qrefine `SUC m` >> simp[dstep]) >>
+    simp[dstep_rel_cases] >> gvs[Once cont_rel_cases] >>
+    simp[astTheory.pat_bindings_def] >>
+    ntac 6 (qrefine `SUC m` >> simp[cstep, dstep, do_app_def]) >>
+    simp[astTheory.pat_bindings_def, pmatch_def] >>
+    ntac 2 (qrefine `SUC m` >> simp[dstep])
     ) >>
   qexists0 >> simp[dstep, store_lookup_def] >>
   simp[dstep_rel_cases, step_rel_cases, PULL_EXISTS] >>
-  goal_assum drule >> gvs[state_rel] >> gvs[Once cont_rel_cases]
+  irule_at Any EQ_REFL >> goal_assum drule >> gvs[state_rel] >>
+  qpat_x_assum `cont_rel _ _ _` mp_tac >> rw[Once cont_rel_cases]
 QED
 
 Theorem compile_safe_itree:
     safe_itree (sinterp sr st sk) ∧
     dstep_rel (sr,st,sk) (step_n benv n dr)
   ⇒ safe_itree ffi_convention (interp benv dr)
 Proof
-  qsuff_tac
-    `∀d.
-      (∃s sr st sk benv n dr.
-        s = sinterp sr st sk ∧ d = interp benv dr ∧
-        safe_itree (sinterp sr st sk) ∧
-        dstep_rel (sr,st,sk) (step_n benv n dr)
-        ) ∨
-      (∃out k. d = Ret (FinalFFI out k))
-    ⇒ safe_itree ffi_convention d`
-  >- (
-    rw[] >> first_x_assum irule >> disj1_tac >>
-    rpt $ goal_assum $ drule_at Any >> simp[]
-    ) >>
-  ho_match_mp_tac safe_itree_coind >> rw[] >>
-  `interp benv dr = interp benv (step_n benv n dr)` by simp[interp_take_steps] >>
-  pop_assum SUBST_ALL_TAC >> qmatch_goalsub_abbrev_tac `interp benv d'` >>
-  `step_until_halt (sr,st,sk) ≠ Err` by (
-    gvs[Once sinterp] >> FULL_CASE_TAC >> gvs[] >>
-    gvs[Once pure_semanticsTheory.safe_itree_cases]) >>
-  drule_all step_until_halt_rel >> disch_then $ qspec_then `benv` assume_tac >>
-  gvs[next_res_rel_cases]
-  >- (once_rewrite_tac[sinterp, interp] >> simp[])
-  >- (once_rewrite_tac[sinterp, interp] >> simp[]) >>
-  ntac 3 disj2_tac >> simp[Once sinterp, Once interp] >>
-  drule $ iffLR dstep_rel_cases >> rw[] >> gvs[] >>
-  drule $ iffLR step_rel_cases >> strip_tac >> gvs[] >>
-  qmatch_goalsub_abbrev_tac `ExpVal _ _ ffi_exp` >>
-  `LENGTH ws = max_FFI_return_size + 2` by gvs[state_rel, store_lookup_def] >>
-  Cases >> rw[Once ffi_convention_def] >> gvs[compile_input_rel_def] >>
-  disj1_tac >> irule_at Any EQ_REFL >>
-  qexistsl [`SOME sst`,`Val $ Atom $ Str s`,`sk'`] >> rw[GSYM PULL_EXISTS]
+  rw[] >> dxrule_all compile_itree_rel >> rename1 `itree_rel a b` >>
+  qsuff_tac `∀b. (∃a. itree_rel a b) ⇒ safe_itree ffi_convention b`
+  >- (rw[PULL_EXISTS] >> res_tac) >>
+  ho_match_mp_tac safe_itree_coind >> rw[] >> gvs[Once itree_rel_cases] >>
+  rw[ffi_convention_def] >> Cases_on `s` >> gvs[]
   >- (
-    last_x_assum mp_tac >> simp[Once sinterp] >>
-    simp[Once pure_semanticsTheory.safe_itree_cases] >>
-    disch_then $ qspec_then `INR s` mp_tac >> simp[Once sinterp]
-    ) >>
-  unabbrev_all_tac >>
-  ntac 7 (qrefine `SUC m` >> simp[dstep, cstep]) >>
-  simp[namespaceTheory.nsOptBind_def] >>
-  `nsLookup cenv.v (Short "ffi_array") = SOME (Loc 0)` by gvs[env_ok_def] >>
-  simp[] >> qrefine `SUC m` >> simp[dstep, cstep, do_app_def] >>
-  Cases_on `dst.refs` >> gvs[store_lookup_def, LUPDATE_DEF] >>
-  ntac 9 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >>
-  simp[store_lookup_def] >>
-  ntac 21 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >>
-  simp[opb_lookup_def, opn_lookup_def, do_if_def] >>
-  `&(256 * (STRLEN s DIV 256) MOD dimword (:8)) + &(STRLEN s MOD dimword (:8)) =
-    &(STRLEN s) : int` by (
-      simp[wordsTheory.dimword_def, wordsTheory.dimindex_8] >>
-      gvs[max_FFI_return_size_def] >> ARITH_TAC) >>
-  pop_assum SUBST_ALL_TAC >> simp[] >>
-  ntac 9 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >>
-  simp[store_lookup_def, copy_array_def, integerTheory.INT_ADD_CALCULATE] >>
-  qmatch_goalsub_abbrev_tac `StrLit str1` >>
-  `str1 = s` by (
-    unabbrev_all_tac >> simp[TAKE_APPEND, GSYM MAP_TAKE] >>
-    simp[ws_to_chars_def, MAP_MAP_o, combinTheory.o_DEF, IMPLODE_EXPLODE_I]) >>
-  pop_assum SUBST_ALL_TAC >>
-  Cases_on `ck'` >> gvs[]
-  >- (
-    qrefine `SUC m` >> simp[dstep] >>
-    simp[astTheory.pat_bindings_def, pmatch_def] >>
-    ntac 2 (qrefine `SUC m` >> simp[dstep]) >>
-    simp[dstep_rel_cases] >> gvs[Once cont_rel_cases]
-    ) >>
-  qexists0 >> simp[dstep, store_lookup_def] >>
-  simp[dstep_rel_cases, step_rel_cases, PULL_EXISTS] >>
-  goal_assum drule >> gvs[state_rel] >> gvs[Once cont_rel_cases]
+    pop_assum $ qspec_then
+      `case x of FFI_failed => FFI_failure | _ => FFI_divergence` mp_tac >>
+    CASE_TAC >> simp[compile_final_ffi_def] >> disch_then $ irule_at Any
+    )
+  >- (first_x_assum $ irule_at Any >> simp[SF SFY_ss])
 QED
 
 
@@ -3597,18 +3552,20 @@ Theorem compile_correct:
   namespace_init_ok ns ∧
   safe_itree (itree_of (exp_of e))
   ⇒ itree_rel (itree_of (exp_of e))
-              (itree_semantics (compile_with_preamble ns e)) ∧
-    safe_itree ffi_convention (itree_semantics (compile_with_preamble ns e))
+              (itree_semantics (compile_with_preamble c ns e)) ∧
+    safe_itree ffi_convention (itree_semantics (compile_with_preamble c ns e))
 Proof
   simp[itree_of_def, semantics_def, itree_semantics_def, cns_ok_def] >> strip_tac >>
   irule_at Any compile_itree_rel >> irule_at Any compile_safe_itree >>
   goal_assum drule >> qrefinel [`n`,`n`] >> simp[] >>
   simp[dstep_rel_cases, step_rel_cases, PULL_EXISTS] >>
+  qrefinel [`_`,`_`,`_`,`_`,`c.do_final_gc`] >>
   simp[Once cont_rel_cases, env_rel_def, state_rel] >>
   gvs[namespace_init_ok_def] >>
   simp[compile_with_preamble_def, initial_namespace_def, preamble_def] >>
   qmatch_goalsub_abbrev_tac `[ffi_array;strle_dec;char_list_dec]` >>
-  once_rewrite_tac[GSYM APPEND_ASSOC] >> qmatch_goalsub_abbrev_tac `_ ++ prog` >>
+  ntac 2 $ once_rewrite_tac[GSYM APPEND_ASSOC] >>
+  qmatch_goalsub_abbrev_tac `compile_namespace _ ++ prog` >>
   qspecl_then [`ns'`,`start_env`,`start_dstate`,`[]`,`HD prog`,`TL prog`]
     mp_tac step_over_compile_namespace >>
   impl_tac
@@ -3621,7 +3578,7 @@ Proof
     PairCases_on `tdef` >> first_x_assum drule >> gvs[]
     ) >>
   strip_tac >> gvs[Abbr `prog`] >>
-  once_rewrite_tac[GSYM APPEND_ASSOC] >> rewrite_tac[APPEND] >> simp[] >>
+  ntac 2 (once_rewrite_tac[GSYM APPEND_ASSOC] >> rewrite_tac[APPEND]) >> simp[] >>
   qrefine `m + n` >> simp[itree_semanticsPropsTheory.step_n_add] >>
   pop_assum kall_tac >>
   qmatch_goalsub_abbrev_tac `Dstep dst'` >> qpat_abbrev_tac `cml_ns = nsAppend _ _` >>

diff --git a/compiler/backend/passes/pure_comp_confScript.sml b/compiler/backend/passes/pure_comp_confScript.sml
@@ -14,7 +14,8 @@ Datatype:
       do_mk_delay   : bool ;  (* thunk-to-thunk smart mk_delay constructor *)
       do_let_force  : bool ;  (* thunk-to-thunk simplify let force *)
       do_split_dlam : bool ;  (* thunk-to-thunk split delayed lambdas *)
-      do_app_unit   : bool    (* state-to-state *)
+      do_app_unit   : bool ;  (* state-to-state *)
+      do_final_gc   : bool ;  (* invoke GC at end of CakeML program *)
     |>
 End
 
@@ -25,6 +26,7 @@ Overload mk_delay_flag[local]   = “strlit "-mk_delay"”
 Overload let_force_flag[local]  = “strlit "-let_force"”
 Overload dlam_flag[local]       = “strlit "-dlam"”
 Overload unit_flag[local]       = “strlit "-unit"”
+Overload final_gc_flag[local]   = “strlit "-final_gc"”
 
 Definition all_flags_def:
   all_flags = [pure_sort_flag;
@@ -33,7 +35,8 @@ Definition all_flags_def:
                mk_delay_flag;
                let_force_flag;
                dlam_flag;
-               unit_flag]
+               unit_flag;
+               final_gc_flag]
 End
 
 Definition read_cline_args_def:
@@ -46,7 +49,8 @@ Definition read_cline_args_def:
                    do_mk_delay   := ¬ MEM mk_delay_flag cl   ;
                    do_let_force  := ¬ MEM let_force_flag cl  ;
                    do_split_dlam := ¬ MEM dlam_flag cl       ;
-                   do_app_unit   := ¬ MEM unit_flag cl       |>
+                   do_app_unit   := ¬ MEM unit_flag cl       ;
+                   do_final_gc   := MEM final_gc_flag cl     |> (* NB final GC only if flag is present *)
 End
 
 val default = EVAL “read_cline_args []” |> concl |> rand |> rand

diff --git a/compiler/backend/passes/pure_to_cakeScript.sml b/compiler/backend/passes/pure_to_cakeScript.sml
@@ -32,7 +32,7 @@ End
 Definition pure_to_cake_def:
   pure_to_cake c ns e =
     let state_prog = pure_to_state c e in
-    let cake_prog = compile_with_preamble ((I ## K ns) initial_namespace) state_prog in
+    let cake_prog = compile_with_preamble c ((I ## K ns) initial_namespace) state_prog in
     let _ = empty_ffi (strlit "to_cake") in
       cake_prog
 End

diff --git a/compiler/backend/passes/state_to_cakeScript.sml b/compiler/backend/passes/state_to_cakeScript.sml
@@ -6,10 +6,11 @@ open stringTheory optionTheory sumTheory pairTheory listTheory alistTheory
      rich_listTheory arithmeticTheory;
 open semanticPrimitivesTheory;
 open pure_miscTheory pure_configTheory pure_typingTheory state_cexpTheory;
+open pure_comp_confTheory
 
 val _ = new_theory "state_to_cake";
 
-val _ = set_grammar_ancestry ["pure_typing", "state_cexp", "semanticPrimitives"]
+val _ = set_grammar_ancestry ["pure_typing", "state_cexp", "semanticPrimitives", "pure_comp_conf"]
 
 
 (********** Primitives operation implementations **********)
@@ -341,10 +342,17 @@ Termination
   WF_REL_TAC `measure cexp_size`
 End
 
+Definition final_gc_def:
+  final_gc flag =
+    if flag then [Dlet unknown_loc (Pvar "gc") $ (App ConfigGC [int 0; int 0])] else []
+End
+
 (* Remove initial built-in datatypes from ns *)
 Definition compile_with_preamble_def:
-  compile_with_preamble ns e =
-    preamble ((TL ## TL) ns) ++ [Dlet unknown_loc (Pvar "prog") $ compile e]
+  compile_with_preamble c ns e =
+    preamble ((TL ## TL) ns) ++
+    [Dlet unknown_loc (Pvar "prog") $ compile e] ++
+    final_gc c.do_final_gc
 End
 
 

diff --git a/compiler/binary/pure_backendProgScript.sml b/compiler/binary/pure_backendProgScript.sml
@@ -137,6 +137,7 @@ val r = translate state_to_cakeTheory.failure_def;
 val r = translate state_to_cakeTheory.list_to_exp_def;
 val r = translate state_to_cakeTheory.cexp_pat_row_def;
 val r = translate state_to_cakeTheory.compile_def;
+val r = translate state_to_cakeTheory.final_gc_def;
 val r = translate compile_with_preamble_def;
 
 (* compositions *)