Changeset 1311 for Deliverables/D3.3/idlookupbranch/ERTL/ERTLToLTL.ma
 Timestamp:
 Oct 6, 2011, 6:45:54 PM (8 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch
 Property svn:mergeinfo changed
/src merged: 1198,12061233,12361260,12621264,1266,12681271,12741276,12781290,1292
 Property svn:mergeinfo changed

Deliverables/D3.3/idlookupbranch/ERTL/ERTLToLTL.ma
r1197 r1311 2 2 include "LTL/LTL.ma". 3 3 include "ERTL/spill.ma". 4 include "ERTL/build.ma".5 include "utilities/Interference.ma".6 4 include "ASM/Arithmetic.ma". 7 8 (* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)9 10 inductive decision: Type[0] ≝11  decision_spill: Byte → decision12  decision_colour: Register → decision.13 14 definition interference_lookup ≝15 λglobals.16 λint_fun.17 λr.18 let 〈liveafter, graph〉 ≝ build globals int_fun in19 let lkup ≝ ig_lookup graph r in20 vm_find lkup colour_colouring.21 22 definition lookup: register → decision ≝23 λr.24 match ? r with25 [ colour_spill26 27 axiom lookup: register → decision.28 5 29 6 definition fresh_label ≝ … … 31 8 λluniv. 32 9 fresh LabelTag luniv. 10 11 definition ltl_statement_graph ≝ 12 λglobals. 13 graph … (ltl_statement globals). 33 14 34 15 definition add_graph ≝ … … 51 32 λglobals. 52 33 λint_fun. 53 colour_locals + ( ertl_if_stacksize globalsint_fun).34 colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun). 54 35 55 36 definition stacksize ≝ 56 37 λglobals. 57 38 λint_fun. 58 colour_locals + ( ertl_if_stacksize globalsint_fun).39 colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun). 59 40 60 41 definition adjust_off ≝ … … 67 48 68 49 definition get_stack: 69 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → 70 ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag) 71 ≝ 50 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝ 72 51 λglobals: list ident. 73 52 λint_fun. … … 76 55 λoff. 77 56 λl. 57 λoriginal_label. 78 58 let off ≝ adjust_off globals int_fun off in 79 let luniv ≝ ertl_if_luniverse globalsint_fun in80 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc r)) l) in81 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_load… globals it it it) l) in82 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterDPH)) l) in83 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Addcit RegisterSPH) l) in84 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_int… globals RegisterA (zero ?)) l) in85 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc RegisterDPL)) l) in86 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_op2 … globals Addit RegisterSPL) l) in87 〈 joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l,graph, luniv〉.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〉. 88 68 89 69 definition set_stack: 90 70 ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte 91 → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag))≝71 → Register → label → ? ≝ 92 72 λglobals: list ident. 93 73 λint_fun. … … 96 76 λr. 97 77 λl. 78 λoriginal_label. 98 79 let off ≝ adjust_off globals int_fun off in 99 let luniv ≝ ertl_if_luniverse globals int_fun in 100 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in 101 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in 102 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 103 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in 104 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in 105 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 106 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in 107 〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉. 108 109 definition write: 110 ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label → 111 ? ≝ 112 λglobals: list ident. 113 λint_fun. 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〉. 89 90 91 definition write ≝ 92 λglobals: list ident. 93 λint_fun: ertl_internal_function globals. 94 λvaluation. 95 λcoloured_graph. 114 96 λgraph. 115 97 λr. 116 98 λl. 117 match lookup r with 99 λoriginal_label: label. 100 match colouring valuation coloured_graph (inl … r) with 118 101 [ decision_spill off ⇒ 119 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST lin120 let 〈 l, graph, int_fun〉 ≝ generate globals luniv graph stmtin102 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 121 104 〈RegisterSST, l, graph, luniv〉 122 105  decision_colour hwr ⇒ 123 let luniv ≝ ertl_if_luniverse globalsint_fun in106 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 124 107 〈hwr, l, graph, luniv〉 125 108 ]. 126 109 127 definition read :128 ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register129 → (Register → ltl_statement globals) → ? ≝130 λ globals.131 λ int_fun.110 definition read ≝ 111 λglobals: list ident. 112 λint_fun: ertl_internal_function globals. 113 λvaluation. 114 λcoloured_graph. 132 115 λgraph. 133 116 λr. 134 117 λstmt. 135 match lookup r with 136 [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr) 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〉 137 123  decision_spill off ⇒ 138 124 let temphwr ≝ RegisterSST in 139 let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr)in140 let 〈 stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off lin141 ge nerate globals luniv graph stmt125 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 142 128 ]. 143 129 … … 149 135 λsrc: decision. 150 136 λl: label. 137 λoriginal_label: label. 151 138 match dest with 152 139 [ decision_colour dest_hwr ⇒ 153 140 match src with 154 141 [ decision_colour src_hwr ⇒ 155 let luniv ≝ ertl_if_luniverse globalsint_fun in142 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 156 143 if eq_Register dest_hwr src_hwr then 157 〈 joint_st_goto … globals l,graph, luniv〉144 〈add_graph globals original_label (GOTO … globals l) graph, luniv〉 158 145 else 159 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move… globals (from_acc dest_hwr)) l) in160 〈 joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l,graph, luniv〉161  decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_offl146 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 162 149 ] 163 150  decision_spill dest_off ⇒ 164 151 match src with 165 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwrl152 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label 166 153  decision_spill src_off ⇒ 167 let luniv ≝ ertl_if_luniverse globalsint_fun in168 if eq_ bv ?dest_off src_off then169 〈 joint_st_goto … globals l,graph, luniv〉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〉 170 157 else 171 158 let temp_hwr ≝ RegisterSST in 172 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in 173 let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in 174 get_stack globals int_fun graph temp_hwr src_off l 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 175 161 ] 176 162 ]. … … 181 167 λgraph: ltl_statement_graph globals. 182 168 λl: label. 169 λoriginal_label: label. 183 170 if eq_nat (stacksize globals int_fun) 0 then 184 〈joint_st_goto ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉 171 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 172 〈add_graph globals original_label (GOTO … globals l) graph, luniv〉 185 173 else 186 let luniv ≝ ertl_if_luniverse globalsint_fun in187 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential ltl_params globals (joint_instr_move… globals (from_acc RegisterSPH)) l) in188 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential ltl_params globals (joint_instr_op2 … globals Subit RegisterDPH) l) in189 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential ltl_params globals (joint_instr_int… globals RegisterDPH (zero ?)) l) in190 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential ltl_params globals (joint_instr_move… globals (to_acc RegisterSPH)) l) in191 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential ltl_params globals (joint_instr_move… globals (from_acc RegisterSPL)) l) in192 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential ltl_params globals (joint_instr_op2 … globals Subit RegisterDPL) l) in193 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential ltl_params globals (joint_instr_clear_carry… globals) l) in194 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential ltl_params globals (joint_instr_int… globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in195 〈 joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l,graph, luniv〉.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〉. 196 184 197 185 definition delframe ≝ … … 200 188 λgraph: graph (ltl_statement globals). 201 189 λl. 190 λoriginal_label: label. 202 191 if eq_nat (stacksize globals int_fun) 0 then 203 〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globals int_fun〉 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〉 204 194 else 205 let luniv ≝ ertl_if_luniverse globals int_fun in 206 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 207 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in 208 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in 209 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in 210 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in 211 〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉. 212 213 definition translate_statement ≝ 214 λglobals: list ident. 215 λint_fun. 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〉. 202 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)) ≝ 207 λglobals: list ident. 208 λint_fun. 209 λvaluation. 210 λcoloured_graph: coloured_graph valuation. 216 211 λgraph: ltl_statement_graph globals. 217 212 λstmt: ertl_statement globals. 213 λoriginal_label: label. 218 214 match stmt with 219 [ joint_st_sequential seq l ⇒220 let luniv ≝ ertl_if_luniverse globalsint_fun in215 [ sequential seq l ⇒ 216 let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in 221 217 match seq with 222 [ joint_instr_comment c ⇒ 223 〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉 224  joint_instr_cost_label cost_lbl ⇒ 225 〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉 226  joint_instr_pop r ⇒ 227 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in 228 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 229 〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉 230  joint_instr_push r ⇒ 231 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in 232 let int_fun ≝ set_luniverse globals int_fun luniv in 233 let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 234 〈joint_st_goto ltl_params globals l, graph, luniv〉 235  joint_instr_cond srcr lbl_true ⇒ 236 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in 237 let int_fun ≝ set_luniverse globals int_fun luniv in 238 let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 239 〈joint_st_goto ltl_params globals l, graph, luniv〉 240  joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉 241  joint_instr_store addr1 addr2 srcr ⇒ 242 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in 243 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in 244 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 245 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 246 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 247 let int_fun ≝ set_luniverse globals int_fun luniv in 248 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 249 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 250 let int_fun ≝ set_luniverse globals int_fun luniv in 251 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 252 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in 253 let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 254 〈joint_st_goto ltl_params globals l, graph, luniv〉 255  joint_instr_load destr addr1 addr2 ⇒ 256 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in 257 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 258 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in 259 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 260 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 261 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 262 let int_fun ≝ set_luniverse globals int_fun luniv in 263 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 264 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 265 let int_fun ≝ set_luniverse globals int_fun luniv in 266 let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 267 〈joint_st_goto ltl_params globals l, graph, luniv〉 268  joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉 269  joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉 270  joint_instr_op2 op2 destr srcr ⇒ 271 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in 272 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 273 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in 274 let luniv ≝ set_luniverse globals int_fun luniv in 275 let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 276 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 277 let luniv ≝ set_luniverse globals int_fun luniv in 278 let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 279 〈joint_st_goto ltl_params globals l, graph, luniv〉 280  joint_instr_op1 op1 acc_a ⇒ 281 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in 282 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 283 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in 284 let int_fun ≝ set_luniverse globals int_fun luniv in 285 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 286 〈joint_st_goto ltl_params globals l, graph, luniv〉 287  joint_instr_int r i ⇒ 288 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in 289 〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉 290  joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒ 291 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in 292 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 293 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 294 let luniv ≝ set_luniverse globals int_fun luniv in 295 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 296 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 297 let luniv ≝ set_luniverse globals int_fun luniv in 298 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 299 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in 300 let luniv ≝ set_luniverse globals int_fun luniv in 301 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in 302 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 303 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in 304 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 305 let luniv ≝ set_luniverse globals int_fun luniv in 306 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 307 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 308 let luniv ≝ set_luniverse globals int_fun luniv in 309 let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 310 〈joint_st_goto ltl_params globals l, graph, luniv〉 311  joint_instr_move pair_regs ⇒ 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 ⇒ 312 315 let regl ≝ \fst pair_regs in 313 316 let regr ≝ \snd pair_regs in 314 317 match regl with 315 318 [ pseudo p1 ⇒ 316 match regr with 317 [ pseudo p2 ⇒ move globals int_fun graph ( lookup p1) (lookup p2)l318  hardware h ⇒ move globals int_fun graph ( lookup p1) (decision_colour h)l319 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 319 322 ] 320 323  hardware h1 ⇒ 321 324 match regr with 322 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) ( lookup p)l325 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label 323 326  hardware h2 ⇒ 324 let 〈l, graph, luniv〉 ≝ generate globals luniv graph ( joint_st_sequential … globals (joint_instr_move … globals(from_acc h1)) l) in325 〈 joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc h2)) l,graph, luniv〉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〉 326 329 ] 327 330 ] 328  joint_instr_address lbl prf dpl dph ⇒ 329 let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun graph dph l in 330 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in 331 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in 332 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in 333 let int_fun ≝ set_luniverse globals int_fun luniv in 334 let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun graph dpl l in 335 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in 336 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in 337 〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉 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〉 338 370 ] 339  joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉 340  joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉 341  joint_st_extension ext ⇒ 342 match ext with 343 [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l 344  ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l 345  ertl_st_ext_frame_size r l ⇒ 346 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in 347 〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉 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〉 373 ]. 374 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 ≝ 429 λglobals: list ident. 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〉 441 in 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 *) 348 455 ] 349 ]. 350 351 definition translate_internal ≝ 352 λglobals: list ident. 353 λf. 354 λint_fun: ertl_internal_function. 355 let lookup ≝ λr. 356 match lookup r with 357  colour_spill > 358 ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring) 359  colour_colour color > 360 ERTLToLTLI.Color color 361 in 362 let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in 363 let stacksize ≝ (ertl_if_params int_fun) + locals in 364 mk_ltl_internal_function 365 globals 366 (ertl_if_luniverse int_fun) 367 (ertl_if_runiverse int_fun) 368 stacksize. 369 370 let () = 371 Label.Map.iter (fun label stmt > 372 let stmt = 373 match Liveness.eliminable (G.liveafter label) stmt with 374  Some successor > 375 LTL.St_skip successor 376  None > 377 I.translate_statement stmt 378 in 379 graph := Label.Map.add label stmt !graph 380 ) int_fun.ERTL.f_graph 381 in 382 383 definition translate_funct ≝ 384 λname_def. 385 let 〈name, def〉 ≝ name_def in 386 let def' ≝ 387 match def with 388 [ Internal def ⇒ Internal ? (translate_internal name def) 389  External def ⇒ External ? def 456 2: % 457 [1: @exit_label 458 2: cases daemon (* XXX *) 390 459 ] 391 in 392 〈name, def'〉. 393 394 definition translate ≝ 395 λp. 396 let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in 397 mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p). 460 ] 461 qed. 462 463 definition ertl_to_ltl: ertl_program → ltl_program ≝ 464 λp.transform_program … p (transf_fundef … (translate_internal …)).
Note: See TracChangeset
for help on using the changeset viewer.