Changeset 1359 for src/joint


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/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • 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.