Changeset 1220
 Timestamp:
 Sep 15, 2011, 6:05:31 PM (8 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTL.ma
r1183 r1220 26 26 definition ertl_statement ≝ joint_statement ertl_params. 27 27 28 definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals). 28 definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝ 29 λglobals. 30 mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …). 29 31 30 record ertl_internal_function (globals: list ident): Type[0] ≝ 31 { 32 ertl_if_luniverse: universe LabelTag; 33 ertl_if_runiverse: universe RegisterTag; 34 ertl_if_params: nat; 35 ertl_if_locals: registers; 36 ertl_if_stacksize: nat; 37 ertl_if_graph: ertl_statement_graph globals; 38 ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?; 39 ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ? 40 }. 41 42 definition set_luniverse ≝ 43 λglobals : list ident. 44 λint_fun : ertl_internal_function globals. 45 λluniverse: universe LabelTag. 46 let runiverse ≝ ertl_if_runiverse globals int_fun in 47 let params ≝ ertl_if_params globals int_fun in 48 let locals ≝ ertl_if_locals globals int_fun in 49 let stacksize ≝ ertl_if_stacksize globals int_fun in 50 let graph ≝ ertl_if_graph globals int_fun in 51 let entry ≝ ertl_if_entry globals int_fun in 52 let exit ≝ ertl_if_exit globals int_fun in 53 mk_ertl_internal_function globals 54 luniverse runiverse params locals 55 stacksize graph entry exit. 56 57 definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals). 58 59 record ertl_program (globals: list ident): Type[0] ≝ 60 { 61 ertl_pr_vars: list (ident × nat); 62 ertl_pr_funcs: list (ident × (ertl_function globals)); 63 ertl_pr_main: option ident 64 }. 65 66 67 (* XXX: changed from O'Caml 68  ertl_st_addr_h: register → ident → label → ertl_statement 69  ertl_st_addr_l: register → ident → label → ertl_statement 32 (* 33 definition ertl_internal_function ≝ 34 λglobals. joint_internal_function globals … (ertl_sem_params_ globals). 70 35 *) 71 36 72 (* XXX: changed from O'Caml 73  ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement 74  ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement 75 *) 37 definition ertl_program ≝ λglobals. joint_program globals … (ertl_sem_params_ globals). 
src/joint/Joint.ma
r1182 r1220 63 63 }. 64 64 65 definition set_luniverse ≝ 66 λglobals : list ident. 67 λpre. 68 λp: sem_params_ pre globals. 69 λint_fun : joint_internal_function globals … p. 70 λluniverse: universe LabelTag. 71 let runiverse ≝ joint_if_runiverse … int_fun in 72 let params ≝ joint_if_params … int_fun in 73 let locals ≝ joint_if_locals … int_fun in 74 let result ≝ joint_if_result … int_fun in 75 let stacksize ≝ joint_if_stacksize … int_fun in 76 let graph ≝ joint_if_graph … int_fun in 77 let entry ≝ joint_if_entry … int_fun in 78 let exit ≝ joint_if_exit … int_fun in 79 mk_joint_internal_function globals ? p 80 luniverse runiverse result params locals 81 stacksize graph entry exit. 82 65 83 definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p). 66 84 67 record joint_program (globals: list ident) (pre) (p:sem_params_ pre globals) : Type[0] ≝ 68 { 69 joint_pr_vars: list (ident × nat); 70 joint_pr_functs: list (ident × (joint_function … p)); 71 joint_pr_main: option ident 72 }. 85 definition joint_program := 86 λglobals:list ident.λpre.λp: sem_params_ pre globals. 87 program (joint_function … p) nat. 73 88 74 89 (****************************************************************************) 
src/joint/semantics.ma
r1217 r1220 307 307 mk_execstep … (is_final globals p exit registersno) (m p) (eval_statement globals p). 308 308 309 (* CSC: XXX the program type does not fit with the globalenv and init_mem *) 310 axiom make_initial_state : ∀globals:list ident.∀sparams: sem_params2 globals. joint_program … (pre_sem_params … sparams) → res ((genv … (pre_sem_params … sparams)) × (state sparams)).(* ≝ 311 λp. 312 do ge ← globalenv Genv ?? p; 313 do m ← init_mem Genv ?? p; 314 let main ≝ rtl_pr_main ?? p in 309 definition make_initial_state : 310 ∀globals:list ident.∀sparams: sem_params2 globals. joint_program ?? (pre_sem_params ? sparams) → 311 res ((genv ?? (pre_sem_params ? sparams)) × (state sparams)) ≝ 312 λglobals,par,p. 313 do ge ← globalenv Genv … (λx.[Init_space x]) p; 314 do m ← init_mem Genv … (λx.[Init_space x]) p; 315 let main ≝ prog_main … p in 315 316 do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main); 316 317 do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b); 317 OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉. 318 ?(* 319 OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉*). 320 (* 321 RTL: 322 init_prog == init_mem 323 init_sp: inizializzare lo stack pointer 324 init_isp: inizializzare l'altro stack pointer 325 init_renv: inizializzare i registri fisici 326 init_main_call: chiamata di funzione 327  init_fun_call: cambia fra ERTL e LTL 328 change_carry: a 0 318 329 *) 319 320 330 definition joint_fullexec : 321 331 ∀globals:list ident. ∀sparams:sem_params2 globals. joint_program globals sparams (pre_sem_params … sparams) → fullexec io_out io_in ≝
Note: See TracChangeset
for help on using the changeset viewer.