source: Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma @ 3031

Last change on this file since 3031 was 1311, checked in by campbell, 8 years ago

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

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