From a3924f657b36abfad0448d0fe7d30fd40e0068de Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Sun, 12 Dec 2021 22:10:22 +0100
Subject: some more fixed etc. constructs

---
 backend/ValueDomain.v | 156 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 156 insertions(+)

(limited to 'backend')

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 5a7cfc12..8c58e32e 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -2269,6 +2269,24 @@ Proof.
   inv H; simpl; auto with va. rewrite E; constructor.
 Qed.
 
+Definition intofsingle_ne (x: aval) :=
+  match x with
+  | FS f =>
+      match Float32.to_int_ne f with
+      | Some i => I i
+      | None => if va_strict tt then Vbot else ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Lemma intofsingle_ne_sound:
+  forall v x w, vmatch v x -> Val.intofsingle_ne v = Some w -> vmatch w (intofsingle_ne x).
+Proof.
+  unfold Val.intofsingle_ne; intros. destruct v; try discriminate.
+  destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl in H0; inv H0.
+  inv H; simpl; auto with va. rewrite E; constructor.
+Qed.
+
 Definition intuofsingle (x: aval) :=
   match x with
   | FS f =>
@@ -2287,6 +2305,24 @@ Proof.
   inv H; simpl; auto with va. rewrite E; constructor.
 Qed.
 
+Definition intuofsingle_ne (x: aval) :=
+  match x with
+  | FS f =>
+      match Float32.to_intu_ne f with
+      | Some i => I i
+      | None => if va_strict tt then Vbot else ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Lemma intuofsingle_ne_sound:
+  forall v x w, vmatch v x -> Val.intuofsingle_ne v = Some w -> vmatch w (intuofsingle_ne x).
+Proof.
+  unfold Val.intuofsingle_ne; intros. destruct v; try discriminate.
+  destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl in H0; inv H0.
+  inv H; simpl; auto with va. rewrite E; constructor.
+Qed.
+
 Definition singleofint (x: aval) :=
   match x with
   | I i => FS(Float32.of_int i)
@@ -2349,6 +2385,42 @@ Proof.
   inv H; simpl; auto with va. rewrite E; constructor.
 Qed.
 
+Definition longoffloat_ne (x: aval) :=
+  match x with
+  | F f =>
+      match Float.to_long_ne f with
+      | Some i => L i
+      | None => if va_strict tt then Vbot else ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Lemma longoffloat_ne_sound:
+  forall v x w, vmatch v x -> Val.longoffloat_ne v = Some w -> vmatch w (longoffloat_ne x).
+Proof.
+  unfold Val.longoffloat_ne; intros. destruct v; try discriminate.
+  destruct (Float.to_long_ne f) as [i|] eqn:E; simpl in H0; inv H0.
+  inv H; simpl; auto with va. rewrite E; constructor.
+Qed.
+
+Definition longuoffloat_ne (x: aval) :=
+  match x with
+  | F f =>
+      match Float.to_longu_ne f with
+      | Some i => L i
+      | None => if va_strict tt then Vbot else ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Lemma longuoffloat_ne_sound:
+  forall v x w, vmatch v x -> Val.longuoffloat_ne v = Some w -> vmatch w (longuoffloat_ne x).
+Proof.
+  unfold Val.longuoffloat_ne; intros. destruct v; try discriminate.
+  destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl in H0; inv H0.
+  inv H; simpl; auto with va. rewrite E; constructor.
+Qed.
+
 Definition floatoflong (x: aval) :=
   match x with
   | L i => F(Float.of_long i)
@@ -2566,6 +2638,46 @@ Definition longuofsingle_total (x: aval) :=
   | _ => ntop1 x
   end.
 
+Definition intofsingle_ne_total (x: aval) :=
+  match x with
+  | FS f =>
+      match Float32.to_int_ne f with
+      | Some i => I i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Definition intuofsingle_ne_total (x: aval) :=
+  match x with
+  | FS f =>
+      match Float32.to_intu_ne f with
+      | Some i => I i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Definition longoffloat_ne_total (x: aval) :=
+  match x with
+  | F f =>
+      match Float.to_long_ne f with
+      | Some i => L i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Definition longuoffloat_ne_total (x: aval) :=
+  match x with
+  | F f =>
+      match Float.to_longu_ne f with
+      | Some i => L i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
 Lemma intoffloat_total_sound:
   forall v x
          (MATCH : vmatch v x),
@@ -2606,6 +2718,26 @@ Proof.
   all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
 Qed.
 
+Lemma intofsingle_ne_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.intofsingle_ne v)) (intofsingle_ne_total x).
+Proof.
+  unfold Val.intofsingle_ne, intofsingle_ne_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
+Lemma intuofsingle_ne_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.intuofsingle_ne v)) (intuofsingle_ne_total x).
+Proof.
+  unfold Val.intofsingle, intofsingle_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
 Lemma singleofint_total_sound:
   forall v x, vmatch v x ->
               vmatch (Val.maketotal (Val.singleofint v)) (singleofint x).
@@ -2648,6 +2780,26 @@ Proof.
   all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
 Qed.
 
+Lemma longoffloat_ne_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.longoffloat_ne v)) (longoffloat_ne_total x).
+Proof.
+  unfold Val.longoffloat_ne, longoffloat_ne_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float.to_long_ne f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
+Lemma longuoffloat_ne_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.longuoffloat_ne v)) (longuoffloat_ne_total x).
+Proof.
+  unfold Val.longoffloat_ne, longoffloat_ne_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
 Lemma longofsingle_total_sound:
   forall v x
          (MATCH : vmatch v x),
@@ -5200,6 +5352,10 @@ Global Hint Resolve cnot_sound symbol_address_sound
        intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound
        longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound
        longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound
+       intofsingle_ne_sound intuofsingle_ne_sound
+       longoffloat_ne_sound longuoffloat_ne_sound
+       intofsingle_ne_total_sound intuofsingle_ne_total_sound
+       longoffloat_ne_total_sound longuoffloat_ne_total_sound
        longofwords_sound loword_sound hiword_sound
        intoffloat_total_sound
        intuoffloat_total_sound
-- 
cgit