Changeset 2443 for src/joint/SemanticUtils.ma
 Timestamp:
 Nov 8, 2012, 2:27:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/SemanticUtils.ma
r2422 r2443 6 6 record hw_register_env : Type[0] ≝ 7 7 { reg_env : BitVectorTrie beval 6 8 ; carry_bit : bebit9 8 ; other_bit : bebit 10 9 }. 11 10 12 11 definition empty_hw_register_env: hw_register_env ≝ 13 mk_hw_register_env (Stub …) BBundef BBundef.12 mk_hw_register_env (Stub …) BBundef. 14 13 15 14 include alias "ASM/BitVectorTrie.ma". … … 20 19 definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝ 21 20 λ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). 26 22 27 23 definition 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 26 definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝ 27 λenv. 28 let spl ≝ hwreg_retrieve env RegisterSPL in 29 let sph ≝ hwreg_retrieve env RegisterSPH in 30 ! ptr ← pointer_of_address 〈spl, sph〉 ; 31 match ptype ptr return λx.ptype ptr = x → res xpointer with 32 [ XData ⇒ λprf.return «ptr, prf» 33  _ ⇒ λ_.Error … [MSG BadPointer] 34 ] (refl …). 35 36 definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝ 37 λenv,sp. 38 let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in 39 hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env). 30 40 31 41 (*** Store/retrieve on pseudoregisters ***) 32 42 include alias "common/Identifiers.ma". 33 43 44 record reg_sp : Type[0] ≝ 45 { reg_sp_env :> identifier_map RegisterTag beval 46 ; stackp : xpointer 47 }. 48 34 49 axiom BadRegister : String. 35 50 … … 39 54 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg). 40 55 56 definition reg_sp_store ≝ λreg,v,locals. 57 ! locals' ← reg_store reg v (reg_sp_env locals) ; 58 return mk_reg_sp locals' (stackp locals). 59 60 definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals. 61 41 62 (*** Store/retrieve on hardware registers ***) 42 63 43 64 definition 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. 55 66 56 67 (******************************** GRAPHS **************************************) … … 150 161 151 162 definition 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. 154 165 sem_params ≝ 155 λpars,g_pars. 166 λpars,spars. 167 let g_pars ≝ mk_graph_params pars in 156 168 mk_sem_params 157 pars169 g_pars 158 170 (mk_more_sem_params 159 pars160 171 g_pars 172 (spars ?) 161 173 graph_offset_of_label 162 174 graph_label_of_offset … … 187 199 λo.nat_of_bitvector ? (offv o). 188 200 189 190 201 definition 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) → 193 204 sem_params ≝ 194 λpars,g_pars. 205 λpars,spars. 206 let lin_pars ≝ mk_lin_params pars in 195 207 mk_sem_params 196 pars208 lin_pars 197 209 (mk_more_sem_params 198 pars199 g_pars210 lin_pars 211 (spars ?) 200 212 lin_offset_of_nat 201 213 lin_nat_of_offset
Note: See TracChangeset
for help on using the changeset viewer.