Changeset 487 for Deliverables/D3.1/Csemantics/Csem.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Csem.ma
r485 r487 36 36 the null pointer) and the float 0.0 are false. *) 37 37 38 ninductive is_false: val → type → Prop ≝38 inductive is_false: val → type → Prop ≝ 39 39  is_false_int: ∀sz,sg. 40 40 is_false (Vint zero) (Tint sz sg) … … 44 44 is_false (Vfloat Fzero) (Tfloat sz). 45 45 46 ninductive is_true: val → type → Prop ≝46 inductive is_true: val → type → Prop ≝ 47 47  is_true_int_int: ∀n,sz,sg. 48 48 n ≠ zero → … … 54 54 is_true (Vfloat f) (Tfloat sz). 55 55 56 ninductive bool_of_val : val → type → val → Prop ≝56 inductive bool_of_val : val → type → val → Prop ≝ 57 57  bool_of_val_true: ∀v,ty. 58 58 is_true v ty → … … 70 70 promoted [e2] to a float. *) 71 71 72 nlet rec sem_neg (v: val) (ty: type) : option val ≝72 let rec sem_neg (v: val) (ty: type) : option val ≝ 73 73 match ty with 74 74 [ Tint _ _ ⇒ … … 85 85 ]. 86 86 87 nlet rec sem_notint (v: val) : option val ≝87 let rec sem_notint (v: val) : option val ≝ 88 88 match v with 89 89 [ Vint n ⇒ Some ? (Vint (xor n mone)) … … 91 91 ]. 92 92 93 nlet rec sem_notbool (v: val) (ty: type) : option val ≝93 let rec sem_notbool (v: val) (ty: type) : option val ≝ 94 94 match ty with 95 95 [ Tint _ _ ⇒ … … 113 113 ]. 114 114 115 nlet rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝115 let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 116 116 match classify_add t1 t2 with 117 117 [ add_case_ii ⇒ (**r integer addition *) … … 145 145 ]. 146 146 147 nlet rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝147 let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 148 148 match classify_sub t1 t2 with 149 149 [ sub_case_ii ⇒ (**r integer subtraction *) … … 179 179 ]. 180 180 181 nlet rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝181 let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 182 182 match classify_mul t1 t2 with 183 183 [ mul_case_ii ⇒ … … 197 197 ]. 198 198 199 nlet rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝199 let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 200 200 match classify_div t1 t2 with 201 201 [ div_case_I32unsi ⇒ … … 221 221 ]. 222 222 223 nlet rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝223 let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 224 224 match classify_mod t1 t2 with 225 225 [ mod_case_I32unsi ⇒ … … 239 239 ]. 240 240 241 nlet rec sem_and (v1,v2: val) : option val ≝241 let rec sem_and (v1,v2: val) : option val ≝ 242 242 match v1 with 243 243 [ Vint n1 ⇒ match v2 with … … 247 247 ]. 248 248 249 nlet rec sem_or (v1,v2: val) : option val ≝249 let rec sem_or (v1,v2: val) : option val ≝ 250 250 match v1 with 251 251 [ Vint n1 ⇒ match v2 with … … 255 255 ]. 256 256 257 nlet rec sem_xor (v1,v2: val) : option val ≝257 let rec sem_xor (v1,v2: val) : option val ≝ 258 258 match v1 with 259 259 [ Vint n1 ⇒ match v2 with … … 263 263 ]. 264 264 265 nlet rec sem_shl (v1,v2: val): option val ≝265 let rec sem_shl (v1,v2: val): option val ≝ 266 266 match v1 with 267 267 [ Vint n1 ⇒ match v2 with … … 271 271  _ ⇒ None ? ]. 272 272 273 nlet rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝273 let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝ 274 274 match classify_shr t1 t2 with 275 275 [ shr_case_I32unsi ⇒ … … 291 291 ]. 292 292 293 nlet rec sem_cmp_mismatch (c: comparison): option val ≝293 let rec sem_cmp_mismatch (c: comparison): option val ≝ 294 294 match c with 295 295 [ Ceq => Some ? Vfalse … … 298 298 ]. 299 299 300 nlet rec sem_cmp_match (c: comparison): option val ≝300 let rec sem_cmp_match (c: comparison): option val ≝ 301 301 match c with 302 302 [ Ceq => Some ? Vtrue … … 305 305 ]. 306 306 307 nlet rec sem_cmp (c:comparison)307 let rec sem_cmp (c:comparison) 308 308 (v1: val) (t1: type) (v2: val) (t2: type) 309 309 (m: mem): option val ≝ … … 349 349 ]. 350 350 351 ndefinition sem_unary_operation351 definition sem_unary_operation 352 352 : unary_operation → val → type → option val ≝ 353 353 λop,v,ty. … … 358 358 ]. 359 359 360 nlet rec sem_binary_operation360 let rec sem_binary_operation 361 361 (op: binary_operation) 362 362 (v1: val) (t1: type) (v2: val) (t2:type) … … 385 385 resulting in value [v2]. *) 386 386 387 nlet rec cast_int_int (sz: intsize) (sg: signedness) (i: int) : int ≝387 let rec cast_int_int (sz: intsize) (sg: signedness) (i: int) : int ≝ 388 388 match sz with 389 389 [ I8 ⇒ match sg with [ Signed ⇒ sign_ext 8 i  Unsigned ⇒ zero_ext 8 i ] … … 392 392 ]. 393 393 394 nlet rec cast_int_float (si : signedness) (i: int) : float ≝394 let rec cast_int_float (si : signedness) (i: int) : float ≝ 395 395 match si with 396 396 [ Signed ⇒ floatofint i … … 398 398 ]. 399 399 400 nlet rec cast_float_int (si : signedness) (f: float) : int ≝400 let rec cast_float_int (si : signedness) (f: float) : int ≝ 401 401 match si with 402 402 [ Signed ⇒ intoffloat f … … 404 404 ]. 405 405 406 nlet rec cast_float_float (sz: floatsize) (f: float) : float ≝406 let rec cast_float_float (sz: floatsize) (f: float) : float ≝ 407 407 match sz with 408 408 [ F32 ⇒ singleoffloat f … … 410 410 ]. 411 411 412 ninductive type_region : type → region → Prop ≝412 inductive type_region : type → region → Prop ≝ 413 413  type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s 414 414  type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s … … 416 416  type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code. 417 417 418 ninductive cast : mem → val → type → type → val → Prop ≝418 inductive cast : mem → val → type → type → val → Prop ≝ 419 419  cast_ii: ∀m,i,sz2,sz1,si1,si2. (**r int to int *) 420 420 cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2) … … 448 448 and function pointers to their definitions. (See module [Globalenvs].) *) 449 449 450 ndefinition genv ≝ (genv_t Genv) fundef.450 definition genv ≝ (genv_t Genv) fundef. 451 451 452 452 (* * The local environment maps local variables to block references. … … 454 454 block. *) 455 455 456 ndefinition env ≝ (tree_t ? PTree) block. (* map variable > location *)457 458 ndefinition empty_env: env ≝ (empty …).456 definition env ≝ (tree_t ? PTree) block. (* map variable > location *) 457 458 definition empty_env: env ≝ (empty …). 459 459 460 460 (* * [load_value_of_type ty m b ofs] computes the value of a datum … … 464 464 reference, the pointer [Vptr b ofs] is returned. *) 465 465 466 nlet rec load_value_of_type (ty: type) (m: mem) (psp:region) (b: block) (ofs: int) : option val ≝466 let rec load_value_of_type (ty: type) (m: mem) (psp:region) (b: block) (ofs: int) : option val ≝ 467 467 match access_mode ty with 468 468 [ By_value chunk ⇒ loadv chunk m (Vptr psp b ofs) … … 476 476 This is allowed only if [ty] indicates an access by value. *) 477 477 478 nlet rec store_value_of_type (ty_dest: type) (m: mem) (psp:region) (loc: block) (ofs: int) (v: val) : option mem ≝478 let rec store_value_of_type (ty_dest: type) (m: mem) (psp:region) (loc: block) (ofs: int) (v: val) : option mem ≝ 479 479 match access_mode ty_dest with 480 480 [ By_value chunk ⇒ storev chunk m (Vptr psp loc ofs) v … … 490 490 and memory state. *) 491 491 492 ninductive alloc_variables: env → mem →492 inductive alloc_variables: env → mem → 493 493 list (ident × type) → 494 494 env → mem → Prop ≝ … … 507 507 [m1] is the initial memory state and [m2] the final memory state. *) 508 508 509 ninductive bind_parameters: env →509 inductive bind_parameters: env → 510 510 mem → list (ident × type) → list val → 511 511 mem → Prop ≝ … … 525 525 (* * Return the list of blocks in the codomain of [e]. *) 526 526 527 ndefinition blocks_of_env : env → list block ≝ λe.527 definition blocks_of_env : env → list block ≝ λe. 528 528 map ?? (λx. snd ?? x) (elements ??? e). 529 529 … … 531 531 of the selector expression. *) 532 532 533 nlet rec select_switch (n: int) (sl: labeled_statements)533 let rec select_switch (n: int) (sl: labeled_statements) 534 534 on sl : labeled_statements ≝ 535 535 match sl with … … 540 540 (* * Turn a labeled statement into a sequence *) 541 541 542 nlet rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝542 let rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝ 543 543 match sl with 544 544 [ LSdefault s ⇒ s … … 562 562 [e] is the current environment and [m] is the current memory state. *) 563 563 564 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝564 inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝ 565 565  eval_Econst_int: ∀i,ty. 566 566 eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0 … … 648 648 eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs tr. 649 649 650 nlet rec eval_expr_ind (ge:genv) (e:env) (m:mem)650 let rec eval_expr_ind (ge:genv) (e:env) (m:mem) 651 651 (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) 652 652 (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty)) … … 684 684 ]. 685 685 686 ninverter eval_expr_inv_ind for eval_expr : Prop.687 688 nlet rec eval_lvalue_ind (ge:genv) (e:env) (m:mem)686 inverter eval_expr_inv_ind for eval_expr : Prop. 687 688 let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem) 689 689 (P:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop) 690 690 (lvl:∀id,l,ty,H. P ????? (eval_Evar_local ge e m id l ty H)) … … 706 706 *) 707 707 708 ndefinition eval_lvalue_inv_ind :708 definition eval_lvalue_inv_ind : 709 709 ∀x1: genv. 710 710 ∀x2: env. … … 755 755 (refl int x7) (refl trace x8))) 756 756 ?)))))))))))))))). 757 ##[ napply (eval_lvalue_ind x1 x2 x3 (λa,psp,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e2:eq ? x5 psp. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a psp loc ofs tr) … Hterm); 758 ##[ napply H1 ## napply H2 ## napply H3 ## napply H4 ## napply H5 ##]759 ## ##*: ##skip760 ##] nqed.761 762 nlet rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)757 [ @(eval_lvalue_ind x1 x2 x3 (λa,psp,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e2:eq ? x5 psp. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a psp loc ofs tr) … Hterm) 758 [ @H1  @H2  @H3  @H4  @H5 ] 759  *: skip 760 ] qed. 761 762 let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem) 763 763 (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) 764 764 (Q:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop) … … 834 834 ]. 835 835 836 ndefinition combined_expr_lvalue_ind ≝836 definition combined_expr_lvalue_ind ≝ 837 837 λge,e,m,P,Q,eci,ecF,elv,ead,esz,eun,ebi,ect,ecf,eo1,eo2,ea1,ea2,ecs,eco,lvl,lvg,lde,lfs,lfu. 838 838 conj ?? … … 852 852 expressions [al] to their values [vl]. *) 853 853 854 ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝854 inductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝ 855 855  eval_Enil: 856 856 eval_exprlist ge e m (nil ?) (nil ?) E0 … … 866 866 (* * Continuations *) 867 867 868 ninductive cont: Type:=868 inductive cont: Type[0] := 869 869  Kstop: cont 870 870  Kseq: statement > cont > cont … … 887 887 (* * Pop continuation until a call or stop *) 888 888 889 nlet rec call_cont (k: cont) : cont :=889 let rec call_cont (k: cont) : cont := 890 890 match k with 891 891 [ Kseq s k => call_cont k … … 898 898 ]. 899 899 900 ndefinition is_call_cont : cont → Prop ≝ λk.900 definition is_call_cont : cont → Prop ≝ λk. 901 901 match k with 902 902 [ Kstop => True … … 907 907 (* * States *) 908 908 909 ninductive state: Type:=909 inductive state: Type[0] := 910 910  State: 911 911 ∀f: function. … … 927 927 corresponding to a label *) 928 928 929 nlet rec find_label (lbl: label) (s: statement) (k: cont)929 let rec find_label (lbl: label) (s: statement) (k: cont) 930 930 on s: option (statement × cont) := 931 931 match s with … … 977 977 978 978 (* Strip off outer pointer for use when comparing function types. *) 979 ndefinition fun_typeof ≝979 definition fun_typeof ≝ 980 980 λe. match typeof e with 981 981 [ Tvoid ⇒ Tvoid … … 992 992 (* XXX: note that cost labels in exprs expose a particular eval order. *) 993 993 994 ninductive step (ge:genv) : state → trace → state → Prop ≝994 inductive step (ge:genv) : state → trace → state → Prop ≝ 995 995 996 996  step_assign: ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2. … … 1172 1172 through the execution of a [break], [continue] or [return] statement. *) 1173 1173 1174 ninductive outcome: Type:=1174 inductive outcome: Type[0] := 1175 1175  Out_break: outcome (**r terminated by [break] *) 1176 1176  Out_continue: outcome (**r terminated by [continue] *) … … 1178 1178  Out_return: option val > outcome. (**r terminated by [return] *) 1179 1179 1180 ninductive out_normal_or_continue : outcome > Prop :=1180 inductive out_normal_or_continue : outcome > Prop := 1181 1181  Out_normal_or_continue_N: out_normal_or_continue Out_normal 1182 1182  Out_normal_or_continue_C: out_normal_or_continue Out_continue. 1183 1183 1184 ninductive out_break_or_return : outcome > outcome > Prop :=1184 inductive out_break_or_return : outcome > outcome > Prop := 1185 1185  Out_break_or_return_B: out_break_or_return Out_break Out_normal 1186 1186  Out_break_or_return_R: ∀ov. … … 1207 1207 evaluation. *) 1208 1208 1209 ninductive exec_stmt: env > mem > statement > trace > mem > outcome > Prop :=1209 inductive exec_stmt: env > mem > statement > trace > mem > outcome > Prop := 1210 1210  exec_Sskip: ∀e,m. 1211 1211 exec_stmt e m Sskip … … 1368 1368 trace of observable events performed during the execution. *) 1369 1369 1370 Co ninductive execinf_stmt: env > mem > statement > traceinf > Prop :=1370 Coinductive execinf_stmt: env > mem > statement > traceinf > Prop := 1371 1371  execinf_Scall_none: ∀e,m,a,al,vf,vargs,f,t. 1372 1372 eval_expr e m a vf > … … 1475 1475 without arguments and with an empty continuation. *) 1476 1476 1477 ninductive initial_state (p: clight_program): state > Prop :=1477 inductive initial_state (p: clight_program): state > Prop := 1478 1478  initial_state_intro: ∀b,f,ge,m0. 1479 1479 globalenv Genv ?? p = OK ? ge → … … 1485 1485 (* * A final state is a [Returnstate] with an empty continuation. *) 1486 1486 1487 ninductive final_state: state > int > Prop :=1487 inductive final_state: state > int > Prop := 1488 1488  final_state_intro: ∀r,m. 1489 1489 final_state (Returnstate (Vint r) Kstop m) r. … … 1494 1494 behavior. *) 1495 1495 1496 ndefinition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.1496 definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh. 1497 1497 ∀ge. globalenv ??? p = OK ? ge → 1498 1498 program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh. … … 1500 1500 (** Bigstep execution of a whole program. *) 1501 1501 1502 ninductive bigstep_program_terminates (p: program): trace > int > Prop :=1502 inductive bigstep_program_terminates (p: program): trace > int > Prop := 1503 1503  bigstep_program_terminates_intro: ∀b,f,m1,t,r. 1504 1504 let ge := Genv.globalenv p in … … 1509 1509 bigstep_program_terminates p t r. 1510 1510 1511 ninductive bigstep_program_diverges (p: program): traceinf > Prop :=1511 inductive bigstep_program_diverges (p: program): traceinf > Prop := 1512 1512  bigstep_program_diverges_intro: ∀b,f,t. 1513 1513 let ge := Genv.globalenv p in … … 1532 1532 (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y). 1533 1533 1534 ninductive outcome_state_match1534 inductive outcome_state_match 1535 1535 (e: env) (m: mem) (f: function) (k: cont): outcome > state > Prop := 1536 1536  osm_normal:
Note: See TracChangeset
for help on using the changeset viewer.