Changeset 5
 Timestamp:
 Jun 8, 2010, 3:25:47 PM (9 years ago)
 Location:
 Csemantics
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Cexec.ma
r4 r5 273 273 #A B P e f; nelim e; nnormalize; /2/; nqed. 274 274 275 nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B  P e}. ∀Q:A→B→res C. ∀R:C→Prop. 276 (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v  Error ⇒ True]) → 277 match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v  Error ⇒ True ]. 278 #A B C P e Q R; ncases e; #e'; ncases e'; nnormalize; 279 ##[ #H; napply (False_ind … H); 280 ## #e''; ncases e''; #a b Pab H; nnormalize; /2/; 281 ##] nqed. 282 275 283 (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with 276 284 a structurally smaller value, we break out the surrounding Expr constructor … … 324 332 ## napply opt_bind_OK; #l el; napply eval_Evar_local; // 325 333 ##] nqed. 334 335 (* Don't really want to use subset rather than sigma here, but can't be bothered 336 with *another* set of coercions. XXX: why do I have to get the recursive 337 call's property manually? *) 338 339 nlet rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : { r:env × mem  alloc_variables en m l (\fst r) (\snd r) } ≝ 340 match l with 341 [ nil ⇒ Some ? 〈en, m〉 342  cons h vars ⇒ 343 match h with [ mk_pair id ty ⇒ 344 match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒ 345 match exec_alloc_variables (set ? PTree ? id b1 en) m1 vars with 346 [ sig_intro r p ⇒ r ] 347 ]]]. nwhd; //; 348 nelim (exec_alloc_variables (set ident PTree block c3 c7 en) c6 c1); 349 #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH; 350 napply (alloc_variables_cons … IH); /2/; 351 nqed. 352 353 (* TODO: can we establish that length params = length vs in advance? *) 354 nlet rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res (Σm2:mem. bind_parameters e m params vs m2) ≝ 355 match params with 356 [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m)  cons _ _ ⇒ Some ? (Error ?) ] 357  cons idty params' ⇒ match idty with [ mk_pair id ty ⇒ 358 match vs with 359 [ nil ⇒ Some ? (Error ?) 360  cons v1 vl ⇒ Some ? ( 361 b ← opt_to_res ? (get ? PTree ? id e);: 362 m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);: 363 err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *) 364 ] 365 ] ]. 366 nwhd; //; 367 napply opt_bind_OK; #b eb; 368 napply opt_bind_OK; #m1 em1; 369 napply reinject; #m2 em2 Hm2; 370 napply (bind_parameters_cons … eb em1 Hm2); 371 nqed. 372 373 ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝ 374 λt. match t with 375 [ Tvoid ⇒ Some ? (Error ?) 376  _ ⇒ Some ? (OK ??) 377 ]. nwhd; //; @; #H; ndestruct; nqed. 378 379 nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝ 380 match st with 381 [ State f s k e m ⇒ 382 match s with 383 [ Sassign a1 a2 ⇒ Some ? ( 384 〈loc, ofs〉 ← exec_lvalue ge e m a1;: 385 v2 ← exec_expr ge e m a2;: 386 m' ← opt_to_res ? (store_value_of_type (typeof a1) m loc ofs v2);: 387 OK ? 〈E0, State f Sskip k e m'〉) 388  Sreturn a_opt ⇒ 389 match a_opt with 390 [ None ⇒ match fn_return f with 391 [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉) 392  _ ⇒ Some ? (Error ?) 393 ] 394  Some a ⇒ Some ? ( 395 u ← is_not_void (fn_return f);: 396 v ← exec_expr ge e m a;: 397 OK ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉) 398 ] 399  _ ⇒ Some ? (Error ?) 400 ] 401  Callstate f0 vargs k m ⇒ 402 match f0 with 403 [ Internal f ⇒ Some ? ( 404 match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒ 405 m2 ← exec_bind_parameters e m1 (fn_params f) vargs;: 406 OK ? 〈E0, State f (fn_body f) k e m2〉 407 ]) 408  _ ⇒ Some ? (Error ?) 409 ] 410  _ ⇒ Some ? (Error ?) 411 ]. nwhd; //; 412 ##[ napply sig_bind2_OK; #loc ofs Hlval; 413 napply sig_bind_OK; #v2 ev2 Hv2; 414 napply opt_bind_OK; #m' em'; 415 nwhd; napply (step_assign … Hlval Hv2 em'); 416 ## napply step_return_0; napply c9; 417 ## napply sig_bind_OK; #u eu Hnotvoid; 418 napply sig_bind_OK; #v ev Hv; 419 nwhd; napply (step_return_1 … Hnotvoid Hv); 420 ## napply extract_subset_pair; #e m1 ealloc Halloc; 421 napply sig_bind_OK; #m2 em1 Hbind; 422 nwhd; napply (step_internal_function … Halloc Hbind); 423 ##] 424 nqed. 425 426 nlet rec make_initial_state (p:program) : res (Σs:state. initial_state p s) ≝ 427 let ge ≝ globalenv Genv ?? p in 428 let m0 ≝ init_mem Genv ?? p in 429 Some ? ( 430 b ← opt_to_res ? (find_symbol Genv ? ge (prog_main ?? p));: 431 f ← opt_to_res ? (find_funct_ptr Genv ? ge b);: 432 OK ? (Callstate f (nil ?) Kstop m0)). 433 nwhd; 434 napply opt_bind_OK; #b eb; 435 napply opt_bind_OK; #f ef; 436 nwhd; napply (initial_state_intro … eb ef); 437 nqed. 
Csemantics/README
r3 r5 30 30 difficult if we keep using a unary representation of integers as 31 31 formalisation involves constants like 2^32. 32 33 * Some experimental work on an executable semantics has been started in 34 Cexec.ma. At present only a small subset of expressions and statements 35 are handled. 32 36 33 37 matita issues and workarounds
Note: See TracChangeset
for help on using the changeset viewer.