Changeset 2588 for src/Clight/SimplifyCasts.ma
 Timestamp:
 Jan 23, 2013, 2:38:06 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r2468 r2588 608 608 λop. match op with [ Oadd ⇒ true  Osub ⇒ true  _ ⇒ false ]. 609 609 610 (* Inversion principle for integer addition *)611 lemma iadd_inv : ∀sz,sg,v1,v2,m, r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m= Some ? r →610 (* Inversion principle for integer addition  wrapper around lemma in frontend_misc *) 611 lemma iadd_inv : ∀sz,sg,v1,v2,m,target_ty,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = Some ? r → 612 612 ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)). 613 #sz #sg #v1 #v2 #m #r 614 elim v1 615 [ 1:  2: #sz' #i  3:  4: #ptr ] 616 whd in ⊢ ((??%?) → ?); normalize nodelta 617 >classify_add_int normalize nodelta #H destruct 618 elim v2 in H; 619 [ 1:  2: #sz'' #i'  3:  4: #ptr' ] 620 whd in ⊢ ((??%?) → ?); #H destruct 621 elim (sz_eq_dec sz' sz'') 622 [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ 623  2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct 624 ] qed. 613 #sz #sg #v1 #v2 #m #ty #r whd @sem_add_ii_inversion qed. 625 614 626 615 (* Inversion principle for integer subtraction. *) 627 lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r → 628 ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)). 629 #sz #sg #v1 #v2 #m #r 630 elim v1 631 [ 1:  2: #sz' #i  3:  4: #ptr ] 632 whd in ⊢ ((??%?) → ?); normalize nodelta 633 >classify_sub_int normalize nodelta #H destruct 634 elim v2 in H; 635 [ 1:  2: #sz'' #i'  3:  4: #ptr' ] 636 whd in ⊢ ((??%?) → ?); #H destruct 637 elim (sz_eq_dec sz' sz'') 638 [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ 639  2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct 640 ] qed. 616 lemma isub_inv : ∀sz,sg,v1,v2,m,target_ty,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = Some ? r → 617 ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)). 618 #sz #sg #v1 #v2 #m #ty #r whd @sem_sub_ii_inversion qed. 641 619 642 620 definition is_int : val → Prop ≝ … … 647 625 648 626 (* "negative" (in the sense of ¬ Some) inversion principle for integer addition *) 649 lemma neg_iadd_inv : ∀sz,sg,v1,v2,m . sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m= None ? →627 lemma neg_iadd_inv : ∀sz,sg,v1,v2,m,target_ty. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = None ? → 650 628 ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ 651 629 ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. 652 #sz #sg #v1 #v2 #m 630 #sz #sg #v1 #v2 #m #ty 653 631 elim v1 654 632 [ 1:  2: #sz' #i  3:  4: #ptr ] … … 666 644 667 645 (* "negative" inversion principle for integer subtraction *) 668 lemma neg_isub_inv : ∀sz,sg,v1,v2,m . sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m= None ? →646 lemma neg_isub_inv : ∀sz,sg,v1,v2,m,target_ty. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = None ? → 669 647 ¬ (is_int v1) ∨ ¬ (is_int v2) ∨ 670 648 ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2. 671 #sz #sg #v1 #v2 #m 649 #sz #sg #v1 #v2 #m #target_ty 672 650 elim v1 673 651 [ 1:  2: #sz' #i  3:  4: #ptr ] … … 684 662 ] qed. 685 663 686 lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m .687 ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?.688 #op #sz #sg #v1 #v2 #m # H664 lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m,target_ty. 665 ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m target_ty = None ?. 666 #op #sz #sg #v1 #v2 #m #target_ty #H 689 667 elim op normalize in match (binop_simplifiable ?); #H destruct 690 668 elim v1 in H; 691 669 [ 1,5:  2,6: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I))  3,7:  4,8: #ptr ] 692 670 #_ 693 whd in match (sem_binary_operation ?????? ); normalize nodelta671 whd in match (sem_binary_operation ???????); normalize nodelta 694 672 >classify_add_int normalize nodelta // 695 673 >classify_sub_int normalize nodelta // … … 1114 1092 cases op in Hop_simplifiable_eq; 1115 1093 [ 1,2:  *: normalize in ⊢ (% → ?); #H destruct (H) ] #_ 1116 [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m )1117  2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m ) ]1118 cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m )1094 [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m (Tint src_sz src_sg)) 1095  2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m (Tint src_sz src_sg)) ] 1096 cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m (Tint src_sz src_sg)) 1119 1097 [ 1,3: #_ #_ #_ normalize @I ] 1120 1098 #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result))) … … 1134 1112 * #val_rhs1 #trace_rhs1 1135 1113 whd in match (m_bind ?????); normalize nodelta 1136 [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) 1137 lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m) 1138  2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m) 1139 lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ] 1140 cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m) 1114 [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg)) 1115 lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg)) 1116  2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg)) 1117 lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m (Tint target_sz target_sg)) ] 1118 cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) 1119 val_rhs1 (Tint target_sz target_sg) m (Tint target_sz target_sg)) 1141 1120 [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?))) 1142 1121 (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *) … … 1270 1249 [ 2,4: * #Heq >Heq #_ elim target_sz // 1271 1250  1,3: #Hlt @(size_lt_to_le ?? Hlt) ] 1272 ] ] ] ] ] 1251 ] ] ] ] ] 1273 1252  23,25: destruct 1274 1253 inversion (Hcast2 ge en m) … … 1461 1440 normalize nodelta >Htype_eq_lhs 1462 1441 cases (exec_bool_of_val lhs_val (typeof lhs1)) 1463 1442 [ 2,4: #error normalize @SimFailNicely 1464 1443  1,3: * 1465 1444 whd in match (m_bind ?????);
Note: See TracChangeset
for help on using the changeset viewer.