Ccompu expansion

1 files changed, 154 insertions, 161 deletions

diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 06b33592..6c722798 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -964,190 +964,183 @@ Proof.
 Opaque Int.eq.
   intros until c; intros TR EV.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl.
-- (* move *)
-  destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl.
-- (* intconst *)
-  exploit loadimm32_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* longconst *)
-  exploit loadimm64_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* floatconst *)
-  destruct (Float.eq_dec n Float.zero).
-+ subst n. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-- (* singleconst *)
-  destruct (Float32.eq_dec n Float32.zero).
-+ subst n. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-- (* addrsymbol *)
-  destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
-+ set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
-  exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. 
-  intros (rs2 & A & B & C).
-  exists rs2; split. 
-  apply exec_straight_step with rs1 m; auto.
-  split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). 
-  rewrite Genv.shift_symbol_address.
-  replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl).
-  exact B.
-  intros. rewrite C by eauto with asmgen. unfold rs1; Simpl.  
-+ TranslOpSimpl.
-- (* stackoffset *)
-  exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C).
-  exists rs'; split; eauto. auto with asmgen.
-- (* cast8signed *)
-  econstructor; split.
+  (* move *)
+  { destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. }
+  (* intconst *)
+  { exploit loadimm32_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* longconst *)
+  { exploit loadimm64_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* floatconst *)
+  { destruct (Float.eq_dec n Float.zero).
+    + subst n. econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. 
+    + econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. }
+  (* singleconst *)
+  { destruct (Float32.eq_dec n Float32.zero).
+    + subst n. econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. 
+    + econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. }
+  (* addrsymbol *)
+  { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
+    + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
+      exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. 
+      intros (rs2 & A & B & C).
+      exists rs2; split. 
+      apply exec_straight_step with rs1 m; auto.
+      split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). 
+      rewrite Genv.shift_symbol_address.
+      replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl).
+      exact B.
+      intros. rewrite C by eauto with asmgen. unfold rs1; Simpl.  
+    + TranslOpSimpl. }
+  (* stackoffset *)
+  { exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C).
+  exists rs'; split; eauto. auto with asmgen. }
+  (* cast8signed *)
+  { econstructor; split.
   eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
   split; intros; Simpl.
   assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
   destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
-  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
-- (* cast16signed *)
-  econstructor; split.
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
+  (* cast16signed *)
+  { econstructor; split.
   eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
   split; intros; Simpl.
   assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
   destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
-  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
-- (* addimm *)
-  exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen.
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
+  (* addimm *)
+  { exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. 
-- (* andimm *)
-  exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* andimm *)
+  { exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* orimm *)
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* orimm *)
   exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen.
+  { intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* xorimm *)
+  { exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* xorimm *)
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* shrximm *)
-  destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn.
-  {
-  exploit Val.shrx_shr_3; eauto. intros E; subst v.
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-  * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  }
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-  * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  
-- (* longofintu *)
-  econstructor; split.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* shrximm *)
+  { destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn.
+    {
+    exploit Val.shrx_shr_3; eauto. intros E; subst v.
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl.
+    }
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl. }
+  (* longofintu *)
+  { econstructor; split.
   eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto.
   split; intros; Simpl. destruct (rs x0); auto. simpl. 
   assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
   rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal.
-  rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto.
-- (* addlimm *)
-  exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
+  rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. }
+  (* addlimm *)
+  { exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. 
-- (* andimm *)
-  exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* andimm *)
+  { exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* orimm *)
-  exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* orimm *)
+  { exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* xorimm *)
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* xorimm *)
+  { exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* shrxlimm *)
-  destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
-  {
-   exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-
-  * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  }
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-
-  * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  
-- (* cond *)
-  exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. eauto with asmgen.
-- destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* shrxlimm *)
+  { destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
+    {
+     exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+
+    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl.
+    }
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+
+    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl. }
+  (* cond *)
+  { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. eauto with asmgen. }
+  (* Expanded instructions from RTL *)
+  1-4: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
   econstructor; split; try apply exec_straight_one; simpl; eauto;
   split; intros; Simpl.
-- destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
   econstructor; split; try apply exec_straight_one; simpl; eauto;
-  split; intros; Simpl.
-- destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
-  econstructor; split; try apply exec_straight_one; simpl; eauto;
-  split; intros; Simpl.
-- econstructor; split; try apply exec_straight_one; simpl; eauto;
   split; intros; Simpl. rewrite Int.add_commut. auto.
 Qed.