Changeset 1655 for src/RTLabs/semantics.ma
 Timestamp:
 Jan 23, 2012, 6:31:27 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/semantics.ma
r1601 r1655 89 89 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝ 90 90 λge,st. 91 match st with91 match st return λ_. IO ??? with 92 92 [ State f fs m ⇒ 93 93 let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in 94 match s return λs. labels_present ? s → ? with95 [ St_skip l ⇒ λH. ret ?〈E0, build_state f fs m l ?〉96  St_cost cl l ⇒ λH. ret ?〈Echarge cl, build_state f fs m l ?〉94 match s return λs. labels_present ? s → IO ??? with 95 [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉 96  St_cost cl l ⇒ λH. return 〈Echarge cl, build_state f fs m l ?〉 97 97  St_const r cst l ⇒ λH. 98 98 ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst); 99 99 ! locals ← reg_store r v (locals f); 100 ret ?〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉100 return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 101 101  St_op1 _ _ op dst src l ⇒ λH. 102 102 ! v ← reg_retrieve (locals f) src; 103 103 ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v); 104 104 ! locals ← reg_store dst v' (locals f); 105 ret ?〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉105 return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 106 106  St_op2 op dst src1 src2 l ⇒ λH. 107 107 ! v1 ← reg_retrieve (locals f) src1; … … 109 109 ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2); 110 110 ! locals ← reg_store dst v' (locals f); 111 ret ?〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉111 return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 112 112  St_load chunk addr dst l ⇒ λH. 113 113 ! vaddr ← reg_retrieve (locals f) addr; 114 114 ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr); 115 115 ! locals ← reg_store dst v (locals f); 116 ret ?〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉116 return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉 117 117  St_store chunk addr src l ⇒ λH. 118 118 ! vaddr ← reg_retrieve (locals f) addr; 119 119 ! v ← reg_retrieve (locals f) src; 120 120 ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v); 121 ret ?〈E0, build_state f fs m' l ?〉121 return 〈E0, build_state f fs m' l ?〉 122 122  St_call_id id args dst l ⇒ λH. 123 123 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); 124 124 ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); 125 ! vs ← m map ??(reg_retrieve (locals f)) args;126 ret ?〈E0, Callstate fd vs dst (adv l f ?::fs) m〉125 ! vs ← m_mmap … (reg_retrieve (locals f)) args; 126 return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉 127 127  St_call_ptr frs args dst l ⇒ λH. 128 128 ! fv ← reg_retrieve (locals f) frs; 129 129 ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv); 130 ! vs ← m map ??(reg_retrieve (locals f)) args;131 ret ?〈E0, Callstate fd vs dst (adv l f ?::fs) m〉130 ! vs ← m_mmap … (reg_retrieve (locals f)) args; 131 return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉 132 132  St_tailcall_id id args ⇒ λH. 133 133 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id); 134 134 ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b); 135 ! vs ← m map ??(reg_retrieve (locals f)) args;136 ret ?〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉135 ! vs ← m_mmap … (reg_retrieve (locals f)) args; 136 return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉 137 137  St_tailcall_ptr frs args ⇒ λH. 138 138 ! fv ← reg_retrieve (locals f) frs; 139 139 ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv); 140 ! vs ← m map ??(reg_retrieve (locals f)) args;141 ret ?〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉140 ! vs ← m_mmap … (reg_retrieve (locals f)) args; 141 return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉 142 142 143 143  St_cond src ltrue lfalse ⇒ λH. 144 144 ! v ← reg_retrieve (locals f) src; 145 145 ! b ← eval_bool_of_val v; 146 ret ?〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉146 return 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉 147 147 148 148  St_jumptable r ls ⇒ λH. … … 151 151 [ Vint _ i ⇒ 152 152 match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with 153 [ None ⇒ λ_. Wrong ??? (msg BadJumpTable)154  Some l ⇒ λE. ret ?〈E0, build_state f fs m l ?〉153 [ None ⇒ λ_. Error ? (msg BadJumpTable) 154  Some l ⇒ λE. return 〈E0, build_state f fs m l ?〉 155 155 ] (refl ??) 156  _ ⇒ Wrong ??? (msg BadJumpValue)156  _ ⇒ Error ? (msg BadJumpValue) 157 157 ] 158 158 159 159  St_return ⇒ λH. 160 160 ! v ← match f_result (func f) with 161 [ None ⇒ ret ?(None ?)161 [ None ⇒ return (None ?) 162 162  Some rt ⇒ 163 163 let 〈r,ty〉 ≝ rt in 164 164 ! v ← reg_retrieve (locals f) r; 165 ret ?(Some ? v)165 return (Some ? v) 166 166 ]; 167 ret ?〈E0, Returnstate v (retdst f) fs (free m (sp f))〉167 return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉 168 168 ] (f_closed (func f) (next f) s ?) 169 169  Callstate fd params dst fs m ⇒ 170 match fd with170 match fd return λ_. IO ??? with 171 171 [ Internal fn ⇒ 172 172 ! locals ← params_store (f_params fn) params (init_locals (f_locals fn)); … … 174 174 here *) 175 175 let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in 176 ret ?〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉176 return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉 177 177  External fn ⇒ 178 ! evargs ← check_eventval_list params (sig_args (ef_sig fn));178 ! evargs ← err_to_io … (check_eventval_list params (sig_args (ef_sig fn))); 179 179 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 180 ret ?〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉180 return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉 181 181 ] 182 182  Returnstate v dst fs m ⇒ … … 189 189  Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch) 190 190  Some v' ⇒ reg_store d v' (locals f) ] ]; 191 ret ?〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉191 return 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉 192 192 ] 193 193 ]. try @(next_ok f) try @lookup_lookup_present try @H … … 250 250 . 251 251 252 lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Prop. 253 (∀a. e = OK A a → f a = OK ? v → P v) → 254 (match e with [ OK v ⇒ f v  Error m ⇒ Error ? m ] = OK ? v → P v). 255 #A #B * 256 [ #a #f #v #P #H #E whd in E:(??%?); @(H a) // 257  #m #f #v #P #H #E whd in E:(??%?); destruct 258 ] qed. 259 260 lemma bind_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop. 261 (∀a. e = OK A a → f a = OK B v → P v) → 262 (match e »= f with [ OK v ⇒ Value … v  Error m ⇒ Wrong … m ] = Value O I B v → P v). 263 #O #I #A #B * 264 [ #a #f #v #P #H #E @H [ @a  @refl  normalize in E; cases (f a) in E ⊢ %; 265 [ #v' #E normalize in E; destruct @refl  #m #E normalize in E; destruct ] ] 266  #m #f #v #P #H #E whd in E:(??%?); destruct 267 ] qed. 268 252 269 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop. 253 270 (∀a. e = Value ??? a → f a = Value ??? v → P v) → … … 270 287 [ #l #LP whd in ⊢ (??%? → ?); #E destruct % % 271 288  #c #l #LP whd in ⊢ (??%? → ?); #E destruct % % 272  #r #c #l #LP whd in ⊢ (??%? → ?); @bind IO_value #v #Ev @bindIO_value#locals' #Eloc #E whd in E:(??%?); destruct % %273  #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind IO_value #v #Ev @bindIO_value #v' #Ev' @bindIO_value#loc #Eloc #E whd in E:(??%?); destruct % %274  #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind IO_value #v1 #Ev1 @bindIO_value #v2 #Ev2 @bindIO_value #v' #Ev' @bindIO_value#loc #Eloc #E whd in E:(??%?); destruct % %275  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind IO_value #v #Ev @bindIO_value #v' #Ev' @bindIO_value#loc #Eloc #E whd in E:(??%?); destruct % %276  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind IO_value #v #Ev @bindIO_value #v' #Ev' @bindIO_value#loc #Eloc #E whd in E:(??%?); destruct % %277  #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind IO_value #b #Eb @bindIO_value #fd #Efd @bindIO_value#vs #Evs #E whd in E:(??%?); destruct %2 [ %  @b  cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]278  #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind IO_value #v #Ev @bindIO_value #fd #Efd @bindIO_value#vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ %  @b  @Efn ]   cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]279  #id #rs #LP whd in ⊢ (??%? → ?); @bind IO_value #b #Eb @bindIO_value #fd #Efd @bindIO_value#vs #Evs #E whd in E:(??%?); destruct %3 [ @b  cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]280  #r #rs #LP whd in ⊢ (??%? → ?); @bind IO_value #v #Ev @bindIO_value #fd #Efd @bindIO_value#vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b  @Efn ]   cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]281  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind IO_value #v #Ev @bindIO_value#b #Eb #E whd in E:(??%?); destruct % %282  #r #ls #LP whd in ⊢ (??%? → ?); @bind IO_value #v #Ev cases v [ #E whd in E:(??%?); destruct  #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct  #l' #e #E whd in E:(??%?); destruct % % ]  *: #vl #E whd in E:(??%?); destruct ]283  #LP whd in ⊢ (??%? → ?); @bind IO_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bindIO_value#v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5289  #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % % 290  #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % % 291  #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % % 292  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % % 293  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % % 294  #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ %  @b  cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ] 295  #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ %  @b  @Efn ]   cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] 296  #id #rs #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b  cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] 297  #r #rs #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b  @Efn ]   cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] 298  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % % 299  #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct  #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct  #l' #e #E whd in E:(??%?); destruct % % ]  *: #vl #E whd in E:(??%?); destruct ] 300  #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5 284 301 ] 285 302  * #fn #args #retdst #stk #m #tr #s' 286 303 whd in ⊢ (??%? → ?); 287 [ @bind IO_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);304 [ @bind_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?); 288 305 #E destruct %4 289  @bindIO_value #evargs #Eargs @bindIO_value #evres #Eres whd in Eres:(??%?); 290 destruct 306  @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct 291 307 ] 292 308  #v #r * [2: #f #fs ] #m #tr #s' 293 309 whd in ⊢ (??%? → ?); 294 [ @bind IO_value #loc #Eloc #E whd in E:(??%?); destruct310 [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct 295 311 %6 cases f #func #locals #next #next_ok #sp #retdst % 296 312  #E destruct
Note: See TracChangeset
for help on using the changeset viewer.