Skip to content

Commit

Permalink
Split mips encoder into many small-ish functions
Browse files Browse the repository at this point in the history
  • Loading branch information
@myreen
myreen committed Jun 17, 2022
1 parent 22c9831 commit 658ac96
Showing 1 changed file with 192 additions and 1 deletion.
193 changes: 192 additions & 1 deletion compiler/bootstrap/translation/mipsProgScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -188,7 +188,198 @@ val mips_simp6 = mips_enc6
val mips_enc_thm = reconstruct_case ``mips_enc i`` rand
[mips_simp1,mips_simp2,mips_simp3,mips_simp4,mips_simp5,mips_simp6]

val res = translate mips_enc_thm
val cases_defs = LIST_CONJ
[TypeBase.case_def_of “:'a asm$inst”,
TypeBase.case_def_of “:asm$cmp”,
TypeBase.case_def_of “:asm$memop”,
TypeBase.case_def_of “:asm$binop”,
TypeBase.case_def_of “:ast$shift”,
TypeBase.case_def_of “:asm$fp”,
TypeBase.case_def_of “:'a asm$arith”,
TypeBase.case_def_of “:'a asm$addr”,
TypeBase.case_def_of “:'a asm$reg_imm”,
TypeBase.case_def_of “:'a asm$asm”];

val d1 = Define ‘mips_enc_Const n c = mips_enc (Inst (Const n c))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Skip = mips_enc (Inst Skip)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Loc n c = mips_enc (Loc n c)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Call c = mips_enc (Call c)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_NotTest_Imm n c c0 =
mips_enc (JumpCmp NotTest n (Imm c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_NotLess_Imm n c c0 =
mips_enc (JumpCmp NotLess n (Imm c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_NotLower_Imm n c c0 =
mips_enc (JumpCmp NotLower n (Imm c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_NotEqual_Imm n c c0 =
mips_enc (JumpCmp NotEqual n (Imm c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_Test_Imm n c c0 =
mips_enc (JumpCmp Test n (Imm c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_Less_Imm n c c0 =
mips_enc (JumpCmp Less n (Imm c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_Lower_Imm n c c0 =
mips_enc (JumpCmp Lower n (Imm c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_Equal_Imm n c c0 =
mips_enc (JumpCmp Equal n (Imm c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_NotTest_Reg n c c0 =
mips_enc (JumpCmp NotTest n (Reg c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_NotLess_Reg n c c0 =
mips_enc (JumpCmp NotLess n (Reg c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_NotLower_Reg n c c0 =
mips_enc (JumpCmp NotLower n (Reg c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_NotEqual_Reg n c c0 =
mips_enc (JumpCmp NotEqual n (Reg c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_Test_Reg n c c0 =
mips_enc (JumpCmp Test n (Reg c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_Less_Reg n c c0 =
mips_enc (JumpCmp Less n (Reg c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_Lower_Reg n c c0 =
mips_enc (JumpCmp Lower n (Reg c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpCmp_Equal_Reg n c c0 =
mips_enc (JumpCmp Equal n (Reg c) c0)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Jump c =
mips_enc (Jump c)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_JumpReg c =
mips_enc (JumpReg c)’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Mem_Store a b c =
mips_enc (Inst (Mem Store a (Addr b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Mem_Store8 a b c =
mips_enc (Inst (Mem Store8 a (Addr b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Mem_Load a b c =
mips_enc (Inst (Mem Load a (Addr b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Mem_Load8 a b c =
mips_enc (Inst (Mem Load8 a (Addr b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_SubOverflow a b c d =
mips_enc (Inst (Arith (SubOverflow a b c d)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_AddOverflow a b c d =
mips_enc (Inst (Arith (AddOverflow a b c d)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_AddCarry a b c d =
mips_enc (Inst (Arith (AddCarry a b c d)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_LongMul a b c d =
mips_enc (Inst (Arith (LongMul a b c d)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_LongDiv a b c d e =
mips_enc (Inst (Arith (LongDiv a b c d e)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Div a b c =
mips_enc (Inst (Arith (Div a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Shift_Ror a b c =
mips_enc (Inst (Arith (Shift Ror a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Shift_Asr a b c =
mips_enc (Inst (Arith (Shift Asr a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Shift_Lsr a b c =
mips_enc (Inst (Arith (Shift Lsr a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Shift_Lsl a b c =
mips_enc (Inst (Arith (Shift Lsl a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Add_Imm a b c =
mips_enc (Inst (Arith (Binop Add a b (Imm c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Sub_Imm a b c =
mips_enc (Inst (Arith (Binop Sub a b (Imm c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_And_Imm a b c =
mips_enc (Inst (Arith (Binop And a b (Imm c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Or_Imm a b c =
mips_enc (Inst (Arith (Binop Or a b (Imm c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Xor_Imm a b c =
mips_enc (Inst (Arith (Binop Xor a b (Imm c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Add_Reg a b c =
mips_enc (Inst (Arith (Binop Add a b (Reg c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Sub_Reg a b c =
mips_enc (Inst (Arith (Binop Sub a b (Reg c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_And_Reg a b c =
mips_enc (Inst (Arith (Binop And a b (Reg c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Or_Reg a b c =
mips_enc (Inst (Arith (Binop Or a b (Reg c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_Arith_Xor_Reg a b c =
mips_enc (Inst (Arith (Binop Xor a b (Reg c))))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]

val d1 = CONJ d1 $ Define ‘mips_enc_FPLess a b c =
mips_enc (Inst (FP (FPLess a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPLessEqual a b c =
mips_enc (Inst (FP (FPLessEqual a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPEqual a b c =
mips_enc (Inst (FP (FPEqual a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPAbs a b =
mips_enc (Inst (FP (FPAbs a b)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPNeg a b =
mips_enc (Inst (FP (FPNeg a b)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPSqrt a b =
mips_enc (Inst (FP (FPSqrt a b)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPAdd a b c =
mips_enc (Inst (FP (FPAdd a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPSub a b c =
mips_enc (Inst (FP (FPSub a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPMul a b c =
mips_enc (Inst (FP (FPMul a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPDiv a b c =
mips_enc (Inst (FP (FPDiv a b c)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPMov a b =
mips_enc (Inst (FP (FPMov a b)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPToInt a b =
mips_enc (Inst (FP (FPToInt a b)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]
val d1 = CONJ d1 $ Define ‘mips_enc_FPFromInt a b =
mips_enc (Inst (FP (FPFromInt a b)))’
|> SIMP_RULE std_ss [mips_enc_thm,cases_defs,APPEND]

val def = mips_enc_thm |> SIMP_RULE std_ss [APPEND] |> SIMP_RULE std_ss [GSYM d1];

val res = CONJUNCTS d1 |> map SPEC_ALL |> map translate;

val res = translate def;

Theorem mips_config_v_thm = translate (mips_config_def |> SIMP_RULE bool_ss
[IN_INSERT,NOT_IN_EMPTY]|> econv)
Expand Down

0 comments on commit 658ac96

Please sign in to comment.