source: src/ERTL/semantics.ma @ 1303

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