x86: operators Ointoffloat and Ointofsingle are total

This matches the semantics of the corresponding machine instructions,
and will help with branchless code.

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