source: src/RTL/semantics.ma @ 2176

Last change on this file since 2176 was 2176, checked in by campbell, 7 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 7.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) (λ_.empty_map …) [] [](*dummy*)
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).
22definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
23
24definition rtl_init_locals :
25 list register → register_env beval → register_env beval ≝
26 λlocals,env.
27  foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
28
29(*CSC: could we use here a dependent type to avoid the Error case? *)
30axiom EmptyStack: String.
31axiom OutOfBounds: String.
32
33definition rtl_fetch_ra:
34 state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
35 λst.
36  match st_frms ? st with
37  [ nil ⇒ Error ? [MSG EmptyStack]
38  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
39
40definition rtl_result_regs:
41 ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝
42 λglobals,ge,st.
43  do fn ← graph_fetch_function … globals ge st ;
44  OK … (joint_if_result … fn).
45
46(*CSC: we could use a dependent type here: the list of return values should have
47  the same length of the list of return registers that store the values. This
48  saves the OutOfBounds exception *)
49definition rtl_pop_frame:
50 ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
51 λglobals,ge,st.
52  do ret_regs ← rtl_result_regs … ge st ;
53  do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ;
54  match st_frms ? st with
55  [ nil ⇒ Error ? [MSG EmptyStack]
56  | cons hd tl ⇒
57     do st ←
58      mfold_left_i ??
59       (λi.λst.λreg.
60         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
61         greg_store rtl_sem_params reg v st)
62       (OK … st) (fr_ret_regs hd) ;
63     OK …
64      (set_frms rtl_sem_params tl
65        (set_regs rtl_sem_params (fr_regs hd)
66         (set_sp … (fr_sp hd)
67          (set_carry … (fr_carry hd)
68           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
69
70definition rtl_call_function:
71 nat → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
72  λstacksize,formal_arg_regs,actual_arg_regs,st.
73  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
74  do new_regs ←
75   mfold_left2 …
76    (λlenv,dest,src.
77      do v ← greg_retrieve … st src ;
78      OK … (add … lenv dest v))
79    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
80  OK …
81   (set_regs rtl_sem_params new_regs
82    (set_m … mem
83     (set_sp … (mk_pointer b (mk_offset 0)) st))).
84(*cases b * #r #off #E >E %
85qed.*)
86
87definition rtl_save_frame:
88 address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
89 λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
90  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st) in
91  let st ≝ set_frms rtl_sem_params frame st in
92  rtl_call_function stacksize formal_arg_regs actual_arg_regs st.
93
94(*CSC: XXXX, for external functions only*)
95axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
96axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
97
98definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
99 λglobals.
100  mk_more_sem_params1 … rtl_more_sem_params graph_succ_p (graph_pointer_of_label …)
101   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
102   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
103   rtl_fetch_external_args rtl_set_result.
104definition rtl_sem_params1: ∀globals. sem_params1 … globals ≝
105 λglobals. mk_sem_params1 … (rtl_more_sem_params1 globals).
106
107definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
108 λr1,r2,st.
109 do v1 ← greg_retrieve rtl_sem_params st r1 ;
110 do v2 ← greg_retrieve rtl_sem_params st r2 ;
111 do ptr ← pointer_of_address 〈v1,v2〉 ;
112 OK … (pblock ptr). 
113
114(* This code is quite similar to eval_call_block: can we factorize it out? *)
115definition eval_tail_call_block:
116 ∀globals.genv … (rtl_params globals) → state rtl_sem_params →
117  block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
118 λglobals,ge,st,b,args.
119  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr … ge b);
120    match fd with
121    [ Internal fn ⇒
122      let st ≝ set_m … (free … (m … st) (pblock (sp … st))) st in
123      ! st ← rtl_call_function (joint_if_stacksize … fn) (joint_if_params … fn) args st ;
124      let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
125      let l' ≝ joint_if_entry … fn in
126      ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
127       return 〈 E0, st〉
128    | External fn ⇒ ?(*
129      ! params ← fetch_external_args … fn st;
130      ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
131      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
132      (* CSC: XXX bug here; I think I should split it into Byte-long
133         components; instead I am making a singleton out of it. To be
134         fixed once we fully implement external functions. *)
135        let vs ≝ [mk_val ? evres] in
136      ! st ← set_result … vs st;
137      let st ≝ set_pc … ra st in
138        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 *)
139     ].
140cases daemon (*CSC: XXX tailcall to external function not implemented yet;
141                    it needs alls other functions on external calls *)
142qed.
143
144definition rtl_exec_extended:
145 ∀globals. genv globals (rtl_params globals) →
146  rtl_statement_extension → label → state rtl_sem_params →
147   IO io_out io_in (trace × (state rtl_sem_params)) ≝
148 λglobals,ge,stm,l,st.
149  match stm with
150   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
151      let sp ≝ sp ? st in
152      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
153      ! st ← greg_store rtl_sem_params dreg1 dpl st ;
154      ! st ← greg_store rtl_sem_params dreg2 dph st ;
155      ! st ← next … (rtl_sem_params1 globals) l st ;
156       return 〈E0, st〉
157   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
158      ! b ← block_of_register_pair r1 r2 st : IO ??? ;
159      ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) : IO ??? ;
160      eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
161       ge st b args dest ra
162   | rtl_st_ext_tailcall_id id args ⇒
163      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
164      eval_tail_call_block … ge st b args
165   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
166      ! b ← block_of_register_pair r1 r2 st : IO ???;
167      eval_tail_call_block … ge st b args
168   ].
169
170definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
171 λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
172
173definition rtl_fullexec ≝
174 joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
Note: See TracBrowser for help on using the repository browser.