From 4df03aaf5204d2f15885b49fe3f5c9cb61b4596d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Feb 2021 18:31:46 +0100 Subject: Ccompu expansion --- riscV/Asmgenproof1.v | 315 +++++++++++++++++++++++++-------------------------- 1 file changed, 154 insertions(+), 161 deletions(-) (limited to 'riscV/Asmgenproof1.v') 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. -- cgit