source: src/ERTL/semantics.ma @ 1313

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

(E)RTL semantics ported to new data type for save/pop frame (but not implemented
yet)

File size: 18.6 KB
Line 
1include "joint/SemanticUtils.ma".
2include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
3
4definition ps_reg_store ≝
5 λr,v.λlocal_env:(register_env beval) × hw_register_env.
6  do res ← reg_store r v (\fst local_env) ;
7  OK … 〈res, \snd local_env〉.
8
9definition ps_reg_retrieve ≝
10 λlocal_env:(register_env beval) × hw_register_env. reg_retrieve … (\fst local_env).
11
12definition hw_reg_store ≝
13 λr,v.λlocal_env:(register_env beval) × hw_register_env.
14  do res ← hwreg_store r v (\snd local_env) ;
15  OK … 〈\fst local_env,res〉.
16
17definition hw_reg_retrieve ≝
18 λlocal_env:(register_env beval) × hw_register_env. hwreg_retrieve … (\snd local_env).
19
20definition ertl_more_sem_params: more_sem_params ertl_params_ :=
21 mk_more_sem_params ertl_params_
22  (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p
23   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
24    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
25     (λlocals,dest_src.
26       do v ←
27        match \snd dest_src with
28        [ pseudo reg ⇒ ps_reg_retrieve locals reg
29        | hardware reg ⇒ hw_reg_retrieve locals reg] ;
30       match \fst dest_src with
31       [ pseudo reg ⇒ ps_reg_store reg v locals
32       | hardware reg ⇒ hw_reg_store reg v locals])
33     pointer_of_label.
34definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
35
36(*CSC: XXXXX *)
37axiom ertl_init_locals : list register → (register_env beval) × hw_register_env → (register_env beval) × hw_register_env.
38axiom ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params).
39axiom ertl_save_frame: state … ertl_sem_params → state … ertl_sem_params.
40
41definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
42 mk_more_sem_params1 ? ertl_params1 ertl_more_sem_params
43  ertl_init_locals ertl_pop_frame ertl_save_frame.
44
45(*CSC: XXXXX, for is_final only *)
46axiom ertl_fetch_result: state ertl_sem_params → nat → res val.
47
48(*CSC: XXXX, for external functions only*)
49axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val).
50axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
51
52axiom ertl_exec_extended: ∀globals. genv globals (ertl_params globals) → ertl_statement_extension → state ertl_sem_params → IO io_out io_in (trace × (state ertl_sem_params)).
53
54definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
55 λglobals.
56  mk_more_sem_params2 … ertl_more_sem_params1
57   (graph_fetch_statement …) ertl_fetch_result ertl_fetch_external_args ertl_set_result
58    (ertl_exec_extended …).
59
60definition ertl_fullexec ≝
61 joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).
62
63(*
64(* CSC: external functions never fail (??) and always return something of the
65   size of one register, both in the frontend and in the backend.
66   Is this reasonable??? In OCaml it always return a list, but in the frontend
67   only the head is kept (or Undef if the list is empty) ??? *)
68
69(* CSC: carries are values and booleans are not values; so we use integers.
70   But why using values at all? To have undef? *)
71(* CSC: ???????????? *)
72axiom smerge: val → val → res val.
73(* CSC: ???????????? In OCaml: IntValue.Int32.merge
74   Note also that the translation can fail; so it should be a res int! *)
75axiom smerge2: list val → int.
76(* CSC: I have a byte, I need a value, but it is complex to do so *)
77axiom val_of_Byte: Byte → val.
78axiom Byte_of_val: val → res Byte.
79axiom val_of_nat: nat → val.
80(* Map from the front-end memory model to the back-end memory model *)
81axiom represent_block: block → val × val.
82(* CSC: fixed size chunk *)
83axiom chunk: memory_chunk.
84axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
85
86axiom address: Type[0].
87axiom val_of_address: address → val. (* CSC: only to shift the sp *)
88axiom address_of_val: val → address. (* CSC: only to shift the sp *)
89axiom addr_sub: address → nat → address.
90axiom addr_add: address → nat → address.
91(* CSC: ??? *)
92axiom address_of_label: mem → label → address.
93axiom address_chunks_of_label: mem → label → Byte × Byte.
94axiom label_of_address_chunks: Byte → Byte → label.
95axiom address_of_address_chunks: Byte → Byte → address.
96axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
97axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
98axiom hwreg_retrieve : mRegisterMap → Register → res val.
99axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
100
101definition genv ≝ λglobals. (genv_t Genv) (fundef (joint_internal_function globals … (ertl_sem_params_ globals))).
102
103(* CSC: frame reduced to this *)
104definition frame: Type[0] ≝ register_env val.
105
106(* CSC: exit not put in the state, like in OCaml. It is constant througout
107   execution *)
108record state : Type[0] ≝
109 { st_frms: list frame
110 ; pc: address
111 ; sp: address
112 ; locals: register_env val
113 ; carry: val
114 ; regs: mRegisterMap
115 ; m: mem
116 }.
117
118definition set_m: mem → state → state ≝
119 λm,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) m.
120
121definition set_locals: register_env val → state → state ≝
122 λlocals,st. mk_state (st_frms st) (pc st) (sp st) locals (carry st) (regs st) (m st).
123
124definition set_regs: mRegisterMap → state → state ≝
125 λregs,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) regs (m st).
126
127definition set_sp: address → state → state ≝
128 λsp,st. mk_state (st_frms st) (pc st) sp (locals st) (carry st) (regs st) (m st).
129
130definition set_carry: val → state → state ≝
131 λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
132
133definition set_pc: address → state → state ≝
134 λpc,st. mk_state (st_frms st) pc (sp st) (locals st) (carry st) (regs st) (m st).
135
136(* CSC: was build_state in RTL *)
137definition goto: label → state → state ≝
138 λl,st. set_pc (address_of_label (m st) l) st.
139
140(* pushes the locals (i.e. the current frame) on top of the frames list *)
141definition save_frame: state → state ≝
142 λst. mk_state (locals st::st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) (m st).
143
144axiom FailedPopFrame: String.
145
146(* removes the top frame from the frames list *)
147definition pop_frame: state → res state ≝
148 λst.
149  match st_frms st with
150   [ nil ⇒ Error ? (msg FailedPopFrame)
151   | cons _ frms ⇒
152      OK ? (mk_state frms (pc st) (sp st) (locals st) (carry st) (regs st) (m st)) ].
153
154axiom FailedStore: String.
155
156definition push: state → Byte → res state ≝
157 λst,v.
158  let sp ≝ val_of_address (sp st) in
159  (*CSC: no monadic notation here *)
160  bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m st) sp (val_of_Byte v)))
161   (λm.
162    let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
163    OK ? (set_m m (set_sp sp st))).
164
165
166definition pop: state → res (state × Byte) ≝
167 λst:state.
168  let sp ≝ val_of_address (sp st) in
169  let sp ≝ sub sp (val_of_memory_chunk chunk) in
170  let st ≝ set_sp (address_of_val sp) st in
171  (*CSC: no monadic notation here *)
172  bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m st) sp))
173   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
174
175definition save_ra : state → label → res state ≝
176 λst,l.
177  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
178  (* No monadic notation here *)
179  bind ?? (push st addrl) (λst.push st addrh).
180
181definition fetch_ra : state → res (state × label) ≝
182 λst.
183  (* No monadic notation here *)
184  bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
185  bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
186   OK ? 〈st, label_of_address_chunks addrl addrh〉)).
187
188(*CSC: To be implemented *)
189
190axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
191axiom fetch_function: ∀globals: list ident. state → res (joint_internal_function globals … (ertl_sem_params_ globals)).
192
193definition init_locals : list register → register_env val ≝
194foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
195
196definition reg_store ≝
197λreg,v,locals. update RegisterTag val locals reg v.
198
199axiom BadRegister : String.
200
201definition reg_retrieve : register_env val → register → res val ≝
202λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
203
204axiom MissingSymbol : String.
205axiom FailedLoad : String.
206axiom BadFunction : String.
207
208(*CSC: to be implemented *)
209axiom fetch_external_args: external_function → state → res (list val).(* ≝
210 λfn,st.
211  let registerno ≝ ? fn in
212  ! vs ←
213   mmap …
214    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
215  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
216  ?.*)
217
218(*CSC: to be implemented; fails if the first list is longer *)
219axiom fold_left2_first_not_longer:
220 ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
221  ∀acc:C. ∀l1:list A. ∀l2: list B.
222   res C.
223
224(* CSC: the list should be a vector or have an upper bounded length *)
225definition set_result: list val → state → res state ≝
226 λvs,st.
227  (* CSC: monadic notation not used *)
228  bind ?? (
229   fold_left2_first_not_longer …
230    (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
231  (λregs.OK ? (set_regs regs st)).
232
233definition fetch_result: state → nat → res (list val) ≝
234 λst,registersno.
235  let retregs ≝ prefix … registersno RegisterRets in
236  mmap … (λr. hwreg_retrieve (regs st) r) retregs.
237
238definition framesize: list ident → state → res nat ≝
239  λglobals: list ident.
240  λst.
241  (* CSC: monadic notation missing here *)
242    bind ?? (fetch_function globals st) (λf.
243    OK ? (joint_if_stacksize globals … f)).
244
245definition get_hwsp : state → res address ≝
246 λst.
247  (* CSC: monadic notation missing here *)
248  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
249  (* CSC: monadic notation missing here *)
250  bind ?? (Byte_of_val spl) (λspl.
251  (* CSC: monadic notation missing here *)
252  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
253  (* CSC: monadic notation missing here *)
254  bind ?? (Byte_of_val sph) (λsph.
255  OK ? (address_of_address_chunks spl sph))))).
256
257definition set_hwsp : address → state → res state ≝
258 λsp,st.
259  let 〈spl,sph〉 ≝ address_chunks_of_address sp in
260  (* CSC: monadic notation missing here *) 
261  bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
262  (* CSC: monadic notation missing here *) 
263  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
264  OK ? (set_regs regs st))).
265
266definition retrieve: state → move_registers → res val ≝
267  λst.
268  λr.
269  match r with
270  [ pseudo   src ⇒ reg_retrieve (locals st) src
271  | hardware src ⇒ hwreg_retrieve (regs st) src
272  ].
273
274definition store ≝
275  λst.
276  λv.
277  λr.
278  match r with
279  [ pseudo   dst ⇒
280    ! locals ← reg_store dst v (locals st);
281      ret ? (set_locals locals st)
282  | hardware dst ⇒
283    ! regs ← hwreg_store dst v (regs st);
284      ret ? (set_regs regs st)
285  ].
286
287definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
288  λglobals. λge,st.
289  ! s ← fetch_statement globals st;
290  match s with
291  [ ertl_st_lift_pre pre ⇒
292    match pre with
293    [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
294    | joint_st_sequential seq l ⇒
295      match seq with
296      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
297      | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
298      | joint_instr_int dest v ⇒
299        ! locals ← reg_store dest (val_of_Byte v) (locals st);
300          ret ? 〈E0, goto l (set_locals locals st)〉
301      | joint_instr_load addrl addrh dst ⇒
302        ! vaddrh ← reg_retrieve (locals st) addrh;
303        ! vaddrl ← reg_retrieve (locals st) addrl;
304        ! vaddr ← smerge vaddrl vaddrh;
305        ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
306        ! locals ← reg_store dst v (locals st);
307          ret ? 〈E0, goto l (set_locals locals st)〉
308      | joint_instr_store addrl addrh src ⇒
309        ! vaddrh ← reg_retrieve (locals st) addrh;
310        ! vaddrl ← reg_retrieve (locals st) addrl;
311        ! vaddr ← smerge vaddrl vaddrh;
312        ! v ← reg_retrieve (locals st) src;
313        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
314          ret ? 〈E0, goto l (set_m m' st)〉
315      | joint_instr_cond src ltrue ⇒
316        ! v ← reg_retrieve (locals st) src;
317        ! b ← eval_bool_of_val v;
318          ret ? 〈E0, goto (if b then ltrue else l) st〉
319      | joint_instr_address ident prf ldest hdest ⇒
320        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
321          let 〈laddr,haddr〉 ≝ represent_block addr in
322        ! locals ← reg_store ldest laddr (locals st);
323        ! locals ← reg_store hdest haddr locals;
324          ret ? 〈E0, goto l (set_locals locals st)〉
325      | joint_instr_op1 op acc_a ⇒
326        ! v ← reg_retrieve (locals st) acc_a;
327        ! v ← Byte_of_val v;
328          let v' ≝ val_of_Byte (op1 eval op v) in
329        ! locals ← reg_store acc_a v' (locals st);
330          ret ? 〈E0, goto l (set_locals locals st)〉
331      | joint_instr_op2 op acc_a_reg dest ⇒
332        ! v1 ← reg_retrieve (locals st) acc_a_reg;
333        ! v1 ← Byte_of_val v1;
334        ! v2 ← reg_retrieve (locals st) acc_a_reg;
335        ! v2 ← Byte_of_val v2;
336        ! carry ← eval_bool_of_val (carry st);
337          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
338          let v' ≝ val_of_Byte v' in
339          let carry ≝ of_bool carry in
340        ! locals ← reg_store dest v' (locals st);
341          ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
342      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
343      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
344      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
345        ! v1 ← reg_retrieve (locals st) acc_a_reg;
346        ! v1 ← Byte_of_val v1;
347        ! v2 ← reg_retrieve (locals st) acc_b_reg;
348        ! v2 ← Byte_of_val v2;
349          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
350          let v1' ≝ val_of_Byte v1' in
351          let v2' ≝ val_of_Byte v2' in
352        ! locals ← reg_store acc_a_reg v1' (locals st);
353        ! locals ← reg_store acc_b_reg v2' locals;
354          ret ? 〈E0, goto l (set_locals locals st)〉
355      | joint_instr_pop dst ⇒
356        ! 〈st,v〉 ← pop st;
357        ! locals ← reg_store dst (val_of_Byte v) (locals st);
358          ret ? 〈E0, goto l (set_locals locals st)〉
359      | joint_instr_push src ⇒
360        ! v ← reg_retrieve (locals st) src;
361        ! v ← Byte_of_val v;
362        ! st ← push st v;
363          ret ? 〈E0, goto l st〉
364      | joint_instr_move dst_src ⇒
365        let 〈dst, src〉 ≝ dst_src in
366        ! v ← retrieve st src;
367        ! st ← store st v dst;
368          ret ? 〈E0, goto l st〉
369      (* CSC: changed, where the meat is *)
370      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
371        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
372        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
373          match fd with
374          [ Internal fn ⇒
375            ! st ← save_ra st l;
376              let st ≝ save_frame st in
377              let locals ≝ init_locals (ertl_if_locals globals fn) in
378              let l' ≝ ertl_if_entry globals fn in
379              ret ? 〈 E0, goto l' (set_locals locals st)〉
380          | External fn ⇒
381            ! params ← fetch_external_args fn st;
382            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
383            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
384            (* CSC: XXX bug here; I think I should split it into Byte-long
385               components; instead I am making a singleton out of it *)
386              let vs ≝ [mk_val ? evres] in
387            ! st ← set_result vs st;
388              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
389          ]
390      ]
391    (* CSC: changed, where the meat is *)
392    | joint_st_return ⇒
393      ! st ← pop_frame st;
394      ! 〈st,pch〉 ← pop st;
395      ! 〈st,pcl〉 ← pop st;
396        let pc ≝ address_of_address_chunks pcl pch in
397        ret ? 〈E0,set_pc pc st〉
398    | _ ⇒ ?
399    ]
400  | ertl_st_new_frame l ⇒
401    ! v ← framesize globals st;
402    ! sp ← get_hwsp st;
403      let newsp ≝ addr_sub sp v in
404    ! st ← set_hwsp newsp st;
405      ret ? 〈E0,goto l st〉
406  | ertl_st_del_frame l ⇒
407    ! v ← framesize globals st;
408    ! sp ← get_hwsp st;
409      let newsp ≝ addr_add sp v in
410    ! st ← set_hwsp newsp st;
411      ret ? 〈E0,goto l st〉
412  | ertl_st_frame_size dst l ⇒
413    ! v ← framesize globals st;
414    ! locals ← reg_store dst (val_of_nat v) (locals st);
415      ret ? 〈E0, goto l (set_locals locals st)〉
416  (* CSC: Dropped:
417      - rtl_st_stackaddr (becomes two get_hdw)
418      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
419      - rtl_st_call_ptr (unimplemented ATM) *)
420  ].
421     
422axiom WrongReturnValueType: String.
423
424definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
425  λglobals: list ident.
426  λexit.
427  λregistersno.
428  λst.
429 (* CSC: monadic notation missing here *)
430  match fetch_statement globals st with
431  [ Error _ ⇒ None ?
432  | OK s ⇒
433    match s with
434    [ ertl_st_lift_pre pre ⇒
435      match pre with
436      [ joint_st_return ⇒
437        match fetch_ra st with
438         [ Error _ ⇒ None ?
439         | OK st_l ⇒
440           let 〈st,l〉 ≝ st_l in
441           match label_eq l exit with
442           [ inl _ ⇒
443             (* CSC: monadic notation missing here *)
444             match fetch_result st registersno with
445             [ Error _ ⇒ None ?
446             | OK vals ⇒ Some ? (smerge2 vals)
447             ]
448           | inr _ ⇒ None ?
449           ]
450         ]
451      | _ ⇒ None ?
452      ]
453    | _ ⇒ None ?
454    ]
455  ].
456
457definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
458  λglobals.
459  λexit.
460  λregistersno.
461  mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).
462
463(* CSC: XXX the program type does not fit with the globalenv and init_mem
464definition make_initial_state : rtl_program → res (genv × state) ≝
465λp.
466  do ge ← globalenv Genv ?? p;
467  do m ← init_mem Genv ?? p;
468  let main ≝ rtl_pr_main ?? p in
469  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
470  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
471  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
472
473definition RTL_fullexec : fullexec io_out io_in ≝
474  mk_fullexec … RTL_exec ? make_initial_state.
475*)
476*)
Note: See TracBrowser for help on using the repository browser.