source: src/RTL/RTL_semantics.ma @ 2645

Last change on this file since 2645 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 7.4 KB
Line 
1include "joint/semanticsUtils.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: cpointer
9 ; fr_sp: xpointer
10 ; fr_carry: bebit
11 ; fr_regs: register_env beval
12 }.
13
14definition RTL_state : 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 : psd_argument.
22  match a with
23  [ Reg r ⇒ reg_retrieve env r
24  | Imm b ⇒ return b
25  ].
26
27(*CSC: could we use here a dependent type to avoid the Error case? *)
28
29definition rtl_fetch_ra:
30 RTL_state → res (RTL_state × cpointer) ≝
31 λst.
32  match st_frms ? st with
33  [ nil ⇒ Error ? [MSG EmptyStack]
34  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
35
36definition rtl_init_local :
37 register → register_env beval → register_env beval ≝
38 λlocal,env.add … env local BVundef.
39
40definition rtl_setup_call:
41 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
42  λstacksize,formal_arg_regs,actual_arg_regs,st.
43  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
44  do new_regs ←
45   mfold_left2 …
46    (λlenv,dest,src.
47      do v ← rtl_arg_retrieve … (regs ? st) src ;
48      OK … (add … lenv dest v))
49    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
50  OK …
51   (set_regs RTL_state new_regs
52    (set_m … mem
53     (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
54cases b * #r #off #E >E %
55qed.
56
57definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state.
58  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
59  OK … (set_frms RTL_state frame st).
60
61(*CSC: XXXX, for external functions only*)
62axiom rtl_fetch_external_args: external_function → RTL_state → res (list val).
63axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
64
65definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
66definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).
67
68definition rtl_read_result :
69 ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝
70 λglobals,ge,rets,st.
71 m_list_map … (rtl_reg_retrieve st) rets.
72
73(*CSC: we could use a dependent type here: the list of return values should have
74  the same length of the list of return registers that store the values. This
75  saves the OutOfBounds exception *)
76definition rtl_pop_frame:
77 ∀globals. genv RTL globals → joint_internal_function RTL globals → RTL_state →
78  res RTL_state ≝
79 λglobals,ge,curr_fn,st.
80  let ret ≝ joint_if_result … curr_fn in
81  do ret_vals ← rtl_read_result … ge ret st ;
82  match st_frms ? st with
83  [ nil ⇒ Error ? [MSG EmptyStack]
84  | cons hd tl ⇒
85     do st ←
86      mfold_left_i …
87       (λi.λst.λreg.
88         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
89         rtl_reg_store reg v st)
90       (OK … st) (fr_ret_regs hd) ;
91     OK …
92      (set_frms RTL_state tl
93        (set_regs RTL_state (fr_regs hd)
94         (set_sp … (fr_sp hd)
95          (set_carry … (fr_carry hd)
96           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
97
98(* This code is quite similar to eval_call_block: can we factorize it out? *)
99definition eval_tailcall_block:
100 ∀globals.genv RTL globals → RTL_state →
101  block → call_args RTL →
102  (* this is where the result of the current function should be stored *)
103  call_dest RTL →
104  IO io_out io_in
105    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝
106 λglobals,ge,st,b,args,ret.
107  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
108    match fd with
109    [ Internal fd ⇒
110      return 〈FTailInit ?? (block_id b) fd args, st〉
111    | External fn ⇒
112      ! params ← rtl_fetch_external_args … fn st : IO ???;
113      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
114      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
115      (* CSC: XXX bug here; I think I should split it into Byte-long
116         components; instead I am making a singleton out of it. To be
117         fixed once we fully implement external functions. *)
118      let vs ≝ [mk_val ? evres] in
119      ! st ← rtl_set_result … vs ret st : IO ???;
120      return 〈FEnd2 ??, st〉
121    ].
122
123definition block_of_register_pair: register → register → RTL_state → res block ≝
124 λr1,r2,st.
125 do v1 ← rtl_reg_retrieve st r1 ;
126 do v2 ← rtl_reg_retrieve st r2 ;
127 do ptr ← pointer_of_address 〈v1,v2〉 ;
128 OK … (pblock ptr). 
129
130definition eval_rtl_seq:
131 ∀globals. genv RTL globals →
132  rtl_seq → joint_internal_function RTL globals → RTL_state →
133   IO io_out io_in RTL_state ≝
134 λglobals,ge,stm,curr_fn,st.
135  match stm with
136   [ rtl_stack_address dreg1 dreg2  ⇒
137      let sp ≝ sp ? st in
138      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
139      ! st ← rtl_reg_store dreg1 dpl st ;
140      rtl_reg_store dreg2 dph st
141   ].
142
143definition eval_rtl_call:
144 ∀globals. genv RTL globals →
145  rtl_call → RTL_state →
146   IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝
147 λglobals,ge,stm,st.
148  match stm with
149  [ rtl_call_ptr r1 r2 args dest ⇒
150    ! b ← block_of_register_pair r1 r2 st : IO ???;
151    ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
152    match fd with
153    [ Internal fd ⇒
154      return 〈Init ?? (block_id b) fd args dest, st〉
155    | External fn ⇒
156      ! params ← rtl_fetch_external_args … fn st : IO ???;
157      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
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 ← rtl_set_result … vs dest st : IO ???;
164      return 〈Proceed ???, st〉
165    ]
166  ].
167
168definition eval_rtl_tailcall:
169 ∀globals. genv RTL globals →
170  rtl_tailcall → joint_internal_function RTL globals → RTL_state →
171   IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝
172   λglobals,ge,stm,curr_fn,st.
173   let ret ≝ joint_if_result … curr_fn in
174   match stm with
175   [ rtl_tailcall_id id args ⇒
176      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
177      eval_tailcall_block … ge st b args ret
178   | rtl_tailcall_ptr r1 r2 args ⇒
179      ! b ← block_of_register_pair r1 r2 st : IO ???;
180      eval_tailcall_block … ge st b args ret
181   ].
182
183definition RTL_semantics ≝
184  make_sem_graph_params RTL
185    (mk_more_sem_unserialized_params ??
186      RTL_state
187      reg_store reg_retrieve rtl_arg_retrieve
188      reg_store reg_retrieve rtl_arg_retrieve
189      reg_store reg_retrieve rtl_arg_retrieve
190      reg_store reg_retrieve rtl_arg_retrieve
191      rtl_arg_retrieve
192      (λenv,p. let 〈dest,src〉 ≝ p in
193        ! v ← rtl_arg_retrieve env src ;
194        reg_store dest v env)
195      rtl_fetch_ra
196      rtl_init_local
197      rtl_save_frame
198      rtl_setup_call
199      rtl_fetch_external_args
200      rtl_set_result
201      [ ] [ ]
202      rtl_read_result
203      eval_rtl_seq
204      eval_rtl_tailcall
205      eval_rtl_call
206      rtl_pop_frame
207      (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)).
Note: See TracBrowser for help on using the repository browser.