Skip to content

Commit

Permalink
Merge pull request #804 from CakeML/currheap
Browse files Browse the repository at this point in the history
Improved use of CurrHeap
  • Loading branch information
myreen authored Nov 17, 2020
2 parents e76d28c + 3db6838 commit 3157c56
Show file tree
Hide file tree
Showing 31 changed files with 636 additions and 250 deletions.
1 change: 1 addition & 0 deletions compiler/backend/backendComputeLib.sml
Original file line number Diff line number Diff line change
Expand Up @@ -631,6 +631,7 @@ val add_backend_compset = computeLib.extend_compset
(* ---- wordLang inst_select and inst flattening ---- *)
,word_instTheory.three_to_two_reg_def
,word_instTheory.pull_exp_def
,word_instTheory.is_Lookup_CurrHeap_def
,word_instTheory.inst_select_def
,word_instTheory.inst_select_exp_def
,word_instTheory.flatten_exp_def
Expand Down
12 changes: 6 additions & 6 deletions compiler/backend/data_to_wordScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -110,13 +110,13 @@ val ptr_bits_def = Define `
val real_addr_def = Define `
(real_addr (conf:data_to_word$config) r): 'a wordLang$exp =
let k = shift (:'a) in
if k <= conf.pad_bits + 1 then
Op Add [Lookup CurrHeap;
Shift Lsr (Var r) (shift_length conf - k)]
let l = shift_length conf in
if k = l ∧ conf.len_bits = 0 ∧ conf.tag_bits = 0 then
Op Add [Lookup CurrHeap; Op Sub [Var r; Const 1w]]
else if k <= conf.pad_bits + 1 then
Op Add [Lookup CurrHeap; Shift Lsr (Var r) (l - k)]
else
Op Add [Lookup CurrHeap;
Shift Lsl (Shift Lsr (Var r)
(shift_length conf)) k]`
Op Add [Lookup CurrHeap; Shift Lsl (Shift Lsr (Var r) l) k]`

val real_offset_def = Define `
(real_offset (conf:data_to_word$config) r): 'a wordLang$exp =
Expand Down
4 changes: 4 additions & 0 deletions compiler/backend/presLangScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -631,6 +631,8 @@ val stack_prog_to_display_def = Define`
store_name_to_display sn]
| Set sn n => Item NONE «Set» [store_name_to_display sn;
num_to_display n]
| OpCurrHeap b n1 n2 => Item NONE «OpCurrHeap»
[asm_binop_to_display b; num_to_display n1; num_to_display n2]
| Call rh tgt eh => Item NONE «Call»
[(case rh of
| NONE => empty_item «Tail»
Expand Down Expand Up @@ -762,6 +764,8 @@ val word_prog_to_display_def = tDefine "word_prog_to_display" `
[word_prog_to_display_ret a; option_to_display num_to_display b;
list_to_display num_to_display c;
word_prog_to_display_handler d]) /\
(word_prog_to_display (OpCurrHeap b n1 n2) = Item NONE «OpCurrHeap»
[asm_binop_to_display b; num_to_display n1; num_to_display n2]) /\
(word_prog_to_display (Seq prog1 prog2) = Item NONE (strlit "Seq")
[word_prog_to_display prog1; word_prog_to_display prog2]) /\
(word_prog_to_display (If cmp n reg p1 p2) = Item NONE (strlit "If")
Expand Down
2 changes: 1 addition & 1 deletion compiler/backend/proofs/data_to_word_assignProofScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -8474,7 +8474,7 @@ Theorem word_exp_insert:
word_exp t (real_addr c m)))
Proof
fs [wordSemTheory.word_exp_def,real_addr_def]
\\ IF_CASES_TAC \\ fs []
\\ rpt (IF_CASES_TAC \\ fs [])
\\ fs [wordSemTheory.word_exp_def,real_addr_def] \\ fs [lookup_insert]
QED

Expand Down
35 changes: 32 additions & 3 deletions compiler/backend/proofs/data_to_word_memoryProofScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -4609,16 +4609,28 @@ val get_real_addr_def = Define `
let k = shift (:α) in
case FLOOKUP st CurrHeap of
| SOME (Word curr) =>
if k <= conf.pad_bits + 1
then SOME (curr + (w >>> (shift_length conf - k)))
else SOME (curr + (w >>> (shift_length conf) << k))
if k = shift_length conf ∧ conf.len_bits = 0 ∧ conf.tag_bits = 0
then SOME (curr + w - 1w)
else
if k <= conf.pad_bits + 1
then SOME (curr + (w >>> (shift_length conf - k)))
else SOME (curr + (w >>> (shift_length conf) << k))
| _ => NONE`

val get_real_offset_def = Define `
get_real_offset (w:'a word) =
if dimindex (:'a) = 32
then SOME (w + bytes_in_word) else SOME (w << 1 + bytes_in_word)`

Triviality or_1:
∀w. (0 -- 0) w ‖ 1w = 1w :'a word
Proof
fs [fcpTheory.CART_EQ,word_or_def,fcpTheory.FCP_BETA,word_lsl_def,
word_0,word_bits_def]
\\ once_rewrite_tac [wordsTheory.word_index_n2w] \\ fs []
\\ rw [] \\ eq_tac \\ rw []
QED

Theorem get_real_addr_get_addr:
heap_length heap <= dimword (:'a) DIV 2 ** shift_length c /\
heap_lookup n heap = SOME anything /\
Expand All @@ -4635,6 +4647,23 @@ Proof
\\ match_mp_tac LESS_LESS_EQ_TRANS
\\ once_rewrite_tac [CONJ_COMM]
\\ asm_exists_tac \\ fs [])
\\ IF_CASES_TAC
THEN1
(Cases_on ‘w’
\\ fs [get_lowerbits_def,small_shift_length_def,or_1]
\\ ‘0w = n2w n ≪ shift_length c && 1w’ by
(fs [fcpTheory.CART_EQ,word_and_def,fcpTheory.FCP_BETA,word_lsl_def,word_0]
\\ rewrite_tac [word_1comp_def]
\\ once_rewrite_tac [wordsTheory.word_index_n2w] \\ fs []
\\ gvs [good_dimindex_def,shift_def])
\\ drule (GSYM WORD_ADD_OR)
\\ pop_assum kall_tac
\\ fs []
\\ gvs [WORD_MUL_LSL,bytes_in_word_def,word_mul_n2w,good_dimindex_def,
dimword_def,shift_def]
\\ qpat_x_assum ‘_ = shift_length _’ (assume_tac o GSYM)
\\ fs [])
\\ pop_assum kall_tac
\\ reverse IF_CASES_TAC THEN1
(drule lsl_lsr \\ fs [get_lowerbits_LSL_shift_length]
\\ fs [] \\ rw []
Expand Down
13 changes: 13 additions & 0 deletions compiler/backend/proofs/stack_allocProofScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -5215,6 +5215,19 @@ Proof
\\ BasicProvers.TOP_CASE_TAC \\ fs[] \\ rw[]
\\ imp_res_tac FLOOKUP_SUBMAP \\ fs[]
\\ full_simp_tac(srw_ss())[state_component_equality] )
\\ conj_tac (* OpCurrHeap *) >- (
fs[Once comp_def,evaluate_def,get_var_def,word_exp_def]
\\ fs [AllCaseEqs(),set_var_def]
\\ full_simp_tac(srw_ss())[state_component_equality]
\\ rw [] \\ fs [PULL_EXISTS]
\\ gs [optionTheory.IS_SOME_EXISTS,AllCaseEqs()]
\\ qpat_x_assum`_ = t.regs`(assume_tac o SYM) \\ fs[]
\\ rename [‘FLOOKUP s.regs src = SOME (Word x7)’]
\\ ‘FLOOKUP regs src = SOME (Word x7)’ by fs [FLOOKUP_DEF,SUBMAP_DEF]
\\ fs []
\\ match_mp_tac SUBMAP_mono_FUPDATE
\\ rw[GSYM SUBMAP_DOMSUB_gen]
\\ metis_tac[SUBMAP_TRANS,SUBMAP_DOMSUB] )
\\ conj_tac (* Tick *) >- (
rpt strip_tac
\\ qexists_tac `0` \\ full_simp_tac(srw_ss())[Once comp_def,evaluate_def,dec_clock_def]
Expand Down
2 changes: 1 addition & 1 deletion compiler/backend/proofs/stack_namesProofScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -208,7 +208,6 @@ val comp_correct = Q.prove(
s.compile = (λcfg. c cfg o (stack_names$compile f))
==>
evaluate (comp f p, rename_state c f s) = (r, rename_state c f t)`,

recInduct evaluate_ind \\ rpt strip_tac
THEN1 (fs [evaluate_def,comp_def] \\ rpt var_eq_tac)
THEN1 (fs [evaluate_def,comp_def] \\ rpt var_eq_tac \\ CASE_TAC \\ fs []
Expand All @@ -219,6 +218,7 @@ val comp_correct = Q.prove(
imp_res_tac inst_rename >> fs[])
THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[])
THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[])
THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[])
THEN1 (fs [evaluate_def,comp_def,rename_state_def] \\ rw []
\\ fs [] \\ rw [] \\ fs [empty_env_def,dec_clock_def])
THEN1
Expand Down
24 changes: 2 additions & 22 deletions compiler/backend/proofs/stack_rawcallProofScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -158,6 +158,8 @@ Proof
(rename [`Get`] \\ simple_case)
THEN1
(rename [`Set`] \\ simple_case)
THEN1
(rename [`OpCurrHeap`] \\ simple_case)
THEN1
(rename [`Tick`] \\ simple_case)
THEN1
Expand Down Expand Up @@ -941,26 +943,4 @@ Proof
\\ simp [stack_get_handler_labels_def]
QED

(*
Theorem get_code_labels_comp:
!i p.
get_code_labels (comp i p) = get_code_labels p /\
get_code_labels (comp_top i p) = get_code_labels p
Proof
recInduct comp_ind \\ rpt gen_tac \\ strip_tac
\\ Cases_on `p` \\ fs [] \\ simp [comp_top_def]
\\ simp [Once comp_def]
\\ TRY (fs [get_code_labels_def] \\ NO_TAC)
THEN1 (every_case_tac \\ fs [get_code_labels_def])
\\ reverse conj_asm2_tac THEN1 fs [get_code_labels_def]
\\ rename [`comp_seq p1 p2`]
\\ Cases_on `comp_seq p1 p2 i (Seq (comp i p1) (comp i p2)) =
Seq (comp i p1) (comp i p2)` \\ simp []
\\ drule comp_seq_neq_IMP \\ strip_tac \\ rveq \\ fs []
\\ fs [comp_seq_def,dest_case_def,CaseEq"option",CaseEq"bool"]
\\ Cases_on `lookup dest i` \\ fs [] \\ rw []
\\ simp [get_code_labels_def]
QED
*)

val _ = export_theory();
87 changes: 53 additions & 34 deletions compiler/backend/proofs/stack_removeProofScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ open preamble
set_sepTheory
semanticsPropsTheory
helperLib
local open dep_rewrite blastLib in end
local open dep_rewrite blastLib labPropsTheory in end

val _ = new_theory"stack_removeProof";

Expand Down Expand Up @@ -597,6 +597,7 @@ Theorem state_rel_word_exp:
word_exp t e = SOME w
Proof
ho_match_mp_tac word_exp_ind
\\ rpt conj_tac
\\ simp[word_exp_def]
\\ rw[]
\\ imp_res_tac state_rel_mem_load_imp
Expand Down Expand Up @@ -990,7 +991,7 @@ val name_cases = prove(
(* Significantly faster than SEP_R_TAC *)
val mem_load_lemma = Q.prove(`
MEM name store_list ∧
FLOOKUP (s:('a,'c,'b)state).store name = SOME x ∧
FLOOKUP (s:('a,'c,'b)stackSem$state).store name = SOME x ∧
(memory s.memory s.mdomain *
word_list
(the_SOME_Word (FLOOKUP s.store BitmapBase) ≪ word_shift (:α))
Expand All @@ -1001,7 +1002,7 @@ val mem_load_lemma = Q.prove(`
bytes_in_word *
n2w (LENGTH s.data_buffer.buffer + LENGTH s.bitmaps))
s.data_buffer.space_left * word_store c s.store *
word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) state).mdomain)) ⇒
word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) stackSem$state).mdomain)) ⇒
mem_load (c+store_offset name) t1 = SOME x`,
strip_tac >>
drule fun2set_STAR_IMP>>
Expand Down Expand Up @@ -1041,7 +1042,7 @@ val mem_load_lemma2 = Q.prove(`
bytes_in_word *
n2w (LENGTH s.data_buffer.buffer + LENGTH s.bitmaps))
s.data_buffer.space_left * word_store c s.store *
word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) state).mdomain)) ⇒
word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) stackSem$state).mdomain)) ⇒
c+store_offset name ∈ t1.mdomain`,
strip_tac >>
drule fun2set_STAR_IMP>>
Expand Down Expand Up @@ -1142,28 +1143,31 @@ Proof
srw_tac[][FUN_EQ_THM,prog_comp_def,FORALL_PROD,LAMBDA_PROD]
QED

val comp_correct = Q.prove(
`!p s1 r s2 t1 k off jump.
Theorem comp_correct[local]:
!p s1 r s2 t1 k off jump.
evaluate (p,s1) = (r,s2) /\ r <> SOME Error /\
state_rel jump off k s1 t1 /\ reg_bound p k ==>
?ck t2. evaluate (comp jump off k p,t1 with clock := ck + t1.clock) = (r,t2) /\
(case r of
| SOME (Halt _) => t2.ffi = s2.ffi
| SOME TimeOut => t2.ffi = s2.ffi
| SOME (FinalFFI _) => t2.ffi = s2.ffi
| _ => (state_rel jump off k s2 t2))`,
| SOME (Halt _) => t2.ffi = s2.ffi
| SOME TimeOut => t2.ffi = s2.ffi
| SOME (FinalFFI _) => t2.ffi = s2.ffi
| _ => (state_rel jump off k s2 t2))
Proof
recInduct evaluate_ind \\ rpt strip_tac
THEN1 (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ rpt var_eq_tac \\ qexists_tac`0` \\ full_simp_tac(srw_ss())[])
THEN1
THEN1 (* Skip *)
(full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ rpt var_eq_tac \\ qexists_tac`0` \\ full_simp_tac(srw_ss())[])
THEN1 (* Halt *)
(full_simp_tac(srw_ss())[comp_def,evaluate_def,reg_bound_def]
\\ imp_res_tac state_rel_get_var \\ full_simp_tac(srw_ss())[]
\\ qexists_tac`0`
\\ BasicProvers.TOP_CASE_TAC \\ srw_tac[][] \\ full_simp_tac(srw_ss())[]
\\ BasicProvers.TOP_CASE_TAC \\ srw_tac[][] \\ full_simp_tac(srw_ss())[]
\\ full_simp_tac(srw_ss())[state_rel_def])
THEN1 (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ full_simp_tac(srw_ss())[state_rel_def])
THEN1 (
full_simp_tac(srw_ss())[comp_def,evaluate_def]
THEN1 (* Alloc *)
(full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ full_simp_tac(srw_ss())[state_rel_def])
THEN1 (* Inst *)
(full_simp_tac(srw_ss())[comp_def,evaluate_def]
\\ last_x_assum mp_tac
\\ BasicProvers.TOP_CASE_TAC \\ full_simp_tac(srw_ss())[]
\\ strip_tac \\ rveq
Expand Down Expand Up @@ -1224,6 +1228,19 @@ val comp_correct = Q.prove(
\\ Q.ABBREV_TAC `d = t1.mdomain`
\\ drule name_cases
\\ metis_tac[store_write_lemma])
THEN1 (* OpCurrHeap *)
(qexists_tac`0`
\\ `s.use_store` by full_simp_tac(srw_ss())[state_rel_def]
\\ full_simp_tac(srw_ss())[comp_def,evaluate_def,reg_bound_def]
\\ gvs [AllCaseEqs(),word_exp_def]
\\ every_case_tac \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]
\\ fs [inst_def,assign_def,word_exp_def]
\\ gvs [AllCaseEqs(),word_exp_def,PULL_EXISTS]
\\ rename [‘FLOOKUP s.regs src = SOME (Word c1)’]
\\ rename [‘FLOOKUP s.store CurrHeap = SOME (Word c2)’]
\\ qsuff_tac ‘FLOOKUP t1.regs src = SOME (Word c1) ∧
FLOOKUP t1.regs (k + 2) = SOME (Word c2)’ THEN1 fs []
\\ fs [state_rel_def])
THEN1 (* Tick *)
(full_simp_tac(srw_ss())[comp_def,evaluate_def]
\\ `s.clock = t1.clock` by full_simp_tac(srw_ss())[state_rel_def] \\ full_simp_tac(srw_ss())[]
Expand Down Expand Up @@ -1516,7 +1533,7 @@ val comp_correct = Q.prove(
\\ disch_then(qspec_then`ck2`mp_tac)
\\ simp[] \\ ntac 2 strip_tac
\\ qexists_tac`ck' + ck2` \\ simp[] )
THEN1 ( (* Install *)
THEN1 ( (* Install *)
rw[comp_def]
\\ fs[evaluate_def]
\\ fs[reg_bound_def]
Expand Down Expand Up @@ -1968,7 +1985,8 @@ val comp_correct = Q.prove(
\\ full_simp_tac(srw_ss())[mem_load_def] \\ SEP_R_TAC \\ full_simp_tac(srw_ss())[])
\\ `good_dimindex(:'a)` by full_simp_tac(srw_ss())[state_rel_def]
\\ full_simp_tac(srw_ss())[labPropsTheory.good_dimindex_def,word_shift_def,FLOOKUP_UPDATE]
\\ full_simp_tac(srw_ss())[mem_load_def] \\ full_simp_tac(srw_ss())[GSYM mem_load_def] \\ full_simp_tac(srw_ss())[GSYM set_var_def]));
\\ full_simp_tac(srw_ss())[mem_load_def] \\ full_simp_tac(srw_ss())[GSYM mem_load_def] \\ full_simp_tac(srw_ss())[GSYM set_var_def])
QED

Theorem compile_semantics:
state_rel jump off k s1 s2 /\ semantics start s1 <> Fail ==>
Expand Down Expand Up @@ -3442,8 +3460,8 @@ Proof
QED

Theorem stack_remove_lab_pres:
∀jump off k p.
extract_labels p = extract_labels (comp jump off k p)
∀jump off k p.
extract_labels p = extract_labels (comp jump off k p)
Proof
ho_match_mp_tac comp_ind>>Cases_on`p`>>rw[]>>
once_rewrite_tac [comp_def]>>fs[extract_labels_def]>>
Expand Down Expand Up @@ -3474,25 +3492,26 @@ Proof
QED

Theorem stack_remove_comp_stack_asm_name:
∀jump off k p.
stack_asm_name c p ∧ stack_asm_remove (c:'a asm_config) p ∧
addr_offset_ok c 0w ∧
good_dimindex (:'a) ∧
(∀n. n ≤ max_stack_alloc ⇒
c.valid_imm (INL Sub) (n2w (n * (dimindex (:'a) DIV 8))) ∧
c.valid_imm (INL Add) (n2w (n * (dimindex (:'a) DIV 8)))) ∧
(* Needed to implement the global store *)
(∀s. addr_offset_ok c (store_offset s)) ∧
reg_name (k+2) c ∧
reg_name (k+1) c ∧
reg_name k c ∧
off = c.addr_offset ⇒
stack_asm_name c (comp jump off k p)
∀jump off k p.
stack_asm_name c p ∧ stack_asm_remove (c:'a asm_config) p ∧
addr_offset_ok c 0w ∧
good_dimindex (:'a) ∧
(∀n. n ≤ max_stack_alloc ⇒
c.valid_imm (INL Sub) (n2w (n * (dimindex (:'a) DIV 8))) ∧
c.valid_imm (INL Add) (n2w (n * (dimindex (:'a) DIV 8)))) ∧
(* Needed to implement the global store *)
(∀s. addr_offset_ok c (store_offset s)) ∧
reg_name (k+2) c ∧
reg_name (k+1) c ∧
reg_name k c ∧
off = c.addr_offset ⇒
stack_asm_name c (comp jump off k p)
Proof
ho_match_mp_tac comp_ind>>Cases_on`p`>>rw[]>>
simp[Once comp_def]>>
rw[]>>
fs[stack_asm_name_def,inst_name_def,stack_asm_remove_def,addr_name_def,arith_name_def,reg_imm_name_def,stackLangTheory.list_Seq_def]
fs[stack_asm_name_def,inst_name_def,stack_asm_remove_def,addr_name_def,
arith_name_def,reg_imm_name_def,stackLangTheory.list_Seq_def]
>-
(every_case_tac>>fs[])
>-
Expand Down
4 changes: 4 additions & 0 deletions compiler/backend/proofs/stack_to_labProofScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -1167,6 +1167,10 @@ Proof
rename [`Set`] >>
srw_tac[][stackSemTheory.evaluate_def,flatten_def] >>
full_simp_tac(srw_ss())[state_rel_def] ) >>
conj_tac >- (
rename [`OpCurrHeap`] >>
srw_tac[][stackSemTheory.evaluate_def,flatten_def] >>
full_simp_tac(srw_ss())[state_rel_def] ) >>
conj_tac >- (
rename [`Tick`] >>
simp[stackSemTheory.evaluate_def,flatten_def] >>
Expand Down
Loading

0 comments on commit 3157c56

Please sign in to comment.