source: src/ERTL/semantics.ma @ 1150

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

Push/pop implemented.

File size: 13.6 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(*
24(* CSC: ???????????? In OCaml: IntValue.Int32.merge
25   Note also that the translation can fail; so it should be a res int! *)
26axiom smerge2: list val → int.
27*)
28(* CSC: I have a byte, I need a value, but it is complex to do so *)
29axiom val_of_Byte: Byte → val.
30axiom Byte_of_val: val → res Byte.
31(* Map from the front-end memory model to the back-end memory model *)
32axiom represent_block: block → val × val.
33(* CSC: fixed size chunk *)
34axiom chunk: memory_chunk.
35axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
36
37axiom address: Type[0].
38axiom val_of_address: address → val. (* CSC: only to shift the sp *)
39axiom address_of_val: val → address. (* CSC: only to shift the sp *)
40(* CSC: ??? *)
41axiom address_of_label: mem → label → address.
42axiom address_chunks_of_label: mem → label → Byte × Byte.
43axiom label_of_address_chunks: Byte → Byte → label.
44axiom address_of_address_chunks: Byte → Byte → address.
45axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
46axiom hwreg_retrieve : mRegisterMap → Register → res val.
47axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
48
49definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).
50
51(* CSC: frame reduced to this *)
52definition frame: Type[0] ≝ register_env val.
53
54record state : Type[0] ≝
55 { st_frms: list frame
56 ; pc: address
57 ; sp: address
58(* ; exit: address *)
59 ; locals: register_env val
60 ; carry: val
61 ; regs: mRegisterMap
62 ; m: mem
63 }.
64
65definition set_m: mem → state → state ≝
66 λm,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) m.
67
68definition set_locals: register_env val → state → state ≝
69 λlocals,st. mk_state (st_frms st) (pc st) (sp st) locals (carry st) (regs st) (m st).
70
71definition set_regs: mRegisterMap → state → state ≝
72 λregs,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) regs (m st).
73
74definition set_sp: address → state → state ≝
75 λsp,st. mk_state (st_frms st) (pc st) sp (locals st) (carry st) (regs st) (m st).
76
77definition set_carry: val → state → state ≝
78 λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
79
80definition set_pc: address → state → state ≝
81 λpc,st. mk_state (st_frms st) pc (sp st) (locals st) (carry st) (regs st) (m st).
82
83(* CSC: was build_state in RTL *)
84definition goto: label → state → state ≝
85 λl,st. set_pc (address_of_label (m st) l) st.
86
87(* pushes the locals (i.e. the current frame) on top of the frames list *)
88definition save_frame: state → state ≝
89 λst. mk_state (locals st::st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) (m st).
90
91axiom FailedPopFrame: String.
92
93(* removes the top frame from the frames list *)
94definition pop_frame: state → res state ≝
95 λst.
96  match st_frms st with
97   [ nil ⇒ Error ? (msg FailedPopFrame)
98   | cons _ frms ⇒
99      OK ? (mk_state frms (pc st) (sp st) (locals st) (carry st) (regs st) (m st)) ].
100
101axiom FailedStore: String.
102
103definition push: state → Byte → res state ≝
104 λst,v.
105  let sp ≝ val_of_address (sp st) in
106  (*CSC: no monadic notation here *)
107  bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m st) sp (val_of_Byte v)))
108   (λm.
109    let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
110    OK ? (set_m m (set_sp sp st))).
111
112
113definition pop: state → res (state × Byte) ≝
114 λst:state.
115  let sp ≝ val_of_address (sp st) in
116  let sp ≝ sub sp (val_of_memory_chunk chunk) in
117  let st ≝ set_sp (address_of_val sp) st in
118  (*CSC: no monadic notation here *)
119  bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m st) sp))
120   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
121
122definition save_ra : state → label → res state ≝
123 λst,l.
124  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
125  (* No monadic notation here *)
126  bind ?? (push st addrl) (λst.push st addrh).
127
128definition fetch_ra : state → res (state × label) ≝
129 λst.
130  (* No monadic notation here *)
131  bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
132  bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
133   OK ? 〈st, label_of_address_chunks addrl addrh〉)).
134
135(*CSC: To be implemented *)
136axiom fetch_statement: state → res ertl_statement.
137
138definition init_locals : list register → register_env val ≝
139foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
140
141definition reg_store ≝
142λreg,v,locals. update RegisterTag val locals reg v.
143
144(*
145axiom WrongNumberOfParameters : String.
146
147(* CSC: modified to take in input a list of registers (untyped) *)
148let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
149match rs with
150[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
151| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
152  let locals' ≝ add RegisterTag val locals r v in
153  params_store rst vst locals'
154] ].
155*)
156
157axiom BadRegister : String.
158
159definition reg_retrieve : register_env val → register → res val ≝
160λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
161
162(*
163axiom FailedOp : String.
164*)
165axiom MissingSymbol : String.
166(*
167axiom MissingStatement : String.
168axiom FailedConstant : String. *)
169axiom FailedLoad : String.
170axiom BadFunction : String.
171(*axiom BadJumpTable : String.
172axiom BadJumpValue : String.
173axiom FinalState : String.
174axiom ReturnMismatch : String.
175*)
176
177(*CSC: to be implemented *)
178axiom fetch_external_args: external_function → state → res (list val).(* ≝
179 λfn,st.
180  let registerno ≝ ? fn in
181  ! vs ←
182   mmap …
183    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
184  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
185  ?.*)
186
187(*CSC: to be implemented; fails if the first list is longer *)
188axiom fold_left2_first_not_longer:
189 ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
190  ∀acc:C. ∀l1:list A. ∀l2: list B.
191   res C.
192
193(* CSC: the list should be a vector or have an upper bounded length *)
194definition set_result: list val → state → res state ≝
195 λvs,st.
196  (* CSC: monadic notation not used *)
197  bind ?? (
198   fold_left2_first_not_longer …
199    (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
200  (λregs.OK ? (set_regs regs st)).
201
202definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
203λge,st.
204  ! s ← fetch_statement st;
205  match s with
206  [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉
207  | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉
208  | ertl_st_int dest v l ⇒
209     ! locals ← reg_store dest (val_of_Byte v) (locals st);
210     ret ? 〈E0, goto l (set_locals locals st)〉
211  | ertl_st_load addrl addrh dst l ⇒
212      ! vaddrh ← reg_retrieve (locals st) addrh;
213      ! vaddrl ← reg_retrieve (locals st) addrl;
214      ! vaddr ← smerge vaddrl vaddrh;
215      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
216      ! locals ← reg_store dst v (locals st);
217      ret ? 〈E0, goto l (set_locals locals st)〉
218  | ertl_st_store addrl addrh src l ⇒
219      ! vaddrh ← reg_retrieve (locals st) addrh;
220      ! vaddrl ← reg_retrieve (locals st) addrl;
221      ! vaddr ← smerge vaddrl vaddrh;
222      ! v ← reg_retrieve (locals st) src;
223      ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
224      ret ? 〈E0, goto l (set_m m' st)〉
225  | ertl_st_cond src ltrue lfalse ⇒
226      ! v ← reg_retrieve (locals st) src;
227      ! b ← eval_bool_of_val v;
228      ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
229  | ertl_st_addr ldest hdest id l ⇒
230     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
231     let 〈laddr,haddr〉 ≝ represent_block addr in
232     ! locals ← reg_store ldest laddr (locals st);
233     ! locals ← reg_store hdest haddr locals;
234     ret ? 〈E0, goto l (set_locals locals st)〉
235  | ertl_st_op1 op dst src l ⇒
236     ! v ← reg_retrieve (locals st) src;
237     ! v ← Byte_of_val v;
238     let v' ≝ val_of_Byte (op1 eval op v) in
239     ! locals ← reg_store dst v' (locals st);
240     ret ? 〈E0, goto l (set_locals locals st)〉
241  | ertl_st_op2 op dst src1 src2 l ⇒
242     ! v1 ← reg_retrieve (locals st) src1;
243     ! v1 ← Byte_of_val v1;
244     ! v2 ← reg_retrieve (locals st) src2;
245     ! v2 ← Byte_of_val v2;
246     ! carry ← eval_bool_of_val (carry st);
247     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
248     let v' ≝ val_of_Byte v' in
249     let carry ≝ of_bool carry in
250     ! locals ← reg_store dst v' (locals st);
251     ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
252  | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
253     ! v1 ← reg_retrieve (locals st) sacc;
254     ! v1 ← Byte_of_val v1;
255     ! v2 ← reg_retrieve (locals st) sbacc;
256     ! v2 ← Byte_of_val v2;
257     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
258     let v1' ≝ val_of_Byte v1' in
259     let v2' ≝ val_of_Byte v2' in
260     ! locals ← reg_store dacc v1' (locals st);
261     ! locals ← reg_store dbacc v2' locals;
262     ret ? 〈E0, goto l (set_locals locals st)〉
263  | ertl_st_clear_carry l ⇒
264    ret ? 〈E0, goto l (set_carry Vfalse st)〉
265  | ertl_st_set_carry l ⇒
266    ret ? 〈E0, goto l (set_carry Vtrue st)〉
267     
268  (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
269         ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
270         be more than enough... *)
271  | ertl_st_move dst src l ⇒
272     ! v ← reg_retrieve (locals st) src;
273     ! locals ← reg_store dst v (locals st);
274     ret ? 〈E0, goto l (set_locals locals st)〉
275  | ertl_st_hdw_to_hdw dst src l ⇒
276     ! v ← hwreg_retrieve (regs st) src;
277     ! regs ← hwreg_store dst v (regs st);
278     ret ? 〈E0, goto l (set_regs regs st)〉
279  | ertl_st_get_hdw dst src l ⇒
280     ! v ← hwreg_retrieve (regs st) src;
281     ! locals ← reg_store dst v (locals st);
282     ret ? 〈E0, goto l (set_locals locals st)〉
283  | ertl_st_set_hdw dst src l ⇒
284     ! v ← reg_retrieve (locals st) src;
285     ! regs ← hwreg_store dst v (regs st);
286     ret ? 〈E0, goto l (set_regs regs st)〉
287
288  (* CSC: Dropped:
289      - rtl_st_stackaddr (becomes two get_hdw)
290      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
291      - rtl_st_call_ptr (unimplemented ATM) *)
292     
293  (* CSC: changed, where the meat is *)
294  | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *)
295      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
296      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
297      match fd with
298      [ Internal fn ⇒
299        ! st ← save_ra st l;
300        let st ≝ save_frame st in
301        let locals ≝ init_locals (ertl_if_locals fn) in
302        let l' ≝ ertl_if_entry fn in
303         ret ? 〈 E0, goto l' (set_locals locals st)〉
304      | External fn ⇒
305        ! params ← fetch_external_args fn st;
306        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
307        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
308        (* CSC: XXX bug here; I think I should split it into Byte-long
309           components; instead I am making a singleton out of it *)
310        let vs ≝ [mk_val ? evres] in
311        ! st ← set_result vs st;
312        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
313      ]
314  | ertl_st_return ⇒
315      ! st ← pop_frame st;
316      ! 〈st,pch〉 ← pop st;
317      ! 〈st,pcl〉 ← pop st;
318      let pc ≝ address_of_address_chunks pcl pch in
319      ret ? 〈E0,set_pc pc st〉
320 
321  (* CSC: new stuff *)
322  | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
323  | ertl_st_new_frame _ ⇒ ?
324  | ertl_st_del_frame _ ⇒ ?
325  | ertl_st_frame_size _ _ ⇒ ?
326  | ertl_st_pop dst l ⇒
327     ! 〈st,v〉 ← pop st;
328     ! locals ← reg_store dst (val_of_Byte v) (locals st);
329     ret ? 〈E0, goto l (set_locals locals st)〉
330  | ertl_st_push src l ⇒
331     ! v ← reg_retrieve (locals st) src;
332     ! v ← Byte_of_val v;
333     ! st ← push st v;
334     ret ? 〈E0, goto l st〉
335  ].
336
337axiom WrongReturnValueType: String.
338
339definition is_final : state → option ((*CSC: why not res*) int) ≝
340λs. match s with
341[ State _ _ _ ⇒ None ?
342| Callstate _ _ _ _ _ ⇒ None ?
343| Returnstate v _ fs _ ⇒
344    match fs with
345     [ nil ⇒ Some ? (smerge2 v)
346     | _ ⇒ None ? ]].
347
348definition RTL_exec : execstep io_out io_in ≝
349  mk_execstep … ? is_final mem_of_state eval_statement.
350
351(* CSC: XXX the program type does not fit with the globalenv and init_mem
352definition make_initial_state : rtl_program → res (genv × state) ≝
353λp.
354  do ge ← globalenv Genv ?? p;
355  do m ← init_mem Genv ?? p;
356  let main ≝ rtl_pr_main ?? p in
357  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
358  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
359  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
360
361definition RTL_fullexec : fullexec io_out io_in ≝
362  mk_fullexec … RTL_exec ? make_initial_state.
363*)
Note: See TracBrowser for help on using the repository browser.