Changeset 2443 for src/joint


Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (7 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

Location:
src/joint
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r2422 r2443  
    66record hw_register_env : Type[0] ≝
    77  { reg_env : BitVectorTrie beval 6
    8   ; carry_bit : bebit
    98  ; other_bit : bebit
    109  }.
    1110
    1211definition empty_hw_register_env: hw_register_env ≝
    13   mk_hw_register_env (Stub …) BBundef BBundef.
     12  mk_hw_register_env (Stub …) BBundef.
    1413
    1514include alias "ASM/BitVectorTrie.ma".
     
    2019definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
    2120 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
    22   (carry_bit env) (other_bit env).
    23 
    24 definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝
    25 λv,env.mk_hw_register_env (reg_env env) v (other_bit env).
     21  (other_bit env).
    2622
    2723definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
    28 λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v.
    29 
     24λv,env.mk_hw_register_env (reg_env env) v.
     25
     26definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
     27λenv.
     28let spl ≝ hwreg_retrieve env RegisterSPL in
     29let sph ≝ hwreg_retrieve env RegisterSPH in
     30! ptr ← pointer_of_address 〈spl, sph〉 ;
     31match ptype ptr return λx.ptype ptr = x → res xpointer with
     32[ XData ⇒ λprf.return «ptr, prf»
     33| _ ⇒ λ_.Error … [MSG BadPointer]
     34] (refl …).
     35
     36definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
     37λenv,sp.
     38let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
     39hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
    3040
    3141(*** Store/retrieve on pseudo-registers ***)
    3242include alias "common/Identifiers.ma".
    3343
     44record reg_sp : Type[0] ≝
     45{ reg_sp_env :> identifier_map RegisterTag beval
     46; stackp : xpointer
     47}.
     48
    3449axiom BadRegister : String.
    3550
     
    3954 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
    4055
     56definition reg_sp_store ≝ λreg,v,locals.
     57! locals' ← reg_store reg v (reg_sp_env locals) ;
     58return mk_reg_sp locals' (stackp locals).
     59
     60definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
     61
    4162(*** Store/retrieve on hardware registers ***)
    4263
    4364definition init_hw_register_env: xpointer → hw_register_env ≝
    44  λsp.
    45   let 〈dpl,dph〉 ≝
    46     match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
    47     [ OK p ⇒ λ_.p
    48     | _ ⇒ λprf.⊥
    49     ] (refl …) in
    50   let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
    51    hwreg_store RegisterDPL dpl env.
    52 @hide_prf
    53 normalize in prf; destruct(prf)
    54 qed.
     65 λsp.hwreg_store_sp empty_hw_register_env sp.
    5566
    5667(******************************** GRAPHS **************************************)
     
    150161
    151162definition make_sem_graph_params :
    152   ∀pars : graph_params.
    153   ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
     163  ∀pars : unserialized_params.
     164  ∀g_pars : ∀F.sem_unserialized_params pars F.
    154165  sem_params ≝
    155   λpars,g_pars.
     166  λpars,spars.
     167  let g_pars ≝ mk_graph_params pars in
    156168  mk_sem_params
    157     pars
     169    g_pars
    158170    (mk_more_sem_params
    159       pars
    160171      g_pars
     172      (spars ?)
    161173      graph_offset_of_label
    162174      graph_label_of_offset
     
    187199  λo.nat_of_bitvector ? (offv o).
    188200
    189 
    190201definition make_sem_lin_params :
    191   ∀pars : lin_params.
    192   ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
     202  ∀pars : unserialized_params.
     203  (∀F.sem_unserialized_params pars F) →
    193204  sem_params ≝
    194   λpars,g_pars.
     205  λpars,spars.
     206  let lin_pars ≝ mk_lin_params pars in
    195207  mk_sem_params
    196     pars
     208    lin_pars
    197209    (mk_more_sem_params
    198       pars
    199       g_pars
     210      lin_pars
     211      (spars ?)
    200212      lin_offset_of_nat
    201213      lin_nat_of_offset
  • src/joint/Traces.ma

    r2442 r2443  
    77 ; exit: cpointer
    88 ; ev_genv: genv sparams globals
    9  ; io_env : state sparams → ∀o:io_out.res (io_in o)
     9(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    1010 }.
    1111 
     
    1313 { prog_spars : sem_params
    1414 ; prog : joint_program prog_spars
    15  ; prog_io : state prog_spars → ∀o.res (io_in o)
     15(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    1616 }.
    1717
     
    2828  «ptr, refl …»
    2929  (mk_genv_gen ?? (globalenv_noinit ? p) ?)
    30   (prog_io pars).
     30 (* (prog_io pars) *).
    3131(* TODO or TOBEFOUND *)
    3232cases daemon
     
    4949  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
    5050  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
    51   let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in
     51(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    5252  let main ≝ prog_main … p in
    53   let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in
     53  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
     54  let st0' ≝ set_sp … spp st0 in
    5455  (* use exit sem_globals as ra and call_dest_for_main as dest *)
    55   ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
    56   let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
     56  ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
     57  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    5758  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
    5859  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
     
    6364  ].
    6465  [ %
    65   | cases ispb
    66   | cases spb
    67   ] normalize //
     66  | cases spb normalize //
     67  ]
    6868qed.
    6969
     
    114114qed.
    115115
     116(*
    116117let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
    117118  match c with
     
    122123  | Wrong e ⇒ Error … e
    123124  ].
     125*)
    124126
    125127definition cost_label_of_stmt :
     
    145147   (* as_status ≝ *) (state_pc p)
    146148   (* as_execute ≝ *)
    147     (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
     149    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
    148150   (* as_pc ≝ *) cpointerDeq
    149151   (* as_pc_of ≝ *) (pc …)
     
    151153    (λs.
    152154      match (
    153         ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) ;
     155        ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???;
    154156        match stmt with
    155157        [ sequential stp nxt ⇒
    156           ! 〈flow, s'〉  ← io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) ;
     158          ! 〈flow, s'〉  ← (* io_evaluate … (io_env p s) *) (eval_step … (ev_genv p) fn s stp) ;
    157159          return step_flow_classifier … flow
    158160        | final stp ⇒
    159           ! flow ← io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
     161          ! flow ← (* io_evaluate … (io_env p s) *) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
    160162          return fin_step_flow_classifier … flow
    161163        ]) with
    162       [ OK c ⇒ c
    163       | Error _ ⇒ cl_other
     164      [ Value c ⇒ c
     165      | _ ⇒ cl_other
    164166      ])
    165167   (* as_label_of_pc ≝ *)
     
    175177      succ_pc p p (pc … s1) nxt = return pc … s2)
    176178   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
    177    (* as_call_ident_≝ *) ?. cases daemon (* TODO *) qed.
     179   (* as_call_ident_≝ *)
     180   (λst.?). cases daemon (* TODO *) qed.
  • src/joint/TranslateUtils.ma

    r2286 r2443  
    22include "joint/blocks.ma".
    33include "utilities/hide.ma".
     4include "utilities/deqsets.ma".
    45
    56(* general type of functions generating fresh things *)
     
    6465    add_graph … mid (final … (\snd b)) def
    6566  ].
     67
     68(* ignoring register allocation for now *)
     69
     70definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
     71λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
     72
     73lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).
     74#tag #A * #l * #m whd in ⊢ (%→?%);
     75elim (lookup tag ???)
     76[ * #ABS elim (ABS ?) %
     77| #a #_ %
     78] qed.
     79
     80lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.
     81#tag #A * #l * #m whd in ⊢ (?%→%);
     82elim (lookup tag ???)
     83[ * | #a * % #ABS destruct(ABS) ] qed.
     84
     85(*
     86lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
     87  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
     88  〈id, u'〉 = fresh tag u →
     89  ¬id ∈ l.
     90#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
     91[ #hd_fresh #tl_fresh #EQfresh
     92  whd in ⊢ (?(?%));
     93  change with (eq_identifier ???) in match (?==?);
     94  >eq_identifier_sym
     95  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
     96  normalize nodelta @(IH … tl_fresh EQfresh)
     97| #_ %
     98]
     99qed.
     100*)
     101
     102lemma fresh_was_fresh : ∀tag,id,id',u,u'.
     103〈id,u'〉 = fresh tag u →
     104fresh_for_univ tag id' u' →
     105id' ≠ id →
     106fresh_for_univ tag id' u.
     107#tag * #id * #id' * #u * #u'
     108normalize #EQfresh destruct
     109#H #NEQ
     110elim (le_to_or_lt_eq … H)
     111[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
     112#H >(succ_injective … H) in NEQ;
     113* #G elim (G (refl …))
     114qed.
     115
     116
     117(* use Russell? *)
     118axiom adds_graph_list_ok :
     119  ∀g_pars,globals,b,src,def.
     120  fresh_for_univ … src (joint_if_luniverse … def) →
     121  luniverse_ok ?? def →
     122  let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in
     123  luniverse_ok ?? def' ∧
     124  ∃l.bool_to_Prop (uniqueb … l) ∧
     125     All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
     126                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     127     src ~❨b,l❩~> dst in joint_if_code … def'.
     128(* #p #g #l elim l
     129[ #src #def #_ #Hdef whd
     130  %{Hdef} %{[ ]} %%%
     131| #hd #tl #IH #src #def #src_fresh #Hdef
     132  whd in match (adds_graph_list ?????);
     133  whd in match (fresh_label ???);
     134  @(pair_elim … (fresh ??)) normalize nodelta
     135  #mid #luniverse' #EQfresh
     136  whd in ⊢ (match % with [ _ ⇒ ?]);
     137  letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
     138  cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
     139  [ cases def // ] #EQ_aux
     140  lapply (IH mid def' ??)
     141  [ #l whd in match def'; #Hpres
     142    lapply (present_to_memb … Hpres) -Hpres
     143    >mem_set_add @eq_identifier_elim
     144    [ #EQ destruct(EQ) *
     145    | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux
     146      #l_in
     147    ]
     148    @(fresh_remains_fresh … (sym_eq … EQfresh))
     149    [2: @Hdef @memb_to_present ] assumption
     150  | whd in match def';
     151    cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
     152    whd in match (set_luniverse ????);
     153    @(fresh_is_fresh … (sym_eq … EQfresh))
     154  ]
     155  elim (adds_graph_list ?????) #def'' #mid' normalize nodelta
     156  * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)}
     157  % [ % ]
     158  [ whd in ⊢ (?%);
     159    elim (true_or_false_Prop (mid∈l)) #H >H normalize nodelta
     160    [ elim (All_memb … Hl2 H)
     161      cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in ⊢ (%→?);
     162      #H #_ @(absurd ?? H)
     163      @(fresh_remains_fresh … (eqEQfresh)
     164      normalize #H10 #H11
     165     
     166    >(All_fresh_not_memb … (sym_eq … EQfresh))
     167    [ assumption ]
     168    @(All_mp … Hl2) #lbl *
     169    cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
     170    normalize #EQfresh #H #lbl_not_mid
     171    lapply(fresh_remains_fresh … H (sym_eq … EQfresh))
     172   
     173    elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l
     174    [ normalize
     175*)
    66176
    67177(* preserves first statement if a cost label (should be an invariant) *)
     
    132242  ].
    133243
     244 
     245
    134246(* translation with inline fresh register allocation *)
    135247definition b_graph_translate :
  • src/joint/lineariseProof.ma

    r2442 r2443  
    2020definition graph_abstract_status:
    2121 ∀p:unserialized_params.
    22   (∀F.more_sem_unserialized_params p F) →
     22  (∀F.sem_unserialized_params p F) →
    2323    joint_program (mk_graph_params p) →
    2424     abstract_status
     
    2727  joint_abstract_status
    2828   (mk_prog_params
    29     (make_sem_graph_params (mk_graph_params p) (p' ?))
    30     prog ⊥).
    31 @daemon (* I/O, TODO *)
    32 qed.
     29    (make_sem_graph_params p p')
     30    prog).
    3331
    3432definition lin_abstract_status:
    3533 ∀p:unserialized_params.
    36   (∀F.more_sem_unserialized_params p F) →
     34  (∀F.sem_unserialized_params p F) →
    3735    joint_program (mk_lin_params p) →
    3836     abstract_status
     
    4139  joint_abstract_status
    4240   (mk_prog_params
    43     (make_sem_lin_params (mk_lin_params p) (p' ?))
    44     prog ⊥).
    45 @daemon (* I/O, TODO *)
    46 qed.
     41    (make_sem_lin_params p p')
     42    prog).
    4743
    4844definition linearise_status_rel:
  • src/joint/semantics.ma

    r2437 r2443  
    3333 ; empty_framesT: framesT
    3434 ; regsT : Type[0]
    35  ; empty_regsT: xpointer → regsT (* Stack pointer *)
     35 ; empty_regsT: xpointer → regsT (* initial stack pointer *)
     36 ; load_sp : regsT → res xpointer
     37 ; save_sp : regsT → xpointer → regsT
    3638 }.
     39
     40inductive internal_stack : Type[0] ≝
     41| empty_is : internal_stack
     42| one_is : beval → internal_stack
     43| both_is : beval → beval → internal_stack.
     44
     45axiom InternalStackFull : String.
     46axiom InternalStackEmpty : String.
     47
     48definition is_push : internal_stack → beval → res internal_stack ≝
     49λis,bv.match is with
     50[ empty_is ⇒ return one_is bv
     51| one_is bv' ⇒ return both_is bv' bv
     52| both_is _ _ ⇒ Error … [MSG … InternalStackFull]
     53].
     54
     55definition is_pop : internal_stack → res (beval × internal_stack) ≝
     56λis.match is with
     57[ empty_is ⇒ Error … [MSG … InternalStackEmpty]
     58| one_is bv' ⇒ return 〈bv', empty_is〉
     59| both_is bv bv' ⇒ return 〈bv', one_is bv〉
     60].
    3761
    3862record state (semp: sem_state_params): Type[0] ≝
    3963 { st_frms: framesT semp
    40  ; sp: xpointer
    41  ; isp: xpointer
     64 ; istack : internal_stack
    4265 ; carry: bebit
    4366 ; regs: regsT semp
     
    4568 }.
    4669
    47 coercion sem_state_params_to_state nocomposites:
    48   ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].
     70definition sp ≝ λp,st.load_sp p (regs ? st).
    4971
    5072record state_pc (semp : sem_state_params) : Type[0] ≝
     
    5476
    5577definition set_m: ∀p. bemem → state p → state p ≝
    56  λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     78 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
    5779
    5880definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    59  λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
     81 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
    6082
    6183definition set_sp: ∀p. ? → state p → state p ≝
    62  λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
    63 
    64 definition set_isp: ∀p. ? → state p → state p ≝
    65  λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
     84 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
     85 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
    6686
    6787definition set_carry: ∀p. bebit → state p → state p ≝
    68  λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
     88 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
     89
     90definition set_istack: ∀p. internal_stack → state p → state p ≝
     91 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
    6992
    7093definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     
    7598
    7699definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    77  λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     100 λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
    78101
    79102axiom BadProgramCounter : String.
     
    111134  | FEnd2  : fin_step_flow p F Call. (* end flow *)
    112135
    113 record more_sem_unserialized_params
     136record sem_unserialized_params
    114137  (uns_pars : unserialized_params)
    115138  (F : list ident → Type[0]) : Type[1] ≝
    116   { st_pars :> sem_state_params (* automatic coercion has issues *)
     139  { st_pars :> sem_state_params
    117140  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
    118141  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
     
    129152  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    130153  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    131   ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
     154  ; fetch_ra: state st_pars → res (cpointer × (state st_pars))
    132155
    133156  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
     
    169192definition helper_def_retrieve :
    170193  ∀X : ? → ? → ? → Type[0].
    171   (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
    172   ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
     194  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
     195  ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
    173196    λX,f,up,F,p,st.f ?? p (regs … st).
    174197
    175198definition helper_def_store :
    176199  ∀X : ? → ? → ? → Type[0].
    177   (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
    178   ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
     200  (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
     201  ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
    179202  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
    180203
     
    193216definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
    194217definition pair_reg_move ≝
    195   λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
     218  λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
    196219    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
    197220    return set_regs ? r st.
    198 
    199221 
    200222axiom BadPointer : String.
     
    208230   serialization and on whether the call is a tail one. *)
    209231definition eval_call_block:
    210  ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
     232 ∀p,F.∀p':sem_unserialized_params p F.∀globals.
    211233  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
    212234    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
     
    232254definition push: ∀p.state p → beval → res (state p) ≝
    233255 λp,st,v.
    234   let isp' ≝ isp ? st in
    235   do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
    236   let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
    237   return set_m … m (set_isp … isp'' st).
    238   normalize elim (isp p st) #p #H @H
    239 qed.
    240 
    241 definition pop: ∀p. state p → res ((state p ) × beval) ≝
     256 ! is ← is_push (istack … st) v ;
     257 return set_istack … is st.
     258
     259definition pop: ∀p. state p → res (beval × (state p)) ≝
    242260 λp,st.
    243   let isp' ≝ isp ? st in
    244   let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
    245   let ist ≝ set_isp … isp'' st in
    246   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
    247   OK ? 〈ist,v〉.
    248   normalize elim (isp p st) #p #H @H
    249 qed.
     261 ! 〈bv, is〉 ← is_pop (istack … st) ;
     262 return 〈bv, set_istack … is st〉.
    250263
    251264definition save_ra : ∀p. state p → cpointer → res (state p) ≝
    252265 λp,st,l.
    253   ! 〈addrl,addrh〉 ← beval_pair_of_pointer l ; (* always succeeds *)
     266  let 〈addrl,addrh〉 ≝  beval_pair_of_pointer l in
    254267  ! st' ← push … st addrl;
    255268  push … st' addrh.
    256269
    257 definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
     270definition load_ra : ∀p.state p → res (cpointer × (state p)) ≝
    258271 λp,st.
    259   do 〈st',addrh〉 ← pop … st;
    260   do 〈st'',addrl〉 ← pop … st';
     272  do 〈addrh, st'〉 ← pop … st;
     273  do 〈addrl, st''〉 ← pop … st';
    261274  do pr ← pointer_of_address 〈addrh, addrl〉;
    262   match ptype pr return λx.ptype pr = x → res (? × cpointer) with
    263   [ Code ⇒ λprf.return 〈st'', «pr,prf»
     275  match ptype pr return λx.ptype pr = x → res (cpointer × ?) with
     276  [ Code ⇒ λprf.return 〈«pr,prf», st''
    264277  | _ ⇒ λ_.Error … [MSG BadPointer]
    265278  ] (refl …).
     
    267280(* parameters that are defined by serialization *)
    268281record more_sem_params (pp : params) : Type[1] ≝
    269   { msu_pars :> more_sem_unserialized_params pp (joint_closed_internal_function pp)
     282  { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
    270283  ; offset_of_point : code_point pp → option offset (* can overflow *)
    271284  ; point_of_offset : offset → code_point pp
     
    463476    return set_m … m' st
    464477  | ADDRESS id prf ldest hdest ⇒
    465     let addr ≝ opt_safe ? (find_symbol … ge id) ? in
    466     ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer addr zero_offset) ;
     478    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
     479    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
    467480    ! st' ← dpl_store … ldest laddr st;
    468481    dph_store … hdest haddr st'
     
    488501    accb_store … dacc_b_reg v2' st'
    489502  | POP dst ⇒
    490     ! 〈st',v〉 ← pop p st;
     503    ! 〈v, st'〉 ← pop p st;
    491504    acca_store … p dst v st'
    492505  | PUSH src ⇒
     
    601614    do_call … ge st id fn args
    602615  | _ ⇒
    603     ! 〈st',ra〉 ← fetch_ra … st ;
     616    ! 〈ra, st'〉 ← fetch_ra … st ;
    604617    ! fn ← fetch_function … ge curr ;
    605618    ! st'' ← pop_frame … ge fn st';
     
    640653    match s' with
    641654    [ RETURN ⇒
    642       do 〈st',ra〉 ← fetch_ra … st;
     655      do 〈ra, st'〉 ← fetch_ra … st;
    643656      if eq_pointer ra exit then
    644657       do vals ← read_result … ge (joint_if_result … fn) st' ;
Note: See TracChangeset for help on using the changeset viewer.