- Timestamp:
- Nov 8, 2012, 2:27:54 PM (7 years ago)
- Location:
- src/joint
- Files:
-
- 5 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 pseudo-registers ***) 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 -
src/joint/Traces.ma
r2442 r2443 7 7 ; exit: cpointer 8 8 ; 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) *) 10 10 }. 11 11 … … 13 13 { prog_spars : sem_params 14 14 ; 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) *) 16 16 }. 17 17 … … 28 28 «ptr, refl …» 29 29 (mk_genv_gen ?? (globalenv_noinit ? p) ?) 30 (prog_io pars).30 (* (prog_io pars) *). 31 31 (* TODO or TOBEFOUND *) 32 32 cases daemon … … 49 49 let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in 50 50 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 *) 52 52 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 54 55 (* 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 in56 ! 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 57 58 ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ; 58 59 ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ; … … 63 64 ]. 64 65 [ % 65 | cases ispb 66 | cases spb 67 ] normalize // 66 | cases spb normalize // 67 ] 68 68 qed. 69 69 … … 114 114 qed. 115 115 116 (* 116 117 let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝ 117 118 match c with … … 122 123 | Wrong e ⇒ Error … e 123 124 ]. 125 *) 124 126 125 127 definition cost_label_of_stmt : … … 145 147 (* as_status ≝ *) (state_pc p) 146 148 (* 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) 148 150 (* as_pc ≝ *) cpointerDeq 149 151 (* as_pc_of ≝ *) (pc …) … … 151 153 (λs. 152 154 match ( 153 ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) ;155 ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???; 154 156 match stmt with 155 157 [ 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) ; 157 159 return step_flow_classifier … flow 158 160 | 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) ; 160 162 return fin_step_flow_classifier … flow 161 163 ]) with 162 [ OKc ⇒ c163 | Error_ ⇒ cl_other164 [ Value c ⇒ c 165 | _ ⇒ cl_other 164 166 ]) 165 167 (* as_label_of_pc ≝ *) … … 175 177 succ_pc p p (pc … s1) nxt = return pc … s2) 176 178 (* 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 2 2 include "joint/blocks.ma". 3 3 include "utilities/hide.ma". 4 include "utilities/deqsets.ma". 4 5 5 6 (* general type of functions generating fresh things *) … … 64 65 add_graph … mid (final … (\snd b)) def 65 66 ]. 67 68 (* ignoring register allocation for now *) 69 70 definition 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 73 lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m). 74 #tag #A * #l * #m whd in ⊢ (%→?%); 75 elim (lookup tag ???) 76 [ * #ABS elim (ABS ?) % 77 | #a #_ % 78 ] qed. 79 80 lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l. 81 #tag #A * #l * #m whd in ⊢ (?%→%); 82 elim (lookup tag ???) 83 [ * | #a * % #ABS destruct(ABS) ] qed. 84 85 (* 86 lemma 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 ] 99 qed. 100 *) 101 102 lemma fresh_was_fresh : ∀tag,id,id',u,u'. 103 〈id,u'〉 = fresh tag u → 104 fresh_for_univ tag id' u' → 105 id' ≠ id → 106 fresh_for_univ tag id' u. 107 #tag * #id * #id' * #u * #u' 108 normalize #EQfresh destruct 109 #H #NEQ 110 elim (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 …)) 114 qed. 115 116 117 (* use Russell? *) 118 axiom 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 *) 66 176 67 177 (* preserves first statement if a cost label (should be an invariant) *) … … 132 242 ]. 133 243 244 245 134 246 (* translation with inline fresh register allocation *) 135 247 definition b_graph_translate : -
src/joint/lineariseProof.ma
r2442 r2443 20 20 definition graph_abstract_status: 21 21 ∀p:unserialized_params. 22 (∀F. more_sem_unserialized_params p F) →22 (∀F.sem_unserialized_params p F) → 23 23 joint_program (mk_graph_params p) → 24 24 abstract_status … … 27 27 joint_abstract_status 28 28 (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). 33 31 34 32 definition lin_abstract_status: 35 33 ∀p:unserialized_params. 36 (∀F. more_sem_unserialized_params p F) →34 (∀F.sem_unserialized_params p F) → 37 35 joint_program (mk_lin_params p) → 38 36 abstract_status … … 41 39 joint_abstract_status 42 40 (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). 47 43 48 44 definition linearise_status_rel: -
src/joint/semantics.ma
r2437 r2443 33 33 ; empty_framesT: framesT 34 34 ; 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 36 38 }. 39 40 inductive internal_stack : Type[0] ≝ 41 | empty_is : internal_stack 42 | one_is : beval → internal_stack 43 | both_is : beval → beval → internal_stack. 44 45 axiom InternalStackFull : String. 46 axiom InternalStackEmpty : String. 47 48 definition 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 55 definition 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 ]. 37 61 38 62 record state (semp: sem_state_params): Type[0] ≝ 39 63 { st_frms: framesT semp 40 ; sp: xpointer 41 ; isp: xpointer 64 ; istack : internal_stack 42 65 ; carry: bebit 43 66 ; regs: regsT semp … … 45 68 }. 46 69 47 coercion sem_state_params_to_state nocomposites: 48 ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0]. 70 definition sp ≝ λp,st.load_sp p (regs ? st). 49 71 50 72 record state_pc (semp : sem_state_params) : Type[0] ≝ … … 54 76 55 77 definition 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. 57 79 58 80 definition 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). 60 82 61 83 definition 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). 66 86 67 87 definition 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 90 definition 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). 69 92 70 93 definition set_pc: ∀p. ? → state_pc p → state_pc p ≝ … … 75 98 76 99 definition 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). 78 101 79 102 axiom BadProgramCounter : String. … … 111 134 | FEnd2 : fin_step_flow p F Call. (* end flow *) 112 135 113 record more_sem_unserialized_params136 record sem_unserialized_params 114 137 (uns_pars : unserialized_params) 115 138 (F : list ident → Type[0]) : Type[1] ≝ 116 { st_pars :> sem_state_params (* automatic coercion has issues *)139 { st_pars :> sem_state_params 117 140 ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) 118 141 ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval … … 129 152 ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval 130 153 ; 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)) 132 155 133 156 ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars … … 169 192 definition helper_def_retrieve : 170 193 ∀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 ≝ 173 196 λX,f,up,F,p,st.f ?? p (regs … st). 174 197 175 198 definition helper_def_store : 176 199 ∀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)) ≝ 179 202 λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st. 180 203 … … 193 216 definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_. 194 217 definition 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. 196 219 ! r ← pair_reg_move_ ?? p (regs ? st) pm; 197 220 return set_regs ? r st. 198 199 221 200 222 axiom BadPointer : String. … … 208 230 serialization and on whether the call is a tail one. *) 209 231 definition eval_call_block: 210 ∀p,F.∀p': more_sem_unserialized_params p F.∀globals.232 ∀p,F.∀p':sem_unserialized_params p F.∀globals. 211 233 genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p → 212 234 IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝ … … 232 254 definition push: ∀p.state p → beval → res (state p) ≝ 233 255 λ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 259 definition pop: ∀p. state p → res (beval × (state p)) ≝ 242 260 λ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〉. 250 263 251 264 definition save_ra : ∀p. state p → cpointer → res (state p) ≝ 252 265 λp,st,l. 253 ! 〈addrl,addrh〉 ← beval_pair_of_pointer l ; (* always succeeds *)266 let 〈addrl,addrh〉 ≝ beval_pair_of_pointer l in 254 267 ! st' ← push … st addrl; 255 268 push … st' addrh. 256 269 257 definition load_ra : ∀p.state p → res ( (state p) × cpointer) ≝270 definition load_ra : ∀p.state p → res (cpointer × (state p)) ≝ 258 271 λ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'; 261 274 do pr ← pointer_of_address 〈addrh, addrl〉; 262 match ptype pr return λx.ptype pr = x → res ( ? × cpointer) with263 [ 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''〉 264 277 | _ ⇒ λ_.Error … [MSG BadPointer] 265 278 ] (refl …). … … 267 280 (* parameters that are defined by serialization *) 268 281 record 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) 270 283 ; offset_of_point : code_point pp → option offset (* can overflow *) 271 284 ; point_of_offset : offset → code_point pp … … 463 476 return set_m … m' st 464 477 | ADDRESS id prf ldest hdest ⇒ 465 let addr ≝ opt_safe ? (find_symbol … ge id) ? in466 ! 〈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 467 480 ! st' ← dpl_store … ldest laddr st; 468 481 dph_store … hdest haddr st' … … 488 501 accb_store … dacc_b_reg v2' st' 489 502 | POP dst ⇒ 490 ! 〈 st',v〉 ← pop p st;503 ! 〈v, st'〉 ← pop p st; 491 504 acca_store … p dst v st' 492 505 | PUSH src ⇒ … … 601 614 do_call … ge st id fn args 602 615 | _ ⇒ 603 ! 〈 st',ra〉 ← fetch_ra … st ;616 ! 〈ra, st'〉 ← fetch_ra … st ; 604 617 ! fn ← fetch_function … ge curr ; 605 618 ! st'' ← pop_frame … ge fn st'; … … 640 653 match s' with 641 654 [ RETURN ⇒ 642 do 〈 st',ra〉 ← fetch_ra … st;655 do 〈ra, st'〉 ← fetch_ra … st; 643 656 if eq_pointer ra exit then 644 657 do vals ← read_result … ge (joint_if_result … fn) st' ;
Note: See TracChangeset
for help on using the changeset viewer.