From f995bde28d1098b51f42a38f3577b903d0420688 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 13 Jul 2013 14:02:07 +0000 Subject: More accurate model of condition register flags for ARM and IA32. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asm.v | 47 ++++++++++++++++++++-------------------- ia32/Asmgenproof1.v | 62 ++++++++++++----------------------------------------- 2 files changed, 38 insertions(+), 71 deletions(-) (limited to 'ia32') diff --git a/ia32/Asm.v b/ia32/Asm.v index 24dedc71..d86ff19f 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -48,11 +48,10 @@ Proof. decide equality. Defined. Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. Proof. decide equality. Defined. -(** Bits of the flags register. [SOF] is a pseudo-bit representing - the "xor" of the [OF] and [SF] bits. *) +(** Bits of the flags register. *) Inductive crbit: Type := - | ZF | CF | PF | SOF. + | ZF | CF | PF | SF | OF. (** All registers modeled here. *) @@ -304,22 +303,23 @@ Definition eval_addrmode (a: addrmode) (rs: regset) : val := (** Integer comparison between x and y: - ZF = 1 if x = y, 0 if x != y - CF = 1 if x =u y -- SOF = 1 if x =s y +- SF = 1 if x - y is negative, 0 if x - y is positive +- OF = 1 if x - y overflows (signed), 0 if not - PF is undefined - -SOF is (morally) the XOR of the SF and OF flags of the processor. *) +*) Definition compare_ints (x y: val) (rs: regset) (m: mem): regset := rs #ZF <- (Val.cmpu (Mem.valid_pointer m) Ceq x y) #CF <- (Val.cmpu (Mem.valid_pointer m) Clt x y) - #SOF <- (Val.cmp Clt x y) + #SF <- (Val.negative (Val.sub x y)) + #OF <- (Val.sub_overflow x y) #PF <- Vundef. (** Floating-point comparison between x and y: - ZF = 1 if x=y or unordered, 0 if x<>y - CF = 1 if x=y - PF = 1 if unordered, 0 if ordered. -- SOF is undefined +- SF and 0F are undefined *) Definition compare_floats (vx vy: val) (rs: regset) : regset := @@ -328,9 +328,10 @@ Definition compare_floats (vx vy: val) (rs: regset) : regset := rs #ZF <- (Val.of_bool (negb (Float.cmp Cne x y))) #CF <- (Val.of_bool (negb (Float.cmp Cge x y))) #PF <- (Val.of_bool (negb (Float.cmp Ceq x y || Float.cmp Clt x y || Float.cmp Cgt x y))) - #SOF <- Vundef + #SF <- Vundef + #OF <- Vundef | _, _ => - undef_regs (CR ZF :: CR CF :: CR PF :: CR SOF :: nil) rs + undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs end. (** Testing a condition *) @@ -368,24 +369,24 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool := | _, _ => None end | Cond_l => - match rs SOF with - | Vint n => Some (Int.eq n Int.one) - | _ => None + match rs OF, rs SF with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one) + | _, _ => None end | Cond_le => - match rs SOF, rs ZF with - | Vint s, Vint z => Some (Int.eq s Int.one || Int.eq z Int.one) - | _, _ => None + match rs OF, rs SF, rs ZF with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one) + | _, _, _ => None end | Cond_ge => - match rs SOF with - | Vint n => Some (Int.eq n Int.zero) - | _ => None + match rs OF, rs SF with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero) + | _, _ => None end | Cond_g => - match rs SOF, rs ZF with - | Vint s, Vint z => Some (Int.eq s Int.zero && Int.eq z Int.zero) - | _, _ => None + match rs OF, rs SF, rs ZF with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero) + | _, _, _ => None end | Cond_p => match rs PF with @@ -418,7 +419,7 @@ Definition nextinstr (rs: regset) := rs#PC <- (Val.add rs#PC Vone). Definition nextinstr_nf (rs: regset) : regset := - nextinstr (undef_regs (CR ZF :: CR CF :: CR PF :: CR SOF :: nil) rs). + nextinstr (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs). Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) := match label_pos lbl 0 c with diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 0bf030c4..728617ec 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -41,39 +41,6 @@ Proof. intro. simpl. ElimOrEq; auto. Qed. -(* -Lemma agree_undef_move: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, data_preg r = true -> r <> ST0 -> rs'#r = rs#r) -> - agree (undef_move ms) sp rs'. -Proof. - intros. destruct H. split. - rewrite H0; auto. congruence. auto. - intros. unfold undef_move. - destruct (In_dec mreg_eq r destroyed_at_move_regs). - rewrite Mach.undef_regs_same; auto. - rewrite Mach.undef_regs_other; auto. - assert (data_preg (preg_of r) = true /\ preg_of r <> ST0). - simpl in n. destruct r; simpl; auto; intuition congruence. - destruct H. rewrite H0; auto. -Qed. - -Lemma agree_set_undef_move_mreg: - forall ms sp rs r v rs', - agree ms sp rs -> - Val.lessdef v (rs'#(preg_of r)) -> - (forall r', data_preg r' = true /\ r' <> ST0 -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v (undef_move ms)) sp rs'. -Proof. - intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto. - eapply agree_undef_move; eauto. - intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). - congruence. auto. - intros. rewrite Pregmap.gso; auto. -Qed. -*) - (** Useful properties of the PC register. *) Lemma nextinstr_nf_inv: @@ -82,10 +49,7 @@ Lemma nextinstr_nf_inv: (nextinstr_nf rs)#r = rs#r. Proof. intros. unfold nextinstr_nf. rewrite nextinstr_inv. - simpl. repeat rewrite Pregmap.gso; auto. - red; intro; subst; contradiction. - red; intro; subst; contradiction. - red; intro; subst; contradiction. + simpl. repeat rewrite Pregmap.gso; auto; red; intro; subst; contradiction. red; intro; subst; contradiction. Qed. @@ -214,10 +178,8 @@ Proof. apply exec_straight_step with rs3 m. simpl. change (rs2 EAX) with (rs1 EAX). rewrite A. simpl. rewrite (Int.add_commut Int.zero tnm1). rewrite Int.add_zero. auto. auto. - apply exec_straight_step with rs4 m. simpl. - change (rs3 SOF) with (rs2 SOF). unfold rs2. rewrite nextinstr_inv; auto with asmgen. - unfold compare_ints. rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. - unfold Val.cmp. simpl. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto. + apply exec_straight_step with rs4 m. simpl. + rewrite Int.lt_sub_overflow. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto. apply exec_straight_one. auto. auto. split. unfold rs5. Simplifs. unfold rs4. rewrite nextinstr_inv; auto with asmgen. @@ -441,13 +403,15 @@ Lemma compare_ints_spec: let rs' := nextinstr (compare_ints v1 v2 rs m) in rs'#ZF = Val.cmpu (Mem.valid_pointer m) Ceq v1 v2 /\ rs'#CF = Val.cmpu (Mem.valid_pointer m) Clt v1 v2 - /\ rs'#SOF = Val.cmp Clt v1 v2 + /\ rs'#SF = Val.negative (Val.sub v1 v2) + /\ rs'#OF = Val.sub_overflow v1 v2 /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. intros. unfold rs'; unfold compare_ints. split. auto. split. auto. split. auto. + split. auto. intros. Simplifs. Qed. @@ -505,9 +469,11 @@ Lemma testcond_for_signed_comparison_correct: Proof. intros. generalize (compare_ints_spec rs v1 v2 m). set (rs' := nextinstr (compare_ints v1 v2 rs m)). - intros [A [B [C D]]]. + intros [A [B [C [D E]]]]. destruct v1; destruct v2; simpl in H; inv H. - unfold eval_testcond. rewrite A; rewrite B; rewrite C. unfold Val.cmp, Val.cmpu. + unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. + simpl. unfold Val.cmp, Val.cmpu. + rewrite Int.lt_sub_overflow. destruct c; simpl. destruct (Int.eq i i0); auto. destruct (Int.eq i i0); auto. @@ -525,8 +491,8 @@ Lemma testcond_for_unsigned_comparison_correct: Proof. intros. generalize (compare_ints_spec rs v1 v2 m). set (rs' := nextinstr (compare_ints v1 v2 rs m)). - intros [A [B [C D]]]. - unfold eval_testcond. rewrite A; rewrite B; rewrite C. unfold Val.cmpu, Val.cmp. + intros [A [B [C [D E]]]]. + unfold eval_testcond. rewrite A; rewrite B. unfold Val.cmpu, Val.cmp. destruct v1; destruct v2; simpl in H; inv H. (* int int *) destruct c; simpl; auto. @@ -706,11 +672,11 @@ Qed. Remark compare_floats_inv: forall vx vy rs r, - r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SOF -> + r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF -> compare_floats vx vy rs r = rs r. Proof. intros. - assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SOF :: nil) rs r = rs r). + assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs r = rs r). simpl. Simplifs. unfold compare_floats; destruct vx; destruct vy; auto. Simplifs. Qed. -- cgit