diff options
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/Asm.v | 8 | ||||
| -rw-r--r-- | x86/Asmgen.v | 41 | ||||
| -rw-r--r-- | x86/Asmgenproof.v | 2 | ||||
| -rw-r--r-- | x86/Asmgenproof1.v | 119 | ||||
| -rw-r--r-- | x86/Op.v | 27 | ||||
| -rw-r--r-- | x86/PrintOp.ml | 18 | ||||
| -rw-r--r-- | x86/SelectOp.vp | 6 | ||||
| -rw-r--r-- | x86/SelectOpproof.v | 4 | ||||
| -rw-r--r-- | x86/ValueAOp.v | 2 |
9 files changed, 97 insertions, 130 deletions
@@ -451,8 +451,8 @@ Definition compare_longs (x y: val) (rs: regset) (m: mem): regset := Definition compare_floats (vx vy: val) (rs: regset) : regset := match vx, vy with | Vfloat x, Vfloat y => - rs #ZF <- (Val.of_bool (Float.cmp Ceq x y || negb (Float.ordered x y))) - #CF <- (Val.of_bool (negb (Float.cmp Cge x y))) + rs #ZF <- (Val.of_bool (Float.cmp FCeq x y || negb (Float.ordered x y))) + #CF <- (Val.of_bool (negb (Float.cmp FCge x y))) #PF <- (Val.of_bool (negb (Float.ordered x y))) #SF <- Vundef #OF <- Vundef @@ -463,8 +463,8 @@ Definition compare_floats (vx vy: val) (rs: regset) : regset := Definition compare_floats32 (vx vy: val) (rs: regset) : regset := match vx, vy with | Vsingle x, Vsingle y => - rs #ZF <- (Val.of_bool (Float32.cmp Ceq x y || negb (Float32.ordered x y))) - #CF <- (Val.of_bool (negb (Float32.cmp Cge x y))) + rs #ZF <- (Val.of_bool (Float32.cmp FCeq x y || negb (Float32.ordered x y))) + #CF <- (Val.of_bool (negb (Float32.cmp FCge x y))) #PF <- (Val.of_bool (negb (Float32.ordered x y))) #SF <- Vundef #OF <- Vundef diff --git a/x86/Asmgen.v b/x86/Asmgen.v index dedbfbe6..700bbe2c 100644 --- a/x86/Asmgen.v +++ b/x86/Asmgen.v @@ -165,16 +165,16 @@ Definition normalize_addrmode_64 (a: addrmode) := (** Floating-point comparison. We swap the operands in some cases to simplify the handling of the unordered case. *) -Definition floatcomp (cmp: comparison) (r1 r2: freg) : instruction := +Definition floatcomp (cmp: fp_comparison) (r1 r2: freg) : instruction := match cmp with - | Clt | Cle => Pcomisd_ff r2 r1 - | Ceq | Cne | Cgt | Cge => Pcomisd_ff r1 r2 + | FClt | FCle | FCnotlt | FCnotle => Pcomisd_ff r2 r1 + | FCeq | FCne | FCgt | FCge | FCnotgt | FCnotge => Pcomisd_ff r1 r2 end. -Definition floatcomp32 (cmp: comparison) (r1 r2: freg) : instruction := +Definition floatcomp32 (cmp: fp_comparison) (r1 r2: freg) : instruction := match cmp with - | Clt | Cle => Pcomiss_ff r2 r1 - | Ceq | Cne | Cgt | Cge => Pcomiss_ff r1 r2 + | FClt | FCle | FCnotlt | FCnotle => Pcomiss_ff r2 r1 + | FCeq | FCne | FCgt | FCge | FCnotgt | FCnotge => Pcomiss_ff r1 r2 end. (** Translation of a condition. Prepends to [k] the instructions @@ -204,12 +204,8 @@ Definition transl_cond do r1 <- ireg_of a1; OK (Pcmpq_ri r1 n :: k) | Ccompf cmp, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k) - | Cnotcompf cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k) | Ccompfs cmp, a1 :: a2 :: nil => do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp32 cmp r1 r2 :: k) - | Cnotcompfs cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp32 cmp r1 r2 :: k) | Cmaskzero n, a1 :: nil => do r1 <- ireg_of a1; OK (Ptestl_ri r1 n :: k) | Cmasknotzero n, a1 :: nil => @@ -257,21 +253,16 @@ Definition testcond_for_condition (cond: condition) : extcond := | Ccompluimm c n => Cond_base(testcond_for_unsigned_comparison c) | Ccompf c | Ccompfs c => match c with - | Ceq => Cond_and Cond_np Cond_e - | Cne => Cond_or Cond_p Cond_ne - | Clt => Cond_base Cond_a - | Cle => Cond_base Cond_ae - | Cgt => Cond_base Cond_a - | Cge => Cond_base Cond_ae - end - | Cnotcompf c | Cnotcompfs c => - match c with - | Ceq => Cond_or Cond_p Cond_ne - | Cne => Cond_and Cond_np Cond_e - | Clt => Cond_base Cond_be - | Cle => Cond_base Cond_b - | Cgt => Cond_base Cond_be - | Cge => Cond_base Cond_b + | FCeq => Cond_and Cond_np Cond_e + | FCne => Cond_or Cond_p Cond_ne + | FClt => Cond_base Cond_a + | FCle => Cond_base Cond_ae + | FCgt => Cond_base Cond_a + | FCge => Cond_base Cond_ae + | FCnotlt => Cond_base Cond_be + | FCnotle => Cond_base Cond_b + | FCnotgt => Cond_base Cond_be + | FCnotge => Cond_base Cond_b end | Cmaskzero n => Cond_base Cond_e | Cmasknotzero n => Cond_base Cond_ne diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index 3aa87a4c..ab177167 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -205,8 +205,6 @@ Proof. destruct (Int64.eq_dec n Int64.zero); TailNoLabel. destruct c0; simpl; TailNoLabel. destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. Qed. Remark transl_op_label: diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index 904debdc..c638cdcf 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -700,8 +700,8 @@ Qed. Lemma compare_floats_spec: forall rs n1 n2, let rs' := nextinstr (compare_floats (Vfloat n1) (Vfloat n2) rs) in - rs'#ZF = Val.of_bool (Float.cmp Ceq n1 n2 || negb (Float.ordered n1 n2)) - /\ rs'#CF = Val.of_bool (negb (Float.cmp Cge n1 n2)) + rs'#ZF = Val.of_bool (Float.cmp FCeq n1 n2 || negb (Float.ordered n1 n2)) + /\ rs'#CF = Val.of_bool (negb (Float.cmp FCge n1 n2)) /\ rs'#PF = Val.of_bool (negb (Float.ordered n1 n2)) /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. @@ -715,8 +715,8 @@ Qed. Lemma compare_floats32_spec: forall rs n1 n2, let rs' := nextinstr (compare_floats32 (Vsingle n1) (Vsingle n2) rs) in - rs'#ZF = Val.of_bool (Float32.cmp Ceq n1 n2 || negb (Float32.ordered n1 n2)) - /\ rs'#CF = Val.of_bool (negb (Float32.cmp Cge n1 n2)) + rs'#ZF = Val.of_bool (Float32.cmp FCeq n1 n2 || negb (Float32.ordered n1 n2)) + /\ rs'#CF = Val.of_bool (negb (Float32.cmp FCge n1 n2)) /\ rs'#PF = Val.of_bool (negb (Float32.ordered n1 n2)) /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. @@ -743,10 +743,10 @@ Definition eval_extcond (xc: extcond) (rs: regset) : option bool := end end. -Definition swap_floats {A: Type} (c: comparison) (n1 n2: A) : A := +Definition swap_floats {A: Type} (c: fp_comparison) (n1 n2: A) : A := match c with - | Clt | Cle => n2 - | Ceq | Cne | Cgt | Cge => n1 + | FClt | FCle | FCnotlt | FCnotle => n2 + | FCeq | FCne | FCgt | FCge | FCnotgt | FCnotge => n1 end. Lemma testcond_for_float_comparison_correct: @@ -778,38 +778,32 @@ Transparent Float.cmp Float.ordered. unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. - (* ge *) destruct (Float.cmp Cge n1 n2); auto. -Opaque Float.cmp Float.ordered. -Qed. - -Lemma testcond_for_neg_float_comparison_correct: - forall c n1 n2 rs, - eval_extcond (testcond_for_condition (Cnotcompf c)) - (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) - (Vfloat (swap_floats c n2 n1)) rs)) = - Some(negb(Float.cmp c n1 n2)). -Proof. - intros. - generalize (compare_floats_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)). - set (rs' := nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) - (Vfloat (swap_floats c n2 n1)) rs)). - intros [A [B [C D]]]. - unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. - destruct c; simpl. -- (* eq *) -Transparent Float.cmp Float.ordered. - unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. -- (* ne *) - unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. -- (* lt *) - rewrite <- (Float.cmp_swap Clt n2 n1). simpl. unfold Float.ordered. - destruct (Float.compare n2 n1) as [[]|]; reflexivity. -- (* le *) - rewrite <- (Float.cmp_swap Cge n1 n2). simpl. - destruct (Float.compare n1 n2) as [[]|]; auto. -- (* gt *) - unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. -- (* ge *) - destruct (Float.cmp Cge n1 n2); auto. +- (* notlt *) + replace (Float.cmp FCnotlt n1 n2) with (negb (Float.cmp FClt n1 n2)) by (symmetry; apply (Float.cmp_negate FClt)). + rewrite <- (Float.cmp_swap FCge n1 n2). + rewrite <- (Float.cmp_swap FCne n1 n2). + simpl. + rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq. + destruct (Float.cmp FClt n1 n2) eqn:LT; simpl. + destruct (Float.cmp FCeq n1 n2) eqn:EQ; simpl. + exfalso. eapply Float.cmp_lt_eq_false; eauto. + auto. + destruct (Float.cmp FCeq n1 n2); auto. +- (* notle *) + replace (Float.cmp FCnotle n1 n2) with (negb (Float.cmp FCle n1 n2)) by (symmetry; apply (Float.cmp_negate FCle)). + rewrite <- (Float.cmp_swap FCge n1 n2). simpl. + destruct (Float.cmp FCle n1 n2); auto. +- (* notgt *) + replace (Float.cmp FCnotgt n1 n2) with (negb (Float.cmp FCgt n1 n2)) by (symmetry; apply (Float.cmp_negate FCgt)). + rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. + destruct (Float.cmp FCgt n1 n2) eqn:GT; simpl. + destruct (Float.cmp FCeq n1 n2) eqn:EQ; simpl. + exfalso. eapply Float.cmp_gt_eq_false; eauto. + auto. + destruct (Float.cmp FCeq n1 n2); auto. +- (* notge *) + replace (Float.cmp FCnotge n1 n2) with (negb (Float.cmp FCge n1 n2)) by (symmetry; apply (Float.cmp_negate FCge)). + destruct (Float.cmp FCge n1 n2); auto. Opaque Float.cmp Float.ordered. Qed. @@ -823,7 +817,7 @@ Proof. intros. generalize (compare_floats32_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)). set (rs' := nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2)) - (Vsingle (swap_floats c n2 n1)) rs)). + (Vsingle (swap_floats c n2 n1)) rs)). intros [A [B [C D]]]. unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. destruct c; simpl. @@ -874,9 +868,36 @@ Transparent Float32.cmp Float32.ordered. unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. - (* ge *) destruct (Float32.cmp Cge n1 n2); auto. +- (* notlt *) + replace (Float32.cmp FCnotlt n1 n2) with (negb (Float32.cmp FClt n1 n2)) by (symmetry; apply (Float32.cmp_negate FClt)). + rewrite <- (Float32.cmp_swap FCge n1 n2). + rewrite <- (Float32.cmp_swap FCne n1 n2). + simpl. + rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq. + destruct (Float32.cmp FClt n1 n2) eqn:LT; simpl. + destruct (Float32.cmp FCeq n1 n2) eqn:EQ; simpl. + exfalso. eapply Float32.cmp_lt_eq_false; eauto. + auto. + destruct (Float32.cmp FCeq n1 n2); auto. +- (* notle *) + replace (Float32.cmp FCnotle n1 n2) with (negb (Float32.cmp FCle n1 n2)) by (symmetry; apply (Float32.cmp_negate FCle)). + rewrite <- (Float32.cmp_swap FCge n1 n2). simpl. + destruct (Float32.cmp FCle n1 n2); auto. +- (* notgt *) + replace (Float32.cmp FCnotgt n1 n2) with (negb (Float32.cmp FCgt n1 n2)) by (symmetry; apply (Float32.cmp_negate FCgt)). + rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. + destruct (Float32.cmp FCgt n1 n2) eqn:GT; simpl. + destruct (Float32.cmp FCeq n1 n2) eqn:EQ; simpl. + exfalso. eapply Float32.cmp_gt_eq_false; eauto. + auto. + destruct (Float32.cmp FCeq n1 n2); auto. +- (* notge *) + replace (Float32.cmp FCnotge n1 n2) with (negb (Float32.cmp FCge n1 n2)) by (symmetry; apply (Float32.cmp_negate FCge)). + destruct (Float32.cmp FCge n1 n2); auto. Opaque Float32.cmp Float32.ordered. Qed. + Remark swap_floats_commut: forall (A B: Type) c (f: A -> B) x y, swap_floats c (f x) (f y) = f (swap_floats c x y). Proof. @@ -983,15 +1004,6 @@ Proof. split. destruct (rs x); destruct (rs x0); simpl; auto. repeat rewrite swap_floats_commut. apply testcond_for_float_comparison_correct. intros. Simplifs. apply compare_floats_inv; auto with asmgen. -- (* notcompf *) - simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). - exists (nextinstr (compare_floats (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). - split. apply exec_straight_one. - destruct c0; simpl; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. - split. destruct (rs x); destruct (rs x0); simpl; auto. - repeat rewrite swap_floats_commut. apply testcond_for_neg_float_comparison_correct. - intros. Simplifs. apply compare_floats_inv; auto with asmgen. - (* compfs *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). @@ -1001,15 +1013,6 @@ Proof. split. destruct (rs x); destruct (rs x0); simpl; auto. repeat rewrite swap_floats_commut. apply testcond_for_float32_comparison_correct. intros. Simplifs. apply compare_floats32_inv; auto with asmgen. -- (* notcompfs *) - simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). - exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). - split. apply exec_straight_one. - destruct c0; simpl; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. - split. destruct (rs x); destruct (rs x0); simpl; auto. - repeat rewrite swap_floats_commut. apply testcond_for_neg_float32_comparison_correct. - intros. Simplifs. apply compare_floats32_inv; auto with asmgen. - (* maskzero *) simpl. rewrite (ireg_of_eq _ _ EQ). econstructor. split. apply exec_straight_one. simpl; eauto. auto. @@ -46,10 +46,8 @@ Inductive condition : Type := | Ccomplu (c: comparison) (**r unsigned 64-bit integer comparison *) | Ccomplimm (c: comparison) (n: int64) (**r signed 64-bit integer comparison with a constant *) | Ccompluimm (c: comparison) (n: int64) (**r unsigned 64-bit integer comparison with a constant *) - | Ccompf (c: comparison) (**r 64-bit floating-point comparison *) - | Cnotcompf (c: comparison) (**r negation of a floating-point comparison *) - | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) - | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *) + | Ccompf (c: fp_comparison) (**r 64-bit floating-point comparison *) + | Ccompfs (c: fp_comparison) (**r 32-bit floating-point comparison *) | Cmaskzero (n: int) (**r test [(arg & constant) == 0] *) | Cmasknotzero (n: int). (**r test [(arg & constant) != 0] *) @@ -174,7 +172,8 @@ Inductive operation : Type := Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. generalize Int.eq_dec Int64.eq_dec; intro. - assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. + assert (forall (x y: comparison), {x=y}+{x<>y}) by decide equality. + assert (forall (x y: fp_comparison), {x=y}+{x<>y}) by decide equality. decide equality. Defined. @@ -253,9 +252,7 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccomplimm c n, v1 :: nil => Val.cmpl_bool c v1 (Vlong n) | Ccompluimm c n, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong n) | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 - | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) | Cmaskzero n, v1 :: nil => Val.maskzero_bool v1 n | Cmasknotzero n, v1 :: nil => option_map negb (Val.maskzero_bool v1 n) | _, _ => None @@ -461,9 +458,7 @@ Definition type_of_condition (c: condition) : list typ := | Ccomplimm _ _ => Tlong :: nil | Ccompluimm _ _ => Tlong :: nil | Ccompf _ => Tfloat :: Tfloat :: nil - | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfs _ => Tsingle :: Tsingle :: nil - | Cnotcompfs _ => Tsingle :: Tsingle :: nil | Cmaskzero _ => Tint :: nil | Cmasknotzero _ => Tint :: nil end. @@ -775,10 +770,8 @@ Definition negate_condition (cond: condition): condition := | Ccomplu c => Ccomplu(negate_comparison c) | Ccomplimm c n => Ccomplimm (negate_comparison c) n | Ccompluimm c n => Ccompluimm (negate_comparison c) n - | Ccompf c => Cnotcompf c - | Cnotcompf c => Ccompf c - | Ccompfs c => Cnotcompfs c - | Cnotcompfs c => Ccompfs c + | Ccompf c => Ccompf (negate_fp_comparison c) + | Ccompfs c => Ccompfs (negate_fp_comparison c) | Cmaskzero n => Cmasknotzero n | Cmasknotzero n => Cmaskzero n end. @@ -796,10 +789,8 @@ Proof. repeat (destruct vl; auto). apply Val.negate_cmplu_bool. repeat (destruct vl; auto). apply Val.negate_cmpl_bool. repeat (destruct vl; auto). apply Val.negate_cmplu_bool. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto. - repeat (destruct vl; auto). - repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. + repeat (destruct vl; auto). apply Val.negate_cmpf_bool. + repeat (destruct vl; auto). apply Val.negate_cmpfs_bool. destruct vl; auto. destruct vl; auto. destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v n) as [[]|]; auto. Qed. @@ -1119,8 +1110,6 @@ Proof. - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; try discriminate; auto. - inv H3; try discriminate; auto. Qed. diff --git a/x86/PrintOp.ml b/x86/PrintOp.ml index faa5bb5f..356b2027 100644 --- a/x86/PrintOp.ml +++ b/x86/PrintOp.ml @@ -14,17 +14,9 @@ open Printf open Camlcoq -open Integers +open PrintAST open Op -let comparison_name = function - | Ceq -> "==" - | Cne -> "!=" - | Clt -> "<" - | Cle -> "<=" - | Cgt -> ">" - | Cge -> ">=" - let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> fprintf pp "%a %ss %a" reg r1 (comparison_name c) reg r2 @@ -43,13 +35,9 @@ let print_condition reg pp = function | (Ccompluimm(c, n), [r1]) -> fprintf pp "%a %slu %Lu" reg r1 (comparison_name c) (camlint64_of_coqint n) | (Ccompf c, [r1;r2]) -> - fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompf c, [r1;r2]) -> - fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sf %a" reg r1 (fp_comparison_name c) reg r2 | (Ccompfs c, [r1;r2]) -> - fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompfs c, [r1;r2]) -> - fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sfs %a" reg r1 (fp_comparison_name c) reg r2 | (Cmaskzero n, [r1]) -> fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n) | (Cmasknotzero n, [r1]) -> diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index a1583600..a9985528 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -412,10 +412,10 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) end. -Definition compf (c: comparison) (e1: expr) (e2: expr) := +Definition compf (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). -Definition compfs (c: comparison) (e1: expr) (e2: expr) := +Definition compfs (c: fp_comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). (** ** Integer conversions *) @@ -472,7 +472,7 @@ Nondetfunction floatofint (e: expr) := Definition intuoffloat (e: expr) := Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (CEcond (Ccompf FClt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index fdbadaa8..bfd5364c 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -816,9 +816,9 @@ Proof. constructor. auto. econstructor. eauto. econstructor. instantiate (1 := Vfloat fm). EvalOp. - eapply eval_Econdition with (va := Float.cmp Clt f fm). + eapply eval_Econdition with (va := Float.cmp FClt f fm). eauto with evalexpr. - destruct (Float.cmp Clt f fm) eqn:?. + destruct (Float.cmp FClt f fm) eqn:?. exploit Float.to_intu_to_int_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. exploit Float.to_intu_to_int_2; eauto. diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v index 1021a9c8..12a13499 100644 --- a/x86/ValueAOp.v +++ b/x86/ValueAOp.v @@ -27,9 +27,7 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Ccomplimm c n, v1 :: nil => cmpl_bool c v1 (L n) | Ccompluimm c n, v1 :: nil => cmplu_bool c v1 (L n) | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2 - | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 - | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) | Cmaskzero n, v1 :: nil => maskzero v1 n | Cmasknotzero n, v1 :: nil => cnot (maskzero v1 n) | _, _ => Bnone |