moved some "total" value domain functions to a central location

2 files changed, 243 insertions, 272 deletions

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 779e7bb9..661d769d 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -2069,7 +2069,6 @@ Definition divfs := binop_single Float32.div.
 Lemma divfs_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divfs v w) (divfs x y).
 Proof (binop_single_sound Float32.div).
-
 (** Conversions *)
 
 Definition zero_ext (nbits: Z) (v: aval) :=
@@ -2483,6 +2482,235 @@ Proof.
   destruct 1; simpl; auto with va.
 Qed.
 
+
+(* Extensions for KVX and Risc-V *)
+
+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.
+
+Definition intuoffloat_total (x: aval) :=
+  match x with
+  | F f =>
+      match Float.to_intu f with
+      | Some i => I i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
+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.
+
+Definition intuofsingle_total (x: aval) :=
+  match x with
+  | FS f =>
+      match Float32.to_intu f with
+      | Some i => I i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Definition longoffloat_total (x: aval) :=
+  match x with
+  | F f =>
+      match Float.to_long f with
+      | Some i => L i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Definition longuoffloat_total (x: aval) :=
+  match x with
+  | F f =>
+      match Float.to_longu f with
+      | Some i => L i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Definition longofsingle_total (x: aval) :=
+  match x with
+  | FS f =>
+      match Float32.to_long f with
+      | Some i => L i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Definition longuofsingle_total (x: aval) :=
+  match x with
+  | FS f =>
+      match Float32.to_longu f with
+      | Some i => L i
+      | None => ntop
+      end
+  | _ => ntop1 x
+  end.
+
+Lemma intoffloat_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.intoffloat v)) (intoffloat_total x).
+Proof.
+  unfold Val.intoffloat, intoffloat_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
+Lemma intuoffloat_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x).
+Proof.
+  unfold Val.intoffloat, intoffloat_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
+Lemma intofsingle_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.intofsingle v)) (intofsingle_total x).
+Proof.
+  unfold Val.intofsingle, intofsingle_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
+Lemma intuofsingle_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x).
+Proof.
+  unfold Val.intofsingle, intofsingle_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float32.to_intu 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).
+Proof.
+  unfold Val.singleofint, singleofint; intros.
+  inv H; simpl.
+  all: auto with va.
+  all: unfold ntop1, provenance.
+  all: try constructor.
+Qed.
+
+Lemma singleofintu_total_sound:
+  forall v x, vmatch v x ->
+              vmatch (Val.maketotal (Val.singleofintu v)) (singleofintu x).
+Proof.
+  unfold Val.singleofintu, singleofintu; intros.
+  inv H; simpl.
+  all: auto with va.
+  all: unfold ntop1, provenance.
+  all: try constructor.
+Qed.
+
+Lemma longoffloat_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.longoffloat v)) (longoffloat_total x).
+Proof.
+  unfold Val.longoffloat, longoffloat_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
+Lemma longuoffloat_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x).
+Proof.
+  unfold Val.longoffloat, longoffloat_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
+Lemma longofsingle_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.longofsingle v)) (longofsingle_total x).
+Proof.
+  unfold Val.longofsingle, longofsingle_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
+Lemma longuofsingle_total_sound:
+  forall v x
+         (MATCH : vmatch v x),
+    vmatch (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x).
+Proof.
+  unfold Val.longofsingle, longofsingle_total. intros.
+  inv MATCH; simpl in *; try constructor.
+  all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+Qed.
+
+Lemma singleoflong_total_sound:
+  forall v x, vmatch v x ->
+              vmatch (Val.maketotal (Val.singleoflong v)) (singleoflong x).
+Proof.
+  unfold Val.singleoflong, singleoflong; intros.
+  inv H; simpl.
+  all: auto with va.
+  all: unfold ntop1, provenance.
+  all: try constructor.
+Qed.
+
+Lemma singleoflongu_total_sound:
+  forall v x, vmatch v x ->
+              vmatch (Val.maketotal (Val.singleoflongu v)) (singleoflongu x).
+Proof.
+  unfold Val.singleoflongu, singleoflongu; intros.
+  inv H; simpl.
+  all: auto with va.
+  all: unfold ntop1, provenance.
+  all: try constructor.
+Qed.
+
+Lemma floatoflong_total_sound:
+  forall v x, vmatch v x ->
+              vmatch (Val.maketotal (Val.floatoflong v)) (floatoflong x).
+Proof.
+  unfold Val.floatoflong, floatoflong; intros.
+  inv H; simpl.
+  all: auto with va.
+  all: unfold ntop1, provenance.
+  all: try constructor.
+Qed.
+
+Lemma floatoflongu_total_sound:
+  forall v x, vmatch v x ->
+              vmatch (Val.maketotal (Val.floatoflongu v)) (floatoflongu x).
+Proof.
+  unfold Val.floatoflongu, floatoflongu; intros.
+  inv H; simpl.
+  all: auto with va.
+  all: unfold ntop1, provenance.
+  all: try constructor.
+Qed.
+
 (** Comparisons and variation intervals *)
 
 Definition cmp_intv (c: comparison) (i: Z * Z) (n: Z) : abool :=
@@ -4734,6 +4962,20 @@ Hint Resolve cnot_sound symbol_address_sound
        longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound
        longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound
        longofwords_sound loword_sound hiword_sound
+       intoffloat_total_sound
+       intuoffloat_total_sound
+       intofsingle_total_sound
+       intuofsingle_total_sound
+       singleofint_total_sound
+       singleofintu_total_sound
+       longoffloat_total_sound
+       longuoffloat_total_sound
+       longofsingle_total_sound
+       longuofsingle_total_sound
+       singleoflong_total_sound
+       singleoflongu_total_sound
+       floatoflong_total_sound
+       floatoflongu_total_sound
        cmpu_bool_sound cmp_bool_sound cmplu_bool_sound cmpl_bool_sound
        cmpf_bool_sound cmpfs_bool_sound
        maskzero_sound : va.
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v
index e634fdc0..ed8de163 100644
--- a/kvx/ValueAOp.v
+++ b/kvx/ValueAOp.v
@@ -16,87 +16,6 @@
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op ExtValues ExtFloats RTL ValueDomain.
-
-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.
-
-Definition intuoffloat_total (x: aval) :=
-  match x with
-  | F f =>
-      match Float.to_intu f with
-      | Some i => I i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-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.
-
-Definition intuofsingle_total (x: aval) :=
-  match x with
-  | FS f =>
-      match Float32.to_intu f with
-      | Some i => I i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition longoffloat_total (x: aval) :=
-  match x with
-  | F f =>
-      match Float.to_long f with
-      | Some i => L i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition longuoffloat_total (x: aval) :=
-  match x with
-  | F f =>
-      match Float.to_longu f with
-      | Some i => L i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition longofsingle_total (x: aval) :=
-  match x with
-  | FS f =>
-      match Float32.to_long f with
-      | Some i => L i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
-Definition longuofsingle_total (x: aval) :=
-  match x with
-  | FS f =>
-      match Float32.to_longu f with
-      | Some i => L i
-      | None => ntop
-      end
-  | _ => ntop1 x
-  end.
-
 Definition minf := binop_float ExtFloat.min.
 Definition maxf := binop_float ExtFloat.max.
 Definition minfs := binop_single ExtFloat32.min.
@@ -400,196 +319,6 @@ Hypothesis GENV: genv_match bc ge.
 Variable sp: block.
 Hypothesis STACK: bc sp = BCstack.
 
-Lemma intoffloat_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.intoffloat v)) (intoffloat_total x).
-Proof.
-  unfold Val.intoffloat, intoffloat_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve intoffloat_total_sound : va.
-
-Lemma intuoffloat_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x).
-Proof.
-  unfold Val.intoffloat, intoffloat_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve intuoffloat_total_sound : va.
-
-Lemma intofsingle_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.intofsingle v)) (intofsingle_total x).
-Proof.
-  unfold Val.intofsingle, intofsingle_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve intofsingle_total_sound : va.
-
-Lemma intuofsingle_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x).
-Proof.
-  unfold Val.intofsingle, intofsingle_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve intuofsingle_total_sound : va.
-
-Lemma singleofint_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.singleofint v)) (singleofint x).
-Proof.
-  unfold Val.singleofint, singleofint; intros.
-  inv H; simpl.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve singleofint_total_sound : va.
-
-Lemma singleofintu_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.singleofintu v)) (singleofintu x).
-Proof.
-  unfold Val.singleofintu, singleofintu; intros.
-  inv H; simpl.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve singleofintu_total_sound : va.
-
-Lemma longoffloat_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.longoffloat v)) (longoffloat_total x).
-Proof.
-  unfold Val.longoffloat, longoffloat_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve longoffloat_total_sound : va.
-
-Lemma longuoffloat_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x).
-Proof.
-  unfold Val.longoffloat, longoffloat_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve longuoffloat_total_sound : va.
-
-Lemma longofsingle_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.longofsingle v)) (longofsingle_total x).
-Proof.
-  unfold Val.longofsingle, longofsingle_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve longofsingle_total_sound : va.
-
-Lemma longuofsingle_total_sound:
-  forall v x
-         (MATCH : vmatch bc v x),
-    vmatch bc (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x).
-Proof.
-  unfold Val.longofsingle, longofsingle_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
-  unfold ntop1, provenance.
-  destruct (va_strict tt); constructor.
-Qed.
-
-Hint Resolve longuofsingle_total_sound : va.
-
-Lemma singleoflong_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.singleoflong v)) (singleoflong x).
-Proof.
-  unfold Val.singleoflong, singleoflong; intros.
-  inv H; simpl.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve singleoflong_total_sound : va.
-
-Lemma singleoflongu_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.singleoflongu v)) (singleoflongu x).
-Proof.
-  unfold Val.singleoflongu, singleoflongu; intros.
-  inv H; simpl.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve singleoflongu_total_sound : va.
-
-Lemma floatoflong_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.floatoflong v)) (floatoflong x).
-Proof.
-  unfold Val.floatoflong, floatoflong; intros.
-  inv H; simpl.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve floatoflong_total_sound : va.
-
-Lemma floatoflongu_total_sound:
-  forall v x, vmatch bc v x ->
-              vmatch bc (Val.maketotal (Val.floatoflongu v)) (floatoflongu x).
-Proof.
-  unfold Val.floatoflongu, floatoflongu; intros.
-  inv H; simpl.
-  all: auto with va.
-  all: unfold ntop1, provenance.
-  all: try constructor.
-Qed.
-
-Hint Resolve floatoflongu_total_sound : va.
-
 Lemma minf_sound:
   forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y).
 Proof.