source: src/joint/semantics.ma @ 1176

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

...

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