source: src/ERTL/semantics.ma @ 1312

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

Type of frame operations (pop_frame/save_frame) generalized to take in account
the RTL semantics. LTL and LIN semantics fixed. Fixing of ERTL/RTL still to
be done.

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