fix for KVX

1 files changed, 19 insertions, 307 deletions

diff --git a/kvx/ValueAOpSSA.v b/kvx/ValueAOpSSA.v
index 85d39c0d..8b76f77e 100644
--- a/kvx/ValueAOpSSA.v
+++ b/kvx/ValueAOpSSA.v
@@ -15,89 +15,7 @@
 
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats Values Memory Globalenvs.
-Require Import Op SSA ValueDomainSSA.
-Require Import ExtFloats ExtValues.
-
-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.
-
+Require Import Op ExtValues ExtFloats RTL ValueDomainSSA.
 Definition minf := binop_float ExtFloat.min.
 Definition maxf := binop_float ExtFloat.max.
 Definition minfs := binop_single ExtFloat32.min.
@@ -153,7 +71,7 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
   | Aindexed2, v1::v2::nil => addl v1 v2
   | Aindexed2XS scale, v1::v2::nil => addl v1 (shll v2 (I (Int.repr scale)))
   | Aglobal s ofs, nil => Ptr (Gl s ofs)
-  | Ainstack ofs, nil => Vtop
+  | Ainstack ofs, nil => Ptr (Stk ofs)
   | _, _ => Vbot
   end.
 
@@ -246,7 +164,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop
   | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop
   | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs)
-  | Oaddrstack ofs, nil => Vtop
+  | Oaddrstack ofs, nil => Ptr (Stk ofs)
   | Ocast8signed, v1 :: nil => sign_ext 8 v1
   | Ocast16signed, v1 :: nil => sign_ext 16 v1
   | Oadd, v1::v2::nil => add v1 v2
@@ -396,200 +314,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
 Section SOUNDNESS.
 
 Variable bc: block_classification.
-Variable ge: genv.
+Variable ge: SSA.genv.
 Hypothesis GENV: genv_match bc ge.
 Variable sp: block.
-Hypothesis STACK: bc sp <> BCinvalid.
-
-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.
+Hypothesis STACK: bc sp = BCstack.
 
 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).
@@ -621,7 +349,7 @@ Proof.
   intros v x;
   intro MATCH;
   inversion MATCH;
-  simpl;
+  cbn;
   constructor.
 Qed.
 
@@ -633,9 +361,9 @@ Lemma triple_op_float_sound:
 Proof.
   intros until z.
   intros Hax Hby Hcz.
-  inv Hax; simpl; try constructor;
-  inv Hby; simpl; try constructor;
-  inv Hcz; simpl; try constructor.
+  inv Hax; cbn; try constructor;
+  inv Hby; cbn; try constructor;
+  inv Hcz; cbn; try constructor.
 Qed.
 
 Lemma triple_op_single_sound:
@@ -646,9 +374,9 @@ Lemma triple_op_single_sound:
 Proof.
   intros until z.
   intros Hax Hby Hcz.
-  inv Hax; simpl; try constructor;
-  inv Hby; simpl; try constructor;
-  inv Hcz; simpl; try constructor.
+  inv Hax; cbn; try constructor;
+  inv Hby; cbn; try constructor;
+  inv Hcz; cbn; try constructor.
 Qed.
 
 Lemma fmaddf_sound :
@@ -692,9 +420,9 @@ Proof.
   intros until aargs; intros VM. inv VM.
   destruct cond; auto with va.
   inv H0.
-  destruct cond; simpl; eauto with va.
+  destruct cond; cbn; eauto with va.
   inv H2.
-  destruct cond; simpl; eauto with va.
+  destruct cond; cbn; eauto with va.
   destruct cond; auto with va.
 Qed.
 
@@ -704,7 +432,7 @@ Theorem eval_static_condition0_sound:
   cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg).
 Proof.
   intros until aarg; intro VM.
-  destruct cond; simpl; eauto with va.
+  destruct cond; cbn; eauto with va.
 Qed.
 
 Lemma symbol_address_sound:
@@ -744,7 +472,6 @@ Proof.
   unfold eval_addressing, eval_static_addressing; intros;
   destruct addr; InvHyps; eauto with va.
   rewrite Ptrofs.add_zero_l; eauto with va.
-  constructor; constructor; auto.
 Qed.
 
 Theorem eval_static_addressing_sound_none:
@@ -796,7 +523,6 @@ Proof.
   - destruct (propagate_float_constants tt); constructor.
   - destruct (propagate_float_constants tt); constructor.
   - rewrite Ptrofs.add_zero_l; eauto with va.
-    constructor; constructor; auto.
   - replace(match Val.shl a1 (Vint (int_of_shift1_4 shift)) with
     | Vint n2 => Vint (Int.add n n2)
     | Vptr b2 ofs2 =>
@@ -815,19 +541,9 @@ Proof.
     + eauto with va.
     + destruct n; destruct shift; reflexivity.
   - (* shrx *)
-    inv H1; simpl; try constructor.
-    all: destruct Int.ltu; [simpl | constructor; fail].
+    inv H1; cbn; try constructor.
+    all: destruct Int.ltu; [cbn | constructor; fail].
     all: auto with va.
-  - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
-    | Vlong n2 => Vlong (Int64.add n n2)
-    | Vptr b2 ofs2 =>
-        if Archi.ptr64
-        then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n))
-        else Vundef
-    | _ => Vundef
-             end) with (Val.addl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
-    + eauto with va.
-    + destruct a1; destruct shift; reflexivity.
   - inv H1; constructor.
   - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
     | Vlong n2 => Vlong (Int64.sub n n2)
@@ -835,10 +551,6 @@ Proof.
              end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
     + eauto with va.
     + destruct a1; destruct shift; reflexivity.
-  - (* shrxl *)
-    inv H1; simpl; try constructor.
-    all: destruct Int.ltu; [simpl | constructor; fail].
-    all: auto with va.
   - apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
 
   (* extfz *)
@@ -868,12 +580,12 @@ Proof.
   (* insf *)
   - unfold insf, eval_static_insf.
     destruct (is_bitfield _ _).
-    + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor.
+    + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor.
     + constructor.
   (* insfl *)
   - unfold insfl, eval_static_insfl.
     destruct (is_bitfieldl _ _).
-    + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor.
+    + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor.
     + constructor.
     (* select *)
   - apply select_sound; auto. eapply eval_static_condition0_sound; eauto.