Changeset 1410

Timestamp:

Oct 19, 2011, 11:54:13 AM (9 years ago)

Author:

campbell

Message:

Remove a few old workarounds.

Location:

src

Files:

• Clight/CexecSound.ma (modified) (11 diffs)
• Cminor/toRTLabs.ma (modified) (2 diffs)
• common/FrontEndOps.ma (modified) (1 diff)

src/Clight/CexecSound.ma

@@ -1 +1 @@
 include "Clight/Cexec.ma".
 
-(*include "Plogic/connectives.ma".*)
-
-(* Is rather careful about using destruct because it currently uses excessive
-   normalization. *)
 lemma exec_bool_of_val_sound: ∀v,ty,r.
  exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
@@ -15 +11 @@
   | *; whd @eq_bv_elim
     [ #E1 #E2 destruct @bool_of_val_false @is_false_int
-    | #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E1 | destruct @refl ]
+    | #E1 #E2 destruct @bool_of_val_true @is_true_int_int @E1
     ]
   ]
 | 8: #H cases (eq_dec f Fzero)
   [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
-  | #ne >Feq_zero_false in H // #E >(?:r=¬false) [ @bool_of_val_true @is_true_float @ne | destruct @refl ] 
-  ]
-| 14: #H >(?:r=false) [ @bool_of_val_false @is_false_pointer | destruct @refl ]
-| 15: #H >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer | destruct @refl ]
+  | #ne >Feq_zero_false in H // #E destruct @bool_of_val_true @is_true_float @ne
+  ]
+| 14: #H destruct @bool_of_val_false @is_false_pointer
+| 15: #H destruct @bool_of_val_true @is_true_pointer_pointer
 | *: #H destruct
 ] qed.
 
 lemma bool_val_distinct: Vtrue ≠ Vfalse.
-% #H whd in H:(??%%); (*Wilmer: XXX*) cases daemon (*destruct; @(absurd ? e0 one_not_zero)*)
+% normalize #H destruct
 qed.
 
@@ -50 +46 @@
 qed. 
 
-axiom exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
-(*Wilmer: XXXX #m #v #ty #ty' #v'
+lemma exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
+#m #v #ty #ty' #v'
 cases v;
 [ #H whd in H:(??%?); destruct;
@@ -122 +118 @@
         ]
     ]
-] qed.*)
+] qed.
 
 let rec expr_lvalue_ind
@@ -194 +190 @@
 (P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
 #ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
-(* XXX // fails [ 1,2: #ty #c whd //  *)
 [ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%)
   @eq_intsize_elim #E try @I <E whd % 
-| #ty #c whd %2
+| #ty #c whd //
 (* expressions that are lvalues *)
 | #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %;
@@ -263 +258 @@
         [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
     ]
-| #ty #ty' cases ty try #sz try #sg try #x try @I whd; (* XXX //*) @eval_Esizeof
+| #ty #ty' cases ty try #sz try #sg try #x //
 | #ty #e' #ty' #i cases ty'; //;
     [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
@@ -337 +332 @@
 lemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l).
 #ge #e #m #l elim l;
- whd; (* XXX //; *)
+ whd
 [ %
 | #e1 #es #IH
@@ -402 +397 @@
         //; #H whd;
         @step_skip_call //;
-    | #s' #k' whd; (* XXX //; *) @step_skip_seq
+    | #s' #k' whd; //
     | #ex #s' #k' @step_skip_or_continue_while % //;
     | #ex #s' #k'
@@ -442 +437 @@
         whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety)
     ]
-  | #s1 #s2 whd; (* XXX //; *) @step_seq
+  | #s1 #s2 //
   | #ex #s1 #s2
     @res_bindIO2_OK #v #tr #Hv
@@ -459 +454 @@
     | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     ]
-  | #ex #s' whd; (* XXX //; *) @step_dowhile
+  | #ex #s' // 
   | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
     [ >Hs1
@@ -495 +490 @@
   | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv
     @step_switch @(exec_expr_sound' … Hv)
-  | #l #s' whd; @step_label (* XXX //; *)
+  | #l #s' //
   | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k)));
       cases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
       #sk cases sk; #s' #k' #H
       @(step_goto … H)
-  | #l #s' whd; (* XXX //; *) @step_cost
+  | #l #s' //
   ]
 | #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;

src/Cminor/toRTLabs.ma

@@ -26 +26 @@
       generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
       whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
-      whd in E:(??%?);
-      >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
+      whd in E:(??%?); destruct;
       whd >lookup_add_hit % #A destruct
     | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
@@ -33 +32 @@
       cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)
       * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
-      whd in ⊢ (??%? → ?) #E
-      >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
+      whd in ⊢ (??%? → ?) #E destruct
       @lookup_add_oblivious
       @(IH … E1 ? H)

src/common/FrontEndOps.ma

@@ -145 +145 @@
   [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?) #E' destruct cases (eq_bv ???) whd in ⊢ (?%?) %
   | #r #H #v #v' #H1 @(elim_val_typ … H1) whd %
-    [ whd in ⊢ (??%? → ?) #E'
-      (* XXX need to normalize or destruct is intractable *)
-      normalize in E'; destruct (E') ; %
+    [ whd in ⊢ (??%? → ?) #E' destruct; %
     | #b #c #o whd in ⊢ (??%? → ?) #E' destruct %
     ]