From f92ca339e9d1851fa4d469cdc867bfe1719c42a1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 6 Jun 2019 16:54:17 +0200 Subject: x86: operators Ointoffloat and Ointofsingle are total This matches the semantics of the corresponding machine instructions, and will help with branchless code. --- backend/ValueDomain.v | 35 +++++++++++++++++++++++++++++++++++ x86/Asmgenproof1.v | 4 ---- x86/Op.v | 14 ++++++-------- x86/SelectOpproof.v | 6 ++++-- x86/ValueAOp.v | 4 ++-- 5 files changed, 47 insertions(+), 16 deletions(-) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index f6afa836..7ad138cf 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2187,6 +2187,23 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition intoffloat_total (x: aval) := + match x with + | F f => + match Float.to_int f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Lemma intoffloat_total_sound: + forall v x, vmatch v x -> vmatch (Val.maketotal (Val.intoffloat v)) (intoffloat_total x). +Proof. + unfold Val.maketotal, Val.intoffloat, intoffloat_total; intros. + inv H; auto with va; destruct (Float.to_int f); auto with va. +Qed. + Definition intuoffloat (x: aval) := match x with | F f => @@ -2249,6 +2266,23 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition intofsingle_total (x: aval) := + match x with + | FS f => + match Float32.to_int f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Lemma intofsingle_total_sound: + forall v x, vmatch v x -> vmatch (Val.maketotal (Val.intofsingle v)) (intofsingle_total x). +Proof. + unfold Val.maketotal, Val.intofsingle, intofsingle_total; intros. + inv H; auto with va; destruct (Float32.to_int f); auto with va. +Qed. + Definition intuofsingle (x: aval) := match x with | FS f => @@ -4675,6 +4709,7 @@ Hint Resolve cnot_sound symbol_address_sound singleoffloat_sound floatofsingle_sound intoffloat_sound intuoffloat_sound floatofint_sound floatofintu_sound intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound + intoffloat_total_sound intofsingle_total_sound longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound longofwords_sound loword_sound hiword_sound diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index fd88954e..225c71ba 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -1431,12 +1431,8 @@ Transparent destroyed_by_op. rewrite Pregmap.gss. rewrite <- EV; auto. intros; Simplifs. TranslOp. rewrite nextinstr_inv; auto with asmgen. rewrite Pregmap.gss; auto. rewrite <- EV; auto. -(* intoffloat *) - apply SAME. TranslOp. rewrite H0; auto. (* floatofint *) apply SAME. TranslOp. rewrite H0; auto. -(* intofsingle *) - apply SAME. TranslOp. rewrite H0; auto. (* singleofint *) apply SAME. TranslOp. rewrite H0; auto. (* longoffloat *) diff --git a/x86/Op.v b/x86/Op.v index 16d75426..6191d607 100644 --- a/x86/Op.v +++ b/x86/Op.v @@ -400,9 +400,9 @@ Definition eval_operation | Odivfs, v1::v2::nil => Some(Val.divfs v1 v2) | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1) - | Ointoffloat, v1::nil => Val.intoffloat v1 + | Ointoffloat, v1::nil => Some(Val.maketotal (Val.intoffloat v1)) | Ofloatofint, v1::nil => Val.floatofint v1 - | Ointofsingle, v1::nil => Val.intofsingle v1 + | Ointofsingle, v1::nil => Some(Val.maketotal (Val.intofsingle v1)) | Osingleofint, v1::nil => Val.singleofint v1 | Olongoffloat, v1::nil => Val.longoffloat v1 | Ofloatoflong, v1::nil => Val.floatoflong v1 @@ -730,9 +730,9 @@ Proof with (try exact I; try reflexivity). destruct v0; destruct v1... destruct v0... destruct v0... - destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... + destruct v0... simpl; destruct (Float.to_int f)... destruct v0; simpl in H0; inv H0... - destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2... + destruct v0... simpl; destruct (Float32.to_int f)... destruct v0; simpl in H0; inv H0... destruct v0; simpl in H0; inv H0. destruct (Float.to_long f); inv H2... destruct v0; simpl in H0; inv H0... @@ -1298,11 +1298,9 @@ Proof. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. inv H4; simpl; auto. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2. - exists (Vint i); auto. + inv H4; simpl; auto. destruct (Float.to_int f0); simpl; auto. inv H4; simpl in H1; inv H1. simpl. TrivialExists. - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2. - exists (Vint i); auto. + inv H4; simpl; auto. destruct (Float32.to_int f0); simpl; auto. inv H4; simpl in H1; inv H1. simpl. TrivialExists. inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_long f0); simpl in H2; inv H2. exists (Vlong i); auto. diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index 908d6e4a..f7f043eb 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -811,7 +811,8 @@ Theorem eval_intoffloat: Val.intoffloat x = Some y -> exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v. Proof. - intros; unfold intoffloat. TrivialExists. + intros; unfold intoffloat. exists y; split; auto. + EvalOp. simpl; rewrite H0; auto. Qed. Theorem eval_floatofint: @@ -909,7 +910,8 @@ Theorem eval_intofsingle: 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. + intros; unfold intoffloat. exists y; split; auto. + EvalOp. simpl; rewrite H0; auto. Qed. Theorem eval_singleofint: diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v index d0b8427a..f9169add 100644 --- a/x86/ValueAOp.v +++ b/x86/ValueAOp.v @@ -151,9 +151,9 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Odivfs, v1::v2::nil => divfs v1 v2 | Osingleoffloat, v1::nil => singleoffloat v1 | Ofloatofsingle, v1::nil => floatofsingle v1 - | Ointoffloat, v1::nil => intoffloat v1 + | Ointoffloat, v1::nil => intoffloat_total v1 | Ofloatofint, v1::nil => floatofint v1 - | Ointofsingle, v1::nil => intofsingle v1 + | Ointofsingle, v1::nil => intofsingle_total v1 | Osingleofint, v1::nil => singleofint v1 | Olongoffloat, v1::nil => longoffloat v1 | Ofloatoflong, v1::nil => floatoflong v1 -- cgit