Changeset 1872 for src/Clight
 Timestamp:
 Apr 4, 2012, 6:48:23 PM (9 years ago)
 Location:
 src/Clight
 Files:

 1 added
 5 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csem.ma
r1713 r1872 27 27 (*include "Events.ma".*) 28 28 include "common/Smallstep.ma". 29 include "Clight/ClassifyOp.ma". 29 30 30 31 (* * * Semantics of typedependent operations *) … … 117 118 let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 118 119 match classify_add t1 t2 with 119 [ add_case_ii ⇒ (**r integer addition *)120 [ add_case_ii _ _ ⇒ (**r integer addition *) 120 121 match v1 with 121 122 [ Vint sz1 n1 ⇒ match v2 with … … 124 125  _ ⇒ None ? ] 125 126  _ ⇒ None ? ] 126  add_case_ff ⇒ (**r float addition *)127  add_case_ff _ ⇒ (**r float addition *) 127 128 match v1 with 128 129 [ Vfloat n1 ⇒ match v2 with … … 130 131  _ ⇒ None ? ] 131 132  _ ⇒ None ? ] 132  add_case_pi ty⇒ (**r pointer plus integer *)133  add_case_pi _ _ ty _ _ ⇒ (**r pointer plus integer *) 133 134 match v1 with 134 135 [ Vptr ptr1 ⇒ match v2 with … … 139 140  _ ⇒ None ? ] 140 141  _ ⇒ None ? ] 141  add_case_ip ty ⇒ (**r integer plus pointer *)142  add_case_ip _ _ _ _ ty ⇒ (**r integer plus pointer *) 142 143 match v1 with 143 144 [ Vint sz1 n1 ⇒ match v2 with … … 146 147  _ ⇒ None ? ] 147 148  _ ⇒ None ? ] 148  add_default ⇒ None ?149  add_default _ _ ⇒ None ? 149 150 ]. 150 151 151 152 let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 152 153 match classify_sub t1 t2 with 153 [ sub_case_ii ⇒ (**r integer subtraction *)154 [ sub_case_ii _ _ ⇒ (**r integer subtraction *) 154 155 match v1 with 155 156 [ Vint sz1 n1 ⇒ match v2 with … … 158 159  _ ⇒ None ? ] 159 160  _ ⇒ None ? ] 160  sub_case_ff ⇒ (**r float subtraction *)161  sub_case_ff _ ⇒ (**r float subtraction *) 161 162 match v1 with 162 163 [ Vfloat f1 ⇒ match v2 with … … 164 165  _ ⇒ None ? ] 165 166  _ ⇒ None ? ] 166  sub_case_pi ty⇒ (**r pointer minus integer *)167  sub_case_pi _ _ ty _ _ ⇒ (**r pointer minus integer *) 167 168 match v1 with 168 169 [ Vptr ptr1 ⇒ match v2 with … … 173 174  _ ⇒ None ? ] 174 175  _ ⇒ None ? ] 175  sub_case_pp ty⇒ (**r pointer minus pointer *)176  sub_case_pp _ _ _ ty _ _ ⇒ (**r pointer minus pointer *) 176 177 match v1 with 177 178 [ Vptr ptr1 ⇒ match v2 with … … 187 188  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?))  _ ⇒ None ? ] 188 189  _ ⇒ None ? ] 189  sub_default ⇒ None ?190  sub_default _ _ ⇒ None ? 190 191 ]. 191 192 192 193 let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 193 match classify_ mult1 t2 with194 [ mul_case_ii⇒194 match classify_aop t1 t2 with 195 [ aop_case_ii _ _ ⇒ 195 196 match v1 with 196 197 [ Vint sz1 n1 ⇒ match v2 with … … 199 200  _ ⇒ None ? ] 200 201  _ ⇒ None ? ] 201  mul_case_ff⇒202  aop_case_ff _ ⇒ 202 203 match v1 with 203 204 [ Vfloat f1 ⇒ match v2 with … … 205 206  _ ⇒ None ? ] 206 207  _ ⇒ None ? ] 207  mul_default⇒208  aop_default _ _ ⇒ 208 209 None ? 209 210 ]. 210 211 211 212 let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 212 match classify_div t1 t2 with 213 [ div_case_I32unsi ⇒ 214 match v1 with 215 [ Vint sz1 n1 ⇒ match v2 with 216 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 217 (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?) 218  _ ⇒ None ? ] 219  _ ⇒ None ? ] 220  div_case_ii ⇒ 213 match classify_aop t1 t2 with 214 [ aop_case_ii _ sg ⇒ 221 215 match v1 with 222 216 [ Vint sz1 n1 ⇒ match v2 with 223 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 217 [ Vint sz2 n2 ⇒ 218 match sg with 219 [ Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1 224 220 (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?) 221  Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1 222 (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?) 223 ] 225 224  _ ⇒ None ? ] 226 225  _ ⇒ None ? ] 227  div_case_ff⇒226  aop_case_ff _ ⇒ 228 227 match v1 with 229 228 [ Vfloat f1 ⇒ match v2 with … … 231 230  _ ⇒ None ? ] 232 231  _ ⇒ None ? ] 233  div_default⇒232  aop_default _ _ ⇒ 234 233 None ? 235 234 ]. 236 235 237 236 let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 238 match classify_ modt1 t2 with239 [ mod_case_I32unsi⇒237 match classify_aop t1 t2 with 238 [ aop_case_ii sz sg ⇒ 240 239 match v1 with 241 240 [ Vint sz1 n1 ⇒ match v2 with 242 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 241 [ Vint sz2 n2 ⇒ 242 match sg with 243 [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1 243 244 (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?) 244  _ ⇒ None ? ] 245  _ ⇒ None ? ] 246  mod_case_ii ⇒ 247 match v1 with 248 [ Vint sz1 n1 ⇒ match v2 with 249 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 250 (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?) 251  _ ⇒ None ? ] 252  _ ⇒ None ? ] 253  mod_default ⇒ 245  Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1 246 (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?) 247 ] 248  _ ⇒ None ? ] 249  _ ⇒ None ? ] 250  _ ⇒ 254 251 None ? 255 252 ]. … … 293 290 294 291 let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝ 295 match classify_ shrt1 t2 with296 [ shr_case_I32unsi ⇒292 match classify_aop t1 t2 with 293 [ aop_case_ii _ sg ⇒ 297 294 match v1 with 298 295 [ Vint sz1 n1 ⇒ match v2 with 299 296 [ Vint sz2 n2 ⇒ 297 match sg with 298 [ Unsigned ⇒ 300 299 if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) 301 300 then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false)) 302 301 else None ? 303  _ ⇒ None ? ] 304  _ ⇒ None ? ] 305  shr_case_ii => 306 match v1 with 307 [ Vint sz1 n1 ⇒ match v2 with 308 [ Vint sz2 n2 ⇒ 302  Signed ⇒ 309 303 if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) 310 304 then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1))) 311 305 else None ? 312  _ ⇒ None ? ] 313  _ ⇒ None ? ] 314  shr_default ⇒ 306 ] 307  _ ⇒ None ? ] 308  _ ⇒ None ? ] 309  _ ⇒ 315 310 None ? 316 311 ]. … … 318 313 let rec sem_cmp_mismatch (c: comparison): option val ≝ 319 314 match c with 320 [ Ceq =>Some ? Vfalse321  Cne =>Some ? Vtrue322  _ =>None ?315 [ Ceq ⇒ Some ? Vfalse 316  Cne ⇒ Some ? Vtrue 317  _ ⇒ None ? 323 318 ]. 324 319 325 320 let rec sem_cmp_match (c: comparison): option val ≝ 326 321 match c with 327 [ Ceq =>Some ? Vtrue328  Cne =>Some ? Vfalse329  _ =>None ?322 [ Ceq ⇒ Some ? Vtrue 323  Cne ⇒ Some ? Vfalse 324  _ ⇒ None ? 330 325 ]. 331 326 … … 334 329 (m: mem): option val ≝ 335 330 match classify_cmp t1 t2 with 336 [ cmp_case_ I32unsi⇒331 [ cmp_case_ii _ sg ⇒ 337 332 match v1 with 338 333 [ Vint sz1 n1 ⇒ match v2 with 339 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 334 [ Vint sz2 n2 ⇒ 335 match sg with 336 [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1 340 337 (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?) 341  _ ⇒ None ? ] 342  _ ⇒ None ? ] 343  cmp_case_ii ⇒ 344 match v1 with 345 [ Vint sz1 n1 ⇒ match v2 with 346 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 347 (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?) 338  Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1 339 (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?) 340 ] 348 341  _ ⇒ None ? 349 342 ] 350 343  _ ⇒ None ? 351 344 ] 352  cmp_case_pp ⇒345  cmp_case_pp _ _ _ ⇒ 353 346 match v1 with 354 347 [ Vptr ptr1 ⇒ … … 370 363 ] 371 364  _ ⇒ None ? ] 372  cmp_case_ff ⇒365  cmp_case_ff _ ⇒ 373 366 match v1 with 374 367 [ Vfloat f1 ⇒ … … 377 370  _ ⇒ None ? ] 378 371  _ ⇒ None ? ] 379  cmp_default ⇒ None ?372  cmp_default _ _ ⇒ None ? 380 373 ]. 381 374 … … 499 492  inr _ ⇒ None ? 500 493 ] 501  By_nothing ⇒ None ?494  By_nothing _ ⇒ None ? 502 495 ]. 503 496 cases b // … … 513 506 [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer Any loc ? ofs)) v 514 507  By_reference _ ⇒ None ? 515  By_nothing ⇒ None ?508  By_nothing _ ⇒ None ? 516 509 ]. 517 510 cases loc // 
src/Clight/Csyntax.ma
r1599 r1872 591 591 Qed. 592 592 *) 593 (* * The [access_mode] function describes how a variable of the given 594 type must be accessed: 595  [By_value ch]: access by value, i.e. by loading from the address 596 of the variable using the memory chunk [ch]; 597  [By_reference]: access by reference, i.e. by just returning 598 the address of the variable; 599  [By_nothing]: no access is possible, e.g. for the [void] type. 600 601 We currently do not support 64bit integers and 128bit floats, so these 602 have an access mode of [By_nothing]. 603 *) 604 605 inductive mode: Type[0] ≝ 606  By_value: memory_chunk → mode 607  By_reference: region → mode 608  By_nothing: mode. 609 610 definition access_mode : type → mode ≝ λty. 611 match ty with 612 [ Tint i s ⇒ 613 match i with [ I8 ⇒ 614 match s with [ Signed ⇒ By_value Mint8signed 615  Unsigned ⇒ By_value Mint8unsigned ] 616  I16 ⇒ 617 match s with [ Signed ⇒ By_value Mint16signed 618  Unsigned ⇒ By_value Mint16unsigned ] 619  I32 ⇒ By_value Mint32 ] 620  Tfloat f ⇒ match f with [ F32 ⇒ By_value Mfloat32 621  F64 ⇒ By_value Mfloat64 ] 622  Tvoid ⇒ By_nothing 623  Tpointer r _ ⇒ By_value (Mpointer r) 624  Tarray r _ _ ⇒ By_reference r 625  Tfunction _ _ ⇒ By_reference Code 626  Tstruct _ fList ⇒ By_nothing 627  Tunion _ fList ⇒ By_nothing 628  Tcomp_ptr r _ ⇒ By_value (Mpointer r) 629 ]. 630 631 (* * Classification of arithmetic operations and comparisons. 632 The following [classify_] functions take as arguments the types 633 of the arguments of an operation. They return enough information 634 to resolve overloading for this operator applications, such as 635 ``both arguments are floats'', or ``the first is a pointer 636 and the second is an integer''. These functions are used to resolve 637 overloading both in the dynamic semantics (module [Csem]) and in the 638 compiler (module [Cshmgen]). 639 *) 640 641 inductive classify_add_cases : Type[0] ≝ 642  add_case_ii: classify_add_cases (**r int , int *) 643  add_case_ff: classify_add_cases (**r float , float *) 644  add_case_pi: type → classify_add_cases (**r ptr or array, int *) 645  add_case_ip: type → classify_add_cases (**r int, ptr or array *) 646  add_default: classify_add_cases. (**r other *) 647 648 definition classify_add ≝ λty1: type. λty2: type. 649 (* 650 match ty1, ty2 with 651 [ Tint _ _, Tint _ _ ⇒ add_case_ii 652  Tfloat _, Tfloat _ ⇒ add_case_ff 653  Tpointer ty, Tint _ _ ⇒ add_case_pi ty 654  Tarray ty _, Tint _ _ ⇒ add_case_pi ty 655  Tint _ _, Tpointer ty ⇒ add_case_ip ty 656  Tint _ _, Tarray ty _ ⇒ add_case_ip ty 657  _, _ ⇒ add_default 658 ]. 659 *) 660 match ty1 with 661 [ Tint _ _ ⇒ 662 match ty2 with 663 [ Tint _ _ ⇒ add_case_ii 664  Tpointer _ ty ⇒ add_case_ip ty 665  Tarray _ ty _ ⇒ add_case_ip ty 666  _ ⇒ add_default ] 667  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff  _ ⇒ add_default ] 668  Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty  _ ⇒ add_default ] 669  Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty  _ ⇒ add_default ] 670  _ ⇒ add_default 671 ]. 672 673 inductive classify_sub_cases : Type[0] ≝ 674  sub_case_ii: classify_sub_cases (**r int , int *) 675  sub_case_ff: classify_sub_cases (**r float , float *) 676  sub_case_pi: type → classify_sub_cases (**r ptr or array , int *) 677  sub_case_pp: type → classify_sub_cases (**r ptr or array , ptr or array *) 678  sub_default: classify_sub_cases . (**r other *) 679 680 definition classify_sub ≝ λty1: type. λty2: type. 681 (* match ty1, ty2 with 682  Tint _ _ , Tint _ _ ⇒ sub_case_ii 683  Tfloat _ , Tfloat _ ⇒ sub_case_ff 684  Tpointer ty , Tint _ _ ⇒ sub_case_pi ty 685  Tarray ty _ , Tint _ _ ⇒ sub_case_pi ty 686  Tpointer ty , Tpointer _ ⇒ sub_case_pp ty 687  Tpointer ty , Tarray _ _⇒ sub_case_pp ty 688  Tarray ty _ , Tpointer _ ⇒ sub_case_pp ty 689  Tarray ty _ , Tarray _ _ ⇒ sub_case_pp ty 690  _ ,_ ⇒ sub_default 691 end. 692 *) 693 match ty1 with 694 [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii  _ ⇒ sub_default ] 695  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff  _ ⇒ sub_default ] 696  Tpointer _ ty ⇒ 697 match ty2 with 698 [ Tint _ _ ⇒ sub_case_pi ty 699  Tpointer _ _ ⇒ sub_case_pp ty 700  Tarray _ _ _ ⇒ sub_case_pp ty 701  _ ⇒ sub_default ] 702  Tarray _ ty _ ⇒ 703 match ty2 with 704 [ Tint _ _ ⇒ sub_case_pi ty 705  Tpointer _ _ ⇒ sub_case_pp ty 706  Tarray _ _ _ ⇒ sub_case_pp ty 707  _ ⇒ sub_default ] 708  _ ⇒ sub_default 709 ]. 710 711 inductive classify_mul_cases : Type[0] ≝ 712  mul_case_ii: classify_mul_cases (**r int , int *) 713  mul_case_ff: classify_mul_cases (**r float , float *) 714  mul_default: classify_mul_cases . (**r other *) 715 716 definition classify_mul ≝ λty1: type. λty2: type. 717 match ty1 with 718 [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ mul_case_ii  _ ⇒ mul_default ] 719  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ mul_case_ff  _ ⇒ mul_default ] 720  _ ⇒ mul_default 721 ]. 722 (* 723 match ty1,ty2 with 724  Tint _ _, Tint _ _ ⇒ mul_case_ii 725  Tfloat _ , Tfloat _ ⇒ mul_case_ff 726  _,_ ⇒ mul_default 727 end. 728 *) 729 inductive classify_div_cases : Type[0] ≝ 730  div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *) 731  div_case_ii: classify_div_cases (**r int , int *) 732  div_case_ff: classify_div_cases (**r float , float *) 733  div_default: classify_div_cases. (**r other *) 734 735 definition classify_32un_aux ≝ λT:Type[0].λi.λs.λr1:T.λr2:T. 736 match i with [ I32 ⇒ 737 match s with [ Unsigned ⇒ r1  _ ⇒ r2 ] 738  _ ⇒ r2 ]. 739 740 definition classify_div ≝ λty1: type. λty2: type. 741 match ty1 with 742 [ Tint i1 s1 ⇒ 743 match ty2 with 744 [ Tint i2 s2 ⇒ 745 classify_32un_aux ? i1 s1 div_case_I32unsi 746 (classify_32un_aux ? i2 s2 div_case_I32unsi div_case_ii) 747  _ ⇒ div_default ] 748  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ div_case_ff  _ ⇒ div_default ] 749  _ ⇒ div_default 750 ]. 751 (* 752 definition classify_div ≝ λty1: type. λty2: type. 753 match ty1,ty2 with 754  Tint I32 Unsigned, Tint _ _ ⇒ div_case_I32unsi 755  Tint _ _ , Tint I32 Unsigned ⇒ div_case_I32unsi 756  Tint _ _ , Tint _ _ ⇒ div_case_ii 757  Tfloat _ , Tfloat _ ⇒ div_case_ff 758  _ ,_ ⇒ div_default 759 end. 760 *) 761 inductive classify_mod_cases : Type[0] ≝ 762  mod_case_I32unsi: classify_mod_cases (**r unsigned I32 , int *) 763  mod_case_ii: classify_mod_cases (**r int , int *) 764  mod_default: classify_mod_cases . (**r other *) 765 766 definition classify_mod ≝ λty1:type. λty2:type. 767 match ty1 with 768 [ Tint i1 s1 ⇒ 769 match ty2 with 770 [ Tint i2 s2 ⇒ 771 classify_32un_aux ? i1 s1 mod_case_I32unsi 772 (classify_32un_aux ? i2 s2 mod_case_I32unsi mod_case_ii) 773  _ ⇒ mod_default ] 774  _ ⇒ mod_default 775 ]. 776 (* 777 Definition classify_mod (ty1: type) (ty2: type) := 778 match ty1,ty2 with 779  Tint I32 Unsigned , Tint _ _ ⇒ mod_case_I32unsi 780  Tint _ _ , Tint I32 Unsigned ⇒ mod_case_I32unsi 781  Tint _ _ , Tint _ _ ⇒ mod_case_ii 782  _ , _ ⇒ mod_default 783 end . 784 *) 785 inductive classify_shr_cases :Type[0] ≝ 786  shr_case_I32unsi: classify_shr_cases (**r unsigned I32 , int *) 787  shr_case_ii :classify_shr_cases (**r int , int *) 788  shr_default : classify_shr_cases . (**r other *) 789 790 definition classify_shr ≝ λty1: type. λty2: type. 791 match ty1 with 792 [ Tint i1 s1 ⇒ 793 match ty2 with 794 [ Tint _ _ ⇒ 795 classify_32un_aux ? i1 s1 shr_case_I32unsi shr_case_ii 796  _ ⇒ shr_default ] 797  _ ⇒ shr_default 798 ]. 799 800 (* 801 Definition classify_shr (ty1: type) (ty2: type) := 802 match ty1,ty2 with 803  Tint I32 Unsigned , Tint _ _ ⇒ shr_case_I32unsi 804  Tint _ _ , Tint _ _ ⇒ shr_case_ii 805  _ , _ ⇒ shr_default 806 end. 807 *) 808 inductive classify_cmp_cases : Type[0] ≝ 809  cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *) 810  cmp_case_ii: classify_cmp_cases (**r int, int*) 811  cmp_case_pp: classify_cmp_cases (**r ptrarray , ptrarray*) 812  cmp_case_ff: classify_cmp_cases (**r float , float *) 813  cmp_default: classify_cmp_cases . (**r other *) 814 815 definition classify_cmp ≝ λty1:type. λty2:type. 816 match ty1 with 817 [ Tint i1 s1 ⇒ 818 match ty2 with 819 [ Tint i2 s2 ⇒ 820 classify_32un_aux ? i1 s1 cmp_case_I32unsi 821 (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ii) 822  _ ⇒ cmp_default ] 823  Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff  _ ⇒ cmp_default ] 824  Tpointer _ _ ⇒ 825 match ty2 with 826 [ Tpointer _ _ ⇒ cmp_case_pp 827  Tarray _ _ _ ⇒ cmp_case_pp 828  _ ⇒ cmp_default ] 829  Tarray _ _ _ ⇒ 830 match ty2 with 831 [ Tpointer _ _ ⇒ cmp_case_pp 832  Tarray _ _ _ ⇒ cmp_case_pp 833  _ ⇒ cmp_default ] 834  _ ⇒ cmp_default 835 ]. 836 837 (* 838 Definition classify_cmp (ty1: type) (ty2: type) := 839 match ty1,ty2 with 840  Tint I32 Unsigned , Tint _ _ ⇒ cmp_case_I32unsi 841  Tint _ _ , Tint I32 Unsigned ⇒ cmp_case_I32unsi 842  Tint _ _ , Tint _ _ ⇒ cmp_case_ipip 843  Tfloat _ , Tfloat _ ⇒ cmp_case_ff 844  Tpointer _ , Tint _ _ ⇒ cmp_case_ipip 845  Tarray _ _ , Tint _ _ ⇒ cmp_case_ipip 846  Tpointer _ , Tpointer _ ⇒ cmp_case_ipip 847  Tpointer _ , Tarray _ _ ⇒ cmp_case_ipip 848  Tarray _ _ ,Tpointer _ ⇒ cmp_case_ipip 849  Tarray _ _ ,Tarray _ _ ⇒ cmp_case_ipip 850  _ , _ ⇒ cmp_default 851 end. 852 *) 853 inductive classify_fun_cases : Type[0] ≝ 854  fun_case_f: typelist → type → classify_fun_cases (**r (pointer to) function *) 855  fun_default: classify_fun_cases . (**r other *) 856 857 definition classify_fun ≝ λty: type. 858 match ty with 859 [ Tfunction args res ⇒ fun_case_f args res 860  Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res 861  _ ⇒ fun_default 862 ] 863  _ ⇒ fun_default 864 ]. 593 865 594 866 595 (* * Translating Clight types to Cminor types, function signatures, … … 875 604  Tarray r _ _ ⇒ ASTptr r 876 605  Tfunction _ _ ⇒ ASTptr Code 606  Tcomp_ptr r _ ⇒ ASTptr r 877 607  _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *) 878 608 ]. … … 886 616  Tarray r _ _ ⇒ Some ? (ASTptr r) 887 617  Tfunction _ _ ⇒ Some ? (ASTptr Code) 618  Tcomp_ptr r _ ⇒ Some ? (ASTptr r) 888 619  _ ⇒ None ? (* structs and unions shouldn't be converted? *) 889 620 ]. … … 895 626 ]. 896 627 628 629 (* * The [access_mode] function describes how a variable of the given 630 type must be accessed: 631  [By_value ch]: access by value, i.e. by loading from the address 632 of the variable using the memory chunk [ch]; 633  [By_reference]: access by reference, i.e. by just returning 634 the address of the variable; 635  [By_nothing]: no access is possible, e.g. for the [void] type. 636 637 We currently do not support 64bit integers and 128bit floats, so these 638 have an access mode of [By_nothing]. 639 *) 640 641 inductive mode: typ → Type[0] ≝ 642  By_value: ∀t:typ. mode t 643  By_reference: ∀r:region. mode (ASTptr r) 644  By_nothing: ∀t. mode t. 645 646 definition access_mode : ∀ty. mode (typ_of_type ty) ≝ λty. 647 match ty return λty. mode (typ_of_type ty) with 648 [ Tint i s ⇒ By_value (ASTint i s) 649  Tfloat sz ⇒ By_value (ASTfloat sz) 650  Tvoid ⇒ By_nothing … 651  Tpointer r _ ⇒ By_value (ASTptr r) 652  Tarray r _ _ ⇒ By_reference r 653  Tfunction _ _ ⇒ By_reference Code 654  Tstruct _ fList ⇒ By_nothing … 655  Tunion _ fList ⇒ By_nothing … 656  Tcomp_ptr r _ ⇒ By_value (ASTptr r) 657 ]. 658 897 659 definition signature_of_type : typelist → type → signature ≝ λargs. λres. 898 660 mk_signature (typlist_of_typelist args) (opttyp_of_type res). 
src/Clight/SimplifyCasts.ma
r1224 r1872 114 114 〈false, Expr (Ebinop op e1' e2') ty〉 115 115 else 116 let 〈desired_type1, e1'〉 ≝ simplify_expr e1 tyin117 let 〈desired_type2, e2'〉 ≝ simplify_expr e2 tyin116 let 〈desired_type1, e1'〉 ≝ simplify_expr e1 (typeof e1) in 117 let 〈desired_type2, e2'〉 ≝ simplify_expr e2 (typeof e2) in 118 118 〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉 119 119  Ecast ty e1 ⇒ 
src/Clight/TypeComparison.ma
r1515 r1872 93 93 λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true  inr _ ⇒ false ]. 94 94 95 96 definition if_type_eq : ∀t1,t2:type. ∀P:type → type → Type[0]. P t1 t1 → P t1 t2 → P t1 t2 ≝ 97 λt1,t2,P. match type_eq_dec t1 t2 return λ_. P t1 t1 → P t1 t2 → P t1 t2 with [ inl E ⇒ λx,d. x⌈P t1 t1 ↦ P t1 t2⌉  inr _ ⇒ λx,d. d ]. 98 // qed. 
src/Clight/toCminor.ma
r1871 r1872 1 include "Clight/Csyntax.ma". 2 include "Clight/TypeComparison.ma". 1 include "Clight/ClassifyOp.ma". 3 2 include "basics/lists/list.ma". 4 3 include "Clight/fresh.ma". … … 322 321 Consistency of the type is enforced by explicit checks. 323 322 *) 323 324 (* First, how to get rid of a abstractaway pointer or array type *) 325 definition fix_ptr_type : ∀r,ty,n. expr (typ_of_type (ptr_type r ty n)) → expr (ASTptr r) ≝ 326 λr,ty,n,e. e⌈expr (typ_of_type (ptr_type r ty n)) ↦ expr (ASTptr r)⌉. 327 cases n // 328 qed. 329 324 330 definition translate_add ≝ 325 λty1, e1,ty2,e2,ty'.331 λty1,ty2,ty'. 326 332 let ty1' ≝ typ_of_type ty1 in 327 333 let ty2' ≝ typ_of_type ty2 in 328 match classify_add ty1 ty2 with 329 [ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2) 330  add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2) 331 (* XXX using the integer size for e2 as the offset's size isn't right, because 332 if e2 produces an 8bit value then the true offset might overflow *) 333  add_case_pi ty ⇒ 334 match ty2' with 335 [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty)))))) 336  _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) 337 ] 338  add_case_ip ty ⇒ 339 match ty1' with 340 [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty)))))) 341  _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) 342 ] 343  add_default ⇒ Error ? (msg TypeMismatch) 334 match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 335 [ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2) 336  add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2) 337 (* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *) 338  add_case_pi n r ty sz sg ⇒ 339 λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 (repr ? (sizeof ty)))))) 340  add_case_ip n sz sg r ty ⇒ 341 λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 (repr ? (sizeof ty)))))) 342  add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch) 344 343 ]. 345 344 346 345 347 346 definition translate_sub ≝ 348 λty1, e1,ty2,e2,ty'.347 λty1,ty2,ty'. 349 348 let ty1' ≝ typ_of_type ty1 in 350 349 let ty2' ≝ typ_of_type ty2 in 351 match classify_sub ty1 ty2 with 352 [ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2) 353  sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2) 354 (* XXX choosing offset sizes? *) 355  sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty)))))) 356  sub_case_pp ty ⇒ 357 match ty' with (* XXX overflow *) 358 [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty))))) 359  _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) 360 ] 361  sub_default ⇒ Error ? (msg TypeMismatch) 350 match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 351 [ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2) 352  sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2) 353 (* XXX could optimise cast as above *) 354  sub_case_pi n r ty sz sg ⇒ 355 λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 (repr ? (sizeof ty)))))) 356 (* XXX check in detail? *) 357  sub_case_pp n1 n2 r1 ty1 r2 ty2 ⇒ 358 λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with 359 [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16 r1 r2) (fix_ptr_type … e1) (fix_ptr_type ??? e2)) (Cst ? (Ointconst I16 (repr ? (sizeof ty2)))))) 360  _ ⇒ Error ? (msg TypeMismatch) 361 ] 362  sub_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 362 363 ]. 363 364 364 365 definition translate_mul ≝ 365 λty1, e1,ty2,e2,ty'.366 λty1,ty2,ty'. 366 367 let ty1' ≝ typ_of_type ty1 in 367 368 let ty2' ≝ typ_of_type ty2 in 368 match classify_ mul ty1 ty2with369 [ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omule1 e2)370  mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulfe1 e2)371  mul_default ⇒Error ? (msg TypeMismatch)369 match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 370 [ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omul …) e1 e2) 371  aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2) 372  aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 372 373 ]. 373 374 374 375 definition translate_div ≝ 375 λty1, e1,ty2,e2,ty'.376 λty1,ty2,ty'. 376 377 let ty1' ≝ typ_of_type ty1 in 377 378 let ty2' ≝ typ_of_type ty2 in 378 match classify_div ty1 ty2 with 379 [ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2) 380  div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2) 381  div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2) 382  div_default ⇒ Error ? (msg TypeMismatch) 379 match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 380 [ aop_case_ii sz sg ⇒ 381 match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with 382 [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivu …) e1 e2) 383  Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odiv …) e1 e2) 384 ] 385  aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2) 386  aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 383 387 ]. 384 388 385 389 definition translate_mod ≝ 386 λty1, e1,ty2,e2,ty'.390 λty1,ty2,ty'. 387 391 let ty1' ≝ typ_of_type ty1 in 388 392 let ty2' ≝ typ_of_type ty2 in 389 match classify_mod ty1 ty2 with 390 [ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2) 391  mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2) 392  mod_default ⇒ Error ? (msg TypeMismatch) 393 match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 394 [ aop_case_ii sz sg ⇒ 395 match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with 396 [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2) 397  Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2) 398 ] 399 (* no float case *) 400  _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 393 401 ]. 394 402 395 403 definition translate_shr ≝ 396 λty1, e1,ty2,e2,ty'.404 λty1,ty2,ty'. 397 405 let ty1' ≝ typ_of_type ty1 in 398 406 let ty2' ≝ typ_of_type ty2 in 399 match classify_shr ty1 ty2 with 400 [ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2) 401  shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2) 402  shr_default ⇒ Error ? (msg TypeMismatch) 407 match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 408 [ aop_case_ii sz sg ⇒ 409 match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with 410 [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2) 411  Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2) 412 ] 413 (* no float case *) 414  _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 415 ]. 416 417 definition complete_cmp : ∀ty'. CMexpr (ASTint I8 Unsigned) → res (CMexpr (typ_of_type ty')) ≝ 418 λty',e. 419 match ty' return λty'. res (CMexpr (typ_of_type ty')) with 420 [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e) 421  _ ⇒ Error ? (msg TypeMismatch) 403 422 ]. 404 423 405 424 definition translate_cmp ≝ 406 λc,ty1, e1,ty2,e2,ty'.425 λc,ty1,ty2,ty'. 407 426 let ty1' ≝ typ_of_type ty1 in 408 427 let ty2' ≝ typ_of_type ty2 in 409 match classify_cmp ty1 ty2 with 410 [ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2) 411  cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2) 412  cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2) 413  cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2) 414  cmp_default ⇒ Error ? (msg TypeMismatch) 428 match classify_cmp ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 429 [ cmp_case_ii sz sg ⇒ 430 match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with 431 [ Unsigned ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpu … c) e1 e2) 432  Signed ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmp … c) e1 e2) 433 ] 434  cmp_case_pp n r ty ⇒ 435 λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2)) 436  cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2) 437  cmp_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 438 ]. 439 440 definition translate_misc_aop ≝ 441 λty1,ty2,ty',op. 442 let ty1' ≝ typ_of_type ty1 in 443 let ty2' ≝ typ_of_type ty2 in 444 match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with 445 [ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ?? (ASTint sz sg) (op sz sg) e1 e2) 446  _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) 415 447 ]. 416 448 … … 419 451 let ty' ≝ typ_of_type ty in 420 452 match op with 421 [ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty' 422  Osub ⇒ translate_sub ty1 e1 ty2 e2 ty' 423  Omul ⇒ translate_mul ty1 e1 ty2 e2 ty' 424  Omod ⇒ translate_mod ty1 e1 ty2 e2 ty' 425  Odiv ⇒ translate_div ty1 e1 ty2 e2 ty' 426  Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2) 427  Oor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2) 428  Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2) 429  Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2) 430  Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty' 431  Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty' 432  One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty' 433  Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty' 434  Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty' 435  Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty' 436  Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty' 437 ]. 453 [ Oadd ⇒ translate_add ty1 ty2 ty e1 e2 454  Osub ⇒ translate_sub ty1 ty2 ty e1 e2 455  Omul ⇒ translate_mul ty1 ty2 ty e1 e2 456  Omod ⇒ translate_mod ty1 ty2 ty e1 e2 457  Odiv ⇒ translate_div ty1 ty2 ty e1 e2 458  Oand ⇒ translate_misc_aop ty1 ty2 ty Oand e1 e2 459  Oor ⇒ translate_misc_aop ty1 ty2 ty Oor e1 e2 460  Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2 461  Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2 462  Oshr ⇒ translate_shr ty1 ty2 ty e1 e2 463  Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2 464  One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2 465  Olt ⇒ translate_cmp Clt ty1 ty2 ty e1 e2 466  Ogt ⇒ translate_cmp Cgt ty1 ty2 ty e1 e2 467  Ole ⇒ translate_cmp Cle ty1 ty2 ty e1 e2 468  Oge ⇒ translate_cmp Cge ty1 ty2 ty e1 e2 469 ]. 470 471 lemma typ_equals : ∀t1,t2. ∀P:∀t. expr t → Prop. ∀v1,v2. 472 typ_should_eq t1 t2 expr v1 = OK ? v2 → 473 P t1 v1 → 474 P t2 v2. 475 * [ * *  *  * ] 476 * try * try * 477 #P #v1 #v2 #E whd in E:(??%?); destruct 478 #H @H 479 qed. 480 481 lemma unfix_ptr_type : ∀r,ty,n,e.∀P:∀t. expr t → Prop. 482 P (typ_of_type (ptr_type r ty n)) e → 483 P (ASTptr r) (fix_ptr_type r ty n e). 484 #r #ty * [ 2: #n ] #e #P #H @H 485 qed. 438 486 439 487 (* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on … … 442 490 a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this 443 491 predicate. *) 492 444 493 lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e. 445 494 expr_vars ? e1 P → … … 449 498 #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2 450 499 whd in ⊢ (??%? → ?); 451 [ cases (classify_add ty1 ty2) 452 [ 3,4: #z ] whd in ⊢ (??%? → ?); 453 [ generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?); 454 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 455 whd in c:(??%?); destruct % [ @H1  % // @H2 ] 456  generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?); 457 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 458 whd in c:(??%?); destruct % [ @H2  % // @H1 ] 459  *: #E destruct (E) % try @H1 @H2 500 [ inversion (classify_add ty1 ty2) in ⊢ ?; 501 [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 E3 change with (typ_should_eq ???? = OK ??) in E4; 502 @(typ_equals … E4) % // 503  #sz #E1 #E2 #E3 destruct >E3 #E4 504 @(typ_equals … E4) % // 505  #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4 506 @(typ_equals … E4) E4 E3 % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) % // ] 507  #n #sz #sg #r #ty0 #E1 #E2 #E3 destruct >E3 #E4 508 @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) % // ] 509  #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct 460 510 ] 461  cases (classify_sub ty1 ty2) 462 [ 3,4: #z] whd in ⊢ (??%? → ?); 463 [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ])? → ?); 464 * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) 465 whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I 466  *: #E destruct (E) % try @H1 try @H2 % // @H2 511  inversion (classify_sub ty1 ty2) in ⊢ ?; 512 [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 513 @(typ_equals … E4) % // 514  #sz #E1 #E2 #E3 destruct >E3 #E4 515 @(typ_equals … E4) % // 516  #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4 517 @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) % // ] 518  #n1 #n2 #r1 #ty1' #r2 #ty2' #E1 #E2 #E3 destruct >E3 519 whd in ⊢ (??%? → ?); cases ty in e ⊢ %; 520 [ 2: #sz #sg #e #E4  4: #r #ty #e #E4  5: #r #ty' #n' #e #E4 521  *: normalize #X1 #X2 try #X3 try #X4 destruct 522 ] whd in E4:(??%?); destruct % // % 523 [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)  @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) ] 524  #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct 467 525 ] 468  cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct 469 % try @H1 @H2 470  cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct 471 % try @H1 @H2 472  cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct 473 % try @H1 @H2 474  6,7,8,9: #E destruct % try @H1 @H2 475  cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 476  11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 526  3,4,5,6,7,8,9,10: inversion (classify_aop ty1 ty2) in ⊢ ?; 527 (* Note that some cases require a split on signedness of integer type. *) 528 [ 1,4,7,10,13,16,19,22: #sz * #E1 #E2 #E3 destruct >E3 #E4 529 @(typ_equals … E4) % // 530  2,5: #sz #E1 #E2 #E3 destruct >E3 #E4 531 @(typ_equals … E4) % // 532  8,11,14,17,20,23: #sz #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct 533  3,6,9,12,15,18,21,24: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct 534 ] 535  11,12,13,14,15,16: inversion (classify_cmp ty1 ty2) in ⊢ ?; 536 [ 1,5,9,13,17,21: #sz * #E1 #E2 #E3 destruct >E3 537  2,6,10,14,18,22: #n #r #ty' #E1 #E2 #E3 destruct >E3 538  3,7,11,15,19,23: #sz #E1 #E2 #E3 destruct >E3 539  *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct 540 ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %; 541 try (normalize #X1 #X2 try #X3 try #X4 try #X5 destruct #FAIL) 542 #sz #sg #e #E4 543 whd in E4:(??%?); destruct % 544 [ 25,27,29,31,33,35: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) 545  26,28,30,32,34,36: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) 546  *: // 547 ] 477 548 ] qed. 549 478 550 479 551 (* We'll need to implement proper translation of pointers if we really do memory … … 532 604 ]. whd normalize nodelta @pi2 533 605 qed. 534 535 (* Small inversion lemma : if the access mode of a type is by reference, then it must be a ptr type. *)536 lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.537 *538 [ 5: #r #ty #n #r' normalize #E destruct @refl539  6: #args #ret #r normalize #E destruct @refl540  *: normalize #a #b try #c try #d destruct541 [ cases a in d; normalize; cases b; normalize #E destruct542  cases a in c; normalize #E destruct543 ]544 ] qed.545 606 546 607 (* Translate Clight exprs into Cminor ones. … … 570 631  By_nothing : error 571 632 *) 572 match access_mode ty with573 [ By_value q ⇒ OK ? «Mem ? r q(Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)633 match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with 634 [ By_value t ⇒ OK ? «Mem t r (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *) 574 635  By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?» 575  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]636  By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 576 637 ] 577 638  Stack n ⇒ λE. 578 639 (* We have decided that the variable should be allocated on the stack, 579 640 * because its adress was taken somewhere or becauste it's a structured data. *) 580 match access_mode ty with581 [ By_value q ⇒ OK ? «Mem ? Any q(Cst ? (Oaddrstack n)), ?»641 match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with 642 [ By_value t ⇒ OK ? «Mem t Any (Cst ? (Oaddrstack n)), ?» 582 643  By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?» 583  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]644  By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 584 645 ] 585 646 (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *) … … 596 657 match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with 597 658 [ ASTptr r ⇒ λe1'. 598 match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with 599 [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (pi1 … e1'), ?» 600  By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; 601 OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉ 602  By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) 603 ] (access_mode_typ ty) 659 match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with 660 [ By_value t ⇒ OK ? «Mem t ? (pi1 … e1'), ?» 661  By_reference r' ⇒ region_should_eq r r' ? e1' 662  By_nothing _ ⇒ Error ? (msg BadlyTypedAccess) 663 ] 604 664  _ ⇒ λ_. Error ? (msg TypeMismatch) 605 665 ] e1' … … 673 733 [ mk_DPair r e1' ⇒ 674 734 do off ← field_offset id fl; 675 match access_mode ty with 676 [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?» 677  By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?» 678  By_nothing ⇒ Error ? (msg BadlyTypedAccess) 735 match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with 736 [ By_value t ⇒ 737 OK ? «Mem t r (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ? 738 (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off)))),?» 739  By_reference r' ⇒ 740 do e1' ← region_should_eq r r' ? e1'; 741 OK ? «Op2 (ASTptr r') (ASTint I16 Signed (* XXX efficiency? *)) (ASTptr r') 742 (Oaddp …) e1' (Cst ? (Ointconst I16 (repr ? off))),?» 743  By_nothing _ ⇒ Error ? (msg BadlyTypedAccess) 679 744 ] 680 745 ] … … 683 748 match e1' with 684 749 [ mk_DPair r e1' ⇒ 685 match access_mode ty return λx. access_mode ty = x → res ? with 686 [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?» 687  By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; 688 OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉ 689  By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) 690 ] (refl ? (access_mode ty)) 750 match access_mode ty return λt.λ_. res (Σz:CMexpr t.?) with 751 [ By_value t ⇒ OK ? «Mem t ? e1', ?» 752  By_reference r' ⇒ region_should_eq r r' ? e1' 753  By_nothing _ ⇒ Error ? (msg BadlyTypedAccess) 754 ] 691 755 ] 692 756  _ ⇒ Error ? (msg BadlyTypedAccess) … … 723 787 do off ← field_offset id fl; 724 788 match e1' with 725 [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?) (❬r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» ❭) 789 [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?) 790 (❬r, «Op2 (ASTptr r) (ASTint I16 Signed (* FIXME inefficient?*)) (ASTptr r) 791 (Oaddp I16 r) e1'' (Cst ? (Ointconst I16 (repr ? off))), ?» ❭) 726 792 ] 727 793  Tunion _ _ ⇒ translate_addr vars e1 … … 733 799 whd try @I 734 800 [ >E whd @refl 735  >(E ? (refl ??)) @refl 736  3,4: @pi2 801  2,3: @pi2 737 802  @(translate_binop_vars … E) @pi2 738 803  % [ % ] @pi2 … … 741 806  % [ @pi2  @I ] 742 807  % [ @pi2  @I ] 743  >(access_mode_typ … E) @refl744 808  @pi2 745 809  @pi2 … … 747 811 ] qed. 748 812 813 (* We provide a function to work out how to do an assignment to an lvalue 814 expression. It is used for both Clight assignments and Clight function call 815 destinations, but doesn't take the value to be assigned so that we can use 816 it to form a single St_store when possible (and avoid introducing an 817 unnecessary temporary variable and assignment). 818 *) 749 819 inductive destination (vars:var_types) : Type[0] ≝ 750 820  IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars 751  MemDest : ∀r:region. memory_chunk →(Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.821  MemDest : ∀r:region. (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars. 752 822 753 823 (* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a … … 767 837 *) 768 838 definition translate_dest ≝ 769 λvars,e1,ty2. 770 do q ← match access_mode ty2 with 771 [ By_value q ⇒ OK ? q 772  By_reference r ⇒ OK ? (Mpointer r) 773  By_nothing ⇒ Error ? (msg BadlyTypedAccess) 774 ]; 775 match e1 with 776 [ Expr ed1 ty1 ⇒ 777 match ed1 with 778 [ Evar id ⇒ 779 do 〈c,t〉 as E ← lookup' vars id; 780 match c return λx.? → ? with 781 [ Local ⇒ λE. OK ? (IdDest vars id t ?) 782  Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0))) 783  Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n))) 784 ] E 785  _ ⇒ 786 do e1' ← translate_addr vars e1; 787 match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r q e1') ] 788 ] 789 ]. 839 λvars,e1. 840 match e1 with 841 [ Expr ed1 ty1 ⇒ 842 match ed1 with 843 [ Evar id ⇒ 844 do 〈c,t〉 as E ← lookup' vars id; 845 match c return λx.? → ? with 846 [ Local ⇒ λE. OK ? (IdDest vars id t ?) 847  Global r ⇒ λE. OK ? (MemDest ? r (Cst ? (Oaddrsymbol id 0))) 848  Stack n ⇒ λE. OK ? (MemDest ? Any (Cst ? (Oaddrstack n))) 849 ] E 850  _ ⇒ 851 do e1' ← translate_addr vars e1; 852 match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r e1') ] 853 ] 854 ]. 790 855 whd // >E @refl 791 856 qed. … … 884 949 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt. stmt_inv vars s) ≝ 885 950 λvars,e1,e2. 886 do e2' ← translate_expr vars e2; 887 do dest ← translate_dest vars e1 (typeof e2);951 do e2' ← translate_expr vars e2; 952 do dest ← translate_dest vars e1; 888 953 match dest with 889 954 [ IdDest id ty p ⇒ 890 955 do e2' ← type_should_eq (typeof e2) ty ? e2'; 891 956 OK ? «St_assign ? id e2', ?» 892  MemDest r q e1' ⇒ OK ? «St_store ? r qe1' e2', ?»957  MemDest r e1' ⇒ OK ? «St_store ? r e1' e2', ?» 893 958 ]. 894 959 % try (//) try (elim e2' //) elim e1' // … … 1046 1111 [ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?» 1047 1112  Sassign e1 e2 ⇒ 1048 do e2' ← translate_expr vars e2; 1049 do dest ← translate_dest vars e1 (typeof e2); (* e1 *)1113 do e2' ← translate_expr vars e2; (* rhs *) 1114 do dest ← translate_dest vars e1; (* e1 *) 1050 1115 match dest with 1051 1116 [ IdDest id ty p ⇒ 1052 1117 do e2' ← type_should_eq (typeof e2) ty ? e2'; 1053 1118 OK ? «〈uv, ul, St_assign ? id e2'〉, ?» 1054  MemDest r qe1' ⇒1055 OK ? «〈uv, ul, St_store ? r qe1' e2'〉, ?»1119  MemDest r e1' ⇒ 1120 OK ? «〈uv, ul, St_store ? r e1' e2'〉, ?» 1056 1121 ] 1057 1122  Scall ret ef args ⇒ … … 1062 1127 [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?» 1063 1128  Some e1 ⇒ 1064 do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)1129 do dest ← translate_dest vars e1; 1065 1130 match dest with 1066 1131 [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?» 1067  MemDest r qe1' ⇒1132  MemDest r e1' ⇒ 1068 1133 let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in 1069 OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r qe1' (Id ? tmp))〉, ?»1134 OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r e1' (Id ? tmp))〉, ?» 1070 1135 ] 1071 1136 ] … … 1364 1429 [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is» 1365 1430  Stack n ⇒ λE. 1366 do q ← match access_mode ty with 1367 [ By_value q ⇒ OK ? q 1368  By_reference r ⇒ OK ? (Mpointer r) 1369  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 1370 ]; 1371 OK ? «〈fgens1, St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?» 1431 OK ? «〈fgens1, St_seq (St_store ? Any (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?» 1372 1432  Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id] 1373 1433 ] E) (OK ? s) params.
Note: See TracChangeset
for help on using the changeset viewer.