[733] | 1 | include "ASM/I8051.ma". |
---|
[757] | 2 | include "common/CostLabel.ma". |
---|
[733] | 3 | include "common/AST.ma". |
---|
[757] | 4 | include "common/Registers.ma". |
---|
[1252] | 5 | include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *) |
---|
[1176] | 6 | include "common/Graphs.ma". |
---|
[733] | 7 | |
---|
[1246] | 8 | record params__: Type[1] ≝ |
---|
[1233] | 9 | { acc_a_reg: Type[0] |
---|
| 10 | ; acc_b_reg: Type[0] |
---|
| 11 | ; dpl_reg: Type[0] |
---|
| 12 | ; dph_reg: Type[0] |
---|
| 13 | ; pair_reg: Type[0] |
---|
| 14 | ; generic_reg: Type[0] |
---|
[1176] | 15 | |
---|
[1233] | 16 | ; extend_statements: Type[0] |
---|
[1176] | 17 | |
---|
[1233] | 18 | ; resultT: Type[0] |
---|
| 19 | ; localsT: Type[0] |
---|
| 20 | ; paramsT: Type[0] |
---|
| 21 | }. |
---|
[1164] | 22 | |
---|
[1246] | 23 | record params_: Type[1] ≝ |
---|
| 24 | { pars__:> params__ |
---|
[1233] | 25 | ; succ: Type[0] |
---|
| 26 | }. |
---|
| 27 | |
---|
[1246] | 28 | inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝ |
---|
[1169] | 29 | | joint_instr_comment: String → joint_instruction p globals |
---|
| 30 | | joint_instr_cost_label: costlabel → joint_instruction p globals |
---|
| 31 | | joint_instr_int: generic_reg p → Byte → joint_instruction p globals |
---|
| 32 | | joint_instr_move: pair_reg p → joint_instruction p globals |
---|
| 33 | | joint_instr_pop: acc_a_reg p → joint_instruction p globals |
---|
| 34 | | joint_instr_push: acc_a_reg p → joint_instruction p globals |
---|
| 35 | | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals |
---|
| 36 | | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals |
---|
[1255] | 37 | | joint_instr_op1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals |
---|
| 38 | | joint_instr_op2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals |
---|
[1169] | 39 | | joint_instr_clear_carry: joint_instruction p globals |
---|
| 40 | | joint_instr_set_carry: joint_instruction p globals |
---|
| 41 | | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals |
---|
| 42 | | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals |
---|
| 43 | | joint_instr_call_id: ident → nat → joint_instruction p globals |
---|
[1250] | 44 | | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals |
---|
| 45 | | joint_instr_extension: extend_statements p → joint_instruction p globals. |
---|
[733] | 46 | |
---|
[1246] | 47 | inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝ |
---|
[1233] | 48 | | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals |
---|
[1182] | 49 | | joint_st_goto: label → joint_statement p globals |
---|
[1250] | 50 | | joint_st_return: joint_statement p globals. |
---|
[1169] | 51 | |
---|
[1250] | 52 | |
---|
[1246] | 53 | record params (globals: list ident): Type[1] ≝ |
---|
| 54 | { pars_:> params_ |
---|
| 55 | ; codeT: Type[0] |
---|
| 56 | ; lookup: codeT → label → option (joint_statement pars_ globals) |
---|
| 57 | }. |
---|
| 58 | |
---|
[1252] | 59 | include alias "common/Graphs.ma". (* To pick the right lookup *) |
---|
| 60 | |
---|
| 61 | (* One common instantiation of params via Graphs of joint_statements *) |
---|
| 62 | definition graph_params: params_ → ∀globals: list ident. params globals ≝ |
---|
| 63 | λparams_,globals. mk_params globals params_ (graph (joint_statement params_ globals)) (lookup …). |
---|
| 64 | |
---|
[1246] | 65 | record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝ |
---|
[1176] | 66 | { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) |
---|
| 67 | joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) |
---|
| 68 | (* joint_if_sig: signature; -- dropped in front end *) |
---|
[1233] | 69 | joint_if_result : resultT p; |
---|
| 70 | joint_if_params : paramsT p; |
---|
| 71 | joint_if_locals : localsT p; |
---|
[1236] | 72 | (*CSC: XXXXX stacksize unused for LTL-...*) |
---|
[1176] | 73 | joint_if_stacksize: nat; |
---|
[1246] | 74 | joint_if_code : codeT … p; |
---|
[1236] | 75 | (*CSC: XXXXX entry unused for LIN, but invariant in that case... *) |
---|
[1246] | 76 | joint_if_entry : Σl: label. lookup … joint_if_code l ≠ None ?; |
---|
[1236] | 77 | (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *) |
---|
[1246] | 78 | joint_if_exit : Σl: label. lookup … joint_if_code l ≠ None ? |
---|
[1176] | 79 | }. |
---|
| 80 | |
---|
[1245] | 81 | (* Currified form *) |
---|
| 82 | definition set_joint_if_exit ≝ |
---|
[1252] | 83 | λglobals,pars. |
---|
[1245] | 84 | λexit: label. |
---|
[1252] | 85 | λp:joint_internal_function globals pars. |
---|
[1246] | 86 | λprf: lookup … (joint_if_code … p) exit ≠ None ?. |
---|
[1252] | 87 | mk_joint_internal_function globals pars |
---|
[1245] | 88 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
| 89 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
[1246] | 90 | (joint_if_code … p) (joint_if_entry … p) (dp … exit prf). |
---|
[1245] | 91 | |
---|
[1220] | 92 | definition set_luniverse ≝ |
---|
[1252] | 93 | λglobals,pars. |
---|
| 94 | λp : joint_internal_function globals pars. |
---|
[1220] | 95 | λluniverse: universe LabelTag. |
---|
[1252] | 96 | mk_joint_internal_function globals pars |
---|
| 97 | luniverse (joint_if_runiverse … p) (joint_if_result … p) |
---|
| 98 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
| 99 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
[1220] | 100 | |
---|
[1254] | 101 | definition set_runiverse ≝ |
---|
| 102 | λglobals,pars. |
---|
| 103 | λp : joint_internal_function globals pars. |
---|
| 104 | λruniverse: universe RegisterTag. |
---|
| 105 | mk_joint_internal_function globals pars |
---|
| 106 | (joint_if_luniverse … p) runiverse (joint_if_result … p) |
---|
| 107 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
| 108 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
| 109 | |
---|
[1252] | 110 | (* Specialized for graph_params *) |
---|
| 111 | definition add_graph ≝ |
---|
| 112 | λpars_,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars_ globals). |
---|
| 113 | let code ≝ add … (joint_if_code ?? p) l stmt in |
---|
| 114 | mk_joint_internal_function … (graph_params pars_ globals) |
---|
| 115 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
| 116 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
| 117 | code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)). |
---|
| 118 | normalize nodelta; |
---|
| 119 | [ cases (joint_if_entry … p) | cases (joint_if_exit … p)] |
---|
| 120 | #LBL #LBL_PRF @graph_add_lookup @LBL_PRF |
---|
| 121 | qed. |
---|
| 122 | |
---|
| 123 | definition set_locals ≝ |
---|
| 124 | λglobals,pars. |
---|
| 125 | λp : joint_internal_function globals pars. |
---|
| 126 | λlocals. |
---|
| 127 | mk_joint_internal_function globals pars |
---|
| 128 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
| 129 | (joint_if_params … p) locals (joint_if_stacksize … p) |
---|
| 130 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
| 131 | |
---|
[1233] | 132 | definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals). |
---|
[1176] | 133 | |
---|
[1246] | 134 | definition joint_program ≝ |
---|
| 135 | λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat. |
---|
[1176] | 136 | |
---|
| 137 | (****************************************************************************) |
---|
| 138 | |
---|
[1169] | 139 | (* Used in LTL and LIN *) |
---|
| 140 | inductive registers_move: Type[0] ≝ |
---|
| 141 | | from_acc: Register → registers_move |
---|
[1176] | 142 | | to_acc: Register → registers_move. |
---|