- Timestamp:
- Sep 5, 2011, 1:23:20 PM (10 years ago)
- Location:
- src/joint
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Joint.ma
r1176 r1182 6 6 7 7 record params: Type[1] ≝ 8 { next: Type[0] 8 { 9 acc_a_reg: Type[0]; 10 acc_b_reg: Type[0]; 11 dpl_reg: Type[0]; 12 dph_reg: Type[0]; 13 pair_reg: Type[0]; 14 generic_reg: Type[0]; 9 15 10 ; acc_a_reg: Type[0] 11 ; acc_b_reg: Type[0] 12 ; dpl_reg: Type[0] 13 ; dph_reg: Type[0] 14 ; pair_reg: Type[0] 15 ; generic_reg: Type[0] 16 extend_statements: Type[0]; 16 17 17 ; extend_statements: Type[0] 18 19 ; resultT: Type[0] 20 ; localsT: Type[0] 21 ; paramsT: Type[0] 22 }. 18 resultT: Type[0]; 19 localsT: Type[0]; 20 paramsT: Type[0] 21 }. 23 22 24 23 inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝ … … 38 37 | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals 39 38 | joint_instr_call_id: ident → nat → joint_instruction p globals 40 | joint_instr_cond: acc_a_reg p → next p→ joint_instruction p globals.39 | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals. 41 40 42 41 inductive joint_statement (p:params) (globals: list ident): Type[0] ≝ 43 | joint_st_sequential: joint_instruction p globals → next p→ joint_statement p globals44 | joint_st_goto: next p→ joint_statement p globals42 | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals 43 | joint_st_goto: label → joint_statement p globals 45 44 | joint_st_return: joint_statement p globals 46 45 | joint_st_extension: extend_statements p → joint_statement p globals. … … 48 47 record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝ 49 48 { pmemoryT: Type[0] 50 ; lookup: pmemoryT → next preparams→ option (joint_statement preparams globals)49 ; lookup: pmemoryT → label → option (joint_statement preparams globals) 51 50 }. 52 51 … … 60 59 joint_if_stacksize: nat; 61 60 joint_if_graph : pmemoryT … p; 62 joint_if_entry : Σl: next pre. lookup … p joint_if_graph l ≠ None ?;63 joint_if_exit : Σl: next pre. lookup … p joint_if_graph l ≠ None ?61 joint_if_entry : Σl: label. lookup … p joint_if_graph l ≠ None ?; 62 joint_if_exit : Σl: label. lookup … p joint_if_graph l ≠ None ? 64 63 }. 65 64 -
src/joint/semantics.ma
r1177 r1182 37 37 *) 38 38 (* CSC: ??? *) 39 axiom address_of_label: ∀p. mem → next p→ address.40 axiom address_chunks_of_label: ∀p. mem → next p→ Byte × Byte.39 axiom address_of_label: mem → label → address. 40 axiom address_chunks_of_label: mem → label → Byte × Byte. 41 41 axiom label_of_address_chunks: Byte → Byte → label. 42 42 axiom address_of_address_chunks: Byte → Byte → address. … … 106 106 107 107 (* CSC: was build_state in RTL *) 108 definition goto: ∀p:sem_params. next p→ state p → state p ≝108 definition goto: ∀p:sem_params. label → state p → state p ≝ 109 109 λp,l,st. set_pc … (address_of_label … (m … st) l) st. 110 110 … … 188 188 (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)). 189 189 190 definition save_ra : ∀p. state p → next p→ res (state p) ≝190 definition save_ra : ∀p. state p → label → res (state p) ≝ 191 191 λp,st,l. 192 192 let 〈addrl,addrh〉 ≝ address_chunks_of_label … (m … st) l in
Note: See TracChangeset
for help on using the changeset viewer.