source: src/joint/semantics.ma @ 1174

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

Semantics of most instructions completed.

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