Changeset 961 for src/Clight/CexecComplete.ma

Timestamp:

Jun 15, 2011, 4:15:52 PM (10 years ago)

Author:

campbell

Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:

• src/Clight/CexecComplete.ma (modified) (10 diffs)

src/Clight/CexecComplete.ma

@@ -100 +100 @@
 #m #v #ty #ty' #v' #H
 elim H;
-[ #m #i #sz1 #sz2 #sg1 #sg2 @refl
+[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
 | #m #f #sz #szi #sg @refl
-| #m #i #sz #sz' #sg @refl
+| #m #sz #sz' #sg #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
 | #m #f #sz #sz' @refl
 | #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
@@ -111 +111 @@
     #pc' whd in ⊢ (??%?) 
     @(dec_true ? (pointer_compat_dec b sp2) pc') //
-| #m #sz #si #ty'' #r #H cases H; //;
+| #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?)
+  >intsize_eq_elim_true whd in ⊢ (??%?) cases sz //;
 | #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
     whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
@@ -131 +132 @@
 lemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ? (exec_bool_of_val v ty) b.
 #v #ty #r #H elim H; #v #t #H' elim H';
-  [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //;
+  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true
+    >(eq_bv_false … ne) //
   | #r #b #pc #i #i0 #s %{ true} % //
   | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
-  | #i #s %{ false} % //;
+  | #sz #sg %{ false} % // whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //
   | #r #r' #t %{ false} % //;
   | #s %{ false} % //; whd; >(Feq_zero_true …) //;
@@ -142 +144 @@
 lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
 #v #ty #H elim H;
-  [ #i #is #s #ne whd; >(eq_false … ne) //;
+  [ #i #is #s #ne whd in ⊢ (??%?) >intsize_eq_elim_true >(eq_bv_false … ne) //;
   | #p #b #i #i0 #s //
   | #f #s #ne whd; >(Feq_zero_false … ne) //;
@@ -150 +152 @@
 lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
 #v #ty #H elim H;
-  [ #i #s //;
+  [ #sz #sg whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //;
   | #r #r' #t //;
   | #s whd; >(Feq_zero_true …) //;
@@ -163 +165 @@
   (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
   (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
-[ #i #ty @refl
+[ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl
 | #f #ty @refl
 | #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
@@ -179 +181 @@
     @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
     @refl
-| #ty' #ty @refl
+| #ty' #sz #sg @refl
 | #op #e #ty #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
     >(yields_eq ??? H3)
@@ -342 +344 @@
 lemma eventval_match_complete': ∀ev,ty,v.
   eventval_match ev ty v → yields ? (check_eventval' v ty) ev.
-#ev #ty #v #H elim H; //; qed.
+#ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl qed.
 
 lemma eventval_list_match_complete: ∀vs,tys,evs.
@@ -431 +433 @@
     | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
     ]
-| #f #e #s #k #env #m #i #tr #H1 whd in ⊢ (??%?);
+| #f #e #s #k #env #m #sz #i #tr #H1 whd in ⊢ (??%?);
     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     @refl
@@ -446 +448 @@
     #H1 #H2
     >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
-    whd; inversion H2; #x #sz [ #sg ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
+    whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
     @refl
 | #v #f #env #k #m @refl