some more fixed etc. constructs

6 files changed, 206 insertions, 9 deletions

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
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v
index a9786e0a..ac0b359e 100644
--- a/kvx/Asmblockdeps.v
+++ b/kvx/Asmblockdeps.v
@@ -1537,6 +1537,10 @@ Definition string_of_name_rr (n: arith_name_rr): pstring :=
   | Pfixedudrzz => "Pfixedudrzz"
   | Pfixeddrzz_i32 => "Pfixeddrzz_i32"
   | Pfixedudrzz_i32 => "Pfixedudrzz_i32"
+  | Pfixedwrne => "Pfixedwrne"
+  | Pfixeduwrne => "Pfixeduwrne"
+  | Pfixeddrne => "Pfixeddrne"
+  | Pfixedudrne => "Pfixedudrne"
   end.
 
 Definition string_of_name_ri32 (n: arith_name_ri32): pstring :=
diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v
index 4578b4e8..455af70e 100644
--- a/kvx/NeedOp.v
+++ b/kvx/NeedOp.v
@@ -131,6 +131,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv)
   | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
   | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
+  | Ointofsingle_ne | Ointuofsingle_ne => op1 (default nv)
+  | Olongoffloat_ne | Olonguoffloat_ne => op1 (default nv)
   | Ocmp c => needs_of_condition c
   | Oextfz _ _ | Oextfs _ _  | Oextfzl _ _ | Oextfsl _ _ => op1 (default nv)
   | Oinsf _ _ | Oinsfl _ _ => op2 (default nv)
diff --git a/kvx/Op.v b/kvx/Op.v
index 4458adb3..8549fc38 100644
--- a/kvx/Op.v
+++ b/kvx/Op.v
@@ -209,6 +209,11 @@ Inductive operation : Type :=
   | Olonguofsingle           (**r [rd = unsigned_long_of_float32(r1)] *)
   | Osingleoflong            (**r [rd = float32_of_signed_long(r1)] *)
   | Osingleoflongu           (**r [rd = float32_of_unsigned_int(r1)] *)
+  | Ointofsingle_ne          (**r [rd = signed_int_of_float64(r1)] *)
+  | Ointuofsingle_ne         (**r [rd = unsigned_int_of_float64(r1)] *)
+  | Olongoffloat_ne          (**r [rd = signed_long_of_float64(r1)] *)
+  | Olonguoffloat_ne         (**r [rd = unsigned_long_of_float64(r1)] *)
+
 (*c Boolean tests: *)
   | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
   | Oextfz (stop : Z) (start : Z)
@@ -466,6 +471,11 @@ Definition eval_operation
   | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1))
   | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
+  | Ointofsingle_ne, v1::nil => Some (Val.maketotal (Val.intofsingle_ne v1))
+  | Ointuofsingle_ne, v1::nil => Some (Val.maketotal (Val.intuofsingle_ne v1))
+  | Olongoffloat_ne, v1::nil => Some (Val.maketotal (Val.longoffloat_ne v1))
+  | Olonguoffloat_ne, v1::nil => Some (Val.maketotal (Val.longuoffloat_ne v1))
+                                    
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   | (Oextfz stop start), v0::nil => Some (extfz stop start v0)
   | (Oextfs stop start), v0::nil => Some (extfs stop start v0)
@@ -683,6 +693,12 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Olonguofsingle => (Tsingle :: nil, Tlong)
   | Osingleoflong => (Tlong :: nil, Tsingle)
   | Osingleoflongu => (Tlong :: nil, Tsingle)
+
+  | Ointofsingle_ne => (Tsingle :: nil, Tint)
+  | Ointuofsingle_ne => (Tsingle :: nil, Tint)
+  | Olongoffloat_ne => (Tfloat :: nil, Tlong)
+  | Olonguoffloat_ne => (Tfloat :: nil, Tlong)
+                        
   | Ocmp c => (type_of_condition c, Tint)                
   | Oextfz _ _ | Oextfs _ _ => (Tint :: nil, Tint)
   | Oextfzl _ _ | Oextfsl _ _ => (Tlong :: nil, Tlong)
@@ -980,6 +996,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* singleoflong, singleoflongu *)
   - destruct v0; cbn...
   - destruct v0; cbn...
+  (* intofsingle_ne, intuofsingle_ne *)
+  - destruct v0; cbn... destruct (Float32.to_int_ne f); cbn; trivial.
+  - destruct v0; cbn... destruct (Float32.to_intu_ne f); cbn; trivial.
+  (* longoffloat_ne, longuoffloat_ne *)
+  - destruct v0; cbn... destruct (Float.to_long_ne f); cbn; trivial.
+  - destruct v0; cbn... destruct (Float.to_longu_ne f); cbn; trivial.
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
  (* extfz *)
@@ -1669,6 +1691,14 @@ Proof.
   (* singleoflong, singleoflongu *)
   - inv H4; cbn; auto.
   - inv H4; cbn; auto.
+
+  (* intofsingle_ne, intuofsingle_ne *)
+  - inv H4; cbn; auto. destruct (Float32.to_int_ne f0); cbn; auto.
+  - inv H4; cbn; auto. destruct (Float32.to_intu_ne f0); cbn; auto.
+  (* longoffloat_ne, longuoffloat_ne *)
+  - inv H4; cbn; auto. destruct (Float.to_long_ne f0); cbn; auto.
+  - inv H4; cbn; auto. destruct (Float.to_longu_ne f0); cbn; auto.
+    
   (* cmp *)
   - subst v1. destruct (eval_condition cond vl1 m1) eqn:?.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
diff --git a/kvx/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml
index 3f4520a6..f53da14b 100644
--- a/kvx/PostpassSchedulingOracle.ml
+++ b/kvx/PostpassSchedulingOracle.ml
@@ -47,7 +47,8 @@ type real_instruction =
   | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw
   | Fmind | Fminw | Fmaxd | Fmaxw | Finvw
   | Ffmaw | Ffmad | Ffmsw | Ffmsd
-  | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz
+  | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz
+  | Fixedw | Fixeduw | Fixedd | Fixedud
   | Fcompw | Fcompd
 
 type ab_inst_rec = {
@@ -86,12 +87,12 @@ let arith_rr_real = function
   | Pfloatuwrnsz ->     Floatuwz
   | Pfloatudrnsz ->     Floatudz
   | Pfloatdrnsz ->      Floatdz
-  | Pfixedwrzz ->       Fixedwz
-  | Pfixeduwrzz ->      Fixeduwz
-  | Pfixeddrzz ->       Fixeddz
-  | Pfixedudrzz ->      Fixedudz
-  | Pfixeddrzz_i32 ->   Fixeddz
-  | Pfixedudrzz_i32 ->  Fixedudz
+  | Pfixedwrzz | Pfixedwrne ->       Fixedw
+  | Pfixeduwrzz | Pfixeduwrne ->      Fixeduw
+  | Pfixeddrzz | Pfixeddrne -> Fixedd
+  | Pfixedudrzz| Pfixedudrne -> Fixedud
+  | Pfixeddrzz_i32 ->   Fixedd
+  | Pfixedudrzz_i32 ->  Fixedud
 
 let arith_rrr_real = function
   | Pcompw it ->      Compw
@@ -643,7 +644,7 @@ let rec_to_usage r =
   (* TODO: check *)
   | Srsw | Srsd | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding)
   | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
-  | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau
+  | Fixeduw | Fixedw | Floatwz | Floatuwz | Fixedd | Fixedud | Floatdz | Floatudz -> mau
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 
       (match encoding with None | Some U6 | Some S10 -> lsu_auxw
                           | Some U27L5 | Some U27L10 -> lsu_auxw_x
@@ -681,7 +682,7 @@ let real_inst_to_latency = function
   | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved | Addxw | Addxd
   | Fmind | Fmaxd | Fminw | Fmaxw
         -> 1
-  | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
+  | Floatwz | Floatuwz | Fixeduw | Fixedw | Floatdz | Floatudz | Fixedd | Fixedud -> 4
   | Mulw | Muld | Maddw | Maddd | Msbfw | Msbfd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 3
   | Sb | Sh | Sw | Sd | Sq | So -> 1 (* See kvx-Optimization.pdf page 19 *)
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v
index 87554258..4909a25b 100644
--- a/kvx/ValueAOp.v
+++ b/kvx/ValueAOp.v
@@ -298,6 +298,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Olonguofsingle, v1::nil => longuofsingle_total v1
   | Osingleoflong, v1::nil => singleoflong v1
   | Osingleoflongu, v1::nil => singleoflongu v1
+  | Ointofsingle_ne, v1::nil => intofsingle_ne_total v1
+  | Ointuofsingle_ne, v1::nil => intuofsingle_ne_total v1
+  | Olongoffloat_ne, v1::nil => longoffloat_ne_total v1
+  | Olonguoffloat_ne, v1::nil => longuoffloat_ne_total v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
   | (Oextfz stop start), v0::nil => eval_static_extfz stop start v0
   | (Oextfs stop start), v0::nil => eval_static_extfs stop start v0