cond and branches expanded

1 files changed, 71 insertions, 10 deletions

diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 49635ebd..429c5fec 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -292,7 +292,7 @@ Qed.
 
 (** Translation of conditional branches *)
 
-Lemma transl_cbranch_int32s_correct:
+(* TODO REMOVE Lemma transl_cbranch_int32s_correct:
   forall cmp r1 r2 lbl (rs: regset) m b,
   Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
   exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m =
@@ -375,16 +375,16 @@ Proof.
   rewrite <- Float32.cmp_swap. auto.
 - simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
   rewrite <- Float32.cmp_swap. auto.
-Qed.
+   Qed.*)
 
-Remark branch_on_X31:
+(* TODO UNUSUED ? Remark branch_on_X31:
   forall normal lbl (rs: regset) m b,
   rs#X31 = Val.of_bool (eqb normal b) -> 
   exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m =
   eval_branch fn lbl rs m (Some b).
 Proof.
   intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. 
-Qed.
+   Qed.*)
 
 Ltac ArgsInv :=
   repeat (match goal with
@@ -417,7 +417,7 @@ Proof.
   { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
   clear EVAL MEXT AG.
   destruct cond; simpl in TRANSL; ArgsInv.
-- exists rs, (transl_cbranch_int32s c0 x x0 lbl).
+  (* TODO REMOVE - exists rs, (transl_cbranch_int32s c0 x x0 lbl).
   intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
 - exists rs, (transl_cbranch_int32u c0 x x0 lbl).
   intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
@@ -492,7 +492,68 @@ Proof.
   econstructor; econstructor.
   split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
   split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
+     intros; Simpl.*)
+
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero32, Op.zero32 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
+- destruct optR0 as [[]|];
+  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+  unfold zero64, Op.zero64 in *;
+  eexists; eexists; eauto; split; constructor;
+  simpl in *; try rewrite EVAL'; auto.
 Qed.
 
 Lemma transl_cbranch_correct_true:
@@ -528,7 +589,7 @@ Qed.
 
 (** Translation of condition operators *)
 
-Lemma transl_cond_int32s_correct:
+(* TODO REMOVE Lemma transl_cond_int32s_correct:
   forall cmp rd r1 r2 k rs m,
   exists rs',
      exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
@@ -830,9 +891,9 @@ Proof.
 + apply DFL.
 + apply DFL.
 + apply DFL.
-Qed.
+   Qed.
 
-(* TODO Lemma transl_cond_op_correct:
+Lemma transl_cond_op_correct:
   forall cond rd args k c rs m,
   transl_cond_op cond rd args k = OK c ->
   exists rs',
@@ -1134,7 +1195,7 @@ Opaque Int.eq.
       apply exec_straight_one. simpl; reflexivity. auto. 
       split; intros; Simpl. }
   (* cond *)
-  (* TODO { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
+  (* TODO REMOVE { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
      exists rs'; split. eexact A. eauto with asmgen. }*)
   (* Expanded instructions from RTL *)
   5: econstructor; split; try apply exec_straight_one; simpl; eauto;