source: src/ERTL/semantics.ma @ 1377

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

pop_frame now incorporates the fetch_result (that made sense only for RTL).
pop_frame and save_frame are now also more symmetric

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