Changeset 1170 for src/ERTL/ERTLToLTL.ma
 Timestamp:
 Sep 2, 2011, 12:28:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1168 r1170 72 72 〈joint_st_sequential ? ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉. 73 73 74 definition set_stack ≝ 75 λint_fun. 76 λglobals. 74 definition set_stack: 75 ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte 76 → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag)) ≝ 77 λglobals: list ident. 78 λint_fun. 77 79 λgraph: graph (ltl_statement (globals)). 78 80 λoff. 79 81 λr. 80 82 λl. 81 let off ≝ adjust_off int_fun off in 82 let luniv ≝ ertl_if_luniverse int_fun in 83 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_store globals) l) in 84 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in 85 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 86 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in 87 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in 88 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 89 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in 90 〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, 〈graph, luniv〉〉. 91 92 definition write ≝ 93 λint_fun. 94 λglobals. 95 λgraph: graph (ltl_statement (globals)). 96 λr: register. 97 λl: label. 83 let off ≝ adjust_off globals int_fun off in 84 let luniv ≝ ertl_if_luniverse globals int_fun in 85 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? ? globals (joint_instr_store ltl_params … globals it it it) l) in 86 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in 87 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in 88 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in 89 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in 90 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 91 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in 92 〈joint_st_sequential ? ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉. 93 94 definition write: 95 ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label → 96 ? ≝ 97 λglobals: list ident. 98 λint_fun. 99 λgraph. 100 λr. 101 λl. 98 102 match lookup r with 99 103 [ decision_spill off ⇒ 100 let 〈stmt, graph, luniv〉 ≝ set_stack int_fun globalsgraph off RegisterSST l in104 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST l in 101 105 let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in 102 〈RegisterSST, 〈l, 〈graph, luniv〉〉〉106 〈RegisterSST, l, graph, luniv〉 103 107  decision_colour hwr ⇒ 104 let luniv ≝ ertl_if_luniverse int_fun in105 〈hwr, 〈l, 〈graph, luniv〉〉〉108 let luniv ≝ ertl_if_luniverse globals int_fun in 109 〈hwr, l, graph, luniv〉 106 110 ]. 107 111 108 definition read ≝ 109 λint_fun. 110 λglobals. 111 λgraph: graph (ltl_statement (globals)). 112 λr: register. 113 λstmt: Register → ltl_statement globals. 112 definition read: 113 ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register 114 → (Register → ltl_statement globals) → ? ≝ 115 λglobals. 116 λint_fun. 117 λgraph. 118 λr. 119 λstmt. 114 120 match lookup r with 115 [ decision_colour hwr ⇒ generate globals graph (stmt hwr)121 [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr) 116 122  decision_spill off ⇒ 117 123 let temphwr ≝ RegisterSST in 118 let 〈l, graph 〉 ≝ generate globalsgraph (stmt temphwr) in119 let 〈stmt, graph 〉 ≝ get_stack int_fun globalsgraph temphwr off l in120 generate globals graph stmt124 let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr) in 125 let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off l in 126 generate globals luniv graph stmt 121 127 ]. 122 128 123 129 definition move ≝ 124 λ int_fun.125 λ globals: list ident.130 λglobals: list ident. 131 λint_fun. 126 132 λgraph: graph (ltl_statement globals). 127 133 λdest: decision. … … 132 138 match src with 133 139 [ decision_colour src_hwr ⇒ 140 let luniv ≝ ertl_if_luniverse globals int_fun in 134 141 if eq_Register dest_hwr src_hwr then 135 〈joint_st_goto ? globals l, graph〉142 〈joint_st_goto … globals l, graph, luniv〉 136 143 else 137 let 〈l, graph 〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in138 〈joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l, graph〉139  decision_spill src_off ⇒ get_stack int_fun globalsgraph dest_hwr src_off l144 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in 145 〈joint_st_sequential ? ? globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉 146  decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l 140 147 ] 141 148  decision_spill dest_off ⇒ 142 149 match src with 143 [ decision_colour src_hwr ⇒ set_stack int_fun globalsgraph dest_off src_hwr l150 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwr l 144 151  decision_spill src_off ⇒ 152 let luniv ≝ ertl_if_luniverse globals int_fun in 145 153 if eq_bv ? dest_off src_off then 146 〈joint_st_goto ? globals l, graph〉154 〈joint_st_goto … globals l, graph, luniv〉 147 155 else 148 156 let temp_hwr ≝ RegisterSST in 149 let 〈stmt, graph 〉 ≝ set_stack int_fun globalsgraph dest_off temp_hwr l in150 let 〈l, graph 〉 ≝ generate globalsgraph stmt in151 get_stack int_fun globalsgraph temp_hwr src_off l157 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in 158 let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in 159 get_stack globals int_fun graph temp_hwr src_off l 152 160 ] 153 161 ]. 154 162 155 163 definition newframe ≝ 156 λ int_fun.157 λ globals.158 λgraph: graph (ltl_statement globals).159 λl. 160 if eq_nat (stacksize int_fun) 0 then164 λglobals. 165 λint_fun. 166 λgraph: ltl_statement_graph globals. 167 λl. 168 if eq_nat (stacksize globals int_fun) 0 then 161 169 〈joint_st_goto ? globals l, graph〉 162 170 else 163 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in 164 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in 165 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in 166 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in 167 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in 168 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in 169 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in 170 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in 171 〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph〉. 171 let luniv ≝ ertl_if_luniverse globals int_fun in 172 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in 173 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in 174 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in 175 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in 176 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in 177 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in 178 let 〈l, graph, lunive〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in 179 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in 180 〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph, luniv〉. 172 181 173 182 definition delframe ≝
Note: See TracChangeset
for help on using the changeset viewer.