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

changed joint's stack pointer and internal stack

File:
1 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
Note: See TracChangeset for help on using the changeset viewer.