source: src/ERTL/semantics.ma @ 1327

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

More progress in the implementation of the ERTL specific statements.
The file does not compile ATM because of unimplemented addr_sub and addr_add.

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