Changeset 1233 for src/joint


Ignore:
Timestamp:
Sep 21, 2011, 11:57:20 AM (9 years ago)
Author:
sacerdot
Message:

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1228 r1233  
    55include "common/Graphs.ma".
    66
     7record params_: Type[1] ≝
     8 { acc_a_reg: Type[0]
     9 ; acc_b_reg: Type[0]
     10 ; dpl_reg: Type[0]
     11 ; dph_reg: Type[0]
     12 ; pair_reg: Type[0]
     13 ; generic_reg: Type[0]
     14 
     15 ; extend_statements: Type[0]
     16 
     17 ; resultT: Type[0]
     18 ; localsT: Type[0]
     19 ; paramsT: Type[0]
     20 }.
     21
    722record params: Type[1] ≝
    8 {
    9   acc_a_reg: Type[0];
    10   acc_b_reg: Type[0];
    11   dpl_reg: Type[0];
    12   dph_reg: Type[0];
    13   pair_reg: Type[0];
    14   generic_reg: Type[0];
    15  
    16   extend_statements: Type[0];
    17  
    18   resultT: Type[0];
    19   localsT: Type[0];
    20   paramsT: Type[0]
    21 }.
     23 { pars_:> params_
     24 ; succ: Type[0]
     25 }.
    2226
    23 inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
     27inductive joint_instruction (p:params_) (globals: list ident): Type[0] ≝
    2428  | joint_instr_comment: String → joint_instruction p globals
    2529  | joint_instr_cost_label: costlabel → joint_instruction p globals
     
    4044
    4145inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
    42   | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals
     46  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
    4347  | joint_st_goto: label → joint_statement p globals
    4448  | joint_st_return: joint_statement p globals
    4549  | joint_st_extension: extend_statements p → joint_statement p globals.
    4650
    47 record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
    48  { pmemoryT: Type[0]
    49  ; lookup: pmemoryT → label → option (joint_statement preparams globals)
    50  }.
    51 
    52 record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝
     51record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
    5352{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    5453  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
    5554(*  joint_if_sig: signature;  -- dropped in front end *)
    56   joint_if_result   : resultT pre;
    57   joint_if_params   : paramsT pre;
    58   joint_if_locals   : localsT pre;
     55  joint_if_result   : resultT p;
     56  joint_if_params   : paramsT p;
     57  joint_if_locals   : localsT p;
    5958  joint_if_stacksize: nat;
    60   joint_if_graph    : pmemoryT … p;
    61   joint_if_entry    : Σl: label. lookup … p joint_if_graph l ≠ None ?;
    62   joint_if_exit     : Σl: label. lookup … p joint_if_graph l ≠ None ?
     59  joint_if_lookup   : label → option (joint_statement p globals);
     60  joint_if_entry    : Σl: label. joint_if_lookup l ≠ None ?;
     61  joint_if_exit     : Σl: label. joint_if_lookup l ≠ None ?
    6362}.
    6463
    6564definition set_luniverse ≝
     65  λp:params.
    6666  λglobals  : list ident.
    67   λpre.
    68   λp: sem_params_ pre globals.
    69   λint_fun  : joint_internal_function globals … p.
     67  λint_fun  : joint_internal_function p globals.
    7068  λluniverse: universe LabelTag.
    7169  let runiverse ≝ joint_if_runiverse … int_fun in
     
    7472  let result    ≝ joint_if_result … int_fun in
    7573  let stacksize ≝ joint_if_stacksize … int_fun in
    76   let graph     ≝ joint_if_graph … int_fun in
     74  let lookup    ≝ joint_if_lookup … int_fun in
    7775  let entry     ≝ joint_if_entry … int_fun in
    7876  let exit      ≝ joint_if_exit … int_fun in
    79     mk_joint_internal_function globals ? p
     77    mk_joint_internal_function … globals
    8078      luniverse runiverse result params locals
    81       stacksize graph entry exit.
     79      stacksize lookup entry exit.
    8280
    83 definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
     81definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
    8482
    85 definition joint_program ≝
    86   λglobals: list ident.
    87   λpre.
    88   λp: sem_params_ pre globals.
    89     program (λx. joint_function globals pre p) nat.
     83definition joint_program ≝ λp:params. program (joint_function p) nat.
    9084
    9185(****************************************************************************)
  • src/joint/semantics.ma

    r1220 r1233  
    1717  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
    1818
    19 record sem_params: Type[1] ≝
    20  { p:> params
    21  ; framesT: Type[0]
     19record more_sem_params (p:params): Type[1] ≝
     20 { framesT: Type[0]
    2221 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
    23  
     22
     23 ; succ_pc: succ p → address → address
    2424 ; pop_frame_: framesT → res framesT
    2525 ; save_frame_: framesT → regsT → framesT
     
    4040 }.
    4141
    42 definition address_of_label: sem_params → label → address.
    43  #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label p l)))
    44  cases (beval_pair_of_pointer (pointer_of_label p l)) in ⊢ (???% → ?)
    45   [ #res #_ @res
    46   | #msg cases (pointer_of_label p l) * * #q #com #off #E1 #E2 destruct ]
    47 qed.
     42record sem_params: Type[1] ≝
     43 { spp :> params
     44 ; more_sem_pars :> more_sem_params spp
     45 }.
    4846
    4947record state (p: sem_params): Type[0] ≝
    50  { st_frms: framesT p
     48 { st_frms: framesT ? p
    5149 ; pc: address
    5250 ; sp: pointer
    5351 ; carry: beval
    54  ; regs: regsT p
     52 ; regs: regsT ? p
    5553 ; m: bemem
    5654 }.
    5755
    58 definition genv ≝ λglobals,pre,p. (genv_t Genv) (joint_function globals pre p).
     56definition genv ≝ λp:params.λglobals. (genv_t Genv) (joint_function p globals).
     57
     58(*
     59CSC: fetch_statement credo sia implementabile ⇒ globals non e' necessario ⇒ niente
     60casino e posso back-trackare il cambiamento in SmallstepExec!!! Togliere del
     61tutto il parametro a exec_extended.
     62CSC: NO! RTL ha come exec_extended tail_call e (tail_)call_ptr che usa genv
     63*)
     64
     65record more_sem_params2 (p: params) (globals: list ident): Type[1] ≝
     66 { more_sparams:> more_sem_params p
     67 
     68 ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     69 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
     70 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
     71 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
     72
     73 ; exec_extended: genv p globals → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
     74 }.
    5975
    6076record sem_params2 (globals: list ident): Type[1] ≝
    61  { sparams:> sem_params
    62  ; pre_sem_params:> sem_params_ sparams globals
    63  
    64  ; fetch_statement: state sparams → res (joint_statement sparams globals)
    65  ; fetch_external_args: external_function → state sparams → res (list val)
    66  ; set_result: list val → state sparams → res (state sparams)
    67  ; fetch_result: state sparams → nat → res val
    68 
    69  ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
    70  }.
     77 { p2:> params
     78 ; more_sparams2:> more_sem_params2 p2 globals
     79 }.
     80
     81definition sem_params_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params sp2 sp2.
     82coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
     83 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
     84
     85unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
     86   S ≟ sem_params_of_sem_params2 globals p
     87(* ---------------------------------------- *) ⊢
     88   pars_ (spp (mk_sem_params (p2 globals p)
     89    (more_sparams (p2 globals p) globals
     90    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
     91
     92definition address_of_label: sem_params → label → address.
     93 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
     94 cases (beval_pair_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
     95  [ #res #_ @res
     96  | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 destruct ]
     97qed.
    7198
    7299definition set_m: ∀p. bemem → state p → state p ≝
    73100 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
    74101
    75 definition set_regs: ∀p. regsT p → state p → state p ≝
     102definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
    76103 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
    77104
     
    85112 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
    86113
    87 definition set_frms: ∀p. framesT p → state p → state p ≝
     114definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
    88115 λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
    89116
     
    91118 λp,l,st. set_pc … (address_of_label p l) st.
    92119
     120definition next: ∀p:sem_params. succ … p → state p → state p ≝
     121 λp,l,st. set_pc … (succ_pc … (more_sem_pars p) l (pc … st)) st.
     122
    93123definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
    94124 λp,dst,v,st.
     
    135165
    136166definition save_frame: ∀p:sem_params. state p → state p ≝
    137  λp,st. set_frms … (save_frame_ ? (st_frms ? st) (regs … st)) st.
     167 λp,st. set_frms … (save_frame_ … (st_frms … st) (regs … st)) st.
    138168
    139169(* removes the top frame from the frames list *)
    140170definition pop_frame: ∀p. state p → res (state p) ≝
    141171 λp,st.
    142   do frames ← pop_frame_ p (st_frms … st);
     172  do frames ← pop_frame_ p (st_frms … st);
    143173  OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).
    144174
     
    160190  OK ? 〈st,v〉.
    161191
    162 definition save_ra : ∀p. state p → label → res (state p) ≝
     192definition save_ra : ∀p. state p → succ p → res (state p) ≝
    163193 λp,st,l.
    164   let 〈addrl,addrh〉 ≝ address_of_label p l in
     194  let 〈addrl,addrh〉 ≝ succ_pc … (more_sem_pars p) l (pc … st) in
    165195  do st ← push … st addrl;
    166196  push … st addrh.
     
    181211coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
    182212
    183 definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv … (pre_sem_params … p) → state p → IO io_out io_in (trace × (state p)) ≝
    184   λglobals,p. λge,st.
    185   ! s ← fetch_statement globals p st;
     213definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv p globals → state p → IO io_out io_in (trace × (state p)) ≝
     214 λglobals,p,ge,st.
     215  ! s ← fetch_statement st;
    186216  match s with
    187217    [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
    188218    | joint_st_sequential seq l ⇒
    189219      match seq with
    190       [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto … l st〉
    191       | joint_instr_comment c ⇒ ret ? 〈E0, goto … l st〉
     220      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, next … l st〉
     221      | joint_instr_comment c ⇒ ret ? 〈E0, next … l st〉
    192222      | joint_instr_int dest v ⇒
    193         ! st ← greg_store dest (BVByte v) st;
    194           ret ? 〈E0, goto … l st〉
     223        ! st ← greg_store ? dest (BVByte v) st;
     224          ret ? 〈E0, next … l st〉
    195225      | joint_instr_load dst addrl addrh ⇒
    196226        ! vaddrh ← dph_retrieve … st addrh;
     
    199229        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    200230        ! st ← acca_store … dst v st;
    201           ret ? 〈E0, goto … l st〉
     231          ret ? 〈E0, next … l st〉
    202232      | joint_instr_store addrl addrh src ⇒
    203233        ! vaddrh ← dph_retrieve … st addrh;
     
    206236        ! v ← acca_retrieve … st src;
    207237        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    208           ret ? 〈E0, goto … l (set_m … m' st)〉
     238          ret ? 〈E0, next … l (set_m … m' st)〉
    209239      | joint_instr_cond src ltrue ⇒
    210240        ! v ← acca_retrieve … st src;
    211241        ! b ← bool_of_beval v;
    212           ret ? 〈E0, goto … (if b then ltrue else l) st〉
     242          ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
    213243      | joint_instr_address ident prf ldest hdest ⇒
    214244        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
     
    216246        ! st ← dpl_store … ldest laddr st;
    217247        ! st ← dph_store … hdest haddr st;
    218           ret ? 〈E0, goto … l st〉
     248          ret ? 〈E0, next … l st〉
    219249      | joint_instr_op1 op acc_a ⇒
    220250        ! v ← acca_retrieve … st acc_a;
     
    222252          let v' ≝ BVByte (op1 eval op v) in
    223253        ! st ← acca_store … acc_a v' st;
    224           ret ? 〈E0, goto … l st〉
     254          ret ? 〈E0, next … l st〉
    225255      | joint_instr_op2 op acc_a src ⇒
    226256        ! v1 ← acca_retrieve … st acc_a;
     
    233263          let carry ≝ beval_of_bool carry in
    234264        ! st ← acca_store … acc_a v' st;
    235           ret ? 〈E0, goto … l (set_carry … carry st)〉
    236       | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVfalse st)〉
    237       | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … BVtrue st)〉
     265          ret ? 〈E0, next … l (set_carry … carry st)〉
     266      | joint_instr_clear_carry ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
     267      | joint_instr_set_carry ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
    238268      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    239269        ! v1 ← acca_retrieve … st acc_a_reg;
     
    246276        ! st ← acca_store … acc_a_reg v1' st;
    247277        ! st ← accb_store … acc_b_reg v2' st;
    248           ret ? 〈E0, goto … l st〉
     278          ret ? 〈E0, next … l st〉
    249279      | joint_instr_pop dst ⇒
    250280        ! 〈st,v〉 ← pop … st;
    251281        ! st ← acca_store … dst v st;
    252           ret ? 〈E0, goto … l st〉
     282          ret ? 〈E0, next … l st〉
    253283      | joint_instr_push src ⇒
    254284        ! v ← acca_retrieve … st src;
    255285        ! st ← push … st v;
    256           ret ? 〈E0, goto … l st〉
     286          ret ? 〈E0, next … l st〉
    257287      | joint_instr_move dst_src ⇒
    258           ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉
     288          ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉
    259289      | joint_instr_call_id id argsno ⇒
    260290        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     
    264294            ! st ← save_ra … st l;
    265295              let st ≝ save_frame … st in
    266               let regs ≝ init_locals p (joint_if_locals … fn) in
     296              let regs ≝ init_locals (sem_params_of_sem_params2 globals p) … (joint_if_locals … fn) in
    267297              let l' ≝ joint_if_entry … fn in
    268298             ret ? 〈 E0, goto … l' (set_regs … regs st)〉
     
    275305              let vs ≝ [mk_val ? evres] in
    276306            ! st ← set_result … vs st;
    277               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto … l st〉
     307              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉
    278308          ]]
    279309    | joint_st_return ⇒
     
    287317
    288318definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
    289   λglobals,p,exit,registersno,st. res_to_opt … (
     319 λglobals,p,exit,registersno,st. res_to_opt … (
    290320  do s ← fetch_statement … st;
    291321  match s with
     
    293323      do 〈st,l〉 ← fetch_ra … st;
    294324      if eq_address l exit then
    295        do val ← fetch_result globals p st registersno;
     325       do val ← fetch_result st registersno;
    296326       match val with
    297327        [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? [])
     
    301331   | _ ⇒ Error ? []]).
    302332
    303 definition joint_exec: ∀globals:list ident. sem_params2 globals → address → nat → execstep io_out io_in ≝
    304   λglobals,p.
    305   λexit.
    306   λregistersno.
    307   mk_execstep … (is_final globals p exit registersno) (m p) (eval_statement globals p).
     333record evaluation_parameters : Type[1] ≝
     334 { globals: list ident
     335 ; sparams2: sem_params2 globals
     336 ; exit: address
     337 ; registersno: nat
     338 ; genv2: genv sparams2 globals
     339 }.
     340
     341definition joint_exec: trans_system io_out io_in ≝
     342  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
     343   (λG.is_final (globals G) (sparams2 G) (exit G) (registersno G))
     344   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
     345
     346definition make_global :
     347 ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
     348  joint_program pars → evaluation_parameters
     349
     350 λpars,sparams.
     351  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
     352[1,2: cases daemon ]
     353qed.
    308354
    309355definition 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;
     356 ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
     357 ∀p: joint_program … pars. res (state (mk_sem_params pars (sparams p))) ≝
     358λpars,sparams,p.
     359  let ge ≝ genv2 (make_global pars sparams p) in
    314360  do m ← init_mem Genv … (λx.[Init_space x]) p;
    315361  let main ≝ prog_main … p in
    316362  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    317363  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    318   ?(*
    319   OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉*).
     364  ?.(* OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.*)
     365cases daemon qed.
    320366(*
    321367RTL:
     
    328374 change_carry: a 0
    329375*)
     376
    330377definition joint_fullexec :
    331  ∀globals:list ident. ∀sparams:sem_params2 globals. joint_program globals sparams (pre_sem_params … sparams) → fullexec io_out io_in ≝
    332  λglobals,p,program.
    333   let exit ≝ ? in
    334   let registersno ≝ ? in
    335   mk_fullexec ?? (joint_exec ? p exit registersno) ? (make_initial_state … p).
     378 ∀pars:params.
     379 ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
     380 fullexec io_out io_in ≝
     381 λpars,sparams.
     382  mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
Note: See TracChangeset for help on using the changeset viewer.