Changeset 13
- Timestamp:
- Jul 19, 2010, 4:30:09 PM (11 years ago)
- Location:
- C-semantics
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/Cexec.ma
r11 r13 323 323 match e' with 324 324 [ Evar id ⇒ 325 match (get ? PTree ?id en) with326 [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol Genv? ge id);: OK ? 〈l,zero〉) (* global *)325 match (get … id en) with 326 [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈l,zero〉) (* global *) 327 327 | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *) 328 328 ] … … 388 388 match h with [ mk_pair id ty ⇒ 389 389 match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒ 390 match exec_alloc_variables (set ? PTree ?id b1 en) m1 vars with390 match exec_alloc_variables (set … id b1 en) m1 vars with 391 391 [ sig_intro r p ⇒ r ] 392 392 ]]]. nwhd; //; 393 nelim (exec_alloc_variables (set ident PTreeblock c3 c7 en) c6 c1);393 nelim (exec_alloc_variables (set ident ? block c3 c7 en) c6 c1); 394 394 #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH; 395 395 napply (alloc_variables_cons … IH); /2/; … … 404 404 [ nil ⇒ Some ? (Error ?) 405 405 | cons v1 vl ⇒ Some ? ( 406 b ← opt_to_res ? (get ? PTree ?id e);:406 b ← opt_to_res ? (get … id e);: 407 407 m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);: 408 408 err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *) … … 511 511 vf ← exec_expr ge e m a;: 512 512 vargs ← exec_exprlist ge e m al;: 513 fd ← opt_to_res ? (find_funct Genv? ge vf);:513 fd ← opt_to_res ? (find_funct ? ? ge vf);: 514 514 p ← assert_type_eq (type_of_fundef fd) (typeof a);: 515 515 k' ← match lhs with … … 609 609 let m0 ≝ init_mem Genv ?? p in 610 610 Some ? ( 611 b ← opt_to_res ? (find_symbol Genv? ge (prog_main ?? p));:612 f ← opt_to_res ? (find_funct_ptr Genv? ge b);:611 b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));: 612 f ← opt_to_res ? (find_funct_ptr ? ? ge b);: 613 613 OK ? (Callstate f (nil ?) Kstop m0)). 614 614 nwhd; -
C-semantics/Csem.ma
r3 r13 444 444 ndefinition env ≝ (tree_t ? PTree) block. (* map variable -> location *) 445 445 446 ndefinition empty_env: env ≝ (empty ? PTree block).446 ndefinition empty_env: env ≝ (empty …). 447 447 448 448 (* * [load_value_of_type ty m b ofs] computes the value of a datum … … 487 487 ∀e,m,id,ty,vars,m1,b1,m2,e2. 488 488 alloc m 0 (sizeof ty) = 〈m1, b1〉 → 489 alloc_variables (set ? PTree ?id b1 e) m1 vars e2 m2 →489 alloc_variables (set … id b1 e) m1 vars e2 m2 → 490 490 alloc_variables e m (〈id, ty〉 :: vars) e2 m2. 491 491 … … 503 503 | bind_parameters_cons: 504 504 ∀e,m,id,ty,params,v1,vl,b,m1,m2. 505 get ? PTree? id e = Some ? b →505 get ??? id e = Some ? b → 506 506 store_value_of_type ty m b zero v1 = Some ? m1 → 507 507 bind_parameters e m1 params vl m2 → … … 511 511 512 512 ndefinition blocks_of_env : env → list block ≝ λe. 513 map ?? (snd ident block) (elements ? PTree? e).513 map ?? (snd ident block) (elements ??? e). 514 514 515 515 (* * Selection of the appropriate case of a [switch], given the value [n] … … 611 611 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr -> block -> int -> Prop ≝ 612 612 | eval_Evar_local: ∀id,l,ty. 613 (* XXX notation? e!id*) get ? PTree? id e = Some ? l ->613 (* XXX notation? e!id*) get ??? id e = Some ? l -> 614 614 eval_lvalue ge e m (Expr (Evar id) ty) l zero 615 615 | eval_Evar_global: ∀id,l,ty. 616 (* XXX e!id *) get ? PTree? id e = None ? ->617 find_symbol Genv? ge id = Some ? l ->616 (* XXX e!id *) get ??? id e = None ? -> 617 find_symbol ?? ge id = Some ? l -> 618 618 eval_lvalue ge e m (Expr (Evar id) ty) l zero 619 619 | eval_Ederef: ∀a,ty,l,ofs. … … 774 774 eval_expr ge e m a vf -> 775 775 eval_exprlist ge e m al vargs -> 776 find_funct Genv? ge vf = Some ? fd ->776 find_funct ?? ge vf = Some ? fd -> 777 777 type_of_fundef fd = typeof a -> 778 778 step ge (State f (Scall (None ?) a al) k e m) … … 783 783 eval_expr ge e m a vf -> 784 784 eval_exprlist ge e m al vargs -> 785 find_funct Genv? ge vf = Some ? fd ->785 find_funct ?? ge vf = Some ? fd -> 786 786 type_of_fundef fd = typeof a -> 787 787 step ge (State f (Scall (Some ? lhs) a al) k e m) … … 1245 1245 let ge := globalenv Genv ?? p in 1246 1246 let m0 := init_mem Genv ?? p in 1247 find_symbol Genv? ge (prog_main ?? p) = Some ? b ->1248 find_funct_ptr Genv? ge b = Some ? f ->1247 find_symbol ?? ge (prog_main ?? p) = Some ? b -> 1248 find_funct_ptr ?? ge b = Some ? f -> 1249 1249 initial_state p (Callstate f (nil ?) Kstop m0). 1250 1250 … … 1261 1261 1262 1262 ndefinition exec_program : program → program_behavior → Prop ≝ λp,beh. 1263 program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv Genv?? p) beh.1263 program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh. 1264 1264 (* 1265 1265 (** Big-step execution of a whole program. *)
Note: See TracChangeset
for help on using the changeset viewer.