source: src/RTL/RTL_semantics.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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