- Timestamp:
- Jul 19, 2012, 2:42:02 PM (9 years ago)
- Location:
- src
- Files:
-
- 16 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTLToLTL_paolo.ma
r2208 r2214 1 1 2 include "LTL/LTL_paolo.ma". 2 3 include "ERTL/Interference_paolo.ma". … … 18 19 coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision. 19 20 20 definition stacksize :21 ∀globals.ℕ → joint_internal_function globals ertl_params → ℕ ≝22 λglobals.23 λspilled_no.24 λint_fun.25 spilled_no + joint_if_stacksize … int_fun.26 27 21 (* Paolo: I'm changing the following: before, spilled registers were 28 22 assigned stack addresses going from SP + #frame_size - #stack_params … … 31 25 32 26 definition preserve_carry_bit : 33 ∀globals.bool → list (joint_seq ltl_params globals) → list (joint_seq ltl_paramsglobals) ≝27 ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝ 34 28 λglobals,do_it,steps. 35 29 if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps. … … 42 36 (* spill should be byte-based from the start *) 43 37 definition set_dp_by_offset : 44 ∀globals.nat → list (joint_seq ltl_paramsglobals) ≝38 ∀globals.nat → list (joint_seq LTL globals) ≝ 45 39 λglobals,off. 46 40 [ A ← byte_of_nat off … … 53 47 54 48 definition get_stack: 55 ∀globals.Register → nat → list (joint_seq ltl_paramsglobals) ≝49 ∀globals.Register → nat → list (joint_seq LTL globals) ≝ 56 50 λglobals,r,off. 57 51 set_dp_by_offset ? off @ … … 60 54 61 55 definition set_stack_not_a : 62 ∀globals.nat → Register → list (joint_seq ltl_paramsglobals) ≝56 ∀globals.nat → Register → list (joint_seq LTL globals) ≝ 63 57 λglobals,off,r. 64 58 set_dp_by_offset ? off @ … … 67 61 68 62 definition set_stack_a : 69 ∀globals.nat → list (joint_seq ltl_paramsglobals) ≝63 ∀globals.nat → list (joint_seq LTL globals) ≝ 70 64 λglobals,off. 71 65 [ RegisterST1 ← A ] @ … … 73 67 74 68 definition set_stack : 75 ∀globals.nat → Register → list (joint_seq ltl_paramsglobals) ≝69 ∀globals.nat → Register → list (joint_seq LTL globals) ≝ 76 70 λglobals,off,r. 77 71 if eq_Register r RegisterA then … … 81 75 82 76 definition set_stack_int : 83 ∀globals.nat → beval → list (joint_seq ltl_paramsglobals) ≝77 ∀globals.nat → beval → list (joint_seq LTL globals) ≝ 84 78 λglobals,off,int. 85 79 set_dp_by_offset ? off @ … … 88 82 89 83 definition move : 90 ∀globals.bool → decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝84 ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝ 91 85 λglobals,carry_lives_after,dst,src. 92 86 match dst with … … 128 122 129 123 definition newframe : 130 ∀globals.ℕ → list (joint_seq ltl_paramsglobals) ≝124 ∀globals.ℕ → list (joint_seq LTL globals) ≝ 131 125 λglobals,stack_sz. 132 126 [ CLEAR_CARRY … … … 140 134 141 135 definition delframe : 142 ∀globals.ℕ → list (joint_seq ltl_paramsglobals) ≝136 ∀globals.ℕ → list (joint_seq LTL globals) ≝ 143 137 λglobals,stack_sz. 144 138 [ A ← RegisterSPL … … 176 170 177 171 definition translate_op2 : 178 ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝172 ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 179 173 λglobals,carry_lives_after,op,dst,arg1,arg2. 180 174 (* this won't preserve the carry bit if op does not set it: left to next function *) … … 189 183 190 184 definition translate_op2_smart : 191 ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝185 ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 192 186 λglobals,carry_lives_after,op,dst,arg1,arg2. 193 187 (* if op does not set carry bit (⇒ it does not use it either) then it must be … … 232 226 233 227 definition translate_op1 : 234 ∀globals.bool → Op1 → decision → decision → list (joint_seq ltl_paramsglobals) ≝228 ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝ 235 229 λglobals,carry_lives_after,op,dst,arg. 236 230 let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in … … 241 235 242 236 definition translate_opaccs : 243 ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝237 ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 244 238 λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2. 245 239 (* OPACCS always has dead carry bit and sets it to zero *) … … 255 249 (* does not preserve carry bit *) 256 250 definition move_to_dp : 257 ∀globals.arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝251 ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 258 252 λglobals,arg1,arg2. 259 253 if ¬arg_is_spilled arg1 then … … 272 266 273 267 definition translate_store : 274 ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝268 ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 275 269 λglobals,carry_lives_after,addr1,addr2,src. 276 270 (* requires src != RegisterA and RegisterB *) … … 286 280 287 281 definition translate_load : 288 ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq ltl_paramsglobals) ≝282 ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ 289 283 λglobals,carry_lives_after,dst,addr1,addr2. 290 284 preserve_carry_bit ? (carry_lives_after ∧ … … 296 290 definition translate_address : 297 291 ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision → 298 list (joint_seq ltl_paramsglobals) ≝292 list (joint_seq LTL globals) ≝ 299 293 λglobals,carry_lives_after,id,prf,addr1,addr2. 300 294 preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2)) 301 (ADDRESS ltl_params? id prf it it ::295 (ADDRESS LTL ? id prf it it :: 302 296 move ? false addr1 RegisterDPL @ 303 297 move ? false addr2 RegisterDPH). … … 306 300 ∀globals.∀after : valuation register_lattice. 307 301 coloured_graph after → 308 ℕ → label → joint_step ertl_params globals → seq_block ltl_params globals (joint_step ltl_paramsglobals) ≝302 ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals) ≝ 309 303 λglobals,after,grph,stack_sz,lbl,s. 310 304 let lookup ≝ λr.colouring … grph (inl … r) in … … 317 311 match s with 318 312 [ step_seq s' ⇒ 319 match s' return λ_.seq_block ltl_params globals (joint_step ltl_paramsglobals) with313 match s' return λ_.seq_block LTL globals (joint_step LTL globals) with 320 314 [ COMMENT c ⇒ COMMENT … c 321 315 | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl … … 373 367 move (lookup r) (arg_decision_imm (byte_of_nat stack_sz)) 374 368 ] 375 | CALL_ID f n_args _ ⇒ CALL_ID ltl_params? f n_args it369 | CALL_ID f n_args _ ⇒ CALL_ID LTL ? f n_args it 376 370 | extension_call abs ⇒ match abs in void with [ ] 377 371 ] … … 381 375 382 376 definition translate_fin_step: 383 ∀globals.label → joint_fin_step ertl_params → seq_block ltl_params globals (joint_fin_step ltl_params) ≝377 ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL) ≝ 384 378 λglobals,lbl,s. 385 match s return λ_.seq_block ltl_params globals (joint_fin_step ltl_params) with379 match s return λ_.seq_block LTL globals (joint_fin_step LTL) with 386 380 [ RETURN ⇒ RETURN ? 387 381 | GOTO l ⇒ GOTO ? l … … 390 384 391 385 definition translate_internal: ∀globals: list ident. 392 joint_internal_function globals ertl_params →393 joint_internal_function globals ltl_params ≝386 joint_internal_function ERTL globals → 387 joint_internal_function LTL globals ≝ 394 388 λglobals: list ident. 395 λint_fun: joint_internal_function globals ertl_params.389 λint_fun: joint_internal_function ERTL globals. 396 390 (* initialize graph *) 397 391 let entry ≝ pi1 … (joint_if_entry … int_fun) in … … 405 399 let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in 406 400 (* initialize internal function *) 407 let init ≝ mk_joint_internal_function globals ltl_params401 let init ≝ mk_joint_internal_function LTL globals 408 402 (joint_if_luniverse … int_fun) 409 403 (joint_if_runiverse … int_fun) -
src/ERTL/ERTL_paolo.ma
r2208 r2214 1 1 2 include "joint/Joint_paolo.ma". 2 3 include "RTL/RTL_paolo.ma". … … 48 49 (* localsT ≝ *) register). 49 50 50 definition ertl_params≝ mk_graph_params ertl_uns_params.51 definition ertl_program ≝ joint_program ertl_params.51 definition ERTL ≝ mk_graph_params ertl_uns_params. 52 definition ertl_program ≝ joint_program ERTL. 52 53 53 54 interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)). … … 56 57 unification hint 0 ≔ 57 58 (*---------------*) ⊢ 58 pair_move ertl_params≡ move_dst × move_src.59 pair_move ERTL ≡ move_dst × move_src. 59 60 unification hint 0 ≔ 60 61 (*---------------*) ⊢ 61 acc_a_reg ertl_params≡ register.62 acc_a_reg ERTL ≡ register. 62 63 unification hint 0 ≔ 63 64 (*---------------*) ⊢ 64 acc_b_reg ertl_params≡ register.65 acc_b_reg ERTL ≡ register. 65 66 unification hint 0 ≔ 66 67 (*---------------*) ⊢ 67 acc_a_arg ertl_params≡ psd_argument.68 acc_a_arg ERTL ≡ psd_argument. 68 69 unification hint 0 ≔ 69 70 (*---------------*) ⊢ 70 acc_b_arg ertl_params≡ psd_argument.71 acc_b_arg ERTL ≡ psd_argument. 71 72 unification hint 0 ≔ 72 73 (*---------------*) ⊢ 73 dpl_reg ertl_params≡ register.74 dpl_reg ERTL ≡ register. 74 75 unification hint 0 ≔ 75 76 (*---------------*) ⊢ 76 dph_reg ertl_params≡ register.77 dph_reg ERTL ≡ register. 77 78 unification hint 0 ≔ 78 79 (*---------------*) ⊢ 79 dpl_arg ertl_params≡ psd_argument.80 dpl_arg ERTL ≡ psd_argument. 80 81 unification hint 0 ≔ 81 82 (*---------------*) ⊢ 82 dph_arg ertl_params≡ psd_argument.83 dph_arg ERTL ≡ psd_argument. 83 84 unification hint 0 ≔ 84 85 (*---------------*) ⊢ 85 snd_arg ertl_params≡ psd_argument.86 snd_arg ERTL ≡ psd_argument. 86 87 unification hint 0 ≔ 87 88 (*---------------*) ⊢ 88 call_args ertl_params≡ ℕ.89 call_args ERTL ≡ ℕ. 89 90 unification hint 0 ≔ 90 91 (*---------------*) ⊢ 91 call_dest ertl_params≡ unit.92 call_dest ERTL ≡ unit. 92 93 93 94 unification hint 0 ≔ 94 95 (*---------------*) ⊢ 95 ext_seq ertl_params≡ ertl_seq.96 ext_seq ERTL ≡ ertl_seq. 96 97 unification hint 0 ≔ 97 98 (*---------------*) ⊢ 98 ext_call ertl_params≡ void.99 ext_call ERTL ≡ void. 99 100 unification hint 0 ≔ 100 101 (*---------------*) ⊢ 101 ext_tailcall ertl_params≡ void.102 ext_tailcall ERTL ≡ void. 102 103 103 coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params≝104 coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝ 104 105 psd_argument_from_reg 105 on _r : register to snd_arg ertl_params.106 coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params≝106 on _r : register to snd_arg ERTL. 107 coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝ 107 108 psd_argument_from_byte 108 on _b : Byte to snd_arg ertl_params.109 on _b : Byte to snd_arg ERTL. 109 110 110 definition ertl_seq_joint ≝ extension_seq ertl_params. 111 coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ertl_params globals ≝ ertl_seq_joint 112 on _s : ertl_seq to joint_seq ertl_params. 113 111 definition ertl_seq_joint ≝ extension_seq ERTL. 112 coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint 113 on _s : ertl_seq to joint_seq ERTL. -
src/ERTL/liveness_paolo.ma
r2208 r2214 1 1 2 include "ASM/Util.ma". 2 3 include "ERTL/ERTL_paolo.ma". … … 42 43 definition defined ≝ 43 44 λglobals: list ident. 44 λs: joint_statement ertl_paramsglobals.45 λs: joint_statement ERTL globals. 45 46 match s with 46 47 [ sequential seq l ⇒ … … 100 101 definition used ≝ 101 102 λglobals: list ident. 102 λs: joint_statement ertl_paramsglobals.103 λs: joint_statement ERTL globals. 103 104 match s with 104 105 [ sequential seq l ⇒ … … 155 156 λglobals: list ident. 156 157 λl: register_lattice. 157 λs: joint_statement ertl_paramsglobals.158 λs: joint_statement ERTL globals. 158 159 let pliveafter ≝ \fst l in 159 160 let hliveafter ≝ \snd l in … … 225 226 226 227 definition statement_semantics: ∀globals: list ident. 227 joint_statement ertl_paramsglobals → register_lattice → register_lattice ≝228 joint_statement ERTL globals → register_lattice → register_lattice ≝ 228 229 λglobals. 229 230 λstmt. … … 236 237 definition livebefore ≝ 237 238 λglobals: list ident. 238 λint_fun: joint_internal_function globals ertl_params.239 λint_fun: joint_internal_function ERTL globals. 239 240 λlabel. 240 241 λliveafter: valuation register_lattice. … … 246 247 definition liveafter ≝ 247 248 λglobals: list ident. 248 λint_fun: joint_internal_function globals ertl_params.249 λint_fun: joint_internal_function ERTL globals. 249 250 λlabel. 250 251 λliveafter: valuation register_lattice. -
src/LIN/LIN_paolo.ma
r2182 r2214 1 1 include "LIN/joint_LTL_LIN_paolo.ma". 2 2 3 definition lin_params ≝ mk_lin_params ltl_lin_params.3 definition LIN ≝ mk_lin_params LTL_LIN. 4 4 5 5 (* aid unification *) 6 6 unification hint 0 ≔ 7 7 (*---------------*) ⊢ 8 acc_a_reg lin_params≡ unit.8 acc_a_reg LIN ≡ unit. 9 9 unification hint 0 ≔ 10 10 (*---------------*) ⊢ 11 acc_a_arg lin_params≡ unit.11 acc_a_arg LIN ≡ unit. 12 12 unification hint 0 ≔ 13 13 (*---------------*) ⊢ 14 acc_b_reg lin_params≡ unit.14 acc_b_reg LIN ≡ unit. 15 15 unification hint 0 ≔ 16 16 (*---------------*) ⊢ 17 acc_a_arg lin_params≡ unit.17 acc_a_arg LIN ≡ unit. 18 18 unification hint 0 ≔ 19 19 (*---------------*) ⊢ 20 snd_arg lin_params ≡ ltl_argument.20 snd_arg LIN ≡ hdw_argument. 21 21 unification hint 0 ≔ 22 22 (*---------------*) ⊢ 23 ext_seq lin_params≡ ltl_lin_seq.23 ext_seq LIN ≡ ltl_lin_seq. 24 24 unification hint 0 ≔ 25 25 (*---------------*) ⊢ 26 pair_move lin_params≡ registers_move.26 pair_move LIN ≡ registers_move. 27 27 28 definition lin_program ≝ joint_program lin_params.28 definition lin_program ≝ joint_program LIN. -
src/LIN/joint_LTL_LIN_paolo.ma
r2208 r2214 12 12 | RESTORE_CARRY : ltl_lin_seq. 13 13 14 definition ltl_lin_params: unserialized_params ≝ mk_unserialized_params14 definition LTL_LIN : unserialized_params ≝ mk_unserialized_params 15 15 (mk_step_params 16 16 (* acc_a_reg ≝ *) unit -
src/LTL/LTL_paolo.ma
r2208 r2214 1 1 include "LIN/joint_LTL_LIN_paolo.ma". 2 2 3 definition ltl_params ≝ mk_graph_params ltl_lin_params.3 definition LTL ≝ mk_graph_params LTL_LIN. 4 4 5 5 (* aid unification *) 6 6 unification hint 0 ≔ 7 7 (*---------------*) ⊢ 8 acc_a_reg ltl_params≡ unit.8 acc_a_reg LTL ≡ unit. 9 9 unification hint 0 ≔ 10 10 (*---------------*) ⊢ 11 acc_a_arg ltl_params≡ unit.11 acc_a_arg LTL ≡ unit. 12 12 unification hint 0 ≔ 13 13 (*---------------*) ⊢ 14 acc_b_reg ltl_params≡ unit.14 acc_b_reg LTL ≡ unit. 15 15 unification hint 0 ≔ 16 16 (*---------------*) ⊢ 17 acc_a_arg ltl_params≡ unit.17 acc_a_arg LTL ≡ unit. 18 18 unification hint 0 ≔ 19 19 (*---------------*) ⊢ 20 snd_arg ltl_params≡ hdw_argument.20 snd_arg LTL ≡ hdw_argument. 21 21 unification hint 0 ≔ 22 22 (*---------------*) ⊢ 23 ext_seq ltl_params≡ ltl_lin_seq.23 ext_seq LTL ≡ ltl_lin_seq. 24 24 unification hint 0 ≔ 25 25 (*---------------*) ⊢ 26 pair_move ltl_params≡ registers_move.26 pair_move LTL ≡ registers_move. 27 27 28 definition ltl_program ≝ joint_program ltl_params.28 definition ltl_program ≝ joint_program LTL. 29 29 30 coercion byte_to_ltl_argument : ∀b: Byte.snd_arg ltl_params≝31 hdw_argument_from_byte on _b : Byte to snd_arg ltl_params.32 coercion reg_to_ltl_argument : ∀r: Register.snd_arg ltl_params≝33 hdw_argument_from_reg on _r : Register to snd_arg ltl_params.30 coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝ 31 hdw_argument_from_byte on _b : Byte to snd_arg LTL. 32 coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝ 33 hdw_argument_from_reg on _r : Register to snd_arg LTL. -
src/RTL/RTLTailcall_paolo.ma
r2162 r2214 5 5 λexit: label. 6 6 λlbl: label. 7 λstmt: rtl_statementglobals.8 λgraph: codeT rtlntc_paramsglobals.7 λstmt: joint_statement RTL globals. 8 λgraph: codeT RTL_ntc globals. 9 9 match stmt with 10 10 [ final fin ⇒ … … 13 13 match ext with 14 14 [ rtl_tailcall_id f args ⇒ 15 add … graph lbl (sequential … (CALL_ID rtlntc_params? f args [ ]) exit)15 add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit) 16 16 | rtl_tailcall_ptr f1 f2 args ⇒ 17 add … graph lbl (sequential rtlntc_params ? (rtl_call_ptr f1 f2 args [ ] : ext_call rtlntc_params) exit)17 add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit) 18 18 ] 19 19 | _ ⇒ graph ] … … 23 23 λglobals. 24 24 λexit: label. 25 λgraph: codeT rtl_paramsglobals.25 λgraph: codeT RTL globals. 26 26 foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …). 27 27 28 28 axiom simplify_graph_preserves_labels: 29 29 ∀globals. 30 ∀g: codeT rtl_paramsglobals.30 ∀g: codeT RTL globals. 31 31 ∀exit: label. 32 32 ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g. … … 34 34 definition simplify_internal : 35 35 ∀globals. 36 joint_internal_function globals rtl_params →37 joint_internal_function globals rtlntc_params36 joint_internal_function RTL globals → 37 joint_internal_function RTL_ntc globals 38 38 ≝ 39 39 λglobals,def. … … 48 48 qed. 49 49 50 definition tailcall_simplify : rtl_program → rtl ntc_program ≝50 definition tailcall_simplify : rtl_program → rtl_ntc_program ≝ 51 51 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)). -
src/RTL/RTLToERTL_paolo.ma
r2208 r2214 8 8 9 9 definition save_hdws : 10 ∀globals.list (register×Register) → list (joint_seq ertl_paramsglobals) ≝10 ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝ 11 11 λglobals. 12 12 let save_hdws_internal ≝ … … 15 15 16 16 definition restore_hdws : 17 ∀globals.list (psd_argument×Register) → list (joint_seq ertl_paramsglobals) ≝17 ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝ 18 18 λglobals. 19 19 let restore_hdws_internal ≝ … … 22 22 23 23 definition get_params_hdw : 24 ∀globals.list register → list (joint_seq ertl_paramsglobals) ≝24 ∀globals.list register → list (joint_seq ERTL globals) ≝ 25 25 λglobals,params. 26 26 save_hdws … (zip_pottier … params RegisterParams). … … 28 28 definition get_param_stack : 29 29 ∀globals.register → register → register → 30 list (joint_seq ertl_paramsglobals) ≝30 list (joint_seq ERTL globals) ≝ 31 31 λglobals,addr1,addr2,destr. 32 32 (* liveness analysis will erase the last useless ops *) … … 38 38 definition get_params_stack : 39 39 ∀globals.list register → 40 bind_new (localsT ertl_params) (list (joint_seq ertl_paramsglobals)) ≝40 bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝ 41 41 λglobals,params. 42 42 νtmpr,addr1,addr2 in … … 59 59 definition prologue : 60 60 ∀globals.list register → register → register → list (register×Register) → 61 bind_new (localsT ertl_params) (list (joint_seq ertl_paramsglobals)) ≝61 bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝ 62 62 λglobals,params,sral,srah,sregs. 63 63 [ (ertl_new_frame : joint_seq ??) ; … … 67 67 68 68 definition save_return : 69 ∀globals.list psd_argument → list (joint_seq ertl_paramsglobals) ≝69 ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝ 70 70 λglobals,ret_regs. 71 71 match reduce_strong ? ? RegisterSTS ret_regs with … … 79 79 ]. 80 80 81 definition assign_result : ∀globals.list (joint_seq ertl_paramsglobals) ≝81 definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝ 82 82 λglobals. 83 83 match reduce_strong ?? RegisterRets RegisterSTS with … … 90 90 definition epilogue : 91 91 ∀globals.list register → register → register → list (register × Register) → 92 list (joint_seq ertl_paramsglobals) ≝92 list (joint_seq ERTL globals) ≝ 93 93 λglobals,ret_regs,sral,srah,sregs. 94 94 save_return … (map … (Reg ?) ret_regs) @ 95 95 restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @ 96 [ PUSH ertl_params? srah ;96 [ PUSH ERTL ? srah ; 97 97 PUSH … sral ; 98 98 ertl_del_frame ] @ … … 101 101 definition allocate_regs : 102 102 ∀globals,rs.rs_set rs → 103 state_monad (joint_internal_function globals ertl_params) (list (register×Register)) ≝103 state_monad (joint_internal_function ERTL globals) (list (register×Register)) ≝ 104 104 λglobals,rs,saved,def. 105 105 let allocate_regs_internal ≝ … … 112 112 definition add_pro_and_epilogue : 113 113 ∀globals.list register → list register → 114 joint_internal_function globals ertl_params →115 joint_internal_function globals ertl_params ≝114 joint_internal_function ERTL globals → 115 joint_internal_function ERTL globals ≝ 116 116 λglobals,params,ret_regs,def. 117 117 let start_lbl ≝ joint_if_entry … def in … … 129 129 130 130 definition set_params_hdw : 131 ∀globals.list psd_argument → list (joint_seq ertl_paramsglobals) ≝131 ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝ 132 132 λglobals,params. 133 133 restore_hdws globals (zip_pottier ? ? params RegisterParams). … … 137 137 definition set_param_stack : 138 138 ∀globals.register → register → psd_argument → 139 list (joint_seq ertl_paramsglobals) ≝139 list (joint_seq ERTL globals) ≝ 140 140 λglobals,addr1,addr2,arg. 141 141 [ STORE … addr1 addr2 arg ; … … 145 145 146 146 definition set_params_stack : 147 ∀globals.list psd_argument → bind_new (localsT ertl_params) ? ≝147 ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝ 148 148 λglobals,params. 149 149 νaddr1,addr2 in … … 166 166 167 167 definition fetch_result : 168 ∀globals.list register → list (joint_seq ertl_paramsglobals) ≝168 ∀globals.list register → list (joint_seq ERTL globals) ≝ 169 169 λglobals,ret_regs. 170 170 match reduce_strong ?? RegisterSTS RegisterRets with … … 182 182 183 183 definition translate_step : 184 ∀globals.label → joint_step rtlntc_paramsglobals →185 bind_seq_block ertl_params globals (joint_step ertl_paramsglobals) ≝184 ∀globals.label → joint_step RTL_ntc globals → 185 bind_seq_block ERTL globals (joint_step ERTL globals) ≝ 186 186 λglobals.λ_.λs. 187 187 match s return λ_.bind_seq_block ?? (joint_step ??) with … … 194 194 COST_LABEL … lbl 195 195 | ADDRESS x prf r1 r2 ⇒ 196 ADDRESS ertl_params? x prf r1 r2196 ADDRESS ERTL ? x prf r1 r2 197 197 | OPACCS op destr1 destr2 srcr1 srcr2 ⇒ 198 OPACCS ertl_params? op destr1 destr2 srcr1 srcr2198 OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 199 199 | OP1 op1 destr srcr ⇒ 200 OP1 ertl_params? op1 destr srcr200 OP1 ERTL ? op1 destr srcr 201 201 | OP2 op2 destr srcr1 srcr2 ⇒ 202 OP2 ertl_params? op2 destr srcr1 srcr2202 OP2 ERTL ? op2 destr srcr1 srcr2 203 203 | CLEAR_CARRY ⇒ 204 204 CLEAR_CARRY … … … 206 206 SET_CARRY … 207 207 | LOAD destr addr1 addr2 ⇒ 208 LOAD ertl_params? destr addr1 addr2208 LOAD ERTL ? destr addr1 addr2 209 209 | STORE addr1 addr2 srcr ⇒ 210 STORE ertl_params? addr1 addr2 srcr210 STORE ERTL ? addr1 addr2 srcr 211 211 | COMMENT msg ⇒ 212 212 COMMENT … msg … … 218 218 | CALL_ID f args ret_regs ⇒ 219 219 set_params ? args @@ 220 CALL_ID ertl_params? f (|args|) it :::220 CALL_ID ERTL ? f (|args|) it ::: 221 221 fetch_result ? ret_regs 222 222 | extension_call c ⇒ … … 227 227 ] 228 228 | COND r ltrue ⇒ 229 COND ertl_params? r ltrue229 COND ERTL ? r ltrue 230 230 ]. cases daemon (* pointer call to be ported yet *) qed. 231 231 232 232 definition translate_fin_step : 233 ∀globals.label → joint_fin_step rtlntc_params→234 bind_seq_block ertl_params globals (joint_fin_step ertl_params) ≝233 ∀globals.label → joint_fin_step RTL_ntc → 234 bind_seq_block ERTL globals (joint_fin_step ERTL) ≝ 235 235 λglobals.λ_.λs. 236 236 match s with … … 242 242 (* hack with empty graphs used here *) 243 243 definition translate_funct : 244 ∀globals.joint_internal_function globals rtlntc_params →245 joint_internal_function globals ertl_params ≝244 ∀globals.joint_internal_function RTL_ntc globals → 245 joint_internal_function ERTL globals ≝ 246 246 λglobals,def. 247 247 let nb_params ≝ |joint_if_params ?? def| in … … 253 253 let graph' ≝ add ? ? graph' exit' (RETURN …) in 254 254 let def' ≝ 255 mk_joint_internal_function globals ertl_params255 mk_joint_internal_function ERTL globals 256 256 (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *) 257 257 nb_params new_locals ((joint_if_stacksize … def) + added_stacksize) … … 272 272 λglobals. 273 273 λstmt. 274 λdef: joint_internal_function globals ertl_params.274 λdef: joint_internal_function globals ERTL. 275 275 let 〈entry, def〉 ≝ fresh_label … def in 276 276 let graph ≝ add … (joint_if_code … def) entry stmt in 277 set_joint_if_graph … ( ertl_paramsglobals) graph def ??.277 set_joint_if_graph … (ERTL globals) graph def ??. 278 278 [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *) 279 279 | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF … … 295 295 match inst with 296 296 [ COST_LABEL cost_lbl ⇒ 297 〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉297 〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉 298 298 | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ] 299 299 | RETURN ⇒ 〈None …, def〉 … … 310 310 match cost_label with 311 311 [ None ⇒ def 312 | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def312 | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def 313 313 ]. 314 314 -
src/RTL/RTL_paolo.ma
r2208 r2214 11 11 | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall. 12 12 13 definition rtl_uns_params ≝ mk_unserialized_params13 definition RTL_uns ≝ mk_unserialized_params 14 14 (mk_step_params 15 15 (* acc_a_reg ≝ *) register … … 35 35 (* localsT ≝ *) register). 36 36 37 definition rtl_params ≝ mk_graph_params rtl_uns_params. 38 definition lin_rtl_params ≝ mk_lin_params rtl_uns_params. 39 definition rtl_internal_function ≝ 40 λglobals. joint_internal_function globals rtl_params. 41 definition rtl_program ≝ joint_program rtl_params. 42 definition rtl_step ≝ joint_step rtl_params. 43 definition rtl_seq ≝ joint_seq rtl_params. 44 definition rtl_statement ≝ joint_statement rtl_params. 37 definition RTL ≝ mk_graph_params RTL_uns. 38 definition rtl_program ≝ joint_program RTL. 45 39 46 interpretation "move" 'mov r a = (MOVE rtl_params? (mk_Prod ? psd_argument r a)).40 interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)). 47 41 48 42 (* aid unification *) … … 50 44 unification hint 0 ≔ 51 45 (*---------------*) ⊢ 52 acc_a_reg rtl_params≡ register.46 acc_a_reg RTL ≡ register. 53 47 unification hint 0 ≔ 54 48 (*---------------*) ⊢ 55 acc_b_reg rtl_params≡ register.49 acc_b_reg RTL ≡ register. 56 50 unification hint 0 ≔ 57 51 (*---------------*) ⊢ 58 acc_a_arg rtl_params≡ psd_argument.52 acc_a_arg RTL ≡ psd_argument. 59 53 unification hint 0 ≔ 60 54 (*---------------*) ⊢ 61 acc_b_arg rtl_params≡ psd_argument.55 acc_b_arg RTL ≡ psd_argument. 62 56 unification hint 0 ≔ 63 57 (*---------------*) ⊢ 64 dpl_reg rtl_params≡ register.58 dpl_reg RTL ≡ register. 65 59 unification hint 0 ≔ 66 60 (*---------------*) ⊢ 67 dph_reg rtl_params≡ register.61 dph_reg RTL ≡ register. 68 62 unification hint 0 ≔ 69 63 (*---------------*) ⊢ 70 dpl_arg rtl_params≡ psd_argument.64 dpl_arg RTL ≡ psd_argument. 71 65 unification hint 0 ≔ 72 66 (*---------------*) ⊢ 73 dph_arg rtl_params≡ psd_argument.67 dph_arg RTL ≡ psd_argument. 74 68 unification hint 0 ≔ 75 69 (*---------------*) ⊢ 76 snd_arg rtl_params≡ psd_argument.70 snd_arg RTL ≡ psd_argument. 77 71 unification hint 0 ≔ 78 72 (*---------------*) ⊢ 79 pair_move rtl_params≡ register × psd_argument.73 pair_move RTL ≡ register × psd_argument. 80 74 unification hint 0 ≔ 81 75 (*---------------*) ⊢ 82 call_args rtl_params≡ list psd_argument.76 call_args RTL ≡ list psd_argument. 83 77 unification hint 0 ≔ 84 78 (*---------------*) ⊢ 85 call_dest rtl_params≡ list register.79 call_dest RTL ≡ list register. 86 80 87 81 unification hint 0 ≔ 88 82 (*---------------*) ⊢ 89 ext_seq rtl_params≡ rtl_seq.83 ext_seq RTL ≡ rtl_seq. 90 84 unification hint 0 ≔ 91 85 (*---------------*) ⊢ 92 ext_call rtl_params≡ rtl_call.86 ext_call RTL ≡ rtl_call. 93 87 unification hint 0 ≔ 94 88 (*---------------*) ⊢ 95 ext_tailcall rtl_params ≡ rtl_tailcall. 96 unification hint 0 ≔ globals 97 (*---------------*) ⊢ 98 joint_step rtl_params globals ≡ rtl_step globals. 89 ext_tailcall RTL ≡ rtl_tailcall. 99 90 100 unification hint 0 ≔ globals 101 (*---------------*) ⊢ 102 joint_seq rtl_params globals ≡ rtl_seq globals. 103 unification hint 0 ≔ globals 104 (*---------------*) ⊢ 105 joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals. 106 107 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg 108 on _r : register to snd_arg rtl_params. 109 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte 110 on _b : Byte to snd_arg rtl_params. 91 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg 92 on _r : register to snd_arg RTL. 93 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte 94 on _b : Byte to snd_arg RTL. 111 95 112 96 113 97 (************ Same without tail calls ****************) 114 98 115 definition rtlntc_params≝ mk_graph_params (mk_unserialized_params99 definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params 116 100 (mk_step_params 117 101 (* acc_a_reg ≝ *) register … … 137 121 (* localsT ≝ *) register)). 138 122 139 definition rtlntc_statement ≝ joint_statement (rtlntc_params : params). 140 141 definition rtlntc_internal_function ≝ 142 λglobals. joint_internal_function … globals rtlntc_params. 143 144 definition rtlntc_program ≝ joint_program rtlntc_params. 123 definition rtl_ntc_program ≝ joint_program RTL_ntc. -
src/RTLabs/RTLabsToRTL_paolo.ma
r2208 r2214 133 133 ∀srcrs2 : list psd_argument. 134 134 |dests| = |srcrs1| → |srcrs1| = |srcrs2| → 135 list (joint_seq rtl_paramsglobals)135 list (joint_seq RTL globals) 136 136 ≝ 137 137 λglobals: list ident. … … 146 146 | Sub ⇒ [CLEAR_CARRY ??] 147 147 | _ ⇒ [ ] 148 ] @ map3 ???? (OP2 rtl_paramsglobals op) destrs srcrs1 srcrs2 prf1 prf2.148 ] @ map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2. 149 149 150 150 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.|l| = size ≝ … … 174 174 ∀destrs: list register. 175 175 |destrs| = size_of_cst ? cst_sig → 176 list (joint_seq rtl_paramsglobals)176 list (joint_seq RTL globals) 177 177 ≝ 178 178 λty,globals,cst_sig,destrs. … … 186 186 | Oaddrsymbol id offset ⇒ λcst_prf,prf. 187 187 let 〈r1, r2〉 ≝ make_addr … destrs ? in 188 [ADDRESS rtl_paramsglobals id ? r1 r2]188 [ADDRESS RTL globals id ? r1 r2] 189 189 | Oaddrstack offset ⇒ λcst_prf,prf. 190 190 let 〈r1, r2〉 ≝ make_addr … destrs ? in 191 [(rtl_stack_address r1 r2 : joint_seq rtl_paramsglobals)]191 [(rtl_stack_address r1 r2 : joint_seq RTL globals)] 192 192 ] (pi2 … cst_sig). 193 193 [2: cases not_implemented … … 203 203 ∀destrs: list register. 204 204 ∀srcrs: list psd_argument. 205 |destrs| = |srcrs| → list (joint_seq rtl_paramsglobals) ≝205 |destrs| = |srcrs| → list (joint_seq RTL globals) ≝ 206 206 λglobals,destrs,srcrs,length_eq. 207 207 map2 … (λdst,src.dst ← src) destrs srcrs length_eq. … … 216 216 217 217 definition sign_mask : ∀globals.register → register → 218 list (joint_seq rtl_paramsglobals) ≝218 list (joint_seq RTL globals) ≝ 219 219 (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that: 220 220 byte in destr if srcr is: neg | pos … … 234 234 ∀globals : list ident. 235 235 list register → register → 236 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝236 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 237 237 λglobals,destrs,srcr. 238 238 ν tmp in … … 242 242 definition translate_fill_with_zero : 243 243 ∀globals : list ident. 244 list register → list (joint_seq rtl_paramsglobals) ≝244 list register → list (joint_seq RTL globals) ≝ 245 245 λglobals,destrs. 246 246 match nat_to_args (|destrs|) 0 with … … 270 270 ∀globals: list ident. 271 271 signedness → list register → list register → 272 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝272 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 273 273 λglobals,src_sign,destrs,srcrs. 274 274 match reduce_strong ?? destrs srcrs with … … 299 299 ∀destrs : list register. 300 300 ∀srcrs_arg : list register. 301 |destrs| = |srcrs_arg| → list (joint_seq rtl_paramsglobals) ≝301 |destrs| = |srcrs_arg| → list (joint_seq RTL globals) ≝ 302 302 λglobals, destrs, srcrs, prf. 303 map2 ??? (OP1 rtl_paramsglobals Cmpl) destrs srcrs prf.304 305 definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝303 map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf. 304 305 definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 306 306 λglobals: list ident. 307 307 λdestrs: list register. … … 318 318 ∀globals : list ident. 319 319 list register → list register → 320 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝320 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 321 321 λglobals,destrs,srcrs. 322 322 match destrs with … … 328 328 | cons srcr srcrs' ⇒ 329 329 (destr ← srcr) ::: 330 map register (joint_seq rtl_paramsglobals) (λr. destr ← destr .Or. r) srcrs' @@330 map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@ 331 331 (* now destr is non-null iff srcrs was non-null *) 332 332 CLEAR_CARRY ?? ::: … … 341 341 342 342 definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? → 343 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝343 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 344 344 λglobals. 345 345 λty, ty'. … … 351 351 match op1 352 352 return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' → 353 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) with353 bind_new (localsT RTL) (list (joint_seq RTL globals)) with 354 354 [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2. 355 355 translate_cast globals src_sign destrs srcrs … … 410 410 (Σi.i<S k) → 411 411 (* the accumulator *) 412 list (joint_seq rtl_paramsglobals) →413 list (joint_seq rtl_paramsglobals) ≝412 list (joint_seq RTL globals) → 413 list (joint_seq RTL globals) ≝ 414 414 λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2, 415 415 tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc. … … 456 456 ] qed. 457 457 458 definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝458 definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 459 459 λglobals : list ident. 460 460 λdestrs : list register. … … 472 472 (* the step calculating all products with least significant byte going in the 473 473 k-th position of the result *) 474 let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq rtl_paramsglobals) →475 list (joint_seq rtl_paramsglobals) ≝474 let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) → 475 list (joint_seq RTL globals) ≝ 476 476 λk_sig,acc.match k_sig with 477 477 [ mk_Sig k k_prf ⇒ … … 496 496 497 497 definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→ 498 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝498 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 499 499 λglobals: list ident. 500 500 λdiv_not_mod: bool. … … 543 543 544 544 definition translate_ne: ∀globals: list ident.?→?→?→?→ 545 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝545 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 546 546 λglobals: list ident. 547 547 λdestrs: list register. … … 559 559 | cons srcr2 srcrs2' ⇒ λEQ. 560 560 νtmpr in 561 let f : psd_argument → psd_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_paramsglobals) ≝561 let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝ 562 562 λs1,s2,acc. 563 563 tmpr ← s1 .Xor. s2 :: 564 564 destr ← destr .Or. tmpr :: 565 565 acc in 566 let epilogue : list (joint_seq rtl_paramsglobals) ≝566 let epilogue : list (joint_seq RTL globals) ≝ 567 567 [ CLEAR_CARRY ?? ; 568 568 tmpr ← zero_byte .Sub. destr ; … … 577 577 (* if destrs is 0 or 1, it inverses it. To be used after operations that 578 578 ensure this. *) 579 definition translate_toggle_bool : ∀globals.?→list (joint_seq rtl_paramsglobals) ≝579 definition translate_toggle_bool : ∀globals.?→list (joint_seq RTL globals) ≝ 580 580 λglobals: list ident. 581 581 λdestrs: list register. … … 591 591 ∀srcrs2: list psd_argument. 592 592 |srcrs1| = |srcrs2| → 593 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝593 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 594 594 λglobals,destrs,srcrs1,srcrs2,srcrs_prf. 595 595 match destrs with … … 609 609 (tmp : register) 610 610 (srcrs : list psd_argument) on srcrs : 611 Σt : (list psd_argument) × (list (joint_seq rtl_paramsglobals)).|\fst t| = |srcrs| ≝611 Σt : (list psd_argument) × (list (joint_seq RTL globals)).|\fst t| = |srcrs| ≝ 612 612 let byte_128 : Byte ≝ true ::: bv_zero ? in 613 613 match srcrs with … … 631 631 ∀srcrs2: list psd_argument. 632 632 |srcrs1| = |srcrs2| → 633 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝633 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 634 634 λglobals,destrs,srcrs1,srcrs2,srcrs_prf. 635 635 νtmp_last_s1 in … … 649 649 qed. 650 650 651 definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝651 definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 652 652 λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf. 653 653 if is_unsigned then … … 684 684 |srcrs1| = size_of_sig_type ty1 → 685 685 |srcrs2| = size_of_sig_type ty2 → 686 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝686 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 687 687 λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2. 688 688 match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3. … … 728 728 729 729 definition translate_cond: ∀globals: list ident. list register → label → 730 bind_seq_block rtl_params globals (joint_step rtl_paramsglobals) ≝730 bind_seq_block RTL globals (joint_step RTL globals) ≝ 731 731 λglobals: list ident. 732 732 λsrcrs: list register. 733 733 λlbl_true: label. 734 match srcrs return λ_.bind_seq_block rtl_params? (joint_step ??) with734 match srcrs return λ_.bind_seq_block RTL ? (joint_step ??) with 735 735 [ nil ⇒ bret … 〈[ ], NOOP ??〉 736 736 | cons srcr srcrs' ⇒ 737 737 ν tmpr in 738 let f : register → joint_seq rtl_paramsglobals ≝738 let f : register → joint_seq RTL globals ≝ 739 739 λr. tmpr ← tmpr .Or. r in 740 bret … 〈MOVE rtl_paramsglobals 〈tmpr,srcr〉 ::740 bret … 〈MOVE RTL globals 〈tmpr,srcr〉 :: 741 741 map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉 742 742 ]. 743 743 744 744 (* Paolo: to be controlled (original seemed overly complex) *) 745 definition translate_load : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝745 definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝ 746 746 λglobals: list ident. 747 747 λaddr : list psd_argument. … … 750 750 ν tmp_addr_l in 751 751 ν tmp_addr_h in 752 let f ≝ λdestr : register.λacc : list (joint_seq rtl_paramsglobals).753 LOAD rtl_paramsglobals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::752 let f ≝ λdestr : register.λacc : list (joint_seq RTL globals). 753 LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) :: 754 754 translate_op ? Add 755 755 [tmp_addr_l ; tmp_addr_h] … … 761 761 ] // qed. 762 762 763 definition translate_store : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝763 definition translate_store : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝ 764 764 λglobals: list ident. 765 765 λaddr : list psd_argument. … … 768 768 ν tmp_addr_l in 769 769 ν tmp_addr_h in 770 let f ≝ λsrcr : psd_argument.λacc : list (joint_seq rtl_paramsglobals).771 STORE rtl_paramsglobals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::770 let f ≝ λsrcr : psd_argument.λacc : list (joint_seq RTL globals). 771 STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr :: 772 772 translate_op … Add 773 773 [tmp_addr_l ; tmp_addr_h] … … 780 780 definition translate_statement : ∀globals.local_env → statement → 781 781 𝚺b : 782 bind_seq_block rtl_params globals (joint_step rtl_paramsglobals) +783 bind_seq_block rtl_params globals (joint_fin_step rtl_params).782 bind_seq_block RTL globals (joint_step RTL globals) + 783 bind_seq_block RTL globals (joint_fin_step RTL). 784 784 if is_inl … b then label else unit ≝ 785 785 λglobals,lenv,stmt. … … 812 812 ❬(match retr with 813 813 [ Some retr ⇒ 814 CALL_ID rtl_params? f (rtl_args args lenv ?) (find_local_env retr lenv ?)814 CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?) 815 815 | None ⇒ 816 CALL_ID rtl_params? f (rtl_args args lenv ?) [ ]816 CALL_ID RTL ? f (rtl_args args lenv ?) [ ] 817 817 ] : bind_seq_block ???), lbl'❭ 818 818 | St_call_ptr f args retr lbl' ⇒ … … 882 882 let entry' ≝ f_entry def in 883 883 let exit' ≝ f_exit def in 884 let graph' ≝ empty_map LabelTag (joint_statement rtl_paramsglobals) in884 let graph' ≝ empty_map LabelTag (joint_statement RTL globals) in 885 885 let graph' ≝ add LabelTag ? graph' entry' 886 886 (GOTO … exit') in … … 891 891 b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in 892 892 let res ≝ 893 mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'893 mk_joint_internal_function RTL globals luniverse' runiverse' result' params' 894 894 locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in 895 895 foldi … f_trans (f_graph def) res. -
src/joint/Joint_paolo.ma
r2208 r2214 472 472 (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))). 473 473 474 record joint_internal_function ( globals: list ident) (p:params) : Type[0] ≝474 record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝ 475 475 { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) 476 476 joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) … … 489 489 490 490 definition joint_closed_internal_function ≝ 491 λ globals,p.491 λp,globals. 492 492 Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def). 493 493 … … 495 495 λglobals: list ident. 496 496 λpars: params. 497 λint_fun: joint_internal_function globals pars.497 λint_fun: joint_internal_function pars globals. 498 498 λgraph: codeT pars globals. 499 499 λentry. 500 500 λexit. 501 mk_joint_internal_function globals pars501 mk_joint_internal_function pars globals 502 502 (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun) 503 503 (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun) … … 507 507 λglobals.λpars : graph_params. 508 508 λgraph. 509 λp:joint_internal_function globals pars.509 λp:joint_internal_function pars globals. 510 510 λentry_prf. 511 511 λexit_prf. … … 536 536 definition add_graph ≝ 537 537 λg_pars : graph_params.λglobals.λl:label.λstmt. 538 λp:joint_internal_function g lobals g_pars.538 λp:joint_internal_function g_pars globals. 539 539 let code ≝ add … (joint_if_code … p) l stmt in 540 mk_joint_internal_function ? g_pars540 mk_joint_internal_function … 541 541 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) 542 542 (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) … … 550 550 551 551 definition set_locals ≝ 552 λ globals,pars.553 λp : joint_internal_function globals pars.552 λpars,globals. 553 λp : joint_internal_function pars globals. 554 554 λlocals. 555 mk_joint_internal_function globals pars555 mk_joint_internal_function pars globals 556 556 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) 557 557 (joint_if_params … p) locals (joint_if_stacksize … p) … … 561 561 562 562 definition joint_program ≝ 563 λp:params. program ( λglobals. joint_function globalsp) nat.563 λp:params. program (joint_function p) nat. -
src/joint/TranslateUtils_paolo.ma
r2182 r2214 5 5 (* type T is the syntactic type of the generated things *) 6 6 (* (sig for RTLabs registers, unit in others ) *) 7 definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).7 definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g). 8 8 9 9 definition rtl_ertl_fresh_reg: … … 39 39 (globals: list ident) 40 40 (insts: list (joint_seq g_pars globals)) 41 (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝41 (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝ 42 42 match insts with 43 43 [ nil ⇒ return src … … 49 49 ]. 50 50 51 definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with 52 [ inl _ ⇒ true 53 | inr _ ⇒ false 54 ]. 55 definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with 56 [ inl _ ⇒ true 57 | inr _ ⇒ false 58 ]. 59 51 60 definition adds_graph : 52 61 ∀g_pars : graph_params. … … 55 64 seq_block g_pars globals (joint_fin_step g_pars). 56 65 label → if is_inl … b then label else unit → 57 joint_internal_function … g_pars → joint_internal_function … g_pars ≝66 joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝ 58 67 λg_pars,globals,insts,src. 59 68 match insts return λx.if is_inl … x then ? else ? → ? → ? with … … 69 78 definition insert_prologue ≝ 70 79 λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). 71 λdef : joint_internal_function g lobals g_pars.80 λdef : joint_internal_function g_pars globals. 72 81 let entry ≝ joint_if_entry … def in 73 82 match stmt_at … entry … … 99 108 definition insert_epilogue ≝ 100 109 λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals). 101 λdef : joint_internal_function g lobals g_pars.110 λdef : joint_internal_function g_pars globals. 102 111 let exit ≝ joint_if_exit … def in 103 112 match stmt_at … exit … … 121 130 bind_seq_block g_pars globals (joint_fin_step g_pars). 122 131 label → if is_inl … b then label else unit → 123 joint_internal_function g lobals g_pars→124 joint_internal_function g lobals g_pars ≝132 joint_internal_function g_pars globals→ 133 joint_internal_function g_pars globals ≝ 125 134 λg_pars,globals,fresh_r,insts,src. 126 135 match insts return λx.if is_inl … x then ? else ? → ? → ? with … … 140 149 freshT globals dst_g_pars (localsT dst_g_pars) → 141 150 (* initialized function definition with empty graph *) 142 joint_internal_function globals dst_g_pars →151 joint_internal_function dst_g_pars globals → 143 152 (* functions dictating the translation *) 144 153 (label → joint_step src_g_pars globals → … … 147 156 bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) → 148 157 (* source function *) 149 joint_internal_function globals src_g_pars →158 joint_internal_function src_g_pars globals → 150 159 (* destination function *) 151 joint_internal_function globals dst_g_pars ≝160 joint_internal_function dst_g_pars globals ≝ 152 161 λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def. 153 162 let f : label → joint_statement (src_g_pars : params) globals → 154 joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝163 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 155 164 λlbl,stmt,def. 156 165 match stmt with … … 167 176 ∀globals: list ident. 168 177 (* initialized function definition with empty graph *) 169 joint_internal_function … dst_g_pars →178 joint_internal_function dst_g_pars globals → 170 179 (* functions dictating the translation *) 171 180 (label → joint_step src_g_pars globals → … … 174 183 seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) → 175 184 (* source function *) 176 joint_internal_function … src_g_pars →185 joint_internal_function src_g_pars globals → 177 186 (* destination function *) 178 joint_internal_function … dst_g_pars ≝187 joint_internal_function dst_g_pars globals ≝ 179 188 λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def. 180 189 let f : label → joint_statement (src_g_pars : params) globals → 181 joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝190 joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 182 191 λlbl,stmt,def. 183 192 match stmt with -
src/joint/blocks.ma
r2186 r2214 2 2 include "utilities/bindLists.ma". 3 3 4 inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝4 (* inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝ 5 5 | block_seq : joint_seq p globals → block_step p globals 6 6 | block_skip : label → block_step p globals. … … 40 40 41 41 definition skip_block ≝ λp,globals,A. 42 (list (block_step p globals)) × A. 42 (list (block_step p globals)) × A.*) 43 43 44 44 definition seq_block ≝ λp : stmt_params.λglobals,A. 45 45 (list (joint_seq p globals)) × A. 46 46 47 definition seq_to_skip_block :47 (*definition seq_to_skip_block : 48 48 ∀p,g,A.seq_block p g A → skip_block p g A 49 49 ≝ λp,g,A,b.〈\fst b, \snd b〉. … … 51 51 coercion skip_from_seq_block : 52 52 ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝ 53 seq_to_skip_block on _b : seq_block ??? to skip_block ???. 53 seq_to_skip_block on _b : seq_block ??? to skip_block ???.*) 54 54 55 55 definition bind_seq_block ≝ λp : stmt_params.λglobals,A. … … 70 70 bind_seq_list p g ≡ bind_new R L. 71 71 72 definition bind_skip_block ≝ λp : stmt_params.λglobals,A.72 (*definition bind_skip_block ≝ λp : stmt_params.λglobals,A. 73 73 bind_new (localsT p) (skip_block p globals A). 74 74 unification hint 0 ≔ p : stmt_params, g, A; … … 84 84 coercion bind_skip_from_seq_block : 85 85 ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝ 86 bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???. 86 bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.*) 87 87 (* 88 88 definition block_classifier ≝ -
src/joint/linearise.ma
r2200 r2214 652 652 ∀p : unserialized_params. 653 653 ∀globals. 654 joint_internal_function globals (mk_graph_params p)→655 joint_internal_function globals (mk_lin_params p)654 joint_internal_function (mk_graph_params p) globals → 655 joint_internal_function (mk_lin_params p) globals 656 656 (* ∃sigma : identifier_map LabelTag ℕ. 657 657 let g ≝ joint_if_code ?? (pi1 … fin) in … … 670 670 (stmt_implicit_label … s)) (nth_opt … n c)*) ≝ 671 671 λp,globals,f_in. 672 mk_joint_internal_function globals (mk_lin_params p)672 mk_joint_internal_function (mk_lin_params p) globals 673 673 (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in) 674 674 (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in) -
src/joint/semanticsUtils_paolo.ma
r2208 r2214 124 124 definition make_sem_graph_params : 125 125 ∀pars : graph_params. 126 ∀g_pars : more_sem_ genv_params pars.126 ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars). 127 127 sem_params ≝ 128 128 λpars,g_pars. … … 163 163 definition make_sem_lin_params : 164 164 ∀pars : lin_params. 165 ∀g_pars : more_sem_ genv_params pars.165 ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars). 166 166 sem_params ≝ 167 167 λpars,g_pars. -
src/joint/semantics_paolo.ma
r2200 r2214 12 12 only the head is kept (or Undef if the list is empty) ??? *) 13 13 14 definition genv ≝ λ globals.λp:params. genv_t (joint_function globals p).14 definition genv ≝ λp:params.λglobals.genv_t (joint_function p globals). 15 15 definition cpointer ≝ Σp.ptype p = Code. 16 16 definition xpointer ≝ Σp.ptype p = XData. … … 68 68 ∀pars : params. 69 69 ∀globals. 70 genv globals pars →70 genv pars globals → 71 71 block → 72 res (joint_internal_function … pars) ≝73 λpars, blobals,ge,b.72 res (joint_internal_function pars globals) ≝ 73 λpars,globals,ge,b. 74 74 do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; 75 75 match def with … … 81 81 ∀pars : params. 82 82 ∀globals. 83 genv globals pars →83 genv pars globals → 84 84 cpointer → 85 res (joint_internal_function … pars) ≝85 res (joint_internal_function pars globals) ≝ 86 86 λpars,globals,ge,p.function_of_block pars globals ge (pblock p). 87 87 88 inductive step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝ 89 | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p globals (Labels lbls) (* used for goto-like flow alteration *) 90 | Init : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals Call (* call a function with given id, then proceed *) 91 | Proceed : ∀flows.step_flow p globals flows. (* go to implicit successor *) 92 93 (* 94 definition step_flow_cons : ∀p,globals,l,lbls. 95 step_flow p globals lbls → step_flow p globals (l :: lbls) ≝ 96 λp,globals,l1,l2,flow.match flow with 97 [ Redirect l ⇒ Redirect … «l, ?» 98 | Init id f args dest ⇒ Init … id f args dest 99 | Proceed ⇒ Proceed ??? 100 ]. cases l /2 by or_intror/ qed. 101 coercion step_flow_c : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1::l2) ≝ 102 step_flow_cons on _flow : step_flow ??? to step_flow ?? (cons ???). 103 104 definition step_flow_append_l : ∀p,globals,l1,l2. 105 step_flow p globals l1 → step_flow p globals (l1 @ l2) ≝ 106 λp,globals,l1,l2,flow.match flow with 107 [ Redirect l ⇒ Redirect … «l, ?» 108 | Init id f args dest ⇒ Init … id f args dest 109 | Proceed ⇒ Proceed ??? 110 ]. cases l /2 by Exists_append_l/ qed. 111 coercion step_flow_l : ∀p,globals,l1,l2.∀flow : step_flow p globals l1.step_flow p globals (l1@l2) ≝ 112 step_flow_append_l on _flow : step_flow ??? to step_flow ?? (append ???). 113 114 definition step_flow_append_r : ∀p,globals,l1,l2. 115 step_flow p globals l2 → step_flow p globals (l1 @ l2) ≝ 116 λp,globals,l1,l2,flow.match flow with 117 [ Redirect l ⇒ Redirect … «l, ?» 118 | Init id f args dest ⇒ Init … id f args dest 119 | Proceed ⇒ Proceed ??? 120 ]. cases l /2 by Exists_append_r/ qed. 121 coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝ 122 step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???). 123 *) 124 125 inductive fin_step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝ 126 | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p globals (Labels lbls) 127 | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals Call 128 | FEnd1 : fin_step_flow p globals (Labels [ ]) (* end flow *) 129 | FEnd2 : fin_step_flow p globals Call. (* end flow *) 130 131 (* 132 definition fin_step_flow_cons : ∀p,globals,l,lbls. 133 fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝ 134 λp,globals,l1,l2,flow.match flow with 135 [ FRedirect l ⇒ FRedirect … «l, ?» 136 | FTailInit id f args ⇒ FTailInit … id f args 137 | FEnd ⇒ FEnd ??? 138 ]. cases l /2 by or_intror/ qed. 139 coercion fin_step_flow_c : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1::l2) ≝ 140 fin_step_flow_cons on _flow : fin_step_flow ??? to fin_step_flow ?? (cons ???). 141 142 definition fin_step_flow_append_l : ∀p,globals,l1,l2. 143 fin_step_flow p globals l1 → fin_step_flow p globals (l1@l2) ≝ 144 λp,globals,l1,l2,flow.match flow with 145 [ FRedirect l ⇒ FRedirect … «l, ?» 146 | FTailInit id f args ⇒ FTailInit … id f args 147 | FEnd ⇒ FEnd ??? 148 ]. cases l /2 by Exists_append_l/ qed. 149 coercion fin_step_flow_l : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l1.fin_step_flow p globals (l1@l2) ≝ 150 fin_step_flow_append_l on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???). 151 152 definition fin_step_flow_append_r : ∀p,globals,l1,l2. 153 fin_step_flow p globals l2 → fin_step_flow p globals (l1@l2) ≝ 154 λp,globals,l1,l2,flow.match flow with 155 [ FRedirect l ⇒ FRedirect … «l, ?» 156 | FTailInit id f args ⇒ FTailInit … id f args 157 | FEnd ⇒ FEnd ??? 158 ]. cases l /2 by Exists_append_r/ qed. 159 coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝ 160 fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???). 161 *) 162 163 record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝ 164 { st_pars :> sem_state_params 88 inductive step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝ 89 | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *) 90 | Init : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *) 91 | Proceed : ∀flows.step_flow p F flows. (* go to implicit successor *) 92 93 inductive fin_step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝ 94 | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls) 95 | FTailInit : Z → F → call_args p → fin_step_flow p F Call 96 | FEnd1 : fin_step_flow p F (Labels [ ]) (* end flow *) 97 | FEnd2 : fin_step_flow p F Call. (* end flow *) 98 99 record more_sem_unserialized_params 100 (uns_pars : unserialized_params) 101 (F : list ident → Type[0]) : Type[1] ≝ 102 { st_pars :> sem_state_params (* automatic coercion has issues *) 165 103 ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) 166 104 ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval … … 181 119 ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars 182 120 (* Paolo: save_frame separated from call_setup to factorize tailcall code *) 183 ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars121 ; save_frame: cpointer → call_dest uns_pars → state st_pars → res (state st_pars) 184 122 (*CSC: setup_call returns a res only because we can call a function with the wrong number and 185 123 type of arguments. To be fixed using a dependent type *) … … 191 129 ; call_args_for_main: call_args uns_pars 192 130 ; call_dest_for_main: call_dest uns_pars 193 }. 131 132 (* from now on, parameters that use the type of functions *) 133 ; read_result: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (list beval) 134 (* change of pc must be left to *_flow execution *) 135 ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars → 136 state st_pars → IO io_out io_in (state st_pars) 137 ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars → 138 state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars)) 139 ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars. 140 state st_pars → 141 IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars)) 142 ; pop_frame: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (state st_pars) 143 }. 144 145 (*coercion msu_pars_to_ss_pars nocomposites : 146 ∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params 147 ≝ st_pars 148 on _msup : more_sem_unserialized_params ?? to sem_state_params.*) 194 149 195 150 196 151 definition helper_def_retrieve : 197 ∀X : ? → ? → Type[0].198 (∀up .∀p:more_sem_unserialized_params up. regsT p → X upp → res beval) →199 ∀up .∀p : more_sem_unserialized_params up.state p → X upp → res beval ≝200 λX,f,up, p,st.f? p (regs … st).152 ∀X : ? → ? → ? → Type[0]. 153 (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) → 154 ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝ 155 λX,f,up,F,p,st.f ?? p (regs … st). 201 156 202 157 definition helper_def_store : 203 ∀X : ? → ? → Type[0].204 (∀up .∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →205 ∀up .∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝206 λX,f,up, p,x,v,st.! r ← f? p x v (regs … st) ; return set_regs … r st.158 ∀X : ? → ? → ? → Type[0]. 159 (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) → 160 ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝ 161 λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st. 207 162 208 163 definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_. … … 219 174 definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_. 220 175 definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_. 221 definition pair_reg_move : ?→?→?→?→?≝222 λup .λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.223 ! r ← pair_reg_move_ ? p (regs ? st) pm;176 definition pair_reg_move ≝ 177 λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up. 178 ! r ← pair_reg_move_ ?? p (regs ? st) pm; 224 179 return set_regs ? r st. 225 180 226 181 227 182 axiom BadPointer : String. 228 183 229 184 (* this is preamble to all calls (including tail ones). The optional argument in 230 185 input tells the function whether it has to save the frame for internal … … 235 190 serialization and on whether the call is a tail one. *) 236 191 definition eval_call_block: 237 ∀ globals.∀p : params.∀p':more_sem_unserialized_params p.238 genv globals p → state p'→ block → call_args p → call_dest p →239 IO io_out io_in ((step_flow p globals Call)×(state p')) ≝240 λ globals,p,p',ge,st,b,args,dest.241 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr …ge b) : IO ? io_in ?);192 ∀p,F.∀p':more_sem_unserialized_params p F.∀globals. 193 genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p → 194 IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝ 195 λp,F,p',globals,ge,st,b,args,dest. 196 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 242 197 match fd with 243 [ Internal f n⇒244 return 〈Init … (block_id b) fnargs dest, st〉198 [ Internal fd ⇒ 199 return 〈Init ?? (block_id b) fd args dest, st〉 245 200 | External fn ⇒ 246 201 ! params ← fetch_external_args … p' fn st : IO ???; … … 289 244 return 〈st'', pr〉. 290 245 291 (* parameters that need full params to have type of functions,292 but are still independent of serialization *)293 record more_sem_genv_params (pp : params) : Type[1] ≝294 { msu_pars :> more_sem_unserialized_params pp295 ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)296 (* change of pc must be left to *_flow execution *)297 ; eval_ext_seq: ∀globals.genv globals pp → ext_seq pp →298 state msu_pars → IO io_out io_in (state msu_pars)299 ; eval_ext_tailcall : ∀globals.genv globals pp → ext_tailcall pp →300 state msu_pars → IO io_out io_in ((fin_step_flow pp globals Call)×(state msu_pars))301 ; eval_ext_call: ∀globals.genv globals pp →∀s : ext_call pp.302 state msu_pars →303 IO io_out io_in ((step_flow pp globals Call)×(state msu_pars))304 ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)305 }.306 307 246 (* parameters that are defined by serialization *) 308 247 record more_sem_params (pp : params) : Type[1] ≝ 309 { ms g_pars :> more_sem_genv_params pp248 { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp) 310 249 ; offset_of_point : code_point pp → option offset (* can overflow *) 311 250 ; point_of_offset : offset → code_point pp … … 315 254 ∀o.offset_of_point (point_of_offset o) = Some ? o 316 255 }. 256 257 (* 258 coercion ms_pars_to_msu_pars nocomposites : 259 ∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p) 260 ≝ msu_pars 261 on _msp : more_sem_params ? to more_sem_unserialized_params ??. 262 263 definition ss_pars_of_ms_pars ≝ 264 λp.λpp : more_sem_params p. 265 st_pars … (msu_pars … pp). 266 coercion ms_pars_to_ss_pars nocomposites : 267 ∀p : params.∀msp : more_sem_params p.sem_state_params ≝ 268 ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*) 317 269 318 270 axiom CodePointerOverflow : String. … … 374 326 375 327 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals. 376 genv globals p→ cpointer → res (joint_statement p globals) ≝328 genv p globals → cpointer → res (joint_statement p globals) ≝ 377 329 λp,msp,globals,ge,ptr. 378 330 let pt ≝ point_of_pointer ? msp ptr in … … 381 333 382 334 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. 383 genv globals p→ cpointer → label → res cpointer ≝335 genv p globals → cpointer → label → res cpointer ≝ 384 336 λp,msp,globals,ge,ptr,lbl. 385 337 ! fn ← fetch_function … ge ptr ; … … 399 351 }. 400 352 353 (* definition msu_pars_of_s_pars : 354 ∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) 355 ≝ λp : sem_params. 356 msu_pars … (more_sem_pars p). 357 coercion s_pars_to_msu_pars nocomposites : 358 ∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝ 359 msu_pars_of_s_pars 360 on p : sem_params to more_sem_unserialized_params ??. 361 362 definition ss_pars_of_s_pars : 363 ∀p : sem_params.sem_state_params 364 ≝ λp : sem_params. 365 st_pars … (msu_pars … (more_sem_pars p)). 366 coercion s_pars_to_ss_pars nocomposites : 367 ∀p : sem_params.sem_state_params ≝ 368 ss_pars_of_s_pars 369 on _p : sem_params to sem_state_params. 370 371 definition ms_pars_of_s_pars : 372 ∀p : sem_params.more_sem_params (spp p) 373 ≝ more_sem_pars. 374 coercion s_pars_to_ms_pars nocomposites : 375 ∀p : sem_params.more_sem_params (spp p) ≝ 376 ms_pars_of_s_pars 377 on p : sem_params to more_sem_params ?.*) 378 401 379 (* definition address_of_label: ∀globals. ∀p:sem_params. 402 380 genv globals p → pointer → label → res address ≝ … … 405 383 OK … (address_of_code_pointer newptr). *) 406 384 407 definition goto: ∀globals. ∀p:sem_params.408 genv globals p→ label → state p → cpointer → res (state_pc p) ≝385 definition goto: ∀globals.∀p : sem_params. 386 genv p globals → label → state p → cpointer → res (state_pc p) ≝ 409 387 λglobals,p,ge,l,st,b. 410 388 ! newpc ← pointer_of_label ? p … ge b l ; … … 427 405 428 406 definition eval_seq_no_pc : 429 ∀globals.∀p:sem_params. genv globals p→ state p →407 ∀globals.∀p:sem_params. genv p globals → state p → 430 408 ∀s:joint_seq p globals. 431 409 IO io_out io_in (state p) ≝ … … 433 411 match seq return λx.IO ??? with 434 412 [ extension_seq c ⇒ 435 eval_ext_seq ???ge c st413 eval_ext_seq … ge c st 436 414 | LOAD dst addrl addrh ⇒ 437 415 ! vaddrh ← dph_arg_retrieve … st addrh ; … … 484 462 | POP dst ⇒ 485 463 ! 〈st',v〉 ← pop p st; 486 acca_store pp dst v st'464 acca_store … p dst v st' 487 465 | PUSH src ⇒ 488 466 ! v ← acca_arg_retrieve … st src; … … 495 473 return st' 496 474 | extension_call s ⇒ 497 !〈flow, st'〉 ← eval_ext_call ???ge s st ;475 !〈flow, st'〉 ← eval_ext_call … ge s st ; 498 476 return st' 499 477 | _ ⇒ return st … … 504 482 505 483 definition eval_seq_pc : 506 ∀globals.∀p:sem_params. genv globals p→ state p →484 ∀globals.∀p:sem_params. genv p globals → state p → 507 485 ∀s:joint_seq p globals. 508 IO io_out io_in (step_flow p globals(step_flows … s)) ≝486 IO io_out io_in (step_flow p ? (step_flows … s)) ≝ 509 487 λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with 510 488 [ CALL_ID id args dest ⇒ … … 513 491 return flow 514 492 | extension_call s ⇒ 515 !〈flow, st'〉 ← eval_ext_call ???ge s st ;493 !〈flow, st'〉 ← eval_ext_call … ge s st ; 516 494 return flow 517 495 | _ ⇒ return Proceed ??? … … 519 497 520 498 definition eval_step : 521 ∀globals.∀p:sem_params. genv globals p→ state p →499 ∀globals.∀p:sem_params. genv p globals → state p → 522 500 ∀s:joint_step p globals. 523 IO io_out io_in ((step_flow p globals(step_flows … s))×(state p)) ≝501 IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝ 524 502 λglobals,p,ge,st,s. 525 503 match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with … … 538 516 %1 % qed. 539 517 540 definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv globals p→518 definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals → 541 519 state p → ∀s : joint_fin_step p. 542 520 IO io_out io_in (state p) ≝ … … 544 522 match s return λx.IO ??? with 545 523 [ tailcall c ⇒ 546 !〈flow,st'〉 ← eval_ext_tailcall ???ge c st ;524 !〈flow,st'〉 ← eval_ext_tailcall … ge c st ; 547 525 return st' 548 526 | _ ⇒ return st … … 550 528 551 529 definition eval_fin_step_pc : 552 ∀globals.∀p:sem_params. genv globals p→ state p →530 ∀globals.∀p:sem_params. genv p globals → state p → 553 531 ∀s:joint_fin_step p. 554 IO io_out io_in (fin_step_flow p globals(fin_step_flows … s)) ≝532 IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝ 555 533 λg,p,ge,st,s. 556 534 match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with 557 535 [ tailcall c ⇒ 558 !〈flow,st'〉 ← eval_ext_tailcall ???ge c st ;536 !〈flow,st'〉 ← eval_ext_tailcall … ge c st ; 559 537 return flow 560 538 | GOTO l ⇒ return FRedirect … l … … 562 540 ]. %1 % qed. 563 541 564 definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p→565 state p → Z → joint_internal_function globals p→ call_args p →542 definition do_call : ∀globals: list ident.∀p:sem_params. genv p globals → 543 state p → Z → joint_internal_function p globals → call_args p → 566 544 res (state_pc p) ≝ 567 545 λglobals,p,ge,st,id,fn,args. 568 546 ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn) 569 547 args st ; 570 let regs ≝ foldr ?? (allocate_local pp) (regs … st) (joint_if_locals … fn) in548 let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in 571 549 let l' ≝ joint_if_entry … fn in 572 550 let st' ≝ set_regs p regs st in … … 577 555 (* The pointer provided is the one to the *next* instruction. *) 578 556 definition eval_step_flow : 579 ∀globals.∀p:sem_params.∀flows.genv globals p→580 state p → cpointer → step_flow p globalsflows → res (state_pc p) ≝557 ∀globals.∀p:sem_params.∀flows.genv p globals → 558 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝ 581 559 λglobals,p,flows,ge,st,nxt,cmd. 582 560 match cmd with … … 584 562 goto … ge l st nxt 585 563 | Init id fn args dest ⇒ 586 let st' ≝ set_frms … (save_frame … nxt dest st) st in564 ! st' ← save_frame … nxt dest st ; 587 565 do_call ?? ge st' id fn args 588 566 | Proceed _ ⇒ … … 590 568 ]. 591 569 592 definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv globals p→593 state p → cpointer → fin_step_flow p globalsflows → res (state_pc p) ≝570 definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv p globals → 571 state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝ 594 572 λglobals,p,lbls,ge,st,curr,cmd. 595 573 match cmd with … … 604 582 605 583 definition eval_statement : 606 ∀globals.∀p:sem_params.genv globals p→584 ∀globals.∀p:sem_params.genv p globals → 607 585 state_pc p → joint_statement p globals → 608 586 IO io_out io_in (state_pc p) ≝ … … 619 597 ]. 620 598 621 definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p→599 definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals → 622 600 state_pc p → IO io_out io_in (state_pc p) ≝ 623 601 λglobals,p,ge,st. … … 629 607 not static... *) 630 608 definition is_final: ∀globals:list ident. ∀p: sem_params. 631 genv globals p→ cpointer → state_pc p → option int ≝609 genv p globals → cpointer → state_pc p → option int ≝ 632 610 λglobals,p,ge,exit,st.res_to_opt ? ( 633 611 do s ← fetch_statement ? p … ge (pc … st);
Note: See TracChangeset
for help on using the changeset viewer.