| 1 | include "joint/SemanticUtils.ma". |
|---|
| 2 | include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *) |
|---|
| 3 | include alias "common/Identifiers.ma". |
|---|
| 4 | include alias "ASM/Util.ma". |
|---|
| 5 | |
|---|
| 6 | record frame: Type[0] ≝ |
|---|
| 7 | { fr_ret_regs: list register |
|---|
| 8 | ; fr_pc: address |
|---|
| 9 | ; fr_sp: pointer |
|---|
| 10 | ; fr_carry: beval |
|---|
| 11 | ; fr_regs: register_env beval |
|---|
| 12 | }. |
|---|
| 13 | |
|---|
| 14 | definition rtl_more_sem_params: more_sem_params rtl_params_ := |
|---|
| 15 | mk_more_sem_params rtl_params_ |
|---|
| 16 | (list frame) (register_env beval) graph_succ_p |
|---|
| 17 | reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve |
|---|
| 18 | reg_store reg_retrieve reg_store reg_retrieve |
|---|
| 19 | (λlocals,dest_src. |
|---|
| 20 | do v ← reg_retrieve locals (\snd dest_src) ; |
|---|
| 21 | reg_store (\fst dest_src) v locals) |
|---|
| 22 | pointer_of_label. |
|---|
| 23 | definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params. |
|---|
| 24 | |
|---|
| 25 | definition rtl_init_locals : |
|---|
| 26 | list register → register_env beval → register_env beval ≝ |
|---|
| 27 | λlocals,env. |
|---|
| 28 | foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals. |
|---|
| 29 | |
|---|
| 30 | (*CSC: could we use here a dependent type to avoid the Error case? *) |
|---|
| 31 | axiom EmptyStack: String. |
|---|
| 32 | axiom OutOfBounds: String. |
|---|
| 33 | |
|---|
| 34 | definition rtl_fetch_ra: |
|---|
| 35 | state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝ |
|---|
| 36 | λst. |
|---|
| 37 | match st_frms ? st with |
|---|
| 38 | [ nil ⇒ Error ? [MSG EmptyStack] |
|---|
| 39 | | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ]. |
|---|
| 40 | |
|---|
| 41 | definition rtl_fetch_result: |
|---|
| 42 | ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list beval) ≝ |
|---|
| 43 | λglobals,ge,st. |
|---|
| 44 | do fn ← graph_fetch_function … globals ge st ; |
|---|
| 45 | let ret_val_regs ≝ joint_if_result … fn in |
|---|
| 46 | mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs. |
|---|
| 47 | |
|---|
| 48 | (*CSC: we could use a dependent type here: the list of return values should have |
|---|
| 49 | the same length of the list of return registers that store the values. This |
|---|
| 50 | saves the OutOfBounds exception *) |
|---|
| 51 | definition rtl_pop_frame: |
|---|
| 52 | ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝ |
|---|
| 53 | λglobals,ge,st. |
|---|
| 54 | do ret_vals ← rtl_fetch_result … ge st ; |
|---|
| 55 | match st_frms ? st with |
|---|
| 56 | [ nil ⇒ Error ? [MSG EmptyStack] |
|---|
| 57 | | cons hd tl ⇒ |
|---|
| 58 | do st ← |
|---|
| 59 | mfold_left_i ?? |
|---|
| 60 | (λi.λst.λreg. |
|---|
| 61 | do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ; |
|---|
| 62 | greg_store rtl_sem_params reg v st) |
|---|
| 63 | (OK … st) (fr_ret_regs hd) ; |
|---|
| 64 | OK … |
|---|
| 65 | (set_frms rtl_sem_params tl |
|---|
| 66 | (set_regs rtl_sem_params (fr_regs hd) |
|---|
| 67 | (set_sp … (fr_sp hd) |
|---|
| 68 | (set_carry … (fr_carry hd) |
|---|
| 69 | (set_m … (free … (m … st) (pblock (sp … st))) st)))))]. |
|---|
| 70 | |
|---|
| 71 | definition rtl_save_frame: |
|---|
| 72 | address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝ |
|---|
| 73 | λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st. |
|---|
| 74 | let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in |
|---|
| 75 | do new_regs ← |
|---|
| 76 | mfold_left2 … |
|---|
| 77 | (λlenv,dest,src. |
|---|
| 78 | do v ← greg_retrieve … st src ; |
|---|
| 79 | OK … (add … lenv dest v)) |
|---|
| 80 | (OK … (empty_map …)) formal_arg_regs actual_arg_regs ; |
|---|
| 81 | OK … |
|---|
| 82 | (set_frms rtl_sem_params |
|---|
| 83 | (mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st)) |
|---|
| 84 | (set_regs rtl_sem_params new_regs |
|---|
| 85 | (set_m … mem |
|---|
| 86 | (set_sp … (mk_pointer XData b ? (mk_offset 0)) st)))). |
|---|
| 87 | cases daemon (*CSC: XXXX easy lemma on alloc to be turned into a dependent type*) |
|---|
| 88 | qed. |
|---|
| 89 | |
|---|
| 90 | (*CSC: XXXX, for external functions only*) |
|---|
| 91 | axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val). |
|---|
| 92 | axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params). |
|---|
| 93 | |
|---|
| 94 | definition rtl_exec_extended: |
|---|
| 95 | ∀globals. genv globals (rtl_params globals) → |
|---|
| 96 | rtl_statement_extension → label → state rtl_sem_params → |
|---|
| 97 | IO io_out io_in (trace × (state rtl_sem_params)) ≝ |
|---|
| 98 | λglobals,ge,stm,l,st. |
|---|
| 99 | match stm with |
|---|
| 100 | [ rtl_st_ext_stack_address dreg1 dreg2 ⇒ |
|---|
| 101 | let sp ≝ sp ? st in |
|---|
| 102 | ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ; |
|---|
| 103 | ! st ← greg_store rtl_sem_params dreg1 dpl st ; |
|---|
| 104 | ! st ← greg_store rtl_sem_params dreg2 dph st ; |
|---|
| 105 | ret ? 〈E0, goto … l st〉 |
|---|
| 106 | | rtl_st_ext_call_ptr _ _ _ _ ⇒ ? |
|---|
| 107 | | rtl_st_ext_tailcall_id id regs ⇒ ? |
|---|
| 108 | | rtl_st_ext_tailcall_ptr _ _ _ ⇒ ? |
|---|
| 109 | ]. |
|---|
| 110 | [1,2,3: cases not_implemented ] (*CSC: tailcalls and pointer calls not implemented ATM *) |
|---|
| 111 | qed. |
|---|
| 112 | |
|---|
| 113 | definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝ |
|---|
| 114 | λglobals. |
|---|
| 115 | mk_more_sem_params2 … rtl_more_sem_params |
|---|
| 116 | (graph_fetch_statement …) rtl_fetch_ra (rtl_fetch_result …) |
|---|
| 117 | rtl_init_locals rtl_save_frame (rtl_pop_frame …) |
|---|
| 118 | rtl_fetch_external_args rtl_set_result (rtl_exec_extended …). |
|---|
| 119 | |
|---|
| 120 | definition rtl_fullexec ≝ |
|---|
| 121 | joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)). |
|---|
