Changeset 2954


Ignore:
Timestamp:
Mar 26, 2013, 3:52:39 PM (4 years ago)
Author:
tranquil
Message:

resolved circular dependency for ERTLptr's semantics

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptr_semantics.ma

    r2946 r2954  
    1717
    1818definition eval_ertlptr_seq:
    19  ∀F. ∀globals. genv_gen F globals →
     19 ∀F.∀globals. genv_gen F globals →
    2020  ertlptr_seq → ident → state ERTL_state →
    2121   res (state ERTL_state) ≝
     
    2323  match stm with
    2424   [ ertlptr_ertl seq ⇒ eval_ertl_seq F globals ge seq id st
    25    | LOW_ADDRESS r l ⇒  ! pc_lab ← get_pc_from_label … ge id l;
     25   | LOW_ADDRESS r l ⇒  ! pc_lab ← gen_pc_from_label … ge id l;
    2626                        let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
    2727                        ps_reg_store_status r addrl st
    28    | HIGH_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge id l;
     28   | HIGH_ADDRESS r l ⇒ ! pc_lab ← gen_pc_from_label … ge id l;
    2929                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
    3030                        ps_reg_store_status r addrh st
  • src/joint/joint_semantics.ma

    r2952 r2954  
    1818; stack_sizes : ident → option ℕ
    1919; premain : F globals
     20; pc_from_label : (Σbl.block_region bl = Code) → F globals → label →
     21    option program_counter
    2022}.
    21 
    22 definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
    23 coercion genv_to_genv_t :
    24   ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
    25   λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
    26 
    27 record sem_state_params : Type[1] ≝
    28  { framesT: Type[0]
    29  ; empty_framesT: framesT
    30  ; regsT : Type[0]
    31  (* empty_regsT called at the start of each function call *)
    32  ; empty_regsT: xpointer → regsT (* initial stack pointer *)
    33  ; load_sp : regsT → res xpointer
    34  ; save_sp : regsT → xpointer → regsT
    35  }.
    36 
    37 inductive internal_stack : Type[0] ≝
    38 | empty_is : internal_stack
    39 | one_is : beval → internal_stack
    40 | both_is : beval → beval → internal_stack.
    41 
    42 definition is_push : internal_stack → beval → res internal_stack ≝
    43 λis,bv.match is with
    44 [ empty_is ⇒ return one_is bv
    45 | one_is bv' ⇒ return both_is bv' bv
    46 | both_is _ _ ⇒ Error … [MSG … InternalStackFull]
    47 ].
    48 
    49 definition is_pop : internal_stack → res (beval × internal_stack) ≝
    50 λis.match is with
    51 [ empty_is ⇒ Error … [MSG … InternalStackEmpty]
    52 | one_is bv' ⇒ return 〈bv', empty_is〉
    53 | both_is bv bv' ⇒ return 〈bv', one_is bv〉
    54 ].
    55 
    56 record state (semp: sem_state_params): Type[0] ≝
    57  { st_frms: option(framesT semp)
    58  ; istack : internal_stack
    59  ; carry: bebit
    60  ; regs: regsT semp
    61  ; m: bemem
    62  ; stack_usage : ℕ
    63  }.
    64 
    65 definition sp ≝ λp,st.load_sp p (regs ? st).
    66 
    67 record state_pc (semp : sem_state_params) : Type[0] ≝
    68   { st_no_pc :> state semp
    69   ; pc : program_counter
    70   (* for correctness reasons: pc of last popped calling address (null_pc at the start) *)
    71   ; last_pop : program_counter
    72   }.
    73 
    74 definition init_pc : program_counter ≝
    75   mk_program_counter «mk_block (-1), refl …» one.
    76 
    77 definition null_pc : Pos →  program_counter ≝ λpos.
    78     mk_program_counter «dummy_block_code, refl …» pos.
    79 
    80 definition set_m: ∀p. bemem → state p → state p ≝
    81  λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m (stack_usage … st).
    82 
    83 definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    84  λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st) (stack_usage … st).
    85 
    86 definition set_sp: ∀p. ? → state p → state p ≝
    87  λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
    88  mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st) (stack_usage … st).
    89 
    90 definition set_carry: ∀p. bebit → state p → state p ≝
    91  λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st) (stack_usage … st).
    92 
    93 definition set_istack: ∀p. internal_stack → state p → state p ≝
    94  λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st) (stack_usage … st).
    95 
    96 definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
    97  λp,pc,st. mk_state_pc … (st_no_pc … st) pc (last_pop … st).
    98 
    99 definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
    100  λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
    101 
    102 definition set_last_pop: ∀p.state p → program_counter → state_pc p ≝
    103  λp,st,pc. mk_state_pc … st pc pc.
    104 
    105 definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    106  λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st) (stack_usage … st).
    107 
    108 (*
    109 inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
    110   | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
    111   | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
    112   | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
    113 
    114 inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
    115   | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
    116   | FTailInit : Z → F → call_args p → fin_step_flow p F Call
    117   | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
    118   | FEnd2  : fin_step_flow p F Call. (* end flow *)
    119 *)
    12023
    12124definition pre_main_id : ident ≝ an_identifier … one.
     
    14750 | _ ⇒ Error … [MSG BadFunction]
    14851 ].
    149  
     52
     53definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
     54λbl.match block_region bl
     55  return λx.block_region bl = x → option (Σb.block_region b = Code) with
     56  [ Code ⇒ λprf.Some ? «bl, prf»
     57  | XData ⇒ λ_.None ?
     58  ] (refl …).
     59
     60definition block_of_funct_id ≝  λF.
     61  λge: genv_t F.λid.
     62  opt_to_res … [MSG BadFunction; CTX … id] (
     63    ! bl ← find_symbol … ge id;
     64    code_block_of_block bl).
     65
     66(* this is equal to pc_of_label defined later, but can be used in
     67   generic definitions of mk_sem_unserialised_params *)
     68definition gen_pc_from_label :
     69  ∀F.∀globals.
     70  genv_gen F globals →
     71  ident (* current function *) → label → res program_counter ≝
     72  λF,g,ge,id,lbl.
     73  ! bl ← block_of_funct_id … ge id ;
     74  ! 〈ignore, f_def〉 ← fetch_internal_function … ge bl ;
     75  opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
     76    (pc_from_label … ge bl f_def lbl).
     77
     78definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
     79coercion genv_to_genv_t :
     80  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
     81  λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
     82
     83record sem_state_params : Type[1] ≝
     84 { framesT: Type[0]
     85 ; empty_framesT: framesT
     86 ; regsT : Type[0]
     87 (* empty_regsT called at the start of each function call *)
     88 ; empty_regsT: xpointer → regsT (* initial stack pointer *)
     89 ; load_sp : regsT → res xpointer
     90 ; save_sp : regsT → xpointer → regsT
     91 }.
     92
     93inductive internal_stack : Type[0] ≝
     94| empty_is : internal_stack
     95| one_is : beval → internal_stack
     96| both_is : beval → beval → internal_stack.
     97
     98definition is_push : internal_stack → beval → res internal_stack ≝
     99λis,bv.match is with
     100[ empty_is ⇒ return one_is bv
     101| one_is bv' ⇒ return both_is bv' bv
     102| both_is _ _ ⇒ Error … [MSG … InternalStackFull]
     103].
     104
     105definition is_pop : internal_stack → res (beval × internal_stack) ≝
     106λis.match is with
     107[ empty_is ⇒ Error … [MSG … InternalStackEmpty]
     108| one_is bv' ⇒ return 〈bv', empty_is〉
     109| both_is bv bv' ⇒ return 〈bv', one_is bv〉
     110].
     111
     112record state (semp: sem_state_params): Type[0] ≝
     113 { st_frms: option(framesT semp)
     114 ; istack : internal_stack
     115 ; carry: bebit
     116 ; regs: regsT semp
     117 ; m: bemem
     118 ; stack_usage : ℕ
     119 }.
     120
     121definition sp ≝ λp,st.load_sp p (regs ? st).
     122
     123record state_pc (semp : sem_state_params) : Type[0] ≝
     124  { st_no_pc :> state semp
     125  ; pc : program_counter
     126  (* for correctness reasons: pc of last popped calling address (null_pc at the start) *)
     127  ; last_pop : program_counter
     128  }.
     129
     130definition init_pc : program_counter ≝
     131  mk_program_counter «mk_block (-1), refl …» one.
     132
     133definition null_pc : Pos →  program_counter ≝ λpos.
     134    mk_program_counter «dummy_block_code, refl …» pos.
     135
     136definition set_m: ∀p. bemem → state p → state p ≝
     137 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m (stack_usage … st).
     138
     139definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
     140 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st) (stack_usage … st).
     141
     142definition set_sp: ∀p. ? → state p → state p ≝
     143 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
     144 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st) (stack_usage … st).
     145
     146definition set_carry: ∀p. bebit → state p → state p ≝
     147 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st) (stack_usage … st).
     148
     149definition set_istack: ∀p. internal_stack → state p → state p ≝
     150 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st) (stack_usage … st).
     151
     152definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     153 λp,pc,st. mk_state_pc … (st_no_pc … st) pc (last_pop … st).
     154
     155definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
     156 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
     157
     158definition set_last_pop: ∀p.state p → program_counter → state_pc p ≝
     159 λp,st,pc. mk_state_pc … st pc pc.
     160
     161definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
     162 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st) (stack_usage … st).
     163
     164(*
     165inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
     166  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
     167  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
     168  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
     169
     170inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
     171  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
     172  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
     173  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
     174  | FEnd2  : fin_step_flow p F Call. (* end flow *)
     175*)
     176
    150177(* lemma fetch_internal_function_minus_one :
    151178  ∀F,V,i,p,bl.
     
    483510qed.
    484511
    485 definition code_block_of_block : block → option (Σb.block_region b = Code) ≝
    486 λbl.match block_region bl
    487   return λx.block_region bl = x → option (Σb.block_region b = Code) with
    488   [ Code ⇒ λprf.Some ? «bl, prf»
    489   | XData ⇒ λ_.None ?
    490   ] (refl …).
    491 
    492 definition block_of_funct_id ≝  λF.λsp:sem_state_params.
    493   λge: genv_t F.λid.
    494   opt_to_res … [MSG BadFunction; CTX … id] (
    495     ! bl ← find_symbol … ge id;
    496     code_block_of_block bl).
    497 
    498 definition get_pc_from_label :
    499   ∀p : sem_params.∀globals.
    500   genv p globals →
    501   ident (* current function *) → label → res program_counter ≝
    502   λp,g,ge,id,lbl.
    503   ! bl ← block_of_funct_id … p ge id ;
    504   pc_of_label … ge bl lbl.
    505    
    506512definition block_of_call ≝ λp : sem_params.
    507513  λglobals.λge: genv_t (joint_function p globals).λf.λst : state p.
  • src/joint/semanticsUtils.ma

    r2952 r2954  
    405405λp,prog,stacksizes.
    406406let genv ≝ globalenv … (λx.x) prog in
    407 mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog).
     407let pc_from_lbl ≝ λbl.λfn : joint_closed_internal_function p ?.λlbl.
     408  ! pt ← point_of_label … (joint_if_code … fn) lbl ;
     409  return mk_program_counter bl (offset_of_point … p pt) in
     410mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog) pc_from_lbl.
    408411#s #H
    409412elim (find_symbol_exists ?? (λx.x) … prog s ?)
    410413[ #bl #EQ >EQ % #ABS destruct ]
    411414@Exists_append_r
    412 @(Exists_mp … H) //
     415@(Exists_mp … H) @sym_eq
    413416qed.
    414417
Note: See TracChangeset for help on using the changeset viewer.