Ignore:
Timestamp:
Oct 11, 2011, 6:00:03 PM (9 years ago)
Author:
sacerdot
Message:
  1. more work on the RTL semantics
  2. changes to joint/semantics to accomodate the RTL one
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1352 r1359  
    5050   (* Functions that manipulate the st_frms component of the state *)
    5151 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    52  ; pop_frame: state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    53  ; save_frame: state (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams)
     52 ; pop_frame: list beval → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
     53 ; save_frame: call_dest p → state (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams)
    5454 }.
    5555
     
    7070
    7171 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals)
    72  ; fetch_result: state (mk_sem_params … more_sparams1) → nat → res val
     72 ; fetch_result: state (mk_sem_params … more_sparams1) → res (list beval)
    7373
    7474 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val)
     
    102102 cases (address_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
    103103  [ #res #_ @res
    104   | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ]
     104  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 try destruct
     105    normalize in E2; destruct ]
    105106qed.
    106107
     
    293294              let st ≝ save_frame … dest st in
    294295              let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    295 + USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
    296 + ALLOCARE LO STACK FRAME
     296(*+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
     297+ ALLOCARE LO STACK FRAME*)
    297298              let l' ≝ joint_if_entry … fn in
    298299             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
     
    308309          ]]
    309310    | RETURN ⇒
    310 + CHIAMARE UNA FUNZIONE PER ANDARE A SOSTITUIRE IL VALORE TROVATO NEL REGISTRO
    311 DI RITORNO DELLA FUNZIONE AL POSTO GIUSTO
    312 + DEALLOCARE LO STACK FRAME
    313       ! st ← pop_frame … st;
     311(* + DEALLOCARE LO STACK FRAME*)
     312      ! res ← fetch_result … st;
     313      ! st ← pop_frame … res st;
    314314      ! 〈st,pch〉 ← pop … st;
    315315      ! 〈st,pcl〉 ← pop … st;
     
    318318qed.
    319319
    320 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → nat → state p → option int ≝
    321  λglobals,p,ge,exit,registersno,st.res_to_opt … (
     320definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → state p → option int ≝
     321 λglobals,p,ge,exit,st.res_to_opt ? (
    322322  do s ← fetch_statement … ge st;
    323323  match s with
     
    325325      do 〈st,l〉 ← fetch_ra … st;
    326326      if eq_address l exit then
    327        do val ← fetch_result … st registersno;
    328        match val with
    329         [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
    330         | _ ⇒ Error ? []]
     327       do vals ← fetch_result … st ;
     328       Word_of_list_beval vals
    331329      else
    332330       Error ? []
     
    337335 ; sparams2: sem_params2 globals
    338336 ; exit: address
    339  ; registersno: nat
    340337 ; genv2: genv globals sparams2
    341338 }.
     
    343340definition joint_exec: trans_system io_out io_in ≝
    344341  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
    345    (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G) (registersno G))
     342   (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G))
    346343   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
    347344
     
    351348
    352349 λpars,sparams.
    353   (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
    354 [1,2: cases daemon (*CSC: XXXXXXXXXXXXX*) ]
     350  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ? (globalenv Genv … (λx.[Init_space x]) p)).
     351cases daemon (*CSC: XXXXXXXXXXXXX*)
    355352qed.
    356353
Note: See TracChangeset for help on using the changeset viewer.