Changeset 1359


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

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1329 r1359  
    11include "joint/SemanticUtils.ma".
    22include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
     3include alias "common/Identifiers.ma".
    34
    45definition ps_reg_store ≝
     
    4243(*CSC: could we use here a dependent type to avoid the Error case? *)
    4344axiom EmptyStack: String.
    44 definition ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params) ≝
    45  λst.
     45definition ertl_pop_frame: list beval → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     46 λ_.λst.
    4647  let frms ≝ st_frms ? st in
    4748  match frms with
     
    5051     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    5152
    52 definition ertl_save_frame: state … ertl_sem_params → state … ertl_sem_params ≝
    53  λst.
     53definition ertl_save_frame: unit → state … ertl_sem_params → state … ertl_sem_params ≝
     54 λ_.λst.
    5455  set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st)) st.
    5556
     
    5960
    6061(*CSC: XXXXX, for is_final only *)
    61 axiom ertl_fetch_result: state ertl_sem_params → nat → res val.
     62axiom ertl_fetch_result: state ertl_sem_params → res (list beval).
    6263
    6364(*CSC: XXXX, for external functions only*)
  • src/LIN/semantics.ma

    r1324 r1359  
    2626
    2727definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    28 definition lin_pop_frame: state … lin_sem_params → res (state … lin_sem_params) ≝ λst. OK … st.
    29 definition lin_save_frame: state … lin_sem_params → state … lin_sem_params ≝ λst.st.
     28definition lin_pop_frame: list beval → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λst. OK … st.
     29definition lin_save_frame: unit → state … lin_sem_params → state … lin_sem_params ≝ λ_.λst.st.
    3030
    3131definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝
     
    3737
    3838(*CSC: XXXXX, for is_final only *)
    39 axiom lin_fetch_result: state lin_sem_params → nat → res val.
     39axiom lin_fetch_result: state lin_sem_params → res (list beval).
    4040
    4141(*CSC: XXXX, for external functions only*)
  • src/LTL/semantics.ma

    r1324 r1359  
    2121
    2222definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    23 definition ltl_pop_frame: state … ltl_sem_params → res (state … ltl_sem_params) ≝ λst. OK … st.
    24 definition ltl_save_frame: state … ltl_sem_params → state … ltl_sem_params ≝ λst.st.
     23definition ltl_pop_frame: list beval → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λst. OK … st.
     24definition ltl_save_frame: unit → state … ltl_sem_params → state … ltl_sem_params ≝ λ_.λst.st.
    2525
    2626definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝
     
    2929
    3030(*CSC: XXXXX, for is_final only *)
    31 axiom ltl_fetch_result: state ltl_sem_params → nat → res val.
     31axiom ltl_fetch_result: state ltl_sem_params → res (list beval).
    3232
    3333(*CSC: XXXX, for external functions only*)
  • src/RTL/semantics.ma

    r1326 r1359  
    88*)
    99include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
     10include alias "common/Identifiers.ma".
    1011
    1112(* CSC: a streamlined version of the ERTL state *)
    1213record frame: Type[0] ≝
    13  { fr_pc: address
     14 { fr_ret_regs: list register
     15 ; fr_pc: address
    1416 ; fr_sp: pointer
    1517 ; fr_carry: beval
     
    3537(*CSC: could we use here a dependent type to avoid the Error case? *)
    3638axiom EmptyStack: String.
    37 definition rtl_pop_frame: state … rtl_sem_params → res (state … rtl_sem_params) ≝
    38  λst.
     39axiom OutOfBounds: String.
     40include alias "ASM/Util.ma".
     41
     42(*CSC: we could use a dependent type here: the list of return values should have
     43  the same length of the list of return registers that store the values. This
     44  saves the OutOfBounds exception *)
     45definition rtl_pop_frame: list beval → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     46 λret_vals,st.
    3947  let frms ≝ st_frms ? st in
    4048  match frms with
    4149  [ nil ⇒ Error ? [MSG EmptyStack]
    4250  | cons hd tl ⇒
     51     do st ←
     52      mfold_left_i ??
     53       (λi.λst.λreg.
     54         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
     55         greg_store rtl_sem_params reg v st)
     56       (OK … st) (fr_ret_regs hd) ;
    4357     OK …
    4458      (set_frms rtl_sem_params tl
     
    4862          (set_carry … (fr_carry hd) st))))) ].
    4963
    50 definition rtl_save_frame: state … rtl_sem_params → state … rtl_sem_params ≝
    51  λst.
     64definition rtl_save_frame: list register → state … rtl_sem_params → state … rtl_sem_params ≝
     65 λretregs.λst.
    5266  set_frms rtl_sem_params
    53    (mk_frame (pc … st) (sp … st) (carry … st) (regs ? st) :: (st_frms … st)) st.
     67   (mk_frame retregs (pc … st) (sp … st) (carry … st) (regs ? st) :: (st_frms … st)) st.
    5468
    5569definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
     
    5973
    6074(*CSC: XXXXX, for is_final only *)
    61 axiom rtl_fetch_result: state rtl_sem_params → nat → res val.
     75axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
     76(*  let ret_vals ≝ map … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs in
     77*)
    6278
    6379(*CSC: XXXX, for external functions only*)
  • src/joint/BEValues.ma

    r1213 r1359  
    121121  | _ ⇒ Error … [MSG BadByte]].
    122122
     123axiom NotAnInt32Val: String.
     124definition Word_of_list_beval: list beval → res int ≝
     125 λl.
     126  let first_byte ≝ λl.
     127   match l with
     128    [ nil ⇒ Error ? [MSG NotAnInt32Val]
     129    | cons hd tl ⇒ do b ← Byte_of_val hd ; OK ? 〈b,tl〉 ] in
     130  do 〈b1,l〉 ← first_byte l ;
     131  do 〈b2,l〉 ← first_byte l ;
     132  do 〈b3,l〉 ← first_byte l ;
     133  do 〈b4,l〉 ← first_byte l ;
     134   match l with
     135    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
     136    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
     137
    123138(* CSC: maybe we should introduce a type of 1-bit-sized values *)
    124139definition BVtrue: beval ≝ BVByte [[false;false;false;false;false;false;false;true]].
  • src/joint/SemanticUtils.ma

    r1329 r1359  
    11include "joint/semantics.ma".
     2include alias "common/Identifiers.ma".
    23
    34(*** Store/retrieve on pseudo-registers ***)
     
    4344 cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
    4445  [ #res #_ @res
    45   | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
     46  | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct normalize in E2; destruct ]
    4647qed.
    4748
  • 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.