source: src/ERTL/semantics.ma @ 1371

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

save_frame changed to accept also the formal/actual argument pairs, required
in the RTL semantics. The function returns now a res, but this could be fixed
with a dependent type for function call to disallow calling a function with the
wrong arguments.

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