source: src/ERTL/semantics.ma @ 1156

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

ERTL semantics completed up to initialization and memory model.

File size: 15.4 KB
Line 
1
2(* XXX NB: I haven't checked all of these semantics against the prototype
3           compilers yet! *)
4
5include "utilities/lists.ma".
6
7include "common/Errors.ma".
8include "common/Globalenvs.ma".
9include "common/IO.ma".
10include "common/SmallstepExec.ma".
11
12include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
13
14(* CSC: external functions never fail (??) and always return something of the
15   size of one register, both in the frontend and in the backend.
16   Is this reasonable??? In OCaml it always return a list, but in the frontend
17   only the head is kept (or Undef if the list is empty) ??? *)
18
19(* CSC: carries are values and booleans are not values; so we use integers.
20   But why using values at all? To have undef? *)
21(* CSC: ???????????? *)
22axiom smerge: val → val → res val.
23(* CSC: ???????????? In OCaml: IntValue.Int32.merge
24   Note also that the translation can fail; so it should be a res int! *)
25axiom smerge2: list val → int.
26(* CSC: I have a byte, I need a value, but it is complex to do so *)
27axiom val_of_Byte: Byte → val.
28axiom Byte_of_val: val → res Byte.
29axiom val_of_nat: nat → val.
30(* Map from the front-end memory model to the back-end memory model *)
31axiom represent_block: block → val × val.
32(* CSC: fixed size chunk *)
33axiom chunk: memory_chunk.
34axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
35
36axiom address: Type[0].
37axiom val_of_address: address → val. (* CSC: only to shift the sp *)
38axiom address_of_val: val → address. (* CSC: only to shift the sp *)
39axiom addr_sub: address → nat → address.
40axiom addr_add: address → nat → address.
41(* CSC: ??? *)
42axiom address_of_label: mem → label → address.
43axiom address_chunks_of_label: mem → label → Byte × Byte.
44axiom label_of_address_chunks: Byte → Byte → label.
45axiom address_of_address_chunks: Byte → Byte → address.
46axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
47axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
48axiom hwreg_retrieve : mRegisterMap → Register → res val.
49axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
50
51definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).
52
53(* CSC: frame reduced to this *)
54definition frame: Type[0] ≝ register_env val.
55
56(* CSC: exit not put in the state, like in OCaml. It is constant througout
57   execution *)
58record state : Type[0] ≝
59 { st_frms: list frame
60 ; pc: address
61 ; sp: address
62 ; locals: register_env val
63 ; carry: val
64 ; regs: mRegisterMap
65 ; m: mem
66 }.
67
68definition set_m: mem → state → state ≝
69 λm,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) m.
70
71definition set_locals: register_env val → state → state ≝
72 λlocals,st. mk_state (st_frms st) (pc st) (sp st) locals (carry st) (regs st) (m st).
73
74definition set_regs: mRegisterMap → state → state ≝
75 λregs,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) regs (m st).
76
77definition set_sp: address → state → state ≝
78 λsp,st. mk_state (st_frms st) (pc st) sp (locals st) (carry st) (regs st) (m st).
79
80definition set_carry: val → state → state ≝
81 λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
82
83definition set_pc: address → state → state ≝
84 λpc,st. mk_state (st_frms st) pc (sp st) (locals st) (carry st) (regs st) (m st).
85
86(* CSC: was build_state in RTL *)
87definition goto: label → state → state ≝
88 λl,st. set_pc (address_of_label (m st) l) st.
89
90(* pushes the locals (i.e. the current frame) on top of the frames list *)
91definition save_frame: state → state ≝
92 λst. mk_state (locals st::st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) (m st).
93
94axiom FailedPopFrame: String.
95
96(* removes the top frame from the frames list *)
97definition pop_frame: state → res state ≝
98 λst.
99  match st_frms st with
100   [ nil ⇒ Error ? (msg FailedPopFrame)
101   | cons _ frms ⇒
102      OK ? (mk_state frms (pc st) (sp st) (locals st) (carry st) (regs st) (m st)) ].
103
104axiom FailedStore: String.
105
106definition push: state → Byte → res state ≝
107 λst,v.
108  let sp ≝ val_of_address (sp st) in
109  (*CSC: no monadic notation here *)
110  bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m st) sp (val_of_Byte v)))
111   (λm.
112    let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
113    OK ? (set_m m (set_sp sp st))).
114
115
116definition pop: state → res (state × Byte) ≝
117 λst:state.
118  let sp ≝ val_of_address (sp st) in
119  let sp ≝ sub sp (val_of_memory_chunk chunk) in
120  let st ≝ set_sp (address_of_val sp) st in
121  (*CSC: no monadic notation here *)
122  bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m st) sp))
123   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
124
125definition save_ra : state → label → res state ≝
126 λst,l.
127  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
128  (* No monadic notation here *)
129  bind ?? (push st addrl) (λst.push st addrh).
130
131definition fetch_ra : state → res (state × label) ≝
132 λst.
133  (* No monadic notation here *)
134  bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
135  bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
136   OK ? 〈st, label_of_address_chunks addrl addrh〉)).
137
138(*CSC: To be implemented *)
139axiom fetch_function: state → res ertl_internal_function.
140axiom fetch_statement: state → res ertl_statement.
141
142definition init_locals : list register → register_env val ≝
143foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
144
145definition reg_store ≝
146λreg,v,locals. update RegisterTag val locals reg v.
147
148axiom BadRegister : String.
149
150definition reg_retrieve : register_env val → register → res val ≝
151λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
152
153axiom MissingSymbol : String.
154axiom FailedLoad : String.
155axiom BadFunction : String.
156
157(*CSC: to be implemented *)
158axiom fetch_external_args: external_function → state → res (list val).(* ≝
159 λfn,st.
160  let registerno ≝ ? fn in
161  ! vs ←
162   mmap …
163    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
164  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
165  ?.*)
166
167(*CSC: to be implemented; fails if the first list is longer *)
168axiom fold_left2_first_not_longer:
169 ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
170  ∀acc:C. ∀l1:list A. ∀l2: list B.
171   res C.
172
173(* CSC: the list should be a vector or have an upper bounded length *)
174definition set_result: list val → state → res state ≝
175 λvs,st.
176  (* CSC: monadic notation not used *)
177  bind ?? (
178   fold_left2_first_not_longer …
179    (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
180  (λregs.OK ? (set_regs regs st)).
181
182definition fetch_result: state → nat → res (list val) ≝
183 λst,registersno.
184  let retregs ≝ prefix … registersno RegisterRets in
185  mmap … (λr. hwreg_retrieve (regs st) r) retregs.
186
187definition framesize: state → res nat ≝
188 λst.
189  (* CSC: monadic notation missing here *)
190  bind ?? (fetch_function st) (λf.
191  OK ? (ertl_if_stacksize f)).
192
193definition get_hwsp : state → res address ≝
194 λst.
195  (* CSC: monadic notation missing here *)
196  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
197  (* CSC: monadic notation missing here *)
198  bind ?? (Byte_of_val spl) (λspl.
199  (* CSC: monadic notation missing here *)
200  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
201  (* CSC: monadic notation missing here *)
202  bind ?? (Byte_of_val sph) (λsph.
203  OK ? (address_of_address_chunks spl sph))))).
204
205definition set_hwsp : address → state → res state ≝
206 λsp,st.
207  let 〈spl,sph〉 ≝ address_chunks_of_address sp in
208  (* CSC: monadic notation missing here *) 
209  bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
210  (* CSC: monadic notation missing here *) 
211  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
212  OK ? (set_regs regs st))).
213
214definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
215λge,st.
216  ! s ← fetch_statement st;
217  match s with
218  [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉
219  | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉
220  | ertl_st_int dest v l ⇒
221     ! locals ← reg_store dest (val_of_Byte v) (locals st);
222     ret ? 〈E0, goto l (set_locals locals st)〉
223  | ertl_st_load addrl addrh dst l ⇒
224      ! vaddrh ← reg_retrieve (locals st) addrh;
225      ! vaddrl ← reg_retrieve (locals st) addrl;
226      ! vaddr ← smerge vaddrl vaddrh;
227      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
228      ! locals ← reg_store dst v (locals st);
229      ret ? 〈E0, goto l (set_locals locals st)〉
230  | ertl_st_store addrl addrh src l ⇒
231      ! vaddrh ← reg_retrieve (locals st) addrh;
232      ! vaddrl ← reg_retrieve (locals st) addrl;
233      ! vaddr ← smerge vaddrl vaddrh;
234      ! v ← reg_retrieve (locals st) src;
235      ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
236      ret ? 〈E0, goto l (set_m m' st)〉
237  | ertl_st_cond src ltrue lfalse ⇒
238      ! v ← reg_retrieve (locals st) src;
239      ! b ← eval_bool_of_val v;
240      ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
241  | ertl_st_addr ldest hdest id l ⇒
242     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
243     let 〈laddr,haddr〉 ≝ represent_block addr in
244     ! locals ← reg_store ldest laddr (locals st);
245     ! locals ← reg_store hdest haddr locals;
246     ret ? 〈E0, goto l (set_locals locals st)〉
247  | ertl_st_op1 op dst src l ⇒
248     ! v ← reg_retrieve (locals st) src;
249     ! v ← Byte_of_val v;
250     let v' ≝ val_of_Byte (op1 eval op v) in
251     ! locals ← reg_store dst v' (locals st);
252     ret ? 〈E0, goto l (set_locals locals st)〉
253  | ertl_st_op2 op dst src1 src2 l ⇒
254     ! v1 ← reg_retrieve (locals st) src1;
255     ! v1 ← Byte_of_val v1;
256     ! v2 ← reg_retrieve (locals st) src2;
257     ! v2 ← Byte_of_val v2;
258     ! carry ← eval_bool_of_val (carry st);
259     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
260     let v' ≝ val_of_Byte v' in
261     let carry ≝ of_bool carry in
262     ! locals ← reg_store dst v' (locals st);
263     ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
264  | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
265     ! v1 ← reg_retrieve (locals st) sacc;
266     ! v1 ← Byte_of_val v1;
267     ! v2 ← reg_retrieve (locals st) sbacc;
268     ! v2 ← Byte_of_val v2;
269     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
270     let v1' ≝ val_of_Byte v1' in
271     let v2' ≝ val_of_Byte v2' in
272     ! locals ← reg_store dacc v1' (locals st);
273     ! locals ← reg_store dbacc v2' locals;
274     ret ? 〈E0, goto l (set_locals locals st)〉
275  | ertl_st_clear_carry l ⇒
276    ret ? 〈E0, goto l (set_carry Vfalse st)〉
277  | ertl_st_set_carry l ⇒
278    ret ? 〈E0, goto l (set_carry Vtrue st)〉
279     
280  (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
281         ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
282         be more than enough... *)
283  | ertl_st_move dst src l ⇒
284     ! v ← reg_retrieve (locals st) src;
285     ! locals ← reg_store dst v (locals st);
286     ret ? 〈E0, goto l (set_locals locals st)〉
287  | ertl_st_hdw_to_hdw dst src l ⇒
288     ! v ← hwreg_retrieve (regs st) src;
289     ! regs ← hwreg_store dst v (regs st);
290     ret ? 〈E0, goto l (set_regs regs st)〉
291  | ertl_st_get_hdw dst src l ⇒
292     ! v ← hwreg_retrieve (regs st) src;
293     ! locals ← reg_store dst v (locals st);
294     ret ? 〈E0, goto l (set_locals locals st)〉
295  | ertl_st_set_hdw dst src l ⇒
296     ! v ← reg_retrieve (locals st) src;
297     ! regs ← hwreg_store dst v (regs st);
298     ret ? 〈E0, goto l (set_regs regs st)〉
299
300  (* CSC: Dropped:
301      - rtl_st_stackaddr (becomes two get_hdw)
302      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
303      - rtl_st_call_ptr (unimplemented ATM) *)
304     
305  (* CSC: changed, where the meat is *)
306  | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *)
307      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
308      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
309      match fd with
310      [ Internal fn ⇒
311        ! st ← save_ra st l;
312        let st ≝ save_frame st in
313        let locals ≝ init_locals (ertl_if_locals fn) in
314        let l' ≝ ertl_if_entry fn in
315         ret ? 〈 E0, goto l' (set_locals locals st)〉
316      | External fn ⇒
317        ! params ← fetch_external_args fn st;
318        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
319        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
320        (* CSC: XXX bug here; I think I should split it into Byte-long
321           components; instead I am making a singleton out of it *)
322        let vs ≝ [mk_val ? evres] in
323        ! st ← set_result vs st;
324        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
325      ]
326  | ertl_st_return ⇒
327      ! st ← pop_frame st;
328      ! 〈st,pch〉 ← pop st;
329      ! 〈st,pcl〉 ← pop st;
330      let pc ≝ address_of_address_chunks pcl pch in
331      ret ? 〈E0,set_pc pc st〉
332 
333  (* CSC: new stuff *)
334  | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
335  | ertl_st_new_frame l ⇒
336     ! v ← framesize st;
337     ! sp ← get_hwsp st;
338     let newsp ≝ addr_sub sp v in
339     ! st ← set_hwsp newsp st;
340     ret ? 〈E0,goto l st〉
341  | ertl_st_del_frame l ⇒
342     ! v ← framesize st;
343     ! sp ← get_hwsp st;
344     let newsp ≝ addr_add sp v in
345     ! st ← set_hwsp newsp st;
346     ret ? 〈E0,goto l st〉
347  | ertl_st_frame_size dst l ⇒
348     ! v ← framesize st;
349     ! locals ← reg_store dst (val_of_nat v) (locals st);
350     ret ? 〈E0, goto l (set_locals locals st)〉
351  | ertl_st_pop dst l ⇒
352     ! 〈st,v〉 ← pop st;
353     ! locals ← reg_store dst (val_of_Byte v) (locals st);
354     ret ? 〈E0, goto l (set_locals locals st)〉
355  | ertl_st_push src l ⇒
356     ! v ← reg_retrieve (locals st) src;
357     ! v ← Byte_of_val v;
358     ! st ← push st v;
359     ret ? 〈E0, goto l st〉
360  ].
361
362axiom WrongReturnValueType: String.
363
364definition is_final : label → nat → state → option ((*CSC: why not res*) int) ≝
365λexit,registersno,st.
366 (* CSC: monadic notation missing here *)
367 match fetch_statement st with
368  [ Error _ ⇒ None ?
369  | OK s ⇒
370     match s with
371      [ ertl_st_return ⇒
372       (* CSC: monadic notation missing here *)
373        match fetch_ra st with
374         [ Error _ ⇒ None ?
375         | OK st_l ⇒ let 〈st,l〉 ≝ st_l in
376            match label_eq l exit with
377             [ inl _ ⇒
378               (* CSC: monadic notation missing here *)
379                match fetch_result st registersno with
380                 [ Error _ ⇒ None ?
381                 | OK vals ⇒ Some ? (smerge2 vals) ]
382             | inr _ ⇒ None ? ]]
383      | _ ⇒ None … ]].
384
385definition ERTL_exec : label → nat → execstep io_out io_in ≝
386 λexit,registersno.
387  mk_execstep … ? (is_final exit registersno) m eval_statement.
388
389(* CSC: XXX the program type does not fit with the globalenv and init_mem
390definition make_initial_state : rtl_program → res (genv × state) ≝
391λp.
392  do ge ← globalenv Genv ?? p;
393  do m ← init_mem Genv ?? p;
394  let main ≝ rtl_pr_main ?? p in
395  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
396  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
397  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
398
399definition RTL_fullexec : fullexec io_out io_in ≝
400  mk_fullexec … RTL_exec ? make_initial_state.
401*)
Note: See TracBrowser for help on using the repository browser.