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

2 files changed, 38 insertions, 71 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 24dedc7..d86ff19 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, 0 if x >=u y
--       SOF = 1 if x <s y, 0 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 or unordered, 0 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 0bf030c..728617e 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.