Changeset 2457 for src/joint


Ignore:
Timestamp:
Nov 13, 2012, 11:30:23 AM (7 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

Location:
src/joint
Files:
3 edited
1 moved

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2437 r2457  
    2828params : adds type of code and related properties *)
    2929
     30(*
    3031inductive possible_flows : Type[0] ≝
    3132| Labels : list label → possible_flows
    3233| Call : possible_flows.
     34*)
    3335
    3436inductive argument (T : Type[0]) : Type[0] ≝
     
    8284 (* other instructions not fitting in the general framework *)
    8385 ; ext_seq : Type[0]
    84 (* ; ext_branch : Type[0]
    85  ; ext_branch_labels : ext_branch → list label*)
    86  ; ext_call : Type[0]
    87  ; ext_tailcall : Type[0]
     86 ; has_tailcalls : bool
    8887 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
    8988 ; paramsT : Type[0]
     
    143142  step_seq on _s : joint_seq ?? to joint_step ??.
    144143
    145 definition step_flows ≝ λp,globals.λs : joint_step p globals.
    146   match s with
    147   [ step_seq s ⇒
    148     match s with
    149     [ CALL _ _ _ ⇒ Call
    150     | _ ⇒ Labels … [ ]
    151     ]
    152   | COND _ l ⇒ Labels … [l]
    153   ].
    154 
    155144definition step_labels ≝
    156145  λp, globals.λs : joint_step p globals.
    157     match step_flows … s with
    158     [ Labels lbls ⇒ lbls
    159     | Call ⇒ [ ]
    160     ].
     146  match s with
     147  [ step_seq s ⇒ [ ]
     148  | COND _ l ⇒ [l]
     149  ].
    161150
    162151definition step_forall_labels : ∀p.∀globals.
     
    173162  | GOTO: label → joint_fin_step p
    174163  | RETURN: joint_fin_step p
    175   | tailcall : ext_tailcall p → joint_fin_step p.
    176 
    177 definition fin_step_flows ≝ λp.λs : joint_fin_step p.
     164  | TAILCALL :
     165    has_tailcalls p → (ident + (dpl_arg p) × (dph_arg p)) →
     166    call_args p → joint_fin_step p.
     167
     168definition fin_step_labels ≝ λp.λs : joint_fin_step p.
    178169  match s with
    179   [ GOTO l ⇒ Labels … [l]
    180   | tailcall _ ⇒ Call (* tailcalls will need to be integrated in structured traces *)
    181   | _ ⇒ Labels … [ ]
     170  [ GOTO l ⇒ [l]
     171  | _ ⇒ [ ]
    182172  ].
    183 
    184 definition fin_step_labels ≝
    185   λp.λs : joint_fin_step p.
    186     match fin_step_flows … s with
    187     [ Labels lbls ⇒ lbls
    188     | Call ⇒ [ ]
    189     ].
    190173
    191174inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    192175  | sequential: joint_step p globals → succ p → joint_statement p globals
    193176  | final: joint_fin_step p → joint_statement p globals.
    194 
    195 coercion extension_fin_to_fin_step : ∀p : stmt_params.
    196   ∀s : ext_tailcall p.joint_fin_step p ≝
    197   tailcall on _s : ext_tailcall ? to joint_fin_step ?.
    198177
    199178coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
  • src/joint/Traces.ma

    r2443 r2457  
    99(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    1010 }.
    11  
     11
     12axiom is_internal_function_of_program :
     13  ∀p:params.joint_program p → ident → Prop.
     14
     15axiom is_internal_function_of_program_ok :
     16  ∀p.∀prog:joint_program p.∀i.is_internal_function ?? (globalenv_noinit ? prog) i →
     17  is_internal_function_of_program p prog i.
     18
    1219record prog_params : Type[1] ≝
    1320 { prog_spars : sem_params
    1421 ; prog : joint_program prog_spars
     22 ; stack_sizes : (Σi.is_internal_function_of_program prog_spars prog i) → ℕ
    1523(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    1624 }.
     
    2735  (prog_spars pars)
    2836  «ptr, refl …»
    29   (mk_genv_gen ?? (globalenv_noinit ? p) ?)
     37  (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»))
    3038 (* (prog_io pars) *).
    31 (* TODO or TOBEFOUND *)
    32 cases daemon
     39[ @is_internal_function_of_program_ok @(pi2 … i)
     40| (* TODO or TOBEFOUND *)
     41  cases daemon
     42]
    3343qed.
    3444
     
    3646≝ make_global on _p : prog_params to evaluation_params.
    3747
    38 
    39 axiom ExternalMain : String.
     48axiom BadMain : String.
    4049
    4150definition make_initial_state :
     
    5665  ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
    5766  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    58   ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
    59   ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
    60   match main_fd with
    61   [ Internal fn ⇒
    62     do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
    63   | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    64   ].
     67  ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ;
     68  match ? return λx.description_of_function … main = x → ? with
     69  [ Internal fn ⇒ λprf.
     70    let main : Σi : ident.is_internal_function ???? ≝ «main, ?» in
     71    ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
     72    ! pc' ← eval_internal_call_pc … ge main ;
     73    return mk_state_pc … st' pc'
     74  | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
     75  ] (refl …).
    6576  [ %
     77  | @(description_of_internal_function … prf)
    6678  | cases spb normalize //
    6779  ]
    6880qed.
    6981
    70 definition step_flow_classifier :
    71   ∀p : evaluation_params.∀F,flows.
    72   step_flow p F flows → status_class ≝
    73   λp,F,flows,flow.match flow with
    74   [ Redirect _ _ ⇒ cl_jump
    75   | Init bl _ _ _ ⇒
    76     match symbol_for_block … (ev_genv p) (mk_block Code bl) with
    77     [ Some f ⇒ cl_call
    78     | None ⇒ cl_other (* we don't care, as call will fail anyway *)
    79     ]
    80   | Proceed flows ⇒
    81     match flows with
    82     [ Labels lbls ⇒
    83       match lbls with
    84       [ nil ⇒ cl_other
    85       | _ ⇒ cl_jump
    86       ]
    87     | _ ⇒ cl_other
    88     ]
     82definition joint_classify :
     83  ∀p : evaluation_params.state_pc p → status_class ≝
     84  λp,st.
     85  match fetch_statement ? p … (ev_genv p) (pc … st) with
     86  [ OK f_s ⇒
     87    let 〈f, s〉 ≝ f_s in
     88    match s with
     89    [ sequential s _ ⇒
     90      match s with
     91      [ step_seq s ⇒
     92        match s with
     93        [ CALL f' args dest ⇒
     94          match function_of_call ?? (ev_genv p) st f' with
     95          [ OK fn ⇒
     96            match description_of_function … fn with
     97            [ Internal _ ⇒ cl_call
     98            | External _ ⇒ cl_other
     99            ]
     100          | Error _ ⇒ cl_other
     101          ]
     102        | _ ⇒ cl_other
     103        ]
     104      | COND _ _ ⇒ cl_jump
     105      ]
     106    | final s ⇒
     107      match s with
     108      [ GOTO _ ⇒ cl_other
     109      | RETURN ⇒ cl_return
     110      | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
     111      ]
     112    ]
     113  | Error _ ⇒ cl_other
    89114  ].
    90115
    91 definition fin_step_flow_classifier :
    92   ∀p : evaluation_params.∀F,flows.
    93   fin_step_flow p F flows → status_class ≝
    94   λp,F,flows,flow.match flow with
    95   [ FRedirect lbls _ ⇒
    96     match lbls with
    97     [ nil ⇒ (* not really possible, we don't care *) cl_other
    98     | cons _ tl ⇒
    99       match tl with
    100       [ nil ⇒ (* only one label *) cl_other
    101       | _ ⇒ (* fork *) cl_jump
    102       ]
    103     ]
    104   | FTailInit bl _ _ ⇒ (* not implemented for now, probably needs new class *)
    105     cl_other
    106   | _ ⇒ cl_return
    107   ].
     116lemma joint_classify_call : ∀p : evaluation_params.∀st.
     117  joint_classify p st = cl_call →
     118  ∃f,f',args,dest,next,fn,fd.
     119  fetch_statement ? p … (ev_genv p) (pc … st) =
     120    OK ? 〈f, sequential … (CALL … f' args dest) next〉 ∧
     121  function_of_call … (ev_genv p) st f' = OK ? fn ∧
     122  description_of_function … (ev_genv p) fn = Internal … fd.
     123#p #st
     124whd in match joint_classify; normalize nodelta
     125lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st)))
     126elim (fetch_statement ?????) in ⊢ (???%→%);
     127[ * #f * [| * [ #lbl || #b #f #args ]]
     128  [ * [| #a #lbl #next ]
     129    [ *
     130      [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b'
     131      | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
     132      | #ext ] #next
     133      [ normalize nodelta
     134        lapply (refl … (function_of_call … (ev_genv p) st f'))
     135        elim (function_of_call ?????) in ⊢ (???%→%);
     136        [ #fn normalize nodelta
     137          lapply (refl … (description_of_function … (ev_genv p) fn))
     138          elim (description_of_function ????) in ⊢ (???%→%); #fd
     139          #EQfd
     140        | #e
     141        ] #EQfn
     142      ]
     143    ]
     144  ]
     145| #e
     146] #EQfetch
     147[|*: #ABS normalize in ABS; destruct(ABS) ]
     148normalize nodelta #_
     149%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/
     150qed.
     151
     152definition joint_call_ident : ∀p:evaluation_params.
     153  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
     154λp,st.
     155match ?
     156return λx.
     157  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
     158  match s with
     159  [ sequential s next ⇒
     160    match s with
     161    [ step_seq s ⇒
     162      match s with
     163      [ CALL f' args dest ⇒
     164        function_of_call … (ev_genv p) st f'
     165      | _ ⇒ Error … [ ]
     166      ]
     167    | _ ⇒ Error … [ ]
     168    ]
     169  | _ ⇒ Error … [ ]
     170  ] = x → ? with
     171[ OK v ⇒ λ_.v
     172| Error e ⇒ λABS.⊥
     173] (refl …).
     174@hide_prf
     175elim (joint_classify_call … (pi2 … st))
     176#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
     177lapply ABS -ABS
     178>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
     179qed.
    108180
    109181definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
     
    150222   (* as_pc ≝ *) cpointerDeq
    151223   (* as_pc_of ≝ *) (pc …)
    152    (* as_classify ≝ *)
    153     (λs.
    154       match (
    155         ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???;
    156         match stmt with
    157         [ sequential stp nxt ⇒
    158           ! 〈flow, s'〉  ← (* io_evaluate … (io_env p s) *) (eval_step … (ev_genv p) fn s stp) ;
    159           return step_flow_classifier … flow
    160         | final stp ⇒
    161           ! flow ← (* io_evaluate … (io_env p s) *) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
    162           return fin_step_flow_classifier … flow
    163         ]) with
    164       [ Value c ⇒ c
    165       | _ ⇒ cl_other
    166       ])
     224   (* as_classify ≝ *) (joint_classify p)
    167225   (* as_label_of_pc ≝ *)
    168226    (λpc.
     
    177235      succ_pc p p (pc … s1) nxt = return pc … s2)
    178236   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
    179    (* as_call_ident_≝ *)
    180    (λst.?). cases daemon (* TODO *) qed.
     237   (* as_call_ident ≝ *) (joint_call_ident p).
  • src/joint/semantics.ma

    r2443 r2457  
    1111   only the head is kept (or Undef if the list is empty) ??? *)
    1212
     13definition is_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).
     14  λi : ident.∃fd.
     15    ! bl ← find_symbol … ge i ;
     16    find_funct_ptr … ge bl = Some ? fd.
     17
     18definition description_of_function : ∀F,globals,ge.(Σi.is_function F globals ge i) →
     19fundef (F globals) ≝
     20λF,globals,ge,i.
     21match ! bl ← find_symbol … ge i ;
     22        find_funct_ptr … ge bl
     23return λx.(∃fd.x = ?) → ?
     24with
     25[ Some fd ⇒ λ_.fd
     26| None ⇒ λprf.⊥
     27] (pi2 … i).
     28cases prf #fd #ABS destruct
     29qed.
     30
     31definition is_internal_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)).
     32  λi : ident.∃fd.
     33    ! bl ← find_symbol … ge i ;
     34    find_funct_ptr … ge bl = Some ? (Internal ? fd).
     35
     36lemma description_of_internal_function : ∀F,globals,ge,i,fn.
     37  description_of_function F globals ge i = Internal ? fn → is_internal_function … ge i.
     38#F #globals #ge * #i * #fd #EQ
     39#fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ
     40%{EQ}
     41qed.
     42
     43lemma internal_function_is_function : ∀F,globals,ge,i.
     44  is_internal_function F globals ge i → is_function … ge i.
     45#F #globals #ge #i * #fn #prf %{prf} qed.
     46
     47definition if_of_function : ∀F,globals,ge.(Σi.is_internal_function F globals ge i) →
     48F globals ≝
     49λF,globals,ge,i.
     50match ! bl ← find_symbol … ge i ;
     51        find_funct_ptr … ge bl
     52return λx.(∃fn.x = ?) → ?
     53with
     54[ Some fd ⇒
     55  match fd return λx.(∃fn.Some ? x = ?) → ? with
     56  [ Internal fn ⇒ λ_.fn
     57  | External _ ⇒ λprf.⊥
     58  ]
     59| None ⇒ λprf.⊥
     60] (pi2 … i).
     61cases prf #fn #ABS destruct
     62qed.
     63
    1364(* Paolo: I'll put in this record the property about genv we need *)
    1465record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
    1566{ ge :> genv_t (fundef (F globals))
    1667; find_symbol_exists : ∀id.In ? globals id → find_symbol … ge id ≠ None ?
     68; stack_sizes : (Σi.is_internal_function F globals ge i) → ℕ
    1769}.
    1870
     
    102154axiom BadProgramCounter : String.
    103155
    104 definition function_of_block :
    105  ∀pars : params.
    106  ∀globals.
    107   genv pars globals →
    108   block →
    109   res (joint_closed_internal_function pars globals) ≝
    110   λpars,globals,ge,b.
    111   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    112   match def with
    113   [ Internal def' ⇒ OK … def'
    114   | External _ ⇒ Error … [MSG BadProgramCounter]].
    115  
    116 (* this can replace graph_fetch function and lin_fetch_function *)
    117 definition fetch_function:
    118  ∀pars : params.
    119  ∀globals.
    120   genv pars globals →
    121   cpointer →
    122   res (joint_closed_internal_function pars globals) ≝
    123  λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
    124 
     156(*
    125157inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
    126158  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
     
    133165  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
    134166  | FEnd2  : fin_step_flow p F Call. (* end flow *)
     167*)
     168
     169definition funct_of_ident : ∀F,globals,ge.
     170  ident → option (Σi.is_function F globals ge i)
     171≝ λF,globals,ge,i.
     172match ?
     173return λx.! bl ← find_symbol … ge i ;
     174    find_funct_ptr … ge bl = x → ?
     175with
     176[ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»
     177| None ⇒ λ_.None ?
     178] (refl …).
     179
     180lemma match_opt_prf_elim : ∀A,B : Type[0].∀m : option A.
     181∀Q : option A → Prop.
     182∀c1 : ∀a.Q (Some ? a) → B.
     183∀c2 : Q (None ?) → B.
     184∀P : B → Prop.
     185(∀a,prf.P (c1 a prf)) →
     186(∀prf.P (c2 prf)) →
     187∀prf : Q m.
     188P (match m return λx.Q x → ? with
     189   [ Some a ⇒ λprf.c1 a prf
     190   | None ⇒ λprf.c2 prf
     191   ] prf).
     192#A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf
     193normalize [@H1 | @H2]
     194qed.
     195
     196lemma symbol_of_function_block_ok :
     197  ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf).
     198#F #ge #b #FFP
     199whd in ⊢ (???(??%));
     200@match_opt_prf_elim [//] #H @⊥
     201(* cut and paste from global env *)
     202whd in H:(??%?);
     203cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
     204cases (functions_inv … ge b FFP)
     205#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
     206lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
     207cases (find ????)
     208[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
     209| * #id' #b' #_ normalize #_ #E destruct
     210] qed.
     211
     212definition funct_of_block : ∀F,globals,ge.
     213  block → option  (Σi.is_function F globals ge i) ≝
     214λF,globals,ge,bl.
     215   match find_funct_ptr … ge bl
     216   return λx.find_funct_ptr … ge bl = x → ? with
     217   [ Some fd ⇒ λprf.return mk_Sig
     218        ident (λi.is_function F globals ge i)
     219        (symbol_of_function_block … ge bl ?)
     220        (ex_intro … fd ?)
     221   | None ⇒ λ_.None ?
     222   ] (refl …).
     223[ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf
     224| >prf % #ABS destruct(ABS)
     225]
     226qed.
     227
     228definition int_funct_of_block : ∀F,globals,ge.
     229  block → option (Σi.is_internal_function F globals ge i) ≝
     230  λF,globals,ge,bl.
     231  ! f ← funct_of_block … ge bl ;
     232  match ?
     233  return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i)
     234  with
     235  [ Internal fn ⇒ λprf.return «pi1 … f, ?»
     236  | External fn ⇒ λ_.None ?
     237  ] (refl …).
     238@(description_of_internal_function … prf)
     239qed.
     240
     241definition funct_of_bevals : ∀F,globals,ge.
     242  beval → beval → option (Σi.is_function F globals ge i) ≝
     243λF,globals,ge,dpl,dph.
     244! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;
     245if eq_bv … (bv_zero …) (offv (poff ptr)) ∧
     246   match ptype ptr with [ Code ⇒ true | _ ⇒ false] then
     247   funct_of_block … (pblock ptr)
     248else None ?.
     249
     250definition block_of_funct_ident ≝ λF,globals,ge.
     251  λi : Σi.is_function F globals ge i.
     252  match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with
     253  [ Some bl ⇒ λ_.bl
     254  | None ⇒ λprf.⊥
     255  ] (pi2 … i).
     256cases prf #fd normalize #ABS destruct(ABS)
     257qed.
     258
     259axiom ProgramCounterOutOfCode : String.
     260axiom PointNotFound : String.
     261axiom LabelNotFound : String.
     262axiom MissingSymbol : String.
     263axiom FailedLoad : String.
     264axiom BadFunction : String.
     265axiom SuccessorNotProvided : String.
     266axiom BadPointer : String.
     267
     268(* this can replace graph_fetch function and lin_fetch_function *)
     269definition fetch_function:
     270 ∀pars : params.
     271 ∀globals.
     272 ∀ge : genv pars globals.
     273  cpointer →
     274  res (Σi.is_internal_function … ge i) ≝
     275 λpars,globals,ge,p.
     276 opt_to_res … [MSG BadFunction; MSG BadPointer]
     277    (int_funct_of_block … ge (pblock p)).
    135278
    136279record sem_unserialized_params
     
    138281  (F : list ident → Type[0]) : Type[1] ≝
    139282  { st_pars :> sem_state_params
     283
    140284  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
    141285  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
     
    161305  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
    162306      state st_pars → res (state st_pars)
    163   ; fetch_external_args: external_function → state st_pars →
     307  ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
    164308      res (list val)
    165309  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
     
    170314  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
    171315  (* change of pc must be left to *_flow execution *)
    172   ; eval_ext_seq: ∀globals.genv_gen F globals → ext_seq uns_pars →
    173       F globals → state st_pars → IO io_out io_in (state st_pars)
    174   ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
    175       F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
    176   ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
    177       state st_pars → IO io_out io_in ident
    178   ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
    179   (* do something more in some op2 calculations (e.g. mark a register for correction
    180      with spilled_no in ERTL) *)
    181   ; post_op2 : ∀globals.genv_gen F globals →
    182     Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars →
    183     state st_pars → state st_pars
     316  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
     317    (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars)
     318  ; pop_frame: ∀globals.∀ge : genv_gen F globals.
     319    (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars)
    184320  }.
    185321
     
    220356    return set_regs ? r st.
    221357 
    222 axiom BadPointer : String.
    223 
    224 (* this is preamble to all calls (including tail ones). The optional argument in
    225    input tells the function whether it has to save the frame for internal
    226    calls.
    227    the first element of the triple is the entry point of the function if
    228    it is an internal one, or false in case of an external one.
    229    The actual update of the pc is left to later, as it depends on
    230    serialization and on whether the call is a tail one. *)
    231 definition eval_call_block:
    232  ∀p,F.∀p':sem_unserialized_params p F.∀globals.
    233   genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
    234     IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
    235  λp,F,p',globals,ge,st,b,args,dest.
    236   ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    237     match fd with
    238     [ Internal fd ⇒
    239       return 〈Init ?? (block_id b) fd args dest, st〉
    240     | External fn ⇒
    241       ! params ← fetch_external_args … p' fn st : IO ???;
    242       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    243       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    244       (* CSC: XXX bug here; I think I should split it into Byte-long
    245          components; instead I am making a singleton out of it. To be
    246          fixed once we fully implement external functions. *)
    247       let vs ≝ [mk_val ? evres] in
    248       ! st ← set_result … p' vs dest st : IO ???;
    249       return 〈Proceed ???, st〉
    250       ].
    251 
    252358axiom FailedStore: String.
    253359
     
    355461qed.
    356462
    357 axiom ProgramCounterOutOfCode : String.
    358 axiom PointNotFound : String.
    359 axiom LabelNotFound : String.
    360 
    361463definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
    362   genv p globals → cpointer →
    363   res ((joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
     464  ∀ge:genv p globals. cpointer →
     465  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
    364466  λp,msp,globals,ge,ptr.
     467  let bl ≝ pblock ptr in
     468  ! f ← opt_to_res … [MSG BadFunction; MSG BadPointer]
     469    (int_funct_of_block … ge bl) ;
     470  let fn ≝ if_of_function … f in
    365471  let pt ≝ point_of_pointer ? msp ptr in
    366   ! fn ← fetch_function … ge ptr ;
    367472  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
    368   return 〈fn, stmt〉.
    369  
     473  return 〈f, stmt〉.
     474
    370475definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    371476  genv p globals → cpointer → label → res cpointer ≝
    372477  λp,msp,globals,ge,ptr,lbl.
    373   ! fn ← fetch_function … ge ptr ;
     478  ! f ← fetch_function … ge ptr ;
     479  let fn ≝ if_of_function …  ge f in
    374480  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
    375481            (point_of_label … (joint_if_code … fn) lbl) ;
     
    435541 return mk_state_pc … st newpc.
    436542
    437 axiom MissingSymbol : String.
    438 axiom FailedLoad : String.
    439 axiom BadFunction : String.
    440 axiom SuccessorNotProvided : String.
    441 
    442 definition block_of_call ≝ λp:sem_params.λglobals.
     543
     544definition function_of_call ≝ λp:sem_params.λglobals.
    443545  λge: genv p globals.λst : state p.λf.
    444546  match f with
    445547  [ inl id ⇒
    446     opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id)
     548    opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id)
    447549  | inr addr ⇒
    448550    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    449551    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    450     ! ptr ← pointer_of_bevals [addr_l ; addr_h] ;
    451     if eq_bv … (bv_zero …) (offv (poff … ptr)) then
    452       return pblock ptr
    453     else Error … [MSG BadFunction]
     552    opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h)
    454553  ].
    455554
     555(* Paolo: why external calls do not need args?? *)
     556definition eval_external_call ≝
     557λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.
     558      ! params ← fetch_external_args … p' fn st args : IO ???;
     559      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     560      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     561      (* CSC: XXX bug here; I think I should split it into Byte-long
     562         components; instead I am making a singleton out of it. To be
     563         fixed once we fully implement external functions. *)
     564      let vs ≝ [mk_val ? evres] in
     565      set_result … p' vs dest st.
     566
     567lemma block_of_funct_ident_is_code : ∀F,globals,ge,i.
     568  block_region (block_of_funct_ident F globals ge i) = Code.
     569#F #globals #ge * #i * #fd
     570whd in ⊢ (?→??(?%)?);
     571cases (find_symbol ???)
     572[ #ABS normalize in ABS; destruct(ABS) ]
     573#bl normalize nodelta >m_return_bind
     574whd in ⊢ (??%?→?); cases (block_region bl)
     575[ #ABS normalize in ABS; destruct(ABS) ]
     576#_ %
     577qed.
     578
     579definition eval_internal_call_pc ≝
     580λp : sem_params.λglobals : list ident.λge : genv p globals.λi.
     581let fn ≝ if_of_function … ge i in
     582let l' ≝ joint_if_entry ?? fn in
     583let pointer_in_fn ≝ mk_pointer (block_of_funct_ident … ge (pi1 … i)) (mk_offset (bv_zero …)) in
     584pointer_of_point ? p … pointer_in_fn l'.
     585[ @block_of_funct_ident_is_code
     586| cases i /2 by internal_function_is_function/
     587]
     588qed.
     589
     590definition eval_internal_call_no_pc ≝
     591λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st.
     592let fn ≝ if_of_function … ge i in
     593let stack_size ≝ stack_sizes … ge i in
     594! st' ← setup_call … stack_size (joint_if_params … fn) args st ;
     595let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
     596return set_regs p regs st.
     597
    456598definition eval_seq_no_pc :
    457  ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals
    458   state p → ∀s:joint_seq p globals.
     599 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i)
     600  state p → cpointer → joint_seq p globals →
    459601  IO io_out io_in (state p) ≝
    460  λp,globals,ge,curr_fn,st,seq.
     602 λp,globals,ge,curr_fn,st,next,seq.
    461603 match seq return λx.IO ??? with
    462604  [ extension_seq c ⇒
     
    489631    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
    490632    ! st' ← acca_store … dacc_a v' st;
    491     return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')
     633    return set_carry … carry st'
    492634  | CLEAR_CARRY ⇒
    493635    return set_carry … (BBbit false) st
     
    509651    pair_reg_move … st dst_src
    510652  | CALL f args dest ⇒
    511     ! b ← block_of_call … ge st f : IO ???;
    512     ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    513     return st'
     653    ! fn ← function_of_call … ge st f : IO ???;
     654    match description_of_function … fn return λx.description_of_function … fn = x → ? with
     655    [ Internal fd ⇒ λprf.
     656      ! st' ← save_frame … next dest st ;
     657      eval_internal_call_no_pc … ge «fn, ?» args st'  (* only pc changes *)
     658    | External fd ⇒ λ_.eval_external_call … fd args dest st
     659    ] (refl …)
    514660  | _ ⇒ return st
    515661  ].
    516   @find_symbol_exists
     662[ @find_symbol_exists
    517663  lapply prf
    518664  elim globals [*]
    519665  #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
    520666  #G %2 @IH @G
    521   qed.
    522 
    523 definition eval_seq_pc :
    524  ∀p:sem_params.∀globals. genv p globals → state p →
    525   ∀s:joint_seq p globals.
    526   IO io_out io_in (step_flow p ? (step_flows … s)) ≝
    527   λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
     667| @(description_of_internal_function … prf)
     668]
     669qed.
     670
     671definition eval_seq_pc :
     672 ∀p:sem_params.∀globals.∀ge:genv p globals.
     673  state p → cpointer → joint_seq p globals →
     674  res cpointer ≝
     675  λp,globals,ge,st,next,s.
     676  match s with
    528677  [ CALL f args dest ⇒
    529     ! b ← block_of_call … ge st f : IO ???;
    530     ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    531     return flow
    532   | _ ⇒ return Proceed ???
     678    ! fn ← function_of_call … ge st f;
     679    match ? return λx.description_of_function … fn = x → ? with
     680    [ Internal _ ⇒ λprf.eval_internal_call_pc … ge «fn, ?»
     681    | External _ ⇒ λ_.return next
     682    ] (refl …)
     683  | _ ⇒ return next
    533684  ].
    534 
    535 definition eval_step :
    536  ∀p:sem_params.∀globals. genv p globals →
    537   joint_closed_internal_function p globals → state p →
    538   ∀s:joint_step p globals.
    539   IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
    540   λp,globals,ge,curr_fn,st,s.
    541   match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
    542   [ step_seq s ⇒
    543     ! flow ← eval_seq_pc ?? ge st s ;
    544     ! st' ← eval_seq_no_pc ?? ge curr_fn st s ;
    545     return 〈flow,st'〉
    546   | COND src ltrue ⇒
    547     ! v ← acca_retrieve … st src;
    548     ! b ← bool_of_beval v;
    549     if b then
    550       return 〈Redirect ??? ltrue, st〉
    551     else
    552       return 〈Proceed ???, st〉
     685@(description_of_internal_function … prf)
     686qed.
     687
     688definition eval_statement :
     689 ∀p:sem_params.∀globals.∀ge:genv p globals.
     690 (Σi.is_internal_function … ge i) → state_pc p →
     691  ∀s:joint_statement p globals.
     692  IO io_out io_in (state_pc p) ≝
     693  λp,g,ge,curr_fn,st,s.
     694  match s with
     695  [ sequential s next ⇒
     696    ! next_ptr ← succ_pc ? p (pc … st) next : IO ??? ;
     697    match s return λ_.IO ??? with
     698    [ step_seq s ⇒
     699      ! st' ← eval_seq_no_pc … ge curr_fn st next_ptr s ;
     700      ! pc' ← eval_seq_pc … ge st next_ptr s ;
     701      return mk_state_pc … st' pc'
     702    | COND a l ⇒
     703      ! v ← acca_retrieve … st a ;
     704      ! b ← bool_of_beval … v ;
     705      ! pc' ←
     706        if b then
     707          pointer_of_label ? p … ge (pc … st) l
     708        else
     709          succ_pc ? p (pc … st) next ;
     710      return mk_state_pc … st pc'
     711    ]
     712  | final s ⇒
     713    match s with
     714    [ GOTO l ⇒
     715      ! pc' ← pointer_of_label ? p ? ge (pc … st) l ;
     716      return mk_state_pc … st pc'
     717    | RETURN ⇒
     718      ! st' ← pop_frame … curr_fn st ;
     719      ! 〈pc', st''〉 ← fetch_ra … p st' ;
     720      return mk_state_pc … st'' pc'
     721    | TAILCALL _ f args ⇒
     722      ! fn ← function_of_call … ge st f : IO ???;
     723      match ? return λx.description_of_function … fn = x → ? with
     724      [ Internal _ ⇒ λprf.
     725        ! pc' ← eval_internal_call_pc … ge «fn, ?» ;
     726        return mk_state_pc … st pc'
     727      | External fd ⇒ λ_.
     728        let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in
     729        ! st' ← eval_external_call ??? fd args curr_dest st ;
     730        ! st'' ← pop_frame … curr_fn st ;
     731        ! 〈pc', st'''〉 ← fetch_ra … p st'' ;
     732        return mk_state_pc … st''' pc'
     733      ] (refl …)
     734    ]
    553735  ].
    554   %1 % qed.
    555 
    556 definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
    557   (* current function *) joint_closed_internal_function p globals → state p → ∀s : joint_fin_step p.
    558   IO io_out io_in (state p) ≝
    559  λp,globals,ge,curr_fn,st,s.
    560   match s return λx.IO ??? with
    561     [ tailcall c ⇒
    562       !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
    563       return st'
    564     | _ ⇒ return st
    565     ].
    566 
    567 definition eval_fin_step_pc :
    568  ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → state p →
    569   ∀s:joint_fin_step p.
    570   IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
    571   λp,g,ge,curr_fn,st,s.
    572   match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
    573   [ tailcall c ⇒
    574     !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
    575     return flow 
    576   | GOTO l ⇒ return FRedirect … l
    577   | RETURN ⇒ return FEnd1 ??
    578   ]. %1 % qed.
    579 
    580 definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
    581   state p → Z → joint_closed_internal_function p globals → call_args p →
    582   res (state_pc p) ≝
    583   λp,globals,ge,st,id,fn,args.
    584     ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
    585               args st ;
    586     let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
    587     let l' ≝ joint_if_entry … fn in
    588     let st' ≝ set_regs p regs st in
    589     let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
    590     ! pc ← pointer_of_point ? p … pointer_in_fn l' ;
    591     return mk_state_pc ? st' pc. % qed.
    592 
    593 (* The pointer provided is the one to the *next* instruction. *)
    594 definition eval_step_flow :
    595  ∀p:sem_params.∀globals.∀flows.genv p globals →
    596  state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
    597  λp,globals,flows,ge,st,nxt,cmd.
    598  match cmd with
    599   [ Redirect _ l ⇒
    600     goto … ge l st nxt
    601   | Init id fn args dest ⇒
    602     ! st' ← save_frame … nxt dest st ;
    603     do_call ?? ge st' id fn args
    604   | Proceed _ ⇒
    605     return mk_state_pc ? st nxt
    606   ].
    607 
    608 definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals →
    609   state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
    610   λp,globals,lbls,ge,st,curr,cmd.
    611   match cmd with
    612   [ FRedirect _ l ⇒ goto … ge l st curr
    613   | FTailInit id fn args ⇒
    614     do_call … ge st id fn args
    615   | _ ⇒
    616     ! 〈ra, st'〉 ← fetch_ra … st ;
    617     ! fn ← fetch_function … ge curr ;
    618     ! st'' ← pop_frame … ge fn st';
    619     return mk_state_pc ? st'' ra
    620   ].
    621 
    622 definition eval_statement :
    623  ∀globals.∀p:sem_params.genv p globals →
    624   state_pc p → joint_closed_internal_function p globals → joint_statement p globals →
    625     IO io_out io_in (state_pc p) ≝
    626  λglobals,p,ge,st,curr_fn,stmt.
    627  match stmt with
    628  [ sequential s nxt ⇒
    629    ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ;
    630    ! nxtptr ← succ_pc ? p (pc … st) nxt ;
    631    eval_step_flow … ge st' nxtptr flow
    632  | final s ⇒
    633    ! st' ← eval_fin_step_no_pc … ge curr_fn st s ;
    634    ! flow ← eval_fin_step_pc … ge curr_fn st s ;
    635    eval_fin_step_flow … ge st' (pc … st) flow
    636  ].
     736@(description_of_internal_function … prf)
     737qed.
    637738
    638739definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
     
    640741  λglobals,p,ge,st.
    641742  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
    642   eval_statement … ge st fn s.
     743  eval_statement … ge fn st s.
    643744
    644745(* Paolo: what if in an intermediate language main finishes with an external
     
    648749  genv p globals → cpointer → state_pc p → option int ≝
    649750 λglobals,p,ge,exit,st.res_to_opt ? (
    650   do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st);
     751  do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
     752  let fn ≝ if_of_function … f in
    651753  match s with
    652754  [ final s' ⇒
Note: See TracChangeset for help on using the changeset viewer.