From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/SelectOpproof.v | 102 +++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 94 insertions(+), 8 deletions(-) (limited to 'ia32/SelectOpproof.v') diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 0fd6f7b..5068862 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -567,6 +567,31 @@ Proof. red; intros; TrivialExists. Qed. +Theorem eval_negfs: unary_constructor_sound negfs Val.negfs. +Proof. + red; intros. TrivialExists. +Qed. + +Theorem eval_absfs: unary_constructor_sound absfs Val.absfs. +Proof. + red; intros. TrivialExists. +Qed. + +Theorem eval_addfs: binary_constructor_sound addfs Val.addfs. +Proof. + red; intros; TrivialExists. +Qed. + +Theorem eval_subfs: binary_constructor_sound subfs Val.subfs. +Proof. + red; intros; TrivialExists. +Qed. + +Theorem eval_mulfs: binary_constructor_sound mulfs Val.mulfs. +Proof. + red; intros; TrivialExists. +Qed. + Section COMP_IMM. Variable default: comparison -> int -> condition. @@ -674,6 +699,12 @@ Proof. intros; red; intros. unfold compf. TrivialExists. Qed. +Theorem eval_compfs: + forall c, binary_constructor_sound (compfs c) (Val.cmpfs c). +Proof. + intros; red; intros. unfold compfs. TrivialExists. +Qed. + Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). Proof. red; intros until x. unfold cast8signed. case (cast8signed_match a); intros; InvEval. @@ -711,6 +742,11 @@ Proof. red; intros. unfold singleoffloat. TrivialExists. Qed. +Theorem eval_floatofsingle: unary_constructor_sound floatofsingle Val.floatofsingle. +Proof. + red; intros. unfold floatofsingle. TrivialExists. +Qed. + Theorem eval_intoffloat: forall le a x y, eval_expr ge sp e m le a x -> @@ -738,10 +774,10 @@ Theorem eval_intuoffloat: exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v. Proof. intros. destruct x; simpl in H0; try discriminate. - destruct (Float.intuoffloat f) as [n|] eqn:?; simpl in H0; inv H0. + destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. set (im := Int.repr Int.half_modulus). - set (fm := Float.floatofintu im). + set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). constructor. auto. assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar O) (Vfloat fm)). @@ -751,9 +787,9 @@ Proof. eapply eval_Econdition with (va := Float.cmp Clt f fm). eauto with evalexpr. destruct (Float.cmp Clt f fm) eqn:?. - exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ. + exploit Float.to_intu_to_int_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. - exploit Float.intuoffloat_intoffloat_2; eauto. + exploit Float.to_intu_to_int_2; eauto. change Float.ox8000_0000 with im. fold fm. intro EQ. set (t2 := subf (Eletvar (S O)) (Eletvar O)). set (t3 := intoffloat t2). @@ -778,25 +814,75 @@ Proof. intros until y; unfold floatofintu. case (floatofintu_match a); intros. InvEval. TrivialExists. destruct x; simpl in H0; try discriminate. inv H0. - exists (Vfloat (Float.floatofintu i)); split; auto. + exists (Vfloat (Float.of_intu i)); split; auto. econstructor. eauto. - set (fm := Float.floatofintu Float.ox8000_0000). + set (fm := Float.of_intu Float.ox8000_0000). assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)). constructor. auto. eapply eval_Econdition with (va := Int.ltu i Float.ox8000_0000). eauto with evalexpr. destruct (Int.ltu i Float.ox8000_0000) eqn:?. - rewrite Float.floatofintu_floatofint_1; auto. + rewrite Float.of_intu_of_int_1; auto. unfold floatofint. EvalOp. exploit (eval_addimm (Int.neg Float.ox8000_0000) (Vint i :: le) (Eletvar 0)); eauto. simpl. intros [v [A B]]. inv B. unfold addf. EvalOp. constructor. unfold floatofint. EvalOp. simpl; eauto. constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. - fold fm. rewrite Float.floatofintu_floatofint_2; auto. + fold fm. rewrite Float.of_intu_of_int_2; auto. rewrite Int.sub_add_opp. auto. Qed. +Theorem eval_intofsingle: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.intofsingle x = Some y -> + exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v. +Proof. + intros; unfold intofsingle. TrivialExists. +Qed. + +Theorem eval_singleofint: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.singleofint x = Some y -> + exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v. +Proof. + intros until y; unfold singleofint. case (singleofint_match a); intros; InvEval. + TrivialExists. + TrivialExists. +Qed. + +Theorem eval_intuofsingle: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.intuofsingle x = Some y -> + exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v. +Proof. + intros. destruct x; simpl in H0; try discriminate. + destruct (Float32.to_intu f) as [n|] eqn:?; simpl in H0; inv H0. + unfold intuofsingle. apply eval_intuoffloat with (Vfloat (Float.of_single f)). + unfold floatofsingle. EvalOp. + simpl. change (Float.of_single f) with (Float32.to_double f). + erewrite Float32.to_intu_double; eauto. auto. +Qed. + +Theorem eval_singleofintu: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.singleofintu x = Some y -> + exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v. +Proof. + intros until y; unfold singleofintu. case (singleofintu_match a); intros. + InvEval. TrivialExists. + destruct x; simpl in H0; try discriminate. inv H0. + exploit eval_floatofintu. eauto. simpl. reflexivity. + intros (v & A & B). + exists (Val.singleoffloat v); split. + unfold singleoffloat; EvalOp. + inv B; simpl. rewrite Float32.of_intu_double. auto. +Qed. + Theorem eval_addressing: forall le chunk a v b ofs, eval_expr ge sp e m le a v -> -- cgit v1.2.3