source: src/ERTL/semantics.ma @ 1151

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

Only new_/del_frame and framesize left.

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