[733] | 1 | include "ERTL/ERTL.ma". |
---|
[1084] | 2 | include "LTL/LTL.ma". |
---|
[1153] | 3 | include "ERTL/spill.ma". |
---|
[1197] | 4 | include "ASM/Arithmetic.ma". |
---|
[1084] | 5 | |
---|
[1197] | 6 | definition fresh_label ≝ |
---|
| 7 | λglobals: list ident. |
---|
| 8 | λluniv. |
---|
| 9 | fresh LabelTag luniv. |
---|
[1153] | 10 | |
---|
[1311] | 11 | definition ltl_statement_graph ≝ |
---|
| 12 | λglobals. |
---|
| 13 | graph … (ltl_statement globals). |
---|
| 14 | |
---|
[1197] | 15 | definition add_graph ≝ |
---|
| 16 | λglobals. |
---|
| 17 | λlabel. |
---|
| 18 | λstmt: ltl_statement globals. |
---|
| 19 | λgraph: ltl_statement_graph globals. |
---|
| 20 | add LabelTag ? graph label stmt. |
---|
[1153] | 21 | |
---|
[1197] | 22 | definition generate ≝ |
---|
| 23 | λglobals: list ident. |
---|
| 24 | λluniv. |
---|
| 25 | λgraph: ltl_statement_graph globals. |
---|
| 26 | λstmt: ltl_statement globals. |
---|
| 27 | let 〈l, luniv〉 ≝ fresh_label globals luniv in |
---|
| 28 | let graph ≝ add_graph globals l stmt graph in |
---|
| 29 | 〈l, graph, luniv〉. |
---|
[1153] | 30 | |
---|
[1197] | 31 | definition num_locals ≝ |
---|
| 32 | λglobals. |
---|
| 33 | λint_fun. |
---|
[1311] | 34 | colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun). |
---|
[1153] | 35 | |
---|
[1197] | 36 | definition stacksize ≝ |
---|
| 37 | λglobals. |
---|
| 38 | λint_fun. |
---|
[1311] | 39 | colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun). |
---|
[1153] | 40 | |
---|
[1197] | 41 | definition adjust_off ≝ |
---|
| 42 | λglobals. |
---|
| 43 | λint_fun. |
---|
| 44 | λoff. |
---|
| 45 | let 〈ignore, int_off〉 ≝ half_add ? int_size off in |
---|
| 46 | let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in |
---|
| 47 | sub. |
---|
[1153] | 48 | |
---|
[1197] | 49 | definition get_stack: |
---|
[1311] | 50 | ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝ |
---|
[1197] | 51 | λglobals: list ident. |
---|
| 52 | λint_fun. |
---|
| 53 | λgraph: graph (ltl_statement (globals)). |
---|
| 54 | λr. |
---|
| 55 | λoff. |
---|
| 56 | λl. |
---|
[1311] | 57 | λoriginal_label. |
---|
[1197] | 58 | let off ≝ adjust_off globals int_fun off in |
---|
[1311] | 59 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
| 60 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in |
---|
| 61 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (LOAD … globals it it it) l) in |
---|
| 62 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in |
---|
| 63 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in |
---|
| 64 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in |
---|
| 65 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in |
---|
| 66 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in |
---|
| 67 | 〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉. |
---|
[1153] | 68 | |
---|
[1197] | 69 | definition set_stack: |
---|
| 70 | ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte |
---|
[1311] | 71 | → Register → label → ? ≝ |
---|
[1197] | 72 | λglobals: list ident. |
---|
| 73 | λint_fun. |
---|
| 74 | λgraph: graph (ltl_statement (globals)). |
---|
| 75 | λoff. |
---|
| 76 | λr. |
---|
| 77 | λl. |
---|
[1311] | 78 | λoriginal_label. |
---|
[1197] | 79 | let off ≝ adjust_off globals int_fun off in |
---|
[1311] | 80 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
| 81 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in |
---|
| 82 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc r)) l) in |
---|
| 83 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in |
---|
| 84 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in |
---|
| 85 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in |
---|
| 86 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in |
---|
| 87 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in |
---|
| 88 | 〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉. |
---|
[1153] | 89 | |
---|
[1311] | 90 | |
---|
| 91 | definition write ≝ |
---|
[1197] | 92 | λglobals: list ident. |
---|
[1311] | 93 | λint_fun: ertl_internal_function globals. |
---|
| 94 | λvaluation. |
---|
| 95 | λcoloured_graph. |
---|
[1197] | 96 | λgraph. |
---|
| 97 | λr. |
---|
| 98 | λl. |
---|
[1311] | 99 | λoriginal_label: label. |
---|
| 100 | match colouring valuation coloured_graph (inl … r) with |
---|
[1197] | 101 | [ decision_spill off ⇒ |
---|
[1311] | 102 | let luniv ≝ joint_if_luniverse … int_fun in |
---|
| 103 | let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in |
---|
[1197] | 104 | 〈RegisterSST, l, graph, luniv〉 |
---|
| 105 | | decision_colour hwr ⇒ |
---|
[1311] | 106 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
[1197] | 107 | 〈hwr, l, graph, luniv〉 |
---|
| 108 | ]. |
---|
[1153] | 109 | |
---|
[1311] | 110 | definition read ≝ |
---|
| 111 | λglobals: list ident. |
---|
| 112 | λint_fun: ertl_internal_function globals. |
---|
| 113 | λvaluation. |
---|
| 114 | λcoloured_graph. |
---|
[1197] | 115 | λgraph. |
---|
| 116 | λr. |
---|
| 117 | λstmt. |
---|
[1311] | 118 | λoriginal_label: label. |
---|
| 119 | match colouring valuation coloured_graph (inl … r) with |
---|
| 120 | [ decision_colour hwr ⇒ |
---|
| 121 | let luniv ≝ joint_if_luniverse … int_fun in |
---|
| 122 | 〈add_graph globals original_label (stmt hwr) graph, luniv〉 |
---|
[1197] | 123 | | decision_spill off ⇒ |
---|
| 124 | let temphwr ≝ RegisterSST in |
---|
[1311] | 125 | let luniv ≝ joint_if_luniverse … int_fun in |
---|
| 126 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in |
---|
| 127 | get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l original_label |
---|
[1197] | 128 | ]. |
---|
[1153] | 129 | |
---|
[1197] | 130 | definition move ≝ |
---|
| 131 | λglobals: list ident. |
---|
| 132 | λint_fun. |
---|
| 133 | λgraph: graph (ltl_statement globals). |
---|
| 134 | λdest: decision. |
---|
| 135 | λsrc: decision. |
---|
| 136 | λl: label. |
---|
[1311] | 137 | λoriginal_label: label. |
---|
[1197] | 138 | match dest with |
---|
| 139 | [ decision_colour dest_hwr ⇒ |
---|
| 140 | match src with |
---|
| 141 | [ decision_colour src_hwr ⇒ |
---|
[1311] | 142 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
[1197] | 143 | if eq_Register dest_hwr src_hwr then |
---|
[1311] | 144 | 〈add_graph globals original_label (GOTO … globals l) graph, luniv〉 |
---|
[1197] | 145 | else |
---|
[1311] | 146 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc dest_hwr)) l) in |
---|
| 147 | 〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc src_hwr)) l) graph, luniv〉 |
---|
| 148 | | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label |
---|
[1197] | 149 | ] |
---|
| 150 | | decision_spill dest_off ⇒ |
---|
| 151 | match src with |
---|
[1311] | 152 | [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label |
---|
[1197] | 153 | | decision_spill src_off ⇒ |
---|
[1311] | 154 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
| 155 | if eq_nat dest_off src_off then |
---|
| 156 | 〈add_graph globals original_label (GOTO … globals l) graph, luniv〉 |
---|
[1197] | 157 | else |
---|
| 158 | let temp_hwr ≝ RegisterSST in |
---|
[1311] | 159 | let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in |
---|
| 160 | get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label |
---|
[1197] | 161 | ] |
---|
| 162 | ]. |
---|
| 163 | |
---|
| 164 | definition newframe ≝ |
---|
| 165 | λglobals: list ident. |
---|
| 166 | λint_fun: ertl_internal_function globals. |
---|
| 167 | λgraph: ltl_statement_graph globals. |
---|
| 168 | λl: label. |
---|
[1311] | 169 | λoriginal_label: label. |
---|
[1197] | 170 | if eq_nat (stacksize globals int_fun) 0 then |
---|
[1311] | 171 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
| 172 | 〈add_graph globals original_label (GOTO … globals l) graph, luniv〉 |
---|
[1197] | 173 | else |
---|
[1311] | 174 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
| 175 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in |
---|
| 176 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPH) l) in |
---|
| 177 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPH (zero ?)) l) in |
---|
| 178 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterSPH)) l) in |
---|
| 179 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in |
---|
| 180 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPL) l) in |
---|
| 181 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (CLEAR_CARRY … globals) l) in |
---|
| 182 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in |
---|
| 183 | 〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc RegisterSPL)) l) graph, luniv〉. |
---|
[1197] | 184 | |
---|
| 185 | definition delframe ≝ |
---|
| 186 | λglobals. |
---|
| 187 | λint_fun. |
---|
| 188 | λgraph: graph (ltl_statement globals). |
---|
| 189 | λl. |
---|
[1311] | 190 | λoriginal_label: label. |
---|
[1197] | 191 | if eq_nat (stacksize globals int_fun) 0 then |
---|
[1311] | 192 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
| 193 | 〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉 |
---|
[1197] | 194 | else |
---|
[1311] | 195 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
| 196 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in |
---|
| 197 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in |
---|
| 198 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in |
---|
| 199 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in |
---|
| 200 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in |
---|
| 201 | 〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉. |
---|
[1197] | 202 | |
---|
[1311] | 203 | definition translate_statement: |
---|
| 204 | ∀globals: list ident. ertl_internal_function globals → ∀v: valuation. |
---|
| 205 | coloured_graph v → ltl_statement_graph globals → ertl_statement globals → |
---|
| 206 | label → ((ltl_statement_graph globals) × (universe LabelTag)) ≝ |
---|
[1197] | 207 | λglobals: list ident. |
---|
| 208 | λint_fun. |
---|
[1311] | 209 | λvaluation. |
---|
| 210 | λcoloured_graph: coloured_graph valuation. |
---|
[1197] | 211 | λgraph: ltl_statement_graph globals. |
---|
| 212 | λstmt: ertl_statement globals. |
---|
[1311] | 213 | λoriginal_label: label. |
---|
[1197] | 214 | match stmt with |
---|
[1311] | 215 | [ sequential seq l ⇒ |
---|
| 216 | let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in |
---|
[1197] | 217 | match seq with |
---|
[1311] | 218 | [ COMMENT c ⇒ |
---|
| 219 | 〈add_graph globals original_label (sequential … (COMMENT … c) l) graph, luniv〉 |
---|
| 220 | | COST_LABEL cost_lbl ⇒ |
---|
| 221 | 〈add_graph globals original_label (sequential … (COST_LABEL … cost_lbl) l) graph, luniv〉 |
---|
| 222 | | POP r ⇒ |
---|
| 223 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 224 | let int_fun ≝ set_luniverse globals ? int_fun luniv in |
---|
| 225 | let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in |
---|
| 226 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in |
---|
| 227 | 〈add_graph globals original_label (sequential ltl_params_ globals (POP … it) l) graph, luniv〉 |
---|
| 228 | | PUSH r ⇒ |
---|
| 229 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (PUSH … globals it) l) in |
---|
| 230 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 231 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 232 | let int_fun ≝ set_luniverse globals ? int_fun luniv in |
---|
| 233 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 234 | 〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉 |
---|
| 235 | | COND srcr lbl_true ⇒ |
---|
| 236 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (COND … it lbl_true) l) in |
---|
| 237 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 238 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 239 | let int_fun' ≝ set_luniverse globals ? int_fun luniv in |
---|
| 240 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 241 | 〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉 |
---|
| 242 | | CALL_ID f ignore ignore' ⇒ 〈add_graph globals original_label (sequential … (CALL_ID … f ignore ignore') l) graph, luniv〉 |
---|
| 243 | | STORE addr1 addr2 srcr ⇒ |
---|
| 244 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (STORE … it it it) l) in |
---|
| 245 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST1)) l) in |
---|
| 246 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in |
---|
| 247 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in |
---|
| 248 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in |
---|
| 249 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 250 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 251 | let int_fun ≝ set_luniverse globals ? int_fun luniv in |
---|
| 252 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 253 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in |
---|
| 254 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 255 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 256 | let int_fun ≝ set_luniverse globals ? int_fun luniv in |
---|
| 257 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 258 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST1)) fresh_lbl) in |
---|
| 259 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 260 | let int_fun ≝ set_luniverse globals ? int_fun luniv in |
---|
| 261 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 262 | 〈add_graph globals original_label (GOTO … l) graph, luniv〉 |
---|
| 263 | | LOAD destr addr1 addr2 ⇒ |
---|
| 264 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 265 | let int_fun ≝ set_luniverse globals ? int_fun luniv in |
---|
| 266 | let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in |
---|
| 267 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in |
---|
| 268 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (LOAD … it it it) l) in |
---|
| 269 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in |
---|
| 270 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in |
---|
| 271 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in |
---|
| 272 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 273 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 274 | let int_fun ≝ set_luniverse globals ? int_fun luniv in |
---|
| 275 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 276 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in |
---|
| 277 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 278 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 279 | let int_fun ≝ set_luniverse globals ? int_fun luniv in |
---|
| 280 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 281 | 〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉 |
---|
| 282 | | CLEAR_CARRY ⇒ 〈add_graph globals original_label (sequential … (CLEAR_CARRY …) l) graph, luniv〉 |
---|
| 283 | | SET_CARRY ⇒ 〈add_graph globals original_label (sequential … (SET_CARRY …) l) graph, luniv〉 |
---|
| 284 | | OP2 op2 destr srcr1 srcr2 ⇒ |
---|
| 285 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 286 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 287 | let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in |
---|
| 288 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in |
---|
| 289 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP2 … op2 it it RegisterB) l) in |
---|
| 290 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 291 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 292 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 293 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterB)) fresh_lbl) in |
---|
| 294 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 295 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 296 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 297 | 〈add_graph globals original_label (GOTO … l) graph, luniv〉 |
---|
| 298 | | OP1 op1 destr srcr ⇒ |
---|
| 299 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 300 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 301 | let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in |
---|
| 302 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in |
---|
| 303 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP1 … op1 it it) l) in |
---|
| 304 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 305 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 306 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 307 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in |
---|
| 308 | 〈add_graph globals original_label (GOTO … l) graph, luniv〉 |
---|
| 309 | | INT r i ⇒ |
---|
| 310 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 311 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 312 | let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in |
---|
| 313 | 〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw i) l) graph, luniv〉 |
---|
| 314 | | MOVE pair_regs ⇒ |
---|
[1197] | 315 | let regl ≝ \fst pair_regs in |
---|
| 316 | let regr ≝ \snd pair_regs in |
---|
| 317 | match regl with |
---|
| 318 | [ pseudo p1 ⇒ |
---|
[1311] | 319 | match regr with |
---|
| 320 | [ pseudo p2 ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label |
---|
| 321 | | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label |
---|
[1197] | 322 | ] |
---|
| 323 | | hardware h1 ⇒ |
---|
| 324 | match regr with |
---|
[1311] | 325 | [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label |
---|
[1197] | 326 | | hardware h2 ⇒ |
---|
[1311] | 327 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc h1)) l) in |
---|
| 328 | 〈add_graph globals original_label (sequential ltl_params_ … (MOVE … (to_acc h2)) l) graph, luniv〉 |
---|
[1197] | 329 | ] |
---|
| 330 | ] |
---|
[1311] | 331 | | ADDRESS lbl prf dpl dph ⇒ |
---|
| 332 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 333 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 334 | let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in |
---|
| 335 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw1)) l) in |
---|
| 336 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPH)) l) in |
---|
| 337 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (ADDRESS … globals lbl prf it it) l) in |
---|
| 338 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 339 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 340 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 341 | let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in |
---|
| 342 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw2)) l) in |
---|
| 343 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPL)) l) in |
---|
| 344 | 〈add_graph globals original_label (sequential ltl_params_ globals (ADDRESS … lbl prf it it) l) graph, luniv〉 |
---|
| 345 | | extension ext ⇒ |
---|
| 346 | match ext with |
---|
| 347 | [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label |
---|
| 348 | | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l original_label |
---|
| 349 | | ertl_st_ext_frame_size r ⇒ |
---|
| 350 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 351 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 352 | let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in |
---|
| 353 | 〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉 |
---|
| 354 | ] |
---|
| 355 | | OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒ |
---|
| 356 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 357 | let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in |
---|
| 358 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in |
---|
| 359 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OPACCS … opaccs it it it it) l) in |
---|
| 360 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 361 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 362 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 363 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in |
---|
| 364 | let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterB)) fresh_lbl) in |
---|
| 365 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 366 | let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in |
---|
| 367 | let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in |
---|
| 368 | let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in |
---|
| 369 | 〈add_graph globals original_label (GOTO … globals fresh_lbl) graph, luniv〉 |
---|
[1197] | 370 | ] |
---|
[1311] | 371 | | RETURN ⇒ 〈add_graph globals original_label (RETURN ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉 |
---|
| 372 | | GOTO l ⇒ 〈add_graph globals original_label (GOTO ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉 |
---|
[1197] | 373 | ]. |
---|
| 374 | |
---|
[1311] | 375 | lemma Sm_leq_n_m_leq_n: |
---|
| 376 | ∀m, n: nat. |
---|
| 377 | S m ≤ n → m ≤ n. |
---|
| 378 | #m #n /2/ |
---|
| 379 | qed. |
---|
| 380 | |
---|
| 381 | let rec fold_aux |
---|
| 382 | (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat) |
---|
| 383 | on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b ≝ |
---|
| 384 | match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b with |
---|
| 385 | [ O ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16. |
---|
| 386 | match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with |
---|
| 387 | [ Leaf l ⇒ λproof. f path l seed |
---|
| 388 | | Stub s ⇒ λproof. seed |
---|
| 389 | | Node n' l r ⇒ λabsrd. ⊥ |
---|
| 390 | ] (refl … 0) |
---|
| 391 | | S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16 - S n'). |
---|
| 392 | match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with |
---|
| 393 | [ Leaf l ⇒ λabsrd. ⊥ |
---|
| 394 | | Stub s ⇒ λproof. seed |
---|
| 395 | | Node n'' l r ⇒ λproof. |
---|
| 396 | fold_aux a b f (fold_aux a b f seed n' ? (l⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((false:::path)⌈S (16 - S n') ↦ 16 - n'⌉)) n' ? (r⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((true:::path)⌈S (16 - S n') ↦ 16 - n'⌉) |
---|
| 397 | ] (refl … (S n')) |
---|
| 398 | ]. |
---|
| 399 | [ 1, 2: destruct(absrd) |
---|
| 400 | | 3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le // |
---|
| 401 | | 4,7: destruct(proof) % |
---|
| 402 | | 5,6: @Sm_leq_n_m_leq_n // ] |
---|
| 403 | qed. |
---|
| 404 | |
---|
| 405 | definition bvt_fold ≝ |
---|
| 406 | λa, b: Type[0]. |
---|
| 407 | λf: label → a → b → b. |
---|
| 408 | λtrie: BitVectorTrie a 16. |
---|
| 409 | λseed: b. |
---|
| 410 | let f' ≝ λbv: BitVector 16. λa. λb. |
---|
| 411 | f (an_identifier LabelTag bv) a b |
---|
| 412 | in |
---|
| 413 | fold_aux a b f' seed 16 ? trie [[]]. |
---|
| 414 | // |
---|
| 415 | qed. |
---|
| 416 | |
---|
| 417 | definition graph_fold ≝ |
---|
| 418 | λglobals. |
---|
| 419 | λb : Type[0]. |
---|
| 420 | λf : label → ertl_statement globals → b → b. |
---|
| 421 | λgraph: graph (ertl_statement globals). |
---|
| 422 | λseed : b. |
---|
| 423 | match graph with |
---|
| 424 | [ an_id_map tree ⇒ bvt_fold (ertl_statement globals) b f tree seed |
---|
| 425 | ]. |
---|
| 426 | |
---|
| 427 | definition translate_internal: ∀globals: list ident. |
---|
| 428 | ertl_internal_function globals → ltl_internal_function globals ≝ |
---|
[1197] | 429 | λglobals: list ident. |
---|
[1311] | 430 | λint_fun: ertl_internal_function globals. |
---|
| 431 | let graph ≝ (empty_map … : ltl_statement_graph globals) in |
---|
| 432 | let valuation ≝ analyse globals int_fun in |
---|
| 433 | let coloured_graph ≝ build valuation in |
---|
| 434 | let 〈graph, luniv〉 ≝ graph_fold globals ((ltl_statement_graph globals) × (universe LabelTag)) (λlabel: label. λstmt: ertl_statement globals. λgraph_luniv: (? × (universe LabelTag)). |
---|
| 435 | let 〈graph, luniv〉 ≝ graph_luniv in |
---|
| 436 | match eliminable globals (valuation label) stmt with |
---|
| 437 | [ Some successor ⇒ 〈add_graph globals label (GOTO … successor) graph, luniv〉 |
---|
| 438 | | None ⇒ |
---|
| 439 | translate_statement globals int_fun valuation coloured_graph graph stmt label |
---|
| 440 | ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉 |
---|
[1153] | 441 | in |
---|
[1311] | 442 | match joint_if_entry … int_fun with |
---|
| 443 | [ dp entry_label entry_label_prf ⇒ |
---|
| 444 | match joint_if_exit … int_fun with |
---|
| 445 | [ dp exit_label exit_label_prf ⇒ |
---|
| 446 | mk_joint_internal_function globals (ltl_params globals) |
---|
| 447 | luniv (joint_if_runiverse … int_fun) |
---|
| 448 | it it it (joint_if_stacksize … int_fun) |
---|
| 449 | graph ? ? |
---|
| 450 | ] |
---|
| 451 | ]. |
---|
| 452 | [1: % |
---|
| 453 | [1: @entry_label |
---|
| 454 | |2: cases daemon (* XXX *) |
---|
[1084] | 455 | ] |
---|
[1311] | 456 | |2: % |
---|
| 457 | [1: @exit_label |
---|
| 458 | |2: cases daemon (* XXX *) |
---|
| 459 | ] |
---|
| 460 | ] |
---|
| 461 | qed. |
---|
[1084] | 462 | |
---|
[1311] | 463 | definition ertl_to_ltl: ertl_program → ltl_program ≝ |
---|
| 464 | λp.transform_program … p (transf_fundef … (translate_internal …)). |
---|