source: src/joint/semantics.ma @ 1182

Last change on this file since 1182 was 1182, checked in by mulligan, 8 years ago

changes to semantics: removing parameterised "next" element in joint params (representing labels) as these are actually fixed across ertl, ltl and lin.

File size: 17.9 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(* CSC: ???????????? In OCaml: IntValue.Int32.merge
18   Note also that the translation can fail; so it should be a res int! *)
19axiom smerge2: list val → int.
20(* CSC: I have a byte, I need a value, but it is complex to do so *)
21axiom val_of_Byte: Byte → val.
22axiom Byte_of_val: val → res Byte.
23(*
24axiom val_of_nat: nat → val.
25(* Map from the front-end memory model to the back-end memory model *)
26*)
27axiom represent_block: block → val × val.
28(* CSC: fixed size chunk *)
29axiom chunk: memory_chunk.
30axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
31axiom address: Type[0].
32axiom val_of_address: address → val. (* CSC: only to shift the sp *)
33axiom address_of_val: val → address. (* CSC: only to shift the sp *)
34(*
35axiom addr_sub: address → nat → address.
36axiom addr_add: address → nat → address.
37*)
38(* CSC: ??? *)
39axiom address_of_label: mem → label → address.
40axiom address_chunks_of_label: mem → label → Byte × Byte.
41axiom label_of_address_chunks: Byte → Byte → label.
42axiom address_of_address_chunks: Byte → Byte → address.
43(*
44axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
45*)
46(*
47axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
48axiom hwreg_retrieve : mRegisterMap → Register → res val.
49axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
50*)
51
52record sem_params: Type[1] ≝
53 { p:> params
54 ; framesT: Type[0]
55 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
56 
57 ; pop_frame_: framesT → res framesT
58 ; save_frame_: framesT → regsT → framesT
59 ; greg_store_: generic_reg p → val → regsT → res regsT
60 ; greg_retrieve_: regsT → generic_reg p → res val
61 ; acca_store_: acc_a_reg p → val → regsT → res regsT
62 ; acca_retrieve_: regsT → acc_a_reg p → res val
63 ; accb_store_: acc_b_reg p → val → regsT → res regsT
64 ; accb_retrieve_: regsT → acc_b_reg p → res val
65 ; dpl_store_: dpl_reg p → val → regsT → res regsT
66 ; dpl_retrieve_: regsT → dpl_reg p → res val
67 ; dph_store_: dph_reg p → val → regsT → res regsT
68 ; dph_retrieve_: regsT → dph_reg p → res val
69 ; pair_reg_move_: regsT → pair_reg p → regsT
70 }.
71
72record state (p: sem_params): Type[0] ≝
73 { st_frms: framesT p
74 ; pc: address
75 ; sp: address
76 ; carry: val
77 ; regs: regsT p
78 ; m: mem
79 }.
80
81definition genv ≝ λglobals,pre,p. (genv_t Genv) (joint_function globals pre p).
82
83record sem_params2 (globals: list ident): Type[1] ≝
84 { sparams:> sem_params
85 ; pre_sem_params:> sem_params_ sparams globals
86 ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
87 }.
88
89definition set_m: ∀p. mem → state p → state p ≝
90 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
91
92definition set_regs: ∀p. regsT p → state p → state p ≝
93 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
94
95definition set_sp: ∀p. address → state p → state p ≝
96 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
97
98definition set_carry: ∀p. val → state p → state p ≝
99 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
100
101definition set_pc: ∀p. address → state p → state p ≝
102 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
103
104definition set_frms: ∀p. framesT p → state p → state p ≝
105 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
106
107(* CSC: was build_state in RTL *)
108definition goto: ∀p:sem_params. label → state p → state p ≝
109 λp,l,st. set_pc … (address_of_label … (m … st) l) st.
110
111definition greg_store: ∀p:sem_params. generic_reg p → val → state p → res (state p) ≝
112 λp,dst,v,st.
113  (*CSC: monadic notation missing here *)
114  bind ?? (greg_store_ … dst v (regs … st)) (λregs.
115  OK ? (set_regs … regs st)).
116
117definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res val ≝
118 λp,st,dst.greg_retrieve_ … (regs … st) dst.
119
120definition acca_store: ∀p:sem_params. acc_a_reg p → val → state p → res (state p) ≝
121 λp,dst,v,st.
122  (*CSC: monadic notation missing here *)
123  bind ?? (acca_store_ … dst v (regs … st)) (λregs.
124  OK ? (set_regs … regs st)).
125
126definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res val ≝
127 λp,st,dst.acca_retrieve_ … (regs … st) dst.
128
129definition accb_store: ∀p:sem_params. acc_b_reg p → val → state p → res (state p) ≝
130 λp,dst,v,st.
131  (*CSC: monadic notation missing here *)
132  bind ?? (accb_store_ … dst v (regs … st)) (λregs.
133  OK ? (set_regs … regs st)).
134
135definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res val ≝
136 λp,st,dst.accb_retrieve_ … (regs … st) dst.
137
138definition dpl_store: ∀p:sem_params. dpl_reg p → val → state p → res (state p) ≝
139 λp,dst,v,st.
140  (*CSC: monadic notation missing here *)
141  bind ?? (dpl_store_ … dst v (regs … st)) (λregs.
142  OK ? (set_regs … regs st)).
143
144definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res val ≝
145 λp,st,dst.dpl_retrieve_ … (regs … st) dst.
146
147definition dph_store: ∀p:sem_params. dph_reg p → val → state p → res (state p) ≝
148 λp,dst,v,st.
149  (*CSC: monadic notation missing here *)
150  bind ?? (dph_store_ … dst v (regs … st)) (λregs.
151  OK ? (set_regs … regs st)).
152
153definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res val ≝
154 λp,st,dst.dph_retrieve_ … (regs … st) dst.
155
156definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝
157 λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st.
158
159definition save_frame: ∀p:sem_params. state p → state p ≝
160 λp,st. set_frms … (save_frame_ ? (st_frms ? st) (regs … st)) st.
161
162(* removes the top frame from the frames list *)
163definition pop_frame: ∀p. state p → res (state p) ≝
164 (* CSC: monadic notation missing here *)
165 λp,st.
166  bind ?? (pop_frame_ p (st_frms … st)) (λframes.
167  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st))).
168
169axiom FailedStore: String.
170
171definition push: ∀p. state p → Byte → res (state p) ≝
172 λp,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: ∀p. state p → res (state p × Byte) ≝
182 λp,st.
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 : ∀p. state p → label → res (state p) ≝
191 λp,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 : ∀p.state p → res (state p × label) ≝
197 λp,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 *)
204axiom fetch_statement: ∀p.∀globals: list ident. state p → res (joint_statement p globals).
205(*
206axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *)
207*)
208
209(*
210definition init_locals : ∀p.list register → regsT p ≝
211foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
212*)
213
214(*
215definition reg_store ≝
216λreg,v,locals. update RegisterTag val locals reg v.
217
218axiom BadRegister : String.
219
220definition reg_retrieve : register_env val → register → res val ≝
221λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
222*)
223
224axiom MissingSymbol : String.
225
226axiom FailedLoad : String.
227
228axiom BadFunction : String.
229
230(*CSC: to be implemented *)
231axiom fetch_external_args: ∀p. external_function → state p → res (list val). (* ≝
232 λfn,st.
233  let registerno ≝ ? fn in
234  ! vs ←
235   mmap …
236    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
237  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
238  ?.
239*)
240
241
242(*CSC: to be implemented; fails if the first list is longer *)
243axiom fold_left2_first_not_longer:
244 ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
245  ∀acc:C. ∀l1:list A. ∀l2: list B.
246   res C.
247
248(* CSC: the list should be a vector or have an upper bounded length *)
249(*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX *)
250axiom set_result: ∀p. list val → state p → res (state p).
251(* λp,vs,st.
252  (* CSC: monadic notation not used *)
253  bind ?? (
254   fold_left2_first_not_longer …
255    (λregs,v,reg. hwreg_store reg v regs) (regs … st) vs RegisterRets)
256  (λregs.OK ? (set_regs … regs st)).
257*)
258
259(*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX *)
260axiom fetch_result: ∀p. state p → nat → res (list val).
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: ∀p. list ident → label → nat → state p → option ((*CSC: why not res*) int) ≝
410  λp.λglobals: list ident.
411  λexit.
412  λregistersno.
413  λst.
414 (* CSC: monadic notation missing here *)
415  match fetch_statement … 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 joint_exec: ∀globals:list ident. sem_params2 globals → label → nat → execstep io_out io_in ≝
439  λglobals,p.
440  λexit.
441  λregistersno.
442  mk_execstep ? ? ? ? (is_final p globals exit registersno) (m p) (eval_statement globals p).
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.