Changeset 1160
 Timestamp:
 Aug 31, 2011, 12:30:27 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1154 r1160 1 1 include "ERTL/ERTL.ma". 2 include "ERTL/ERTLToLTLI.ma".3 2 include "LTL/LTL.ma". 4 3 include "ERTL/spill.ma". 5 6 include "ERTL/ERTL.ma".7 include "LTL/LTL.ma".8 4 include "ASM/Arithmetic.ma". 9 5 … … 15 11 16 12 axiom lookup: register → decision. 17 axiom generate: ∀globals: list ident. ltl_statement globals → label. 18 axiom fresh_label: ∀globals: list ident. ltl_function_definition globals → ltl_function_definition globals × label. 19 axiom add_graph: ∀globals. label → ltl_statement globals → ltl_statement_graph globals → ltl_statement_graph globals. 20 axiom num_locals: nat. 13 14 definition fresh_label ≝ 15 λglobals: list ident. 16 λluniv. 17 fresh LabelTag luniv. 18 19 definition add_graph ≝ 20 λglobals. 21 λlabel. 22 λstmt: ltl_statement globals. 23 λgraph: ltl_statement_graph globals. 24 add LabelTag ? graph label stmt. 25 26 definition generate ≝ 27 λglobals: list ident. 28 λluniv. 29 λgraph: ltl_statement_graph globals. 30 λstmt: ltl_statement globals. 31 let 〈l, luniv〉 ≝ fresh_label globals luniv in 32 let graph ≝ add_graph globals l stmt graph in 33 〈l, 〈graph, luniv〉〉. 21 34 22 35 definition num_locals ≝ … … 29 42 30 43 definition adjust_off ≝ 44 λint_fun. 31 45 λoff. 32 46 let 〈ignore, int_off〉 ≝ half_add ? int_size off in 33 let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? num_locals) int_off false in47 let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals int_fun)) int_off false in 34 48 sub. 35 49 36 50 definition get_stack ≝ 37 λglobals. 51 λint_fun. 52 λglobals. 53 λgraph: graph (ltl_statement (globals)). 38 54 λr. 39 55 λoff. 40 56 λl. 41 let off ≝ adjust_off off in 42 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in 43 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in 44 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 45 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in 46 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in 47 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 48 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in 49 joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l. 57 let off ≝ adjust_off int_fun off in 58 let luniv ≝ ertl_if_luniverse int_fun in 59 let 〈l, 〈graph, luniv〉〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in 60 let 〈l, graph〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in 61 let 〈l, graph〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 62 let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in 63 let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in 64 let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 65 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in 66 〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, graph〉. 50 67 51 68 definition set_stack ≝ 52 λglobals. 69 λint_fun. 70 λglobals. 71 λgraph: graph (ltl_statement (globals)). 53 72 λoff. 54 73 λr. 55 74 λl. 56 let off ≝ adjust_off off in57 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_store globals) l) in58 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in59 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in60 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in61 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in62 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in63 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in64 joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.75 let off ≝ adjust_off int_fun off in 76 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in 77 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in 78 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 79 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in 80 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in 81 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 82 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in 83 〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, graph〉. 65 84 66 85 definition write ≝ 67 λglobals. 86 λint_fun. 87 λglobals. 88 λgraph: graph (ltl_statement (globals)). 68 89 λr: register. 69 90 λl: label. 70 91 match lookup r with 71 [ decision_spill off ⇒ 〈RegisterSST, generate globals (set_stack globals off RegisterSST l)〉 72  decision_colour hwr ⇒ 〈hwr, l〉 92 [ decision_spill off ⇒ 93 let 〈stmt, graph〉 ≝ set_stack int_fun globals graph off RegisterSST l in 94 〈RegisterSST, generate globals graph stmt〉 95  decision_colour hwr ⇒ 〈hwr, 〈l, graph〉〉 73 96 ]. 74 97 75 98 definition read ≝ 76 λglobals. 99 λint_fun. 100 λglobals. 101 λgraph: graph (ltl_statement (globals)). 77 102 λr: register. 78 103 λstmt: Register → ltl_statement globals. 79 104 match lookup r with 80 [ decision_colour hwr ⇒ generate globals (stmt hwr)105 [ decision_colour hwr ⇒ generate globals graph (stmt hwr) 81 106  decision_spill off ⇒ 82 107 let temphwr ≝ RegisterSST in 83 let l ≝ generate globals (stmt temphwr) in 84 generate globals (get_stack globals temphwr off l) 108 let 〈l, graph〉 ≝ generate globals graph (stmt temphwr) in 109 let 〈stmt, graph〉 ≝ get_stack int_fun globals graph temphwr off l in 110 generate globals graph stmt 85 111 ]. 86 112 87 113 definition move ≝ 88 λglobals: list ident. 114 λint_fun. 115 λglobals: list ident. 116 λgraph: graph (ltl_statement globals). 89 117 λdest: decision. 90 118 λsrc: decision. … … 95 123 [ decision_colour src_hwr ⇒ 96 124 if eq_Register dest_hwr src_hwr then 97 joint_st_goto ? globals l125 〈joint_st_goto ? globals l, graph〉 98 126 else 99 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in100 joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l101  decision_spill src_off ⇒ get_stack globalsdest_hwr src_off l127 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in 128 〈joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l, graph〉 129  decision_spill src_off ⇒ get_stack int_fun globals graph dest_hwr src_off l 102 130 ] 103 131  decision_spill dest_off ⇒ 104 132 match src with 105 [ decision_colour src_hwr ⇒ set_stack globalsdest_off src_hwr l133 [ decision_colour src_hwr ⇒ set_stack int_fun globals graph dest_off src_hwr l 106 134  decision_spill src_off ⇒ 107 135 if eq_bv ? dest_off src_off then 108 joint_st_goto ? globals l136 〈joint_st_goto ? globals l, graph〉 109 137 else 110 138 let temp_hwr ≝ RegisterSST in 111 let l ≝ generate globals (set_stack globals dest_off temp_hwr l) in 112 get_stack globals temp_hwr src_off l 139 let 〈stmt, graph〉 ≝ set_stack int_fun globals graph dest_off temp_hwr l in 140 let 〈l, graph〉 ≝ generate globals graph stmt in 141 get_stack int_fun globals graph temp_hwr src_off l 113 142 ] 114 143 ]. 115 144 116 145 definition newframe ≝ 117 λglobals. 146 λint_fun. 147 λglobals. 148 λgraph: graph (ltl_statement globals). 118 149 λl. 119 if eq_nat stacksize0 then120 joint_st_goto ? globals l150 if eq_nat (stacksize int_fun) 0 then 151 〈joint_st_goto ? globals l, graph〉 121 152 else 122 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in123 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in124 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in125 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in126 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in127 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in128 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in129 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l) in130 joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l.153 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in 154 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in 155 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in 156 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in 157 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in 158 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in 159 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in 160 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in 161 〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph〉. 131 162 132 163 definition delframe ≝ 133 λglobals. 164 λint_fun. 165 λglobals. 166 λgraph: graph (ltl_statement globals). 134 167 λl. 135 if eq_nat stacksize0 then136 joint_st_goto ? globals l168 if eq_nat (stacksize int_fun) 0 then 169 〈joint_st_goto ? globals l, graph〉 137 170 else 138 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in139 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in140 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in141 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in142 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in143 joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l.171 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in 172 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in 173 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in 174 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in 175 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in 176 〈joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? (stacksize int_fun))) l, graph〉. 144 177 145 178 definition translate_statement ≝ 146 λglobals: list ident. 179 λint_fun. 180 λglobals: list ident. 181 λgraph: graph (ltl_statement globals). 147 182 λstmt: ertl_statement. 148 183 match stmt with 149 [ ertl_st_skip l ⇒ joint_st_goto ? globals l150  ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l151  ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l152  ertl_st_get_hdw destr sourcehwr l ⇒ move globals(lookup destr) (decision_colour sourcehwr) l153  ertl_st_set_hdw desthwr srcr l ⇒ move globals(decision_colour desthwr) (lookup srcr) l184 [ ertl_st_skip l ⇒ 〈joint_st_goto ? globals l, graph〉 185  ertl_st_comment s l ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉 186  ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉 187  ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l 188  ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l 154 189  ertl_st_hdw_to_hdw r1 r2 l ⇒ 155 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in156 joint_st_sequential ? globals (joint_instr_to_acc globals r2) l157  ertl_st_new_frame l ⇒ newframe globalsl158  ertl_st_del_frame l ⇒ delframe globalsl190 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in 191 〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉 192  ertl_st_new_frame l ⇒ newframe int_fun globals graph l 193  ertl_st_del_frame l ⇒ delframe int_fun globals graph l 159 194  ertl_st_frame_size r l ⇒ 160 let 〈hdw, l〉 ≝ write globals r l in 161 joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l 195 let 〈hdw, l〉 ≝ write int_fun globals graph r l in 196 let 〈l, graph〉 ≝ l in 197 〈joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? (stacksize int_fun))) l, graph〉 162 198  ertl_st_pop r l ⇒ 163 let 〈hdw, l〉 ≝ write globals r l in 164 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 165 joint_st_sequential ? globals (joint_instr_pop globals) l 199 let 〈hdw, l〉 ≝ write int_fun globals graph r l in 200 let 〈l, graph〉 ≝ l in 201 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 202 〈joint_st_sequential ? globals (joint_instr_pop globals) l, graph〉 166 203  ertl_st_push r l ⇒ 167 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_push globals) l) in168 let l ≝ read globalsr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in169 joint_st_goto ? globals l204 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_push globals) l) in 205 let 〈l, graph〉 ≝ read int_fun globals graph r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 206 〈joint_st_goto ? globals l, graph〉 170 207  ertl_st_addr rl rh x l ⇒ 171 let 〈hdw1, l〉 ≝ write globals rh l in 172 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in 173 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in 174 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in 175 let 〈hdw2, l〉 ≝ write globals rl l in 176 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in 177 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in 178 joint_st_sequential ? globals (joint_instr_address globals x ?) l 208 let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in 209 let 〈l, graph〉 ≝ l in 210 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in 211 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in 212 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in 213 let 〈hdw2, l〉 ≝ write int_fun globals graph rl l in 214 let 〈l, graph〉 ≝ l in 215 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in 216 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in 217 〈joint_st_sequential ? globals (joint_instr_address globals x ?) l, graph〉 179 218 (*  ertl_st_addr_h r x l ⇒ 180 let 〈hdw, l〉 ≝ write globalsr l in181 let l ≝ generate globals(ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in182 let l ≝ generate globals(ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in219 let 〈hdw, l〉 ≝ write int_fun globals graph r l in 220 let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in 221 let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in 183 222 ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) 184 223  ertl_st_addr_l r x l ⇒ 185 let 〈hdw, l〉 ≝ write globalsr l in186 let l ≝ generate globals(ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in187 let l ≝ generate globals(ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in224 let 〈hdw, l〉 ≝ write int_fun globals graph r l in 225 let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in 226 let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in 188 227 ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) 189 228 *) 190 229  ertl_st_int r i l ⇒ 191 let 〈hdw, l〉 ≝ write globals r l in 192 joint_st_sequential ? globals (joint_instr_int globals hdw i) l 193  ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l 230 let 〈hdw, l〉 ≝ write int_fun globals graph r l in 231 let 〈l, graph〉 ≝ l in 232 〈joint_st_sequential ? globals (joint_instr_int globals hdw i) l, graph〉 233  ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l 194 234  ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒ 195 let 〈hdw, l〉 ≝ write globals destr1 l in 196 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 197 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in 198 let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 199 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 200 let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 201 let l ≝ generate globals (joint_st_goto ? globals l) in 202 let 〈hdw, l〉 ≝ write globals destr2 l in 203 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 204 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in 205 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in 206 let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 207 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 208 let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 209 joint_st_goto ? globals l 235 let 〈hdw, l〉 ≝ write int_fun globals graph destr1 l in 236 let 〈l, graph〉 ≝ l in 237 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 238 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in 239 let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 240 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 241 let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 242 let 〈l, graph〉 ≝ generate globals graph (joint_st_goto ? globals l) in 243 let 〈hdw, l〉 ≝ write int_fun globals graph destr2 l in 244 let 〈l, graph〉 ≝ l in 245 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 246 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in 247 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in 248 let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 249 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 250 let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 251 〈joint_st_goto ? globals l, graph〉 210 252 (* 211 253  ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒ 212 let 〈hdw, l〉 ≝ write globalsdestr l in213 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in214 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in215 let l ≝ read globalssrcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in216 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in217 let l ≝ read globalssrcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in254 let 〈hdw, l〉 ≝ write int_fun globals graph destr l in 255 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 256 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in 257 let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 258 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 259 let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 218 260 joint_st_goto ? globals l 219 261  ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒ 220 let 〈hdw, l〉 ≝ write globalsdestr l in221 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in222 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in223 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in224 let l ≝ read globalssrcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in225 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in226 let l ≝ read globalssrcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in262 let 〈hdw, l〉 ≝ write int_fun globals graph destr l in 263 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 264 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in 265 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in 266 let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 267 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 268 let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 227 269 joint_st_goto ? globals l 228 270 *) 229 271  ertl_st_op1 op1 destr srcr l ⇒ 230 let 〈hdw, l〉 ≝ write globals destr l in 231 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 232 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in 233 let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 234 joint_st_goto ? globals l 272 let 〈hdw, l〉 ≝ write int_fun globals graph destr l in 273 let 〈l, graph〉 ≝ l in 274 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 275 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in 276 let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 277 〈joint_st_goto ? globals l, graph〉 235 278  ertl_st_op2 op2 destr srcr1 srcr2 l ⇒ 236 let 〈hdw, l〉 ≝ write globals destr l in 237 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 238 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in 239 let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 240 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 241 let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 242 joint_st_goto ? globals l 243  ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l 244  ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l 279 let 〈hdw, l〉 ≝ write int_fun globals graph destr l in 280 let 〈l, graph〉 ≝ l in 281 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 282 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in 283 let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 284 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in 285 let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 286 〈joint_st_goto ? globals l, graph〉 287  ertl_st_clear_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_clear_carry globals) l, graph〉 288  ertl_st_set_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_set_carry globals) l, graph〉 245 289  ertl_st_load destr addr1 addr2 l ⇒ 246 let 〈hdw, l〉 ≝ write globals destr l in 247 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 248 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in 249 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 250 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in 251 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 252 let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 253 let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in 254 let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 255 joint_st_goto ? globals l 290 let 〈hdw, l〉 ≝ write int_fun globals graph destr l in 291 let 〈l, graph〉 ≝ l in 292 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in 293 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_load globals) l) in 294 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 295 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in 296 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 297 let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 298 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in 299 let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 300 〈joint_st_goto ? globals l, graph〉 256 301  ertl_st_store addr1 addr2 srcr l ⇒ 257 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_store globals) l) in258 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in259 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in260 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in261 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in262 let l ≝ read globalsaddr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in263 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in264 let l ≝ read globalsaddr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in265 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in266 let l ≝ read globalssrcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in267 joint_st_goto ? globals l268  ertl_st_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l302 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in 303 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in 304 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in 305 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in 306 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in 307 let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 308 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in 309 let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 310 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in 311 let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 312 〈joint_st_goto ? globals l, graph〉 313  ertl_st_call_id f ignore l ⇒ 〈joint_st_sequential ? globals (joint_instr_call_id globals f) l, graph〉 269 314  ertl_st_cond srcr lbl_true lbl_false ⇒ 270 let l ≝ generate globals(joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in271 let l ≝ read globalssrcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in272 joint_st_goto ? globals l273  ertl_st_return ⇒ joint_st_return ? globals315 let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in 316 let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in 317 〈joint_st_goto ? globals l, graph〉 318  ertl_st_return ⇒ 〈joint_st_return ? globals, graph〉 274 319 ]. 275 320 cases daemon (* XXX: todo  proofs regarding gvars *)
Note: See TracChangeset
for help on using the changeset viewer.