source: src/joint/semantics.ma @ 1173

Last change on this file since 1173 was 1173, checked in by sacerdot, 8 years ago

Unified semantics for ERTL/LTL/LIN (in progress).
I hope to include RTL too.

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