source: src/RTL/semantics.ma @ 1381

Last change on this file since 1381 was 1381, checked in by sacerdot, 9 years ago

Old commented out code removed.

File size: 4.5 KB
Line 
1include "joint/SemanticUtils.ma".
2include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
3include alias "common/Identifiers.ma".
4include alias "ASM/Util.ma".
5
6record 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
14definition 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.
23definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
24
25definition 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? *)
31axiom EmptyStack: String.
32axiom OutOfBounds: String.
33
34(*CSC: XXXXX, for is_final only *)
35axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
36(*  let ret_vals ≝ map … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs in
37*)
38
39(*CSC: we could use a dependent type here: the list of return values should have
40  the same length of the list of return registers that store the values. This
41  saves the OutOfBounds exception *)
42definition rtl_pop_frame:
43 state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
44 λst.
45  do ret_vals ← rtl_fetch_result … st ;
46  let frms ≝ st_frms ? st in
47  match frms with
48  [ nil ⇒ Error ? [MSG EmptyStack]
49  | cons hd tl ⇒
50     do st ←
51      mfold_left_i ??
52       (λi.λst.λreg.
53         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
54         greg_store rtl_sem_params reg v st)
55       (OK … st) (fr_ret_regs hd) ;
56     OK …
57      〈set_frms rtl_sem_params tl
58        (set_regs rtl_sem_params (fr_regs hd)
59         (set_sp … (fr_sp hd)
60          (set_carry … (fr_carry hd)
61           (set_m … (free … (m … st) (pblock (sp … st))) st)))),
62       fr_pc hd〉 ].
63
64definition rtl_save_frame:
65 address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
66 λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
67  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
68  do new_regs ←
69   mfold_left2 …
70    (λlenv,dest,src.
71      do v ← greg_retrieve … st src ;
72      OK … (add … lenv dest v))
73    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
74  OK …
75   (set_frms rtl_sem_params
76    (mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st))
77     (set_regs rtl_sem_params new_regs
78      (set_m … mem
79       (set_sp … (mk_pointer XData b ? (mk_offset 0)) st)))).
80cases daemon (*CSC: XXXX easy lemma on alloc to be turned into a dependent type*)
81qed.
82
83definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
84 mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
85  rtl_init_locals rtl_pop_frame rtl_save_frame.
86
87(*CSC: XXXX, for external functions only*)
88axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
89axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
90
91definition rtl_exec_extended:
92 ∀globals. genv globals (rtl_params globals) →
93  rtl_statement_extension → label → state rtl_sem_params →
94   IO io_out io_in (trace × (state rtl_sem_params)) ≝
95 λglobals,ge,stm,l,st.
96  match stm with
97   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
98      let sp ≝ sp ? st in
99      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
100      ! st ← greg_store rtl_sem_params dreg1 dpl st ;
101      ! st ← greg_store rtl_sem_params dreg2 dph st ;
102       ret ? 〈E0, goto … l st〉
103   | rtl_st_ext_call_ptr _ _ _ _ ⇒ ?
104   | rtl_st_ext_tailcall_id id regs ⇒ ?
105   | rtl_st_ext_tailcall_ptr _ _ _ ⇒ ?
106   ].
107[1,2,3: cases not_implemented ] (*CSC: tailcalls and pointer calls not implemented ATM *)
108qed.
109
110definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
111 λglobals.
112  mk_more_sem_params2 … rtl_more_sem_params1
113   (graph_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
114    (rtl_exec_extended …).
115
116definition rtl_fullexec ≝
117 joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
Note: See TracBrowser for help on using the repository browser.