Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2185 r2286  
    1 include "basics/lists/list.ma".
    21include "common/Globalenvs.ma".
    32include "common/IO.ma".
    4 include "common/SmallstepExec.ma".
     3(* include "common/SmallstepExec.ma". *)
    54include "joint/BEMem.ma".
    65include "joint/Joint.ma".
     
    1211   only the head is kept (or Undef if the list is empty) ??? *)
    1312
    14 record more_sem_params (p:params_): Type[1] ≝
     13(* Paolo: I'll put in this record the property about genv we need *)
     14record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
     15{ ge :> genv_t (fundef (F globals))
     16; find_symbol_exists : ∀id.In ? globals id → find_symbol … ge id ≠ None ?
     17}.
     18
     19definition genv ≝ λp.genv_gen (joint_internal_function p).
     20coercion genv_to_genv_t :
     21  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
     22  λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
     23
     24definition cpointer ≝ Σp.ptype p = Code.
     25definition xpointer ≝ Σp.ptype p = XData.
     26unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
     27unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
     28
     29record sem_state_params : Type[1] ≝
    1530 { framesT: Type[0]
    1631 ; empty_framesT: framesT
    17  ; regsT: Type[0]
    18  ; empty_regsT: address → regsT (* Stack pointer *)
    19  ; call_args_for_main: call_args p
    20  ; call_dest_for_main: call_dest p
    21 
    22  ; greg_store_: generic_reg p → beval → regsT → res regsT
    23  ; greg_retrieve_: regsT → generic_reg p → res beval
    24  ; acca_store_: acc_a_reg p → beval → regsT → res regsT
    25  ; acca_retrieve_: regsT → acc_a_reg p → res beval
    26  ; accb_store_: acc_b_reg p → beval → regsT → res regsT
    27  ; accb_retrieve_: regsT → acc_b_reg p → res beval
    28  ; dpl_store_: dpl_reg p → beval → regsT → res regsT
    29  ; dpl_retrieve_: regsT → dpl_reg p → res beval
    30  ; dph_store_: dph_reg p → beval → regsT → res regsT
    31  ; dph_retrieve_: regsT → dph_reg p → res beval
    32  ; pair_reg_move_: regsT → pair_reg p → res regsT
     32 ; regsT : Type[0]
     33 ; empty_regsT: xpointer → regsT (* Stack pointer *)
    3334 }.
    3435
    35 record sem_params: Type[1] ≝
    36  { spp :> params_
    37  ; more_sem_pars :> more_sem_params spp
    38  }.
    39 
    40 record state (p: sem_params): Type[0] ≝
    41  { st_frms: framesT ? p
    42  ; pc: address
    43  ; sp: pointer
    44  ; isp: pointer
    45  ; carry: beval
    46  ; regs: regsT ? p
     36record state (semp: sem_state_params): Type[0] ≝
     37 { st_frms: framesT semp
     38 ; sp: xpointer
     39 ; isp: xpointer
     40 ; carry: bebit
     41 ; regs: regsT semp
    4742 ; m: bemem
    4843 }.
    4944
    50 (*
    51 definition empty_state: ∀p. more_sem_params p → state p ≝
    52  mk_state … (empty_framesT …)
    53 *)
    54 
    55 definition genv ≝ λglobals.λp:params globals. genv_t (joint_function globals p).
    56 
    57 record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] ≝
    58  { more_sparams :> more_sem_params p
    59 
    60  (*CSC: XXXX succ_pc, pointer_of_label and fetch_statement all deal with fetching
    61    should we take 'em out in a different record to simplify the code? *)
    62  ; succ_pc: succ p → address → res address
    63  ; pointer_of_label: genv … p → pointer → label → res (Σp:pointer. ptype p = Code)
    64  ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
    65 
    66  ; fetch_ra: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)) × address)
    67  ; result_regs: genv globals p → state (mk_sem_params … more_sparams) → res (list (generic_reg p))
    68 
    69  ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    70    (*CSC: save_frame returns a res only because we can call a function with the wrong number and
     45coercion sem_state_params_to_state nocomposites:
     46  ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].
     47
     48record state_pc (semp : sem_state_params) : Type[0] ≝
     49  { st_no_pc :> state semp
     50  ; pc : cpointer
     51  }.
     52
     53definition set_m: ∀p. bemem → state p → state p ≝
     54 λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     55
     56definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
     57 λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
     58
     59definition set_sp: ∀p. ? → state p → state p ≝
     60 λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
     61
     62definition set_isp: ∀p. ? → state p → state p ≝
     63 λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
     64
     65definition set_carry: ∀p. bebit → state p → state p ≝
     66 λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
     67
     68definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     69 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
     70
     71definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
     72 λp,s,st. mk_state_pc … s (pc … st).
     73
     74definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
     75 λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     76
     77axiom BadProgramCounter : String.
     78
     79definition function_of_block :
     80 ∀pars : params.
     81 ∀globals.
     82  genv pars globals →
     83  block →
     84  res (joint_internal_function pars globals) ≝
     85  λpars,globals,ge,b.
     86  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     87  match def with
     88  [ Internal def' ⇒ OK … def'
     89  | External _ ⇒ Error … [MSG BadProgramCounter]].
     90 
     91(* this can replace graph_fetch function and lin_fetch_function *)
     92definition fetch_function:
     93 ∀pars : params.
     94 ∀globals.
     95  genv pars globals →
     96  cpointer →
     97  res (joint_internal_function pars globals) ≝
     98 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
     99
     100inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
     101  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
     102  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
     103  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
     104
     105inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
     106  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
     107  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
     108  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
     109  | FEnd2  : fin_step_flow p F Call. (* end flow *)
     110
     111record more_sem_unserialized_params
     112  (uns_pars : unserialized_params)
     113  (F : list ident → Type[0]) : Type[1] ≝
     114  { st_pars :> sem_state_params (* automatic coercion has issues *)
     115  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
     116  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
     117  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
     118  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
     119  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
     120  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
     121  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
     122  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
     123  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
     124  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
     125  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
     126  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
     127  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
     128  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
     129  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
     130
     131  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
     132  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
     133  ; save_frame: cpointer → call_dest uns_pars → state st_pars → res (state st_pars)
     134   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    71135     type of arguments. To be fixed using a dependent type *)
    72  ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    73  ; pop_frame: genv globals p → state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)))
    74 
    75  ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
    76  ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    77  }.
    78 
    79 record sem_params1 (globals: list ident): Type[1] ≝
    80  { p1:> params globals
    81  ; more_sparams1:> more_sem_params1 globals p1
    82  }.
    83 
    84 record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
    85  { more_sparams_1 :> more_sem_params1 … p
    86  ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams_1) → succ p → state (mk_sem_params … more_sparams_1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams_1)))
    87  }.
    88 
    89 record sem_params2 (globals: list ident): Type[1] ≝
    90  { p2:> params globals
    91  ; more_sparams2:> more_sem_params2 globals p2
    92  }.
    93 
    94 definition sem_params_of_sem_params1 ≝ λglobals. λsp1: sem_params1 globals. mk_sem_params sp1 sp1.
    95 coercion sem_params_of_sem_params1 : ∀globals. ∀_x:sem_params1 globals. sem_params
    96  ≝ sem_params_of_sem_params1 on _x: sem_params1 ? to sem_params.
    97 
    98 definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 … sp2 sp2.
    99 coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1 globals
    100  ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1 ?.
    101 
    102 definition set_m: ∀p. bemem → state p → state p ≝
    103  λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
    104 
    105 definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
    106  λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
    107 
    108 definition set_sp: ∀p. pointer → state p → state p ≝
    109  λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
    110 
    111 definition set_isp: ∀p. pointer → state p → state p ≝
    112  λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
    113 
    114 definition set_carry: ∀p. beval → state p → state p ≝
    115  λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
    116 
    117 definition set_pc: ∀p. address → state p → state p ≝
    118  λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    119 
    120 definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
    121  λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    122 
    123 
    124 definition address_of_label: ∀globals. ∀p:sem_params1 globals. genv globals p → pointer → label → res address ≝
    125  λglobals,p,ge,ptr,l.
    126   do newptr ← pointer_of_label … p ge … ptr l ;
    127   OK … (address_of_code_pointer newptr).
    128 
    129 definition goto: ∀globals. ∀p:sem_params1 globals. genv globals p → label → state p → res (state p) ≝
    130  λglobals,p,ge,l,st.
    131   do oldpc ← pointer_of_address (pc … st) ;
    132   do newpc ← address_of_label … ge oldpc l ;
    133   OK … (set_pc … newpc st).
    134 
    135 definition next: ∀globals. ∀p:sem_params1 globals. succ … p → state p → res (state p) ≝
    136  λglobals,p,l,st.
    137   do l' ← succ_pc … p l (pc … st) ;
    138   OK … (set_pc … l' st).
    139 
    140 definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
    141  λp,dst,v,st.
    142   do regs  ← greg_store_ … dst v (regs … st);
    143   OK ? (set_regs … regs st).
    144 
    145 definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
    146  λp,st,dst.greg_retrieve_ … (regs … st) dst.
    147 
    148 definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
    149  λp,dst,v,st.
    150   do regs ← acca_store_ … dst v (regs … st);
    151   OK ? (set_regs … regs st).
    152 
    153 definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
    154  λp,st,dst.acca_retrieve_ … (regs … st) dst.
    155 
    156 definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
    157  λp,dst,v,st.
    158   do regs ← accb_store_ … dst v (regs … st);
    159   OK ? (set_regs … regs st).
    160 
    161 definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
    162  λp,st,dst.accb_retrieve_ … (regs … st) dst.
    163 
    164 definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
    165  λp,dst,v,st.
    166   do regs ← dpl_store_ … dst v (regs … st);
    167   OK ? (set_regs … regs st).
    168 
    169 definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
    170  λp,st,dst.dpl_retrieve_ … (regs … st) dst.
    171 
    172 definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
    173  λp,dst,v,st.
    174   do regs ← dph_store_ … dst v (regs … st);
    175   OK ? (set_regs … regs st).
    176 
    177 definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
    178  λp,st,dst.dph_retrieve_ … (regs … st) dst.
    179 
    180 definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → res (state p) ≝
    181  λp,st,rs.
    182   do regs ← pair_reg_move_ … (regs … st) rs;
    183   OK … (set_regs … regs st).
    184 
    185 axiom FailedStore: String.
    186 
    187 definition push: ∀p. state p → beval → res (state p) ≝
    188  λp,st,v.
    189   let isp ≝ isp … st in
    190   do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    191   let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    192   OK … (set_m … m (set_sp … isp st)).
    193 
    194 definition pop: ∀p. state p → res (state p × beval) ≝
    195  λp,st.
    196   let isp ≝ isp ? st in
    197   let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    198   let ist ≝ set_sp … isp st in
    199   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    200   OK ? 〈st,v〉.
    201 
    202 definition save_ra : ∀p. state p → address → res (state p) ≝
    203  λp,st,l.
    204   let 〈addrl,addrh〉 ≝ l in
    205   do st ← push … st addrl;
    206   push … st addrh.
    207 
    208 definition load_ra : ∀p.state p → res (state p × address) ≝
    209  λp,st.
    210   do 〈st,addrh〉 ← pop … st;
    211   do 〈st,addrl〉 ← pop … st;
    212   OK ? 〈st, 〈addrl,addrh〉〉.
    213 
    214 axiom MissingSymbol : String.
    215 axiom FailedLoad : String.
    216 axiom BadFunction : String.
     136  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
     137      state st_pars → res (state st_pars)
     138  ; fetch_external_args: external_function → state st_pars →
     139      res (list val)
     140  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
     141  ; call_args_for_main: call_args uns_pars
     142  ; call_dest_for_main: call_dest uns_pars
     143
     144  (* from now on, parameters that use the type of functions *)
     145  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
     146  (* change of pc must be left to *_flow execution *)
     147  ; eval_ext_seq: ∀globals.genv_gen F globals → ext_seq uns_pars →
     148      F globals → state st_pars → IO io_out io_in (state st_pars)
     149  ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
     150      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
     151  ; eval_ext_call: ∀globals.genv_gen F globals →
     152      ext_call uns_pars → state st_pars →
     153      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
     154  ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
     155  (* do something more in some op2 calculations (e.g. mark a register for correction
     156     with spilled_no in ERTL) *)
     157  ; post_op2 : ∀globals.genv_gen F globals →
     158    Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars →
     159    state st_pars → state st_pars
     160  }.
     161
     162(*coercion msu_pars_to_ss_pars nocomposites :
     163∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params
     164 ≝ st_pars
     165on _msup : more_sem_unserialized_params ?? to sem_state_params.*)
     166
     167
     168definition helper_def_retrieve :
     169  ∀X : ? → ? → ? → Type[0].
     170  (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
     171  ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
     172    λX,f,up,F,p,st.f ?? p (regs … st).
     173
     174definition helper_def_store :
     175  ∀X : ? → ? → ? → Type[0].
     176  (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
     177  ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
     178  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
     179
     180definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
     181definition acca_store ≝ helper_def_store ? acca_store_.
     182definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
     183definition accb_store ≝ helper_def_store ? accb_store_.
     184definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
     185definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
     186definition dpl_store ≝ helper_def_store ? dpl_store_.
     187definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
     188definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
     189definition dph_store ≝ helper_def_store ? dph_store_.
     190definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
     191definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
     192definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
     193definition pair_reg_move ≝
     194  λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
     195    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
     196    return set_regs ? r st.
     197
     198 
    217199axiom BadPointer : String.
    218200
     201(* this is preamble to all calls (including tail ones). The optional argument in
     202   input tells the function whether it has to save the frame for internal
     203   calls.
     204   the first element of the triple is the entry point of the function if
     205   it is an internal one, or false in case of an external one.
     206   The actual update of the pc is left to later, as it depends on
     207   serialization and on whether the call is a tail one. *)
    219208definition eval_call_block:
    220  ∀globals.∀p:sem_params1 globals. genv globals p → state p →
    221   block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    222  λglobals,p,ge,st,b,args,dest,ra.
    223   ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr … ge b) : IO ???;
     209 ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
     210  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
     211    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
     212 λp,F,p',globals,ge,st,b,args,dest.
     213  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    224214    match fd with
    225     [ Internal fn ⇒
    226       ! st ← save_frame … ra (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    227       let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    228       let l' ≝ joint_if_entry … fn in
    229       let st ≝ set_regs p regs st in
    230       let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) zero_offset in
    231       ! newpc ← address_of_label … ge pointer_in_fn l' ;
    232       let st ≝ set_pc … newpc st in
    233        return 〈 E0, st〉
     215    [ Internal fd ⇒
     216      return 〈Init ?? (block_id b) fd args dest, st〉
    234217    | External fn ⇒
    235       ! params ← fetch_external_args … fn st : IO ???;
     218      ! params ← fetch_external_args … p' fn st : IO ???;
    236219      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    237220      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     
    240223         fixed once we fully implement external functions. *)
    241224      let vs ≝ [mk_val ? evres] in
    242       ! st ← set_result … vs st;
    243       let st ≝ set_pc … ra st in
    244         return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    245      ].
    246 (*% qed.*)
    247 
    248 definition eval_call_id:
    249  ∀globals.∀p:sem_params1 globals. genv globals p → state p →
    250   ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    251  λglobals,p,ge,st,id,args,dest,ra.
    252   ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    253   eval_call_block … ge st b args dest ra.
    254 
    255 definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
    256  λglobals,p,ge,st.
    257   ! s ← fetch_statement … ge st : IO ???;
    258   match s return λ_. IO ??? with
    259     [ GOTO l ⇒
    260        ! st ← goto … p ge l st ;
    261        return 〈E0, st〉
    262     | sequential seq l ⇒
    263       match seq return λ_. IO ??? with
    264       [ extension c ⇒ exec_extended … p ge c l st
    265       | COST_LABEL cl ⇒
    266          ! st ← next … p l st ;
    267          return 〈Echarge cl, st〉
    268       | COMMENT c ⇒
    269          ! st ← next … p l st ;
    270          return 〈E0, st〉
    271       | INT dest v ⇒
    272          ! st ← greg_store p dest (BVByte v) st;
    273          ! st ← next … p l st ;
    274           return 〈E0, st〉
    275       | LOAD dst addrl addrh ⇒
    276         ! vaddrh ← dph_retrieve … st addrh;
    277         ! vaddrl ← dpl_retrieve … st addrl;
    278         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    279         ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    280         ! st ← acca_store p … dst v st;
    281         ! st ← next … p l st ;
    282           return 〈E0, st〉
    283       | STORE addrl addrh src ⇒
    284         ! vaddrh ← dph_retrieve … st addrh;
    285         ! vaddrl ← dpl_retrieve … st addrl;
    286         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    287         ! v ← acca_retrieve … st src;
    288         ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    289         let st ≝ set_m … m' st in
    290         ! st ← next … p l st ;
    291           return 〈E0, st〉
    292       | COND src ltrue ⇒
    293         ! v ← acca_retrieve … st src;
    294         ! b ← bool_of_beval v;
    295         if b then
    296          ! st ← goto … p ge ltrue st ;
    297          return 〈E0, st〉
    298         else
    299          ! st ← next … p l st ;
    300          return 〈E0, st〉
    301       | ADDRESS ident prf ldest hdest ⇒
    302         ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol … ge ident);
    303         ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset);
    304         ! st ← dpl_store p ldest laddr st;
    305         ! st ← dph_store p hdest haddr st;
    306         ! st ← next … p l st ;
    307           return 〈E0, st〉
    308       | OP1 op dacc_a sacc_a ⇒
    309         ! v ← acca_retrieve … st sacc_a;
    310         ! v ← Byte_of_val v;
    311           let v' ≝ BVByte (op1 eval op v) in
    312         ! st ← acca_store p dacc_a v' st;
    313         ! st ← next … p l st ;
    314           return 〈E0, st〉
    315       | OP2 op dacc_a sacc_a src ⇒
    316         ! v1 ← acca_retrieve … st sacc_a;
    317         ! v1 ← Byte_of_val v1;
    318         ! v2 ← greg_retrieve … st src;
    319         ! v2 ← Byte_of_val v2;
    320         ! carry ← bool_of_beval (carry … st);
    321           let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    322           let v' ≝ BVByte v' in
    323           let carry ≝ beval_of_bool carry in
    324         ! st ← acca_store p dacc_a v' st;
    325           let st ≝ set_carry … carry st in
    326         ! st ← next … p l st ;
    327           return 〈E0, st〉
    328       | CLEAR_CARRY ⇒
    329         ! st ← next … p l (set_carry … BVfalse st) ;
    330          return 〈E0, st〉
    331       | SET_CARRY ⇒
    332         ! st ← next … p l (set_carry … BVtrue st) ;
    333          return 〈E0, st〉
    334       | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    335         ! v1 ← acca_retrieve … st sacc_a_reg;
    336         ! v1 ← Byte_of_val v1;
    337         ! v2 ← accb_retrieve … st sacc_b_reg;
    338         ! v2 ← Byte_of_val v2;
    339           let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    340           let v1' ≝ BVByte v1' in
    341           let v2' ≝ BVByte v2' in
    342         ! st ← acca_store p dacc_a_reg v1' st;
    343         ! st ← accb_store p dacc_b_reg v2' st;
    344         ! st ← next … p l st ;
    345           return 〈E0, st〉
    346       | POP dst ⇒
    347         ! 〈st,v〉 ← pop … st;
    348         ! st ← acca_store p dst v st;
    349         ! st ← next … p l st ;
    350           return 〈E0, st〉
    351       | PUSH src ⇒
    352         ! v ← acca_retrieve … st src;
    353         ! st ← push … st v;
    354         ! st ← next … p l st ;
    355           return 〈E0, st〉
    356       | MOVE dst_src ⇒
    357         ! st ← pair_reg_move … st dst_src ;
    358         ! st ← next … p l st ;
    359           return 〈E0, st〉
    360       | CALL_ID id args dest ⇒
    361         ! ra ← succ_pc … p l (pc … st) : IO ???;         
    362           eval_call_id … p ge st id args dest ra ]
    363     | RETURN ⇒
    364       ! 〈st,ra〉 ← fetch_ra … st;
    365       ! st ← pop_frame … ge st;
    366         return 〈E0,set_pc … ra st〉].
    367 (*cases addr //
    368 qed.*)
    369 
    370 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → state p → option int ≝
     225      ! st ← set_result … p' vs dest st : IO ???;
     226      return 〈Proceed ???, st〉
     227      ].
     228
     229axiom FailedStore: String.
     230
     231definition push: ∀p.state p → beval → res (state p) ≝
     232 λp,st,v.
     233  let isp' ≝ isp ? st in
     234  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
     235  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
     236  return set_m … m (set_isp … isp'' st).
     237  normalize elim (isp p st) #p #H @H
     238qed.
     239
     240definition pop: ∀p. state p → res ((state p ) × beval) ≝
     241 λp,st.
     242  let isp' ≝ isp ? st in
     243  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
     244  let ist ≝ set_isp … isp'' st in
     245  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
     246  OK ? 〈ist,v〉.
     247  normalize elim (isp p st) #p #H @H
     248qed.
     249
     250definition save_ra : ∀p. state p → cpointer → res (state p) ≝
     251 λp,st,l.
     252  ! 〈addrl,addrh〉 ← address_of_pointer l ; (* always succeeds *)
     253  ! st' ← push … st addrl;
     254  push … st' addrh.
     255
     256definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
     257 λp,st.
     258  do 〈st',addrh〉 ← pop … st;
     259  do 〈st'',addrl〉 ← pop … st';
     260  do pr ← pointer_of_address 〈addrh, addrl〉;
     261  match ptype pr return λx.ptype pr = x → res (? × cpointer) with
     262  [ Code ⇒ λprf.return 〈st'', «pr,prf»〉
     263  | _ ⇒ λ_.Error … [MSG BadPointer]
     264  ] (refl …).
     265
     266(* parameters that are defined by serialization *)
     267record more_sem_params (pp : params) : Type[1] ≝
     268  { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp)
     269  ; offset_of_point : code_point pp → option offset (* can overflow *)
     270  ; point_of_offset : offset → code_point pp
     271  ; point_of_offset_of_point :
     272    ∀pt.opt_All ? (eq ? pt) (option_map ?? point_of_offset (offset_of_point pt))
     273  ; offset_of_point_of_offset :
     274    ∀o.offset_of_point (point_of_offset o) = Some ? o
     275  }.
     276
     277(*
     278coercion ms_pars_to_msu_pars nocomposites :
     279∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
     280 ≝ msu_pars
     281on _msp : more_sem_params ? to more_sem_unserialized_params ??.
     282
     283definition ss_pars_of_ms_pars ≝
     284  λp.λpp : more_sem_params p.
     285  st_pars … (msu_pars … pp).
     286coercion ms_pars_to_ss_pars nocomposites :
     287∀p : params.∀msp : more_sem_params p.sem_state_params ≝
     288ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
     289
     290axiom CodePointerOverflow : String.
     291
     292definition pointer_of_point : ∀p.more_sem_params p →
     293  cpointer→ code_point p → res cpointer ≝
     294  λp,msp,ptr,pt.
     295  ! o ← opt_to_res ? [MSG CodePointerOverflow] (offset_of_point ? msp pt) ;
     296  return «mk_pointer (pblock ptr) o, ?».
     297elim ptr #ptr' #EQ <EQ % qed.
     298
     299definition point_of_pointer :
     300  ∀p.more_sem_params p → cpointer → code_point p ≝
     301  λp,msp,ptr.point_of_offset p msp (poff ptr).
     302
     303lemma point_of_pointer_of_point :
     304  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
     305  pointer_of_point p msp ptr1 pt = return ptr2 →
     306  point_of_pointer p msp ptr2 = pt.
     307#p #msp #ptr1 #ptr2 #pt normalize
     308lapply (point_of_offset_of_point p msp pt)
     309cases (offset_of_point ???) normalize
     310[ * #ABS destruct(ABS)
     311| #o #EQ1 #EQ2 destruct %
     312]
     313qed.
     314
     315lemma pointer_of_point_block :
     316  ∀p,msp,ptr1,ptr2,pt.
     317  pointer_of_point p msp ptr1 pt = return ptr2 →
     318  pblock ptr2 = pblock ptr1.
     319#p #msp #ptr1 #ptr2 #pt normalize
     320cases (offset_of_point ???) normalize
     321[ #ABS destruct(ABS)
     322| #o #EQ destruct(EQ) %
     323]
     324qed.
     325
     326lemma pointer_of_point_uses_block :
     327  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
     328#p #msp ** #b1 #o1 #EQ1
     329        ** #b2 #o2 #EQ2
     330#pt #EQ3 destruct normalize //
     331qed.
     332
     333lemma pointer_of_point_of_pointer :
     334  ∀p,msp.∀ptr1,ptr2 : cpointer.
     335    pblock ptr1 = pblock ptr2 →
     336    pointer_of_point p msp ptr1 (point_of_pointer p msp ptr2) = return ptr2.
     337#p #msp ** #b1 #o1 #EQ1
     338        ** #b2 #o2 #EQ2
     339#EQ3 destruct
     340normalize >offset_of_point_of_offset normalize %
     341qed.
     342
     343axiom ProgramCounterOutOfCode : String.
     344axiom PointNotFound : String.
     345axiom LabelNotFound : String.
     346
     347definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
     348  genv p globals → cpointer →
     349  res ((joint_internal_function p globals) × (joint_statement p globals)) ≝
     350  λp,msp,globals,ge,ptr.
     351  let pt ≝ point_of_pointer ? msp ptr in
     352  ! fn ← fetch_function … ge ptr ;
     353  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
     354  return 〈fn, stmt〉.
     355 
     356definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
     357  genv p globals → cpointer → label → res cpointer ≝
     358  λp,msp,globals,ge,ptr,lbl.
     359  ! fn ← fetch_function … ge ptr ;
     360  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
     361            (point_of_label … (joint_if_code … fn) lbl) ;
     362  pointer_of_point p msp ptr pt.
     363
     364definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     365  cpointer → succ p → res cpointer ≝
     366  λp,msp,ptr,nxt.
     367  let curr ≝ point_of_pointer p msp ptr in
     368  pointer_of_point p msp ptr (point_of_succ p curr nxt).
     369
     370record sem_params : Type[1] ≝
     371  { spp :> params
     372  ; more_sem_pars :> more_sem_params spp
     373  }.
     374
     375(* definition msu_pars_of_s_pars :
     376∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
     377≝ λp : sem_params.
     378  msu_pars … (more_sem_pars p).
     379coercion s_pars_to_msu_pars nocomposites :
     380∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
     381msu_pars_of_s_pars
     382on p : sem_params to more_sem_unserialized_params ??.
     383
     384definition ss_pars_of_s_pars :
     385∀p : sem_params.sem_state_params
     386≝ λp : sem_params.
     387  st_pars … (msu_pars … (more_sem_pars p)).
     388coercion s_pars_to_ss_pars nocomposites :
     389∀p : sem_params.sem_state_params ≝
     390ss_pars_of_s_pars
     391on _p : sem_params to sem_state_params.
     392
     393definition ms_pars_of_s_pars :
     394∀p : sem_params.more_sem_params (spp p)
     395≝ more_sem_pars.
     396coercion s_pars_to_ms_pars nocomposites :
     397∀p : sem_params.more_sem_params (spp p) ≝
     398ms_pars_of_s_pars
     399on p : sem_params to more_sem_params ?.*)
     400
     401(* definition address_of_label: ∀globals. ∀p:sem_params.
     402  genv globals p → pointer → label → res address ≝
     403 λglobals,p,ge,ptr,l.
     404  do newptr ← pointer_of_label … p ? ge … ptr l ;
     405  OK … (address_of_code_pointer newptr). *)
     406
     407definition goto: ∀globals.∀p : sem_params.
     408  genv p globals → label → state p → cpointer → res (state_pc p) ≝
     409 λglobals,p,ge,l,st,b.
     410  ! newpc ← pointer_of_label ? p … ge b l ;
     411  return mk_state_pc ? st newpc.
     412
     413(*
     414definition empty_state: ∀p. more_sem_params p → state p ≝
     415 mk_state … (empty_framesT …)
     416*)
     417
     418definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p) ≝
     419 λp,l,st,pc.
     420 ! newpc ← succ_pc ? p … pc l ;
     421 return mk_state_pc … st newpc.
     422
     423axiom MissingSymbol : String.
     424axiom FailedLoad : String.
     425axiom BadFunction : String.
     426axiom SuccessorNotProvided : String.
     427
     428definition eval_seq_no_pc :
     429 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals →
     430  state p → ∀s:joint_seq p globals.
     431  IO io_out io_in (state p) ≝
     432 λp,globals,ge,curr_fn,st,seq.
     433 match seq return λx.IO ??? with
     434  [ extension_seq c ⇒
     435    eval_ext_seq … ge c curr_fn st
     436  | LOAD dst addrl addrh ⇒
     437    ! vaddrh ← dph_arg_retrieve … st addrh ;
     438    ! vaddrl ← dpl_arg_retrieve … st addrl;
     439    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     440    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
     441    acca_store p … dst v st
     442 | STORE addrl addrh src ⇒
     443    ! vaddrh ← dph_arg_retrieve … st addrh;
     444    ! vaddrl ← dpl_arg_retrieve … st addrl;
     445    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     446    ! v ← acca_arg_retrieve … st src;
     447    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
     448    return set_m … m' st
     449  | ADDRESS id prf ldest hdest ⇒
     450    let addr ≝ opt_safe ? (find_symbol … ge id) ? in
     451    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset) ;
     452    ! st' ← dpl_store … ldest laddr st;
     453    dph_store … hdest haddr st'
     454  | OP1 op dacc_a sacc_a ⇒
     455    ! v ← acca_retrieve … st sacc_a;
     456    ! v' ← be_op1 op v ;
     457    acca_store … dacc_a v' st
     458  | OP2 op dacc_a sacc_a src ⇒
     459    ! v1 ← acca_arg_retrieve … st sacc_a;
     460    ! v2 ← snd_arg_retrieve … st src;
     461    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
     462    ! st' ← acca_store … dacc_a v' st;
     463    return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')
     464  | CLEAR_CARRY ⇒
     465    return set_carry … (BBbit false) st
     466  | SET_CARRY ⇒
     467    return set_carry … (BBbit true) st
     468  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     469    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     470    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
     471    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
     472    ! st' ← acca_store … dacc_a_reg v1' st;
     473    accb_store … dacc_b_reg v2' st'
     474  | POP dst ⇒
     475    ! 〈st',v〉 ← pop p st;
     476    acca_store … p dst v st'
     477  | PUSH src ⇒
     478    ! v ← acca_arg_retrieve … st src;
     479    push … st v
     480  | MOVE dst_src ⇒
     481    pair_reg_move … st dst_src
     482  | CALL_ID id args dest ⇒
     483    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     484    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
     485    return st'
     486  | extension_call s ⇒
     487    !〈flow, st'〉 ← eval_ext_call … ge s st ;
     488    return st'
     489  | _ ⇒ return st
     490  ].
     491  @find_symbol_exists
     492  lapply prf
     493  elim globals [*]
     494  #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
     495  #G %2 @IH @G
     496  qed.
     497
     498definition eval_seq_pc :
     499 ∀p:sem_params.∀globals. genv p globals → state p →
     500  ∀s:joint_seq p globals.
     501  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
     502  λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
     503  [ CALL_ID id args dest ⇒
     504    ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     505    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
     506    return flow
     507  | extension_call s ⇒
     508    !〈flow, st'〉 ← eval_ext_call … ge s st ;
     509    return flow
     510  | _ ⇒ return Proceed ???
     511  ].
     512
     513definition eval_step :
     514 ∀p:sem_params.∀globals. genv p globals →
     515  joint_internal_function p globals → state p →
     516  ∀s:joint_step p globals.
     517  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
     518  λp,globals,ge,curr_fn,st,s.
     519  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
     520  [ step_seq s ⇒
     521    ! flow ← eval_seq_pc ?? ge st s ;
     522    ! st' ← eval_seq_no_pc ?? ge curr_fn st s ;
     523    return 〈flow,st'〉
     524  | COND src ltrue ⇒
     525    ! v ← acca_retrieve … st src;
     526    ! b ← bool_of_beval v;
     527    if b then
     528      return 〈Redirect ??? ltrue, st〉
     529    else
     530      return 〈Proceed ???, st〉
     531  ].
     532  %1 % qed.
     533
     534definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
     535  (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p.
     536  IO io_out io_in (state p) ≝
     537 λp,globals,ge,curr_fn,st,s.
     538  match s return λx.IO ??? with
     539    [ tailcall c ⇒
     540      !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
     541      return st'
     542    | _ ⇒ return st
     543    ].
     544
     545definition eval_fin_step_pc :
     546 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p →
     547  ∀s:joint_fin_step p.
     548  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
     549  λp,g,ge,curr_fn,st,s.
     550  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
     551  [ tailcall c ⇒
     552    !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
     553    return flow 
     554  | GOTO l ⇒ return FRedirect … l
     555  | RETURN ⇒ return FEnd1 ??
     556  ]. %1 % qed.
     557
     558definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
     559  state p → Z → joint_internal_function p globals → call_args p →
     560  res (state_pc p) ≝
     561  λp,globals,ge,st,id,fn,args.
     562    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
     563              args st ;
     564    let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
     565    let l' ≝ joint_if_entry … fn in
     566    let st' ≝ set_regs p regs st in
     567    let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
     568    ! pc ← pointer_of_point ? p … pointer_in_fn l' ;
     569    return mk_state_pc ? st' pc. % qed.
     570
     571(* The pointer provided is the one to the *next* instruction. *)
     572definition eval_step_flow :
     573 ∀p:sem_params.∀globals.∀flows.genv p globals →
     574 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
     575 λp,globals,flows,ge,st,nxt,cmd.
     576 match cmd with
     577  [ Redirect _ l ⇒
     578    goto … ge l st nxt
     579  | Init id fn args dest ⇒
     580    ! st' ← save_frame … nxt dest st ;
     581    do_call ?? ge st' id fn args
     582  | Proceed _ ⇒
     583    return mk_state_pc ? st nxt
     584  ].
     585
     586definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals →
     587  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
     588  λp,globals,lbls,ge,st,curr,cmd.
     589  match cmd with
     590  [ FRedirect _ l ⇒ goto … ge l st curr
     591  | FTailInit id fn args ⇒
     592    do_call … ge st id fn args
     593  | _ ⇒
     594    ! 〈st',ra〉 ← fetch_ra … st ;
     595    ! fn ← fetch_function … ge curr ;
     596    ! st'' ← pop_frame … ge fn st';
     597    return mk_state_pc ? st'' ra
     598  ].
     599
     600definition eval_statement :
     601 ∀globals.∀p:sem_params.genv p globals →
     602  state_pc p → joint_internal_function p globals → joint_statement p globals →
     603    IO io_out io_in (state_pc p) ≝
     604 λglobals,p,ge,st,curr_fn,stmt.
     605 match stmt with
     606 [ sequential s nxt ⇒
     607   ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ;
     608   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
     609   eval_step_flow … ge st' nxtptr flow
     610 | final s ⇒
     611   ! st' ← eval_fin_step_no_pc … ge curr_fn st s ;
     612   ! flow ← eval_fin_step_pc … ge curr_fn st s ;
     613   eval_fin_step_flow … ge st' (pc … st) flow
     614 ].
     615
     616definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
     617  state_pc p → IO io_out io_in (state_pc p) ≝
     618  λglobals,p,ge,st.
     619  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
     620  eval_statement … ge st fn s.
     621
     622(* Paolo: what if in an intermediate language main finishes with an external
     623  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
     624  not static... *)
     625definition is_final: ∀globals:list ident. ∀p: sem_params.
     626  genv p globals → cpointer → state_pc p → option int ≝
    371627 λglobals,p,ge,exit,st.res_to_opt ? (
    372   do s ← fetch_statement … ge st;
     628  do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st);
    373629  match s with
    374    [ RETURN ⇒
    375       do 〈st,ra〉 ← fetch_ra … st;
    376       if eq_address ra exit then
    377        do regs ← result_regs … ge st ;
    378        do vals ← mmap … (λreg.greg_retrieve … st reg) regs ;
     630  [ final s' ⇒
     631    match s' with
     632    [ RETURN ⇒
     633      do 〈st',ra〉 ← fetch_ra … st;
     634      if eq_pointer ra exit then
     635       do vals ← read_result … ge (joint_if_result … fn) st' ;
    379636       Word_of_list_beval vals
    380637      else
    381        Error ? []
    382    | _ ⇒ Error ? []]).
    383 
     638       Error ? [ ]
     639   | _ ⇒ Error ? [ ]
     640   ]
     641 | _ ⇒ Error ? [ ]
     642 ]).
     643
     644(*
    384645record evaluation_parameters : Type[1] ≝
    385646 { globals: list ident
    386  ; sparams2: sem_params2 globals
    387  ; exit: address
    388  ; genv2: genv globals sparams2
     647 ; sparams:> sem_params
     648 ; exit: cpointer
     649 ; genv2: genv globals sparams
    389650 }.
    390651
     652(* Paolo: with structured traces, eval need not emit labels. However, this
     653  changes trans_system. For now, just putting a dummy thing for
     654  the transition. *)
    391655definition joint_exec: trans_system io_out io_in ≝
    392   mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
    393    (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G))
    394    (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
     656  mk_trans_system … evaluation_parameters (λG. state_pc G)
     657   (λG.is_final (globals G) G (genv2 G) (exit G))
     658   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
    395659
    396660definition make_global :
    397  ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
     661 ∀pars: sem_params.
    398662  joint_program pars → evaluation_parameters
    399663
    400  λpars,sparams.
     664 λpars.
    401665 (* Invariant: a -1 block is unused in common/Globalenvs *)
    402666 let b ≝ mk_block Code (-1) in
    403  let ptr ≝ mk_pointer b zero_offset in
    404  let addr ≝ address_of_code_pointer ptr in
    405   (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv_noinit … p)).
     667 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
     668  (λp. mk_evaluation_parameters
     669    (prog_var_names … p)
     670    (mk_sem_params … pars)
     671    ptr
     672    (globalenv_noinit … p)
     673  ).
    406674% qed.
    407675
    408676axiom ExternalMain: String.
     677
    409678definition make_initial_state :
    410  ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
    411  ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
    412 λpars,sparams,p.
    413   let sem_globals ≝ make_global pars sparams p in
     679 ∀pars: sem_params.
     680 ∀p: joint_program … pars. res (state_pc pars) ≝
     681λpars,p.
     682  let sem_globals ≝ make_global pars p in
    414683  let ge ≝ genv2 sem_globals in
    415684  let m ≝ alloc_mem … p in
    416685  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    417686  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    418   let dummy_pc ≝ mk_pointer (mk_block Code (-1)) zero_offset in
    419   let spp ≝ mk_pointer spb (offset_of_Z external_ram_size) in
    420   let ispp ≝ mk_pointer ispb (offset_of_Z 47) in
    421   do sp ← address_of_pointer spp ;
     687  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
     688  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
     689  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
    422690  let main ≝ prog_main … p in
    423   let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
    424   let trace_state ≝
    425    eval_call_id … (mk_sem_params1 … (sparams …)) ge st0 main (call_args_for_main … (sparams …))
    426     (call_dest_for_main … (sparams …)) (exit sem_globals) in
    427   match trace_state with
    428   [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
    429   | Wrong msg ⇒ Error … msg
    430   | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    431   ].
    432 (*[3: % | cases ispb | cases spb] *; #r #off #E >E %
    433 qed.*)
     691  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
     692  (* use exit sem_globals as ra and call_dest_for_main as dest *)
     693  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
     694  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
     695  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
     696  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
     697  match main_fd with
     698  [ Internal fn ⇒
     699    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
     700  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
     701  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
     702qed.
    434703
    435704definition joint_fullexec :
    436  ∀pars:∀globals.params globals.
    437  ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
    438  fullexec io_out io_in ≝
    439  λpars,sparams.
    440   mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
     705 ∀pars:sem_params.fullexec io_out io_in ≝
     706 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
     707*)
Note: See TracChangeset for help on using the changeset viewer.