Skip to content

Commit

Permalink
Merge pull request #674 from CakeML/zero-byte
Browse files Browse the repository at this point in the history 
Tweak representation of strings (and byte arrays)
  • Loading branch information
@myreen
myreen committed Jul 28, 2019
2 parents 7e34c9d + 76201ad commit 112863b
Show file tree
Hide file tree
Showing 3 changed files with 183 additions and 297 deletions.
41 changes: 17 additions & 24 deletions compiler/backend/data_to_wordScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -312,10 +312,10 @@ val WriteLastBytes_def = Define`
WriteLastByte_aux 6w a b n (
WriteLastByte_aux 7w a b n Skip)))))))`;

val RefByte_code_def = Define`
val RefByte_code_def = Define `
RefByte_code c =
let limit = MIN (2 ** c.len_size) (dimword (:'a) DIV 16) in
let h = Op Add [Shift Lsr (Var 2) 2; Const (bytes_in_word - 1w)] in
let h = Op Add [Shift Lsr (Var 2) 2; Const bytes_in_word] in
let x = SmallLsr h (dimindex (:'a) - 63) in
let y = Shift Lsl h (dimindex (:'a) - shift (:'a) - c.len_size) in
list_Seq
Expand All @@ -339,23 +339,17 @@ val RefByte_code_def = Define`
MakeBytes 4;
(* store header *)
Store (Var 9) 5;
(* return for empty byte array *)
If Equal 7 (Imm 0w) (Return 0 3)
(list_Seq [
(* write last word of byte array *)
Assign 11 (Op And [Shift Lsr (Var 2) 2;
Const (bytes_in_word - 1w)]);
If Equal 11 (Imm 0w) Skip
(list_Seq [
(* Assign 9 (Op Add [Var 9; Const bytes_in_word]); *)
Assign 13 (Const 0w);
Store (Var 1) 13;
WriteLastBytes 1 4 11;
Assign 7 (Op Sub [Var 7; Const 4w])]);
(* write rest of byte array *)
Call NONE (SOME Replicate_location)
(* ret_loc, addr, v, n, ret_val *)
[0;9;4;7;3] NONE])]:'a wordLang$prog`;
(* write last word of byte array *)
Assign 11 (Op And [Shift Lsr (Var 2) 2;
Const (bytes_in_word - 1w)]);
Assign 13 (Const 0w);
Store (Var 1) 13;
WriteLastBytes 1 4 11;
Assign 7 (Op Sub [Var 7; Const 4w]);
(* write rest of byte array *)
Call NONE (SOME Replicate_location)
(* ret_loc, addr, v, n, ret_val *)
[0;9;4;7;3] NONE]:'a wordLang$prog`;

val Maxout_bits_code_def = Define `
Maxout_bits_code rep_len k dest n =
Expand Down Expand Up @@ -1251,8 +1245,7 @@ val def = assign_Define `
let header = Load addr in
let extra = (if dimindex (:'a) = 32 then 2 else 3) in
let k = dimindex (:'a) - c.len_size - extra in
let kk = (if dimindex (:'a) = 32 then 3w else 7w) in
Op Sub [Shift Lsr header k; Const kk]);
Op Sub [Shift Lsr header k; Const bytes_in_word]);
Assign 3 (ShiftVar Ror (adjust_var v2) 2);
(if leq then If NotLower 1 (Reg 3) else
If Lower 3 (Reg 1))
Expand Down Expand Up @@ -1371,7 +1364,7 @@ val def = assign_Define `
let header = Load addr in
let k = dimindex(:'a) - shift(:'a) - c.len_size in
let fakelen = Shift Lsr header k in
let len = Op Sub [fakelen; Const (bytes_in_word-1w)] in
let len = Op Sub [fakelen; Const bytes_in_word] in
(Shift Lsl len 2)),l)
: 'a wordLang$prog # num`;

Expand Down Expand Up @@ -1746,9 +1739,9 @@ val def = assign_Define `
let fakelen2 = Shift Lsr header2 k in
(list_Seq [
Assign 1 (Op Add [addr1; Const bytes_in_word]);
Assign 3 (Op Sub [fakelen1; Const (bytes_in_word-1w)]);
Assign 3 (Op Sub [fakelen1; Const bytes_in_word]);
Assign 5 (if ffi_index = "" then Const 0w else (Op Add [addr2; Const bytes_in_word]));
Assign 7 (if ffi_index = "" then Const 0w else (Op Sub [fakelen2; Const (bytes_in_word-1w)]));
Assign 7 (if ffi_index = "" then Const 0w else (Op Sub [fakelen2; Const bytes_in_word]));
FFI ffi_index 1 3 5 7 (adjust_set (dtcase names of SOME names => names | NONE => LN));
Assign (adjust_var dest) Unit]
, l)
Expand Down
95 changes: 25 additions & 70 deletions compiler/backend/proofs/data_to_word_assignProofScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -729,7 +729,7 @@ Proof
\\ `n2w (4 * i) ⋙ 2 = (n2w i):'a word` by
(rewrite_tac [GSYM w2n_11,w2n_lsr]
\\ fs [ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV] \\ NO_TAC) \\ fs []
\\ qabbrev_tac `wA = ((bytes_in_word + n2w i + -1w)
\\ qabbrev_tac `wA = ((bytes_in_word + n2w i)
⋙ (dimindex (:α) − 63)):'a word`
\\ once_rewrite_tac [list_Seq_def]
\\ fs [wordSemTheory.evaluate_def,word_exp_rw]
Expand Down Expand Up @@ -847,7 +847,7 @@ Proof
THEN1 (fs [shift_def,shift_length_def,state_rel_def,
EVAL ``good_dimindex (:'a)``] \\ fs [])
\\ pop_assum kall_tac \\ fs []
\\ qabbrev_tac `var5 = (bytes_in_word + n2w i + -1w:'a word) ⋙ shift (:α)`
\\ qabbrev_tac `var5 = (bytes_in_word + n2w i:'a word) ⋙ shift (:α)`
\\ once_rewrite_tac [list_Seq_def]
\\ fs [wordSemTheory.evaluate_def,word_exp_rw,wordSemTheory.set_var_def,
wordSemTheory.set_store_def]
Expand All @@ -862,7 +862,7 @@ Proof
(unabbrev_all_tac \\ fs [byte_len_def,bytes_in_word_def,w2n_lsr,
labPropsTheory.good_dimindex_def,word_add_n2w,dimword_def] \\ rfs []
\\ fs [GSYM word_add_n2w] \\ fs [word_add_n2w,dimword_def]
\\ fs [DIV_DIV_DIV_MULT] \\ NO_TAC)
\\ fs [ADD_DIV_EQ,DIV_DIV_DIV_MULT] \\ NO_TAC)
\\ fs [wordSemTheory.set_var_def,lookup_insert]
\\ rpt_drule0 memory_rel_RefByte_alt
\\ disch_then (qspecl_then [`w`,`i`,`fl`] mp_tac) \\ fs []
Expand All @@ -874,15 +874,15 @@ Proof
(unabbrev_all_tac
\\ rewrite_tac [GSYM w2n_11,w2n_lsr,byte_len_def]
\\ fs [bytes_in_word_def,shift_def,labPropsTheory.good_dimindex_def]
\\ fs [word_add_n2w]
\\ fs [word_add_n2w,ADD_DIV_EQ]
THEN1
(sg `i + 3 < dimword (:'a)`
\\ sg `i + 3 DIV 4 < dimword (:'a)` \\ fs []
(sg `i + 4 < dimword (:'a)`
\\ sg `i + 4 DIV 4 < dimword (:'a)` \\ fs []
\\ rfs [dimword_def] \\ fs [DIV_LT_X])
THEN1
(sg `i + 7 < dimword (:'a)`
\\ sg `i + 7 DIV 8 < dimword (:'a)` \\ fs []
\\ rfs [dimword_def] \\ fs [DIV_LT_X]) \\ NO_TAC)
(sg `i + 8 < dimword (:'a)`
\\ sg `i + 8 DIV 8 < dimword (:'a)` \\ fs []
\\ rfs [dimword_def] \\ fs [DIV_LT_X]))
\\ fs [] \\ rveq
\\ once_rewrite_tac [list_Seq_def]
\\ fs [wordSemTheory.evaluate_def,word_exp_rw,wordSemTheory.set_var_def,
Expand All @@ -905,31 +905,6 @@ Proof
\\ fs [wordSemTheory.evaluate_def,word_exp_rw,
wordSemTheory.get_var_def,lookup_insert,
wordSemTheory.mem_store_def,store_list_def]
\\ IF_CASES_TAC
>- (
simp[Once wordSemTheory.evaluate_def,
wordSemTheory.get_var_def,lookup_insert,
wordSemTheory.call_env_def]
\\ fs[state_rel_thm,fromList2_def,lookup_def]
\\ fs[make_ptr_def,join_env_NIL,FAPPLY_FUPDATE_THM]
\\ fs[WORD_MUL_LSL,word_mul_n2w]
\\ `4 * byte_len (:'a) i = 0`
by (
match_mp_tac (MP_CANON MOD_EQ_0_0)
\\ qexists_tac`dimword(:'a)`
\\ simp[]
\\ rfs[Abbr`limit`,labPropsTheory.good_dimindex_def,dimword_def]
\\ fs[] \\ NO_TAC)
\\ fs [code_oracle_rel_def,FLOOKUP_UPDATE]
\\ fs[REPLICATE,LUPDATE_def,store_list_def]
\\ rveq
\\ qhdtm_x_assum`memory_rel`mp_tac
\\ simp_tac std_ss [GSYM APPEND_ASSOC]
\\ qmatch_goalsub_abbrev_tac`(RefPtr new,val)::(ll++rest)`
\\ fs[]
\\ match_mp_tac memory_rel_rearrange
\\ rpt (pop_assum kall_tac)
\\ fs [] \\ rw [] \\ fs [])
\\ once_rewrite_tac[list_Seq_def]
\\ simp[wordSemTheory.evaluate_def,word_exp_rw]
\\ simp[wordSemTheory.set_var_def]
Expand All @@ -949,33 +924,7 @@ Proof
\\ `2 ** shift(:'a) = dimindex(:'a) DIV 8`
by ( fs[labPropsTheory.good_dimindex_def,dimword_def,shift_def] )
\\ simp[]
\\ IF_CASES_TAC \\ fs[]
>- (
simp[list_Seq_def]
\\ `lookup Replicate_location r.code = SOME (5,Replicate_code)` by
(imp_res_tac lookup_RefByte_location \\ NO_TAC)
\\ assume_tac (GEN_ALL Replicate_code_thm)
\\ SEP_I_TAC "evaluate"
\\ fs[wordSemTheory.get_var_def,lookup_insert] \\ rfs[]
\\ pop_assum mp_tac \\ disch_then drule0
\\ impl_tac THEN1
(fs [WORD_MUL_LSL,word_mul_n2w,state_rel_def]
\\ fs [labPropsTheory.good_dimindex_def,dimword_def] \\ rfs []
\\ unabbrev_all_tac \\ fs []
\\ `byte_len (:α) i < dimword (:'a)` by (fs [dimword_def])
\\ fs [IMP_LESS_MustTerminate_limit])
\\ fs [WORD_MUL_LSL,word_mul_n2w]
\\ disch_then kall_tac
\\ simp[state_rel_thm,lookup_def]
\\ fs[make_ptr_def,join_env_NIL,FAPPLY_FUPDATE_THM]
\\ fs [WORD_MUL_LSL,word_mul_n2w]
\\ fs [code_oracle_rel_def,FLOOKUP_UPDATE]
\\ qhdtm_x_assum`memory_rel`mp_tac
\\ simp_tac std_ss [GSYM APPEND_ASSOC]
\\ match_mp_tac memory_rel_rearrange
\\ rpt (pop_assum kall_tac)
\\ rw [] \\ fs [] \\ rw [])
\\ simp[CONJUNCT2 (CONJUNCT2 list_Seq_def),
\\ simp[(* CONJUNCT2 (CONJUNCT2 list_Seq_def), *)
wordSemTheory.evaluate_def,word_exp_rw,
wordSemTheory.set_var_def,
wordSemTheory.mem_store_def,
Expand All @@ -994,9 +943,15 @@ Proof
\\ simp[WORD_MULT_CLAUSES,WORD_LEFT_ADD_DISTRIB]
\\ NO_TAC)
\\ fs[]
\\ simp[CONJUNCT2 (CONJUNCT2 list_Seq_def),
wordSemTheory.evaluate_def,word_exp_rw,
wordSemTheory.set_var_def,
wordSemTheory.mem_store_def,
wordSemTheory.get_var_def,lookup_insert]
\\ pairarg_tac \\ fs[]
\\ pairarg_tac \\ fs[]
\\ pop_assum mp_tac
\\ pop_assum mp_tac
\\ assume_tac(GEN_ALL evaluate_WriteLastBytes)
\\ SEP_I_TAC "evaluate"
\\ pop_assum mp_tac
Expand All @@ -1020,14 +975,15 @@ Proof
\\ fs [byte_aligned_bytes_in_word])
\\ simp[] \\ disch_then kall_tac
\\ strip_tac \\ fs[] \\ clean_tac \\ fs[]
\\ fs [lookup_insert]
\\ strip_tac \\ rveq \\ fs []
\\ pop_assum mp_tac \\ simp[list_Seq_def]
\\ simp[Once wordSemTheory.evaluate_def,word_exp_rw,wordSemTheory.set_var_def]
\\ strip_tac \\ clean_tac \\ fs[]
\\ `lookup Replicate_location r.code = SOME (5,Replicate_code)` by
(imp_res_tac lookup_RefByte_location \\ NO_TAC)
(imp_res_tac lookup_RefByte_location \\ NO_TAC) \\ rfs []
\\ qmatch_asmsub_abbrev_tac`LUPDATE lw (len-1) ls`
\\ qmatch_assum_abbrev_tac`Abbrev(ls = REPLICATE len rw)`
\\ `0 < len` by ( Cases_on`len` \\ fs[] )
\\ `0 < len` by ( Cases_on`len` \\ fs[byte_len_def,markerTheory.Abbrev_def] )
\\ `ls = REPLICATE (len-1) rw ++ [rw] ++ []`
by (
simp[Abbr`ls`,LIST_EQ_REWRITE,EL_REPLICATE,LENGTH_REPLICATE]
Expand Down Expand Up @@ -6642,8 +6598,7 @@ Theorem assign_BoundsCheckByte:
let header = Load addr in
let extra = (if dimindex (:'a) = 32 then 2 else 3) in
let k = dimindex (:'a) - c.len_size - extra in
let kk = (if dimindex (:'a) = 32 then 3w else 7w) in
Op Sub [Shift Lsr header k; Const kk]);
Op Sub [Shift Lsr header k; Const bytes_in_word]);
Assign 3 (ShiftVar Ror (adjust_var v2) 2);
(if leq then If NotLower 1 (Reg 3) else
If Lower 3 (Reg 1))
Expand Down Expand Up @@ -6701,7 +6656,7 @@ Proof
\\ impl_tac
\\ TRY (fs [small_int_def,dimword_def,good_dimindex_def] \\ rfs [] \\ NO_TAC)
\\ fs [GSYM word_add_n2w]
\\ strip_tac \\ fs []
\\ strip_tac \\ fs [bytes_in_word_def]
\\ IF_CASES_TAC
\\ fs [] \\ fs [lookup_insert,adjust_var_11] \\ rw [] \\ fs []
\\ simp[inter_insert_ODD_adjust_set,GSYM Boolv_def]
Expand Down Expand Up @@ -10571,7 +10526,7 @@ Proof
>> res_tac >> fs[])
\\ fs[]
\\ qmatch_goalsub_abbrev_tac`read_bytearray aa len g`
\\ qmatch_asmsub_rename_tac`LENGTH ls + 3`
\\ qmatch_asmsub_rename_tac`LENGTH ls + 4`
\\ qispl_then[`ls`,`LENGTH ls`,`aa`]mp_tac IMP_read_bytearray_GENLIST
\\ impl_tac >- simp[]
\\ `len = LENGTH ls`
Expand Down Expand Up @@ -10636,7 +10591,7 @@ Proof
\\ simp[]
\\ simp[wordSemTheory.get_var_def,lookup_insert]
\\ qmatch_goalsub_abbrev_tac`read_bytearray aa len g`
\\ qmatch_asmsub_rename_tac`LENGTH ls + 3`
\\ qmatch_asmsub_rename_tac`LENGTH ls + 4`
\\ qispl_then[`ls`,`LENGTH ls`,`aa`]mp_tac IMP_read_bytearray_GENLIST
\\ impl_tac >- simp[]
\\ `len = LENGTH ls`
Expand Down Expand Up @@ -10962,7 +10917,7 @@ Proof
\\ simp[]
\\ simp[wordSemTheory.get_var_def,lookup_insert]
\\ qmatch_goalsub_abbrev_tac`read_bytearray aa len g`
\\ qmatch_asmsub_rename_tac`LENGTH ls + 3`
\\ qmatch_asmsub_rename_tac`LENGTH ls + 4`
\\ qispl_then[`ls`,`LENGTH ls`,`aa`]mp_tac IMP_read_bytearray_GENLIST
\\ impl_tac >- simp[]
\\ `len = LENGTH ls`
Expand Down
Loading

0 comments on commit 112863b

Please sign in to comment.