source: src/RTL/semantics_paolo.ma @ 1641

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