source: src/ERTL/semantics.ma @ 1329

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