source: src/ERTL/semantics.ma @ 1318

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

Frame management implemented.

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