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 --- arm/Asm.v | 170 +++++++++++++------- arm/Asmgen.v | 84 +++++----- arm/Asmgenproof1.v | 434 ++++++++++++++++++++++++++++++++++++---------------- arm/PrintAsm.ml | 40 ++--- common/Values.v | 12 ++ ia32/Asm.v | 47 +++--- ia32/Asmgenproof1.v | 62 ++------ lib/Floats.v | 6 + lib/Integers.v | 127 ++++++++++++++- 9 files changed, 655 insertions(+), 327 deletions(-) diff --git a/arm/Asm.v b/arm/Asm.v index 769b3f99..43a14351 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -51,18 +51,10 @@ Proof. decide equality. Defined. (** Bits in the condition register. *) Inductive crbit: Type := - | CReq: crbit (**r equal *) - | CRne: crbit (**r not equal *) - | CRhs: crbit (**r unsigned higher or same *) - | CRlo: crbit (**r unsigned lower *) - | CRmi: crbit (**r negative *) - | CRpl: crbit (**r positive *) - | CRhi: crbit (**r unsigned higher *) - | CRls: crbit (**r unsigned lower or same *) - | CRge: crbit (**r signed greater or equal *) - | CRlt: crbit (**r signed less than *) - | CRgt: crbit (**r signed greater *) - | CRle: crbit. (**r signed less than or equal *) + | CN: crbit (**r negative *) + | CZ: crbit (**r zero *) + | CC: crbit (**r carry *) + | CV: crbit. (**r overflow *) Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}. Proof. decide equality. Defined. @@ -123,12 +115,26 @@ Inductive shift_addr : Type := | SAasr: ireg -> int -> shift_addr | SAror: ireg -> int -> shift_addr. +Inductive testcond : Type := + | TCeq: testcond (**r equal *) + | TCne: testcond (**r not equal *) + | TChs: testcond (**r unsigned higher or same *) + | TClo: testcond (**r unsigned lower *) + | TCmi: testcond (**r negative *) + | TCpl: testcond (**r positive *) + | TChi: testcond (**r unsigned higher *) + | TCls: testcond (**r unsigned lower or same *) + | TCge: testcond (**r signed greater or equal *) + | TClt: testcond (**r signed less than *) + | TCgt: testcond (**r signed greater *) + | TCle: testcond. (**r signed less than or equal *) + Inductive instruction : Type := (* Core instructions *) | Padd: ireg -> ireg -> shift_op -> instruction (**r integer addition *) | Pand: ireg -> ireg -> shift_op -> instruction (**r bitwise and *) | Pb: label -> instruction (**r branch to label *) - | Pbc: crbit -> label -> instruction (**r conditional branch to label *) + | Pbc: testcond -> label -> instruction (**r conditional branch to label *) | Pbsymb: ident -> signature -> instruction (**r branch to symbol *) | Pbreg: ireg -> signature -> instruction (**r computed branch *) | Pblsymb: ident -> signature -> instruction (**r branch and link to symbol *) @@ -143,7 +149,7 @@ Inductive instruction : Type := | Pldrsh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *) | Pmla: ireg -> ireg -> ireg -> ireg -> instruction (**r integer multiply-add *) | Pmov: ireg -> shift_op -> instruction (**r integer move *) - | Pmovc: crbit -> ireg -> shift_op -> instruction (**r integer conditional move *) + | Pmovc: testcond -> ireg -> shift_op -> instruction (**r integer conditional move *) | Pmul: ireg -> ireg -> ireg -> instruction (**r integer multiplication *) | Pmvn: ireg -> shift_op -> instruction (**r integer complement *) | Porr: ireg -> ireg -> shift_op -> instruction (**r bitwise or *) @@ -376,44 +382,102 @@ Definition exec_store (chunk: memory_chunk) (addr: val) (r: preg) | Some m' => Next (nextinstr rs) m' end. -(** Operations over condition bits. *) +(** Comparisons. *) Definition compare_int (rs: regset) (v1 v2: val) (m: mem) := - rs#CReq <- (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2) - #CRne <- (Val.cmpu (Mem.valid_pointer m) Cne v1 v2) - #CRhs <- (Val.cmpu (Mem.valid_pointer m) Cge v1 v2) - #CRlo <- (Val.cmpu (Mem.valid_pointer m) Clt v1 v2) - #CRmi <- Vundef - #CRpl <- Vundef - #CRhi <- (Val.cmpu (Mem.valid_pointer m) Cgt v1 v2) - #CRls <- (Val.cmpu (Mem.valid_pointer m) Cle v1 v2) - #CRge <- (Val.cmp Cge v1 v2) - #CRlt <- (Val.cmp Clt v1 v2) - #CRgt <- (Val.cmp Cgt v1 v2) - #CRle <- (Val.cmp Cle v1 v2). + rs#CN <- (Val.negative (Val.sub v1 v2)) + #CZ <- (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2) + #CC <- (Val.cmpu (Mem.valid_pointer m) Cge v1 v2) + #CV <- (Val.sub_overflow v1 v2). (** Semantics of [fcmpd] instruction: << -== EQ=1 NE=0 HS=1 LO=0 MI=0 PL=1 VS=0 VC=1 HI=0 LS=1 GE=1 LT=0 GT=0 LE=1 -< EQ=0 NE=1 HS=0 LO=1 MI=1 PL=0 VS=0 VC=1 HI=0 LS=1 GE=0 LT=1 GT=0 LE=1 -> EQ=0 NE=1 HS=1 LO=0 MI=0 PL=1 VS=0 VC=1 HI=1 LS=0 GE=1 LT=0 GT=1 LE=0 -unord EQ=0 NE=1 HS=1 LO=0 MI=0 PL=1 VS=1 VC=0 HI=1 LS=0 GE=0 LT=1 GT=0 LE=1 +== N=0 Z=1 C=1 V=0 +< N=1 Z=0 C=0 V=0 +> N=0 Z=0 C=1 V=0 +unord N=0 Z=0 C=1 V=1 >> *) Definition compare_float (rs: regset) (v1 v2: val) := - rs#CReq <- (Val.cmpf Ceq v1 v2) - #CRne <- (Val.cmpf Cne v1 v2) - #CRhs <- (Val.notbool (Val.cmpf Clt v1 v2)) (**r not lt *) - #CRlo <- (Val.cmpf Clt v1 v2) (**r lt *) - #CRmi <- (Val.cmpf Clt v1 v2) (**r lt *) - #CRpl <- (Val.notbool (Val.cmpf Clt v1 v2)) (**r not lt *) - #CRhi <- (Val.notbool (Val.cmpf Cle v1 v2)) (**r not le *) - #CRls <- (Val.cmpf Cle v1 v2) (**r le *) - #CRge <- (Val.cmpf Cge v1 v2) (**r ge *) - #CRlt <- (Val.notbool (Val.cmpf Cge v1 v2)) (**r not ge *) - #CRgt <- (Val.cmpf Cgt v1 v2) (**r gt *) - #CRle <- (Val.notbool (Val.cmpf Cgt v1 v2)). (**r not gt *) + match v1, v2 with + | Vfloat f1, Vfloat f2 => + rs#CN <- (Val.of_bool (Float.cmp Clt f1 f2)) + #CZ <- (Val.of_bool (Float.cmp Ceq f1 f2)) + #CC <- (Val.of_bool (negb (Float.cmp Clt f1 f2))) + #CV <- (Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2))) + | _, _ => + rs#CN <- Vundef + #CZ <- Vundef + #CC <- Vundef + #CV <- Vundef + end. + +(** Testing a condition *) + +Definition eval_testcond (c: testcond) (rs: regset) : option bool := + match c with + | TCeq => (**r equal *) + match rs CZ with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + | TCne => (**r not equal *) + match rs CZ with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TClo => (**r unsigned less than *) + match rs CC with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TCls => (**r unsigned less or equal *) + match rs CC, rs CZ with + | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one) + | _, _ => None + end + | TChs => (**r unsigned greater or equal *) + match rs CC with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + | TChi => (**r unsigned greater *) + match rs CC, rs CZ with + | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero) + | _, _ => None + end + | TClt => (**r signed less than *) + match rs CV, rs CN with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one) + | _, _ => None + end + | TCle => (**r signed less or equal *) + match rs CV, rs CN, rs CZ with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one) + | _, _, _ => None + end + | TCge => (**r signed greater or equal *) + match rs CV, rs CN with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero) + | _, _ => None + end + | TCgt => (**r signed greater *) + match rs CV, rs CN, rs CZ with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero) + | _, _, _ => None + end + | TCpl => (**r positive *) + match rs CN with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TCmi => (**r negative *) + match rs CN with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + end. (** Execution of a single instruction [i] in initial state [rs] and [m]. Return updated state. For instructions @@ -441,10 +505,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#r1 <- (Val.and rs#r2 (eval_shift_op so rs)))) m | Pb lbl => goto_label f lbl rs m - | Pbc bit lbl => - match rs#bit with - | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label f lbl rs m - | _ => Stuck + | Pbc cond lbl => + match eval_testcond cond rs with + | Some true => goto_label f lbl rs m + | Some false => Next (nextinstr rs) m + | None => Stuck end | Pbsymb id sg => Next (rs#PC <- (symbol_offset id Int.zero)) m @@ -474,12 +539,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#r1 <- (Val.add (Val.mul rs#r2 rs#r3) rs#r4))) m | Pmov r1 so => Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m - | Pmovc bit r1 so => - match rs#bit with - | Vint n => if Int.eq n Int.zero - then Next (nextinstr rs) m - else Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m - | _ => Next (nextinstr (rs#r1 <- Vundef)) m + | Pmovc cond r1 so => + match eval_testcond cond rs with + | Some true => Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m + | Some false => Next (nextinstr rs) m + | None => Next (nextinstr (rs#r1 <- Vundef)) m end | Pmul r1 r2 r3 => Next (nextinstr (rs#r1 <- (Val.mul rs#r2 rs#r3))) m diff --git a/arm/Asmgen.v b/arm/Asmgen.v index d160b2d2..66451490 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -189,58 +189,58 @@ Definition transl_cond Error(msg "Asmgen.transl_cond") end. -Definition crbit_for_signed_cmp (cmp: comparison) := +Definition cond_for_signed_cmp (cmp: comparison) := match cmp with - | Ceq => CReq - | Cne => CRne - | Clt => CRlt - | Cle => CRle - | Cgt => CRgt - | Cge => CRge + | Ceq => TCeq + | Cne => TCne + | Clt => TClt + | Cle => TCle + | Cgt => TCgt + | Cge => TCge end. -Definition crbit_for_unsigned_cmp (cmp: comparison) := +Definition cond_for_unsigned_cmp (cmp: comparison) := match cmp with - | Ceq => CReq - | Cne => CRne - | Clt => CRlo - | Cle => CRls - | Cgt => CRhi - | Cge => CRhs + | Ceq => TCeq + | Cne => TCne + | Clt => TClo + | Cle => TCls + | Cgt => TChi + | Cge => TChs end. -Definition crbit_for_float_cmp (cmp: comparison) := +Definition cond_for_float_cmp (cmp: comparison) := match cmp with - | Ceq => CReq - | Cne => CRne - | Clt => CRmi - | Cle => CRls - | Cgt => CRgt - | Cge => CRge + | Ceq => TCeq + | Cne => TCne + | Clt => TCmi + | Cle => TCls + | Cgt => TCgt + | Cge => TCge end. -Definition crbit_for_float_not_cmp (cmp: comparison) := +Definition cond_for_float_not_cmp (cmp: comparison) := match cmp with - | Ceq => CRne - | Cne => CReq - | Clt => CRpl - | Cle => CRhi - | Cgt => CRle - | Cge => CRlt + | Ceq => TCne + | Cne => TCeq + | Clt => TCpl + | Cle => TChi + | Cgt => TCle + | Cge => TClt end. -Definition crbit_for_cond (cond: condition) := +Definition cond_for_cond (cond: condition) := match cond with - | Ccomp cmp => crbit_for_signed_cmp cmp - | Ccompu cmp => crbit_for_unsigned_cmp cmp - | Ccompshift cmp s => crbit_for_signed_cmp cmp - | Ccompushift cmp s => crbit_for_unsigned_cmp cmp - | Ccompimm cmp n => crbit_for_signed_cmp cmp - | Ccompuimm cmp n => crbit_for_unsigned_cmp cmp - | Ccompf cmp => crbit_for_float_cmp cmp - | Cnotcompf cmp => crbit_for_float_not_cmp cmp - | Ccompfzero cmp => crbit_for_float_cmp cmp - | Cnotcompfzero cmp => crbit_for_float_not_cmp cmp + | Ccomp cmp => cond_for_signed_cmp cmp + | Ccompu cmp => cond_for_unsigned_cmp cmp + | Ccompshift cmp s => cond_for_signed_cmp cmp + | Ccompushift cmp s => cond_for_unsigned_cmp cmp + | Ccompimm cmp n => cond_for_signed_cmp cmp + | Ccompuimm cmp n => cond_for_unsigned_cmp cmp + | Ccompf cmp => cond_for_float_cmp cmp + | Cnotcompf cmp => cond_for_float_not_cmp cmp + | Ccompfzero cmp => cond_for_float_cmp cmp + | Cnotcompfzero cmp => cond_for_float_not_cmp cmp end. (** Translation of the arithmetic operation [r <- op(args)]. @@ -360,7 +360,7 @@ Definition transl_op do r <- ireg_of res; do r1 <- ireg_of a1; OK (Pcmp r1 (SOimm Int.zero) :: addimm IR14 r1 (Int.sub (Int.shl Int.one n) Int.one) - (Pmovc CRge IR14 (SOreg r1) :: + (Pmovc TCge IR14 (SOreg r1) :: Pmov r (SOasrimm IR14 n) :: k)) | Onegf, a1 :: nil => do r <- freg_of res; do r1 <- freg_of a1; @@ -399,7 +399,7 @@ Definition transl_op do r <- ireg_of res; transl_cond cmp args (Pmov r (SOimm Int.zero) :: - Pmovc (crbit_for_cond cmp) r (SOimm Int.one) :: + Pmovc (cond_for_cond cmp) r (SOimm Int.one) :: k) | _, _ => Error(msg "Asmgen.transl_op") @@ -599,7 +599,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mgoto lbl => OK (Pb lbl :: k) | Mcond cond args lbl => - transl_cond cond args (Pbc (crbit_for_cond cond) lbl :: k) + transl_cond cond args (Pbc (cond_for_cond cond) lbl :: k) | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k) diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 2f5f8680..d77006ad 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -536,39 +536,243 @@ Qed. Lemma compare_int_spec: forall rs v1 v2 m, let rs1 := nextinstr (compare_int rs v1 v2 m) in - rs1#CReq = (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2) - /\ rs1#CRne = (Val.cmpu (Mem.valid_pointer m) Cne v1 v2) - /\ rs1#CRhs = (Val.cmpu (Mem.valid_pointer m) Cge v1 v2) - /\ rs1#CRlo = (Val.cmpu (Mem.valid_pointer m) Clt v1 v2) - /\ rs1#CRhi = (Val.cmpu (Mem.valid_pointer m) Cgt v1 v2) - /\ rs1#CRls = (Val.cmpu (Mem.valid_pointer m) Cle v1 v2) - /\ rs1#CRge = (Val.cmp Cge v1 v2) - /\ rs1#CRlt = (Val.cmp Clt v1 v2) - /\ rs1#CRgt = (Val.cmp Cgt v1 v2) - /\ rs1#CRle = (Val.cmp Cle v1 v2) - /\ forall r', data_preg r' = true -> rs1#r' = rs#r'. + rs1#CN = Val.negative (Val.sub v1 v2) + /\ rs1#CZ = Val.cmpu (Mem.valid_pointer m) Ceq v1 v2 + /\ rs1#CC = Val.cmpu (Mem.valid_pointer m) Cge v1 v2 + /\ rs1#CV = Val.sub_overflow v1 v2. Proof. - intros. unfold rs1. intuition; try reflexivity. - unfold compare_int. Simpl. + intros. unfold rs1. intuition. +Qed. + +Lemma compare_int_inv: + forall rs v1 v2 m, + let rs1 := nextinstr (compare_int rs v1 v2 m) in + forall r', data_preg r' = true -> rs1#r' = rs#r'. +Proof. + intros. unfold rs1, compare_int. + repeat Simplif. +Qed. + +Lemma int_signed_eq: + forall x y, Int.eq x y = zeq (Int.signed x) (Int.signed y). +Proof. + intros. unfold Int.eq. unfold proj_sumbool. + destruct (zeq (Int.unsigned x) (Int.unsigned y)); + destruct (zeq (Int.signed x) (Int.signed y)); auto. + elim n. unfold Int.signed. rewrite e; auto. + elim n. apply Int.eqm_small_eq; auto with ints. + eapply Int.eqm_trans. apply Int.eqm_sym. apply Int.eqm_signed_unsigned. + rewrite e. apply Int.eqm_signed_unsigned. +Qed. + +Lemma int_not_lt: + forall x y, negb (Int.lt y x) = (Int.lt x y || Int.eq x y). +Proof. + intros. unfold Int.lt. rewrite int_signed_eq. unfold proj_sumbool. + destruct (zlt (Int.signed y) (Int.signed x)). + rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + destruct (zeq (Int.signed x) (Int.signed y)). + rewrite zlt_false. auto. omega. + rewrite zlt_true. auto. omega. +Qed. + +Lemma int_lt_not: + forall x y, Int.lt y x = negb (Int.lt x y) && negb (Int.eq x y). +Proof. + intros. rewrite <- negb_orb. rewrite <- int_not_lt. rewrite negb_involutive. auto. +Qed. + +Lemma int_not_ltu: + forall x y, negb (Int.ltu y x) = (Int.ltu x y || Int.eq x y). +Proof. + intros. unfold Int.ltu, Int.eq. + destruct (zlt (Int.unsigned y) (Int.unsigned x)). + rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + destruct (zeq (Int.unsigned x) (Int.unsigned y)). + rewrite zlt_false. auto. omega. + rewrite zlt_true. auto. omega. +Qed. + +Lemma int_ltu_not: + forall x y, Int.ltu y x = negb (Int.ltu x y) && negb (Int.eq x y). +Proof. + intros. rewrite <- negb_orb. rewrite <- int_not_ltu. rewrite negb_involutive. auto. +Qed. + +Lemma cond_for_signed_cmp_correct: + forall c v1 v2 rs m b, + Val.cmp_bool c v1 v2 = Some b -> + eval_testcond (cond_for_signed_cmp c) + (nextinstr (compare_int rs v1 v2 m)) = Some b. +Proof. + intros. generalize (compare_int_spec rs v1 v2 m). + set (rs' := nextinstr (compare_int rs v1 v2 m)). + intros [A [B [C D]]]. + destruct v1; destruct v2; simpl in H; inv H. + 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. + destruct (Int.lt i i0); auto. + rewrite int_not_lt. destruct (Int.lt i i0); simpl; destruct (Int.eq i i0); auto. + rewrite (int_lt_not i i0). destruct (Int.lt i i0); destruct (Int.eq i i0); reflexivity. + destruct (Int.lt i i0); reflexivity. +Qed. + +Lemma cond_for_unsigned_cmp_correct: + forall c v1 v2 rs m b, + Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 = Some b -> + eval_testcond (cond_for_unsigned_cmp c) + (nextinstr (compare_int rs v1 v2 m)) = Some b. +Proof. + intros. generalize (compare_int_spec rs v1 v2 m). + set (rs' := nextinstr (compare_int rs v1 v2 m)). + intros [A [B [C D]]]. + unfold eval_testcond. rewrite B; rewrite C. unfold Val.cmpu, Val.cmp. + destruct v1; destruct v2; simpl in H; inv H. +(* int int *) + destruct c; simpl; auto. + destruct (Int.eq i i0); reflexivity. + destruct (Int.eq i i0); auto. + destruct (Int.ltu i i0); auto. + rewrite (int_not_ltu i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); auto. + rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. + destruct (Int.ltu i i0); reflexivity. +(* int ptr *) + destruct (Int.eq i Int.zero) eqn:?; try discriminate. + destruct c; simpl in *; inv H1. + rewrite Heqb1; reflexivity. + rewrite Heqb1; reflexivity. +(* ptr int *) + destruct (Int.eq i0 Int.zero) eqn:?; try discriminate. + destruct c; simpl in *; inv H1. + rewrite Heqb1; reflexivity. + rewrite Heqb1; reflexivity. +(* ptr ptr *) + simpl. + fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *. + fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *. + destruct (eq_block b0 b1). + destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) && + Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1. + destruct c; simpl; auto. + destruct (Int.eq i i0); reflexivity. + destruct (Int.eq i i0); auto. + destruct (Int.ltu i i0); auto. + rewrite (int_not_ltu i i0). destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto. + rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. + destruct (Int.ltu i i0); reflexivity. + destruct (Mem.valid_pointer m b0 (Int.unsigned i) && + Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate. + destruct c; simpl in *; inv H1; reflexivity. Qed. Lemma compare_float_spec: + forall rs f1 f2, + let rs1 := nextinstr (compare_float rs (Vfloat f1) (Vfloat f2)) in + rs1#CN = Val.of_bool (Float.cmp Clt f1 f2) + /\ rs1#CZ = Val.of_bool (Float.cmp Ceq f1 f2) + /\ rs1#CC = Val.of_bool (negb (Float.cmp Clt f1 f2)) + /\ rs1#CV = Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2)). +Proof. + intros. intuition. +Qed. + +Lemma compare_float_inv: forall rs v1 v2, - let rs' := nextinstr (compare_float rs v1 v2) in - rs'#CReq = (Val.cmpf Ceq v1 v2) - /\ rs'#CRne = (Val.cmpf Cne v1 v2) - /\ rs'#CRmi = (Val.cmpf Clt v1 v2) - /\ rs'#CRpl = (Val.notbool (Val.cmpf Clt v1 v2)) - /\ rs'#CRhi = (Val.notbool (Val.cmpf Cle v1 v2)) - /\ rs'#CRls = (Val.cmpf Cle v1 v2) - /\ rs'#CRge = (Val.cmpf Cge v1 v2) - /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2)) - /\ rs'#CRgt = (Val.cmpf Cgt v1 v2) - /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2)) - /\ forall r', data_preg r' = true -> rs'#r' = rs#r'. + let rs1 := nextinstr (compare_float rs v1 v2) in + forall r', data_preg r' = true -> rs1#r' = rs#r'. Proof. - intros. unfold rs'. intuition; try reflexivity. - unfold compare_float. Simpl. + intros. unfold rs1, compare_float. + assert (nextinstr (rs#CN <- Vundef #CZ <- Vundef #CC <- Vundef #CV <- Vundef) r' = rs r'). + { repeat Simplif. } + destruct v1; destruct v2; auto. + repeat Simplif. +Qed. + +Lemma compare_float_nextpc: + forall rs v1 v2, + nextinstr (compare_float rs v1 v2) PC = Val.add (rs PC) Vone. +Proof. + intros. unfold compare_float. destruct v1; destruct v2; reflexivity. +Qed. + +Lemma cond_for_float_cmp_correct: + forall c n1 n2 rs, + eval_testcond (cond_for_float_cmp c) + (nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))) = + Some(Float.cmp c n1 n2). +Proof. + intros. + generalize (compare_float_spec rs n1 n2). + set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))). + intros [A [B [C D]]]. + unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. + destruct c; simpl. +(* eq *) + destruct (Float.cmp Ceq n1 n2); auto. +(* ne *) + rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto. +(* lt *) + destruct (Float.cmp Clt n1 n2); auto. +(* le *) + rewrite Float.cmp_le_lt_eq. + destruct (Float.cmp Clt n1 n2); destruct (Float.cmp Ceq n1 n2); auto. +(* gt *) + destruct (Float.cmp Ceq n1 n2) eqn:EQ; + destruct (Float.cmp Clt n1 n2) eqn:LT; + destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. + exfalso; eapply Float.cmp_gt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. +(* ge *) + rewrite Float.cmp_ge_gt_eq. + destruct (Float.cmp Ceq n1 n2) eqn:EQ; + destruct (Float.cmp Clt n1 n2) eqn:LT; + destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float.cmp_lt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. +Qed. + +Lemma cond_for_float_not_cmp_correct: + forall c n1 n2 rs, + eval_testcond (cond_for_float_not_cmp c) + (nextinstr (compare_float rs (Vfloat n1) (Vfloat n2)))= + Some(negb(Float.cmp c n1 n2)). +Proof. + intros. + generalize (compare_float_spec rs n1 n2). + set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))). + intros [A [B [C D]]]. + unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. + destruct c; simpl. +(* eq *) + destruct (Float.cmp Ceq n1 n2); auto. +(* ne *) + rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto. +(* lt *) + destruct (Float.cmp Clt n1 n2); auto. +(* le *) + rewrite Float.cmp_le_lt_eq. + destruct (Float.cmp Clt n1 n2) eqn:LT; destruct (Float.cmp Ceq n1 n2) eqn:EQ; auto. +(* gt *) + destruct (Float.cmp Ceq n1 n2) eqn:EQ; + destruct (Float.cmp Clt n1 n2) eqn:LT; + destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. + exfalso; eapply Float.cmp_gt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. +(* ge *) + rewrite Float.cmp_ge_gt_eq. + destruct (Float.cmp Ceq n1 n2) eqn:EQ; + destruct (Float.cmp Clt n1 n2) eqn:LT; + destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float.cmp_lt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. Qed. Ltac ArgsInv := @@ -591,119 +795,92 @@ Lemma transl_cond_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ match eval_condition cond (map rs (map preg_of args)) m with - | Some b => rs'#(CR (crbit_for_cond cond)) = Val.of_bool b + | Some b => eval_testcond (cond_for_cond cond) rs' = Some b | None => True end /\ forall r, data_preg r = true -> rs'#r = rs r. Proof. intros until c; intros TR. - assert (MATCH: forall v ob, - v = Val.of_optbool ob -> - match ob with Some b => v = Val.of_bool b | None => True end). - intros. subst v. destruct ob; auto. - assert (MATCH2: forall cmp v1 v2 v, - v = Val.cmpu (Mem.valid_pointer m) cmp v1 v2 -> - cmp = Ceq \/ cmp = Cne -> - match Val.cmp_bool cmp v1 v2 with - | Some b => v = Val.of_bool b - | None => True - end). - intros. destruct v1; simpl; auto; destruct v2; simpl; auto. - unfold Val.cmpu, Val.cmpu_bool in H. subst v. destruct H0; subst cmp; auto. - unfold transl_cond in TR; destruct cond; ArgsInv. - (* Ccomp *) - generalize (compare_int_spec rs (rs x) (rs x0) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto. + apply compare_int_inv. - (* Ccompu *) - generalize (compare_int_spec rs (rs x) (rs x0) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto. + apply compare_int_inv. - (* Ccompshift *) - generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - rewrite transl_shift_correct. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. rewrite transl_shift_correct. + destruct (Val.cmp_bool c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto. + apply compare_int_inv. - (* Ccompushift *) - generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - rewrite transl_shift_correct. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. rewrite transl_shift_correct. + destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto. + apply compare_int_inv. - (* Ccompimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs (rs x) (Vint i) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. apply exec_straight_one. simpl. eauto. auto. + split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto. + apply compare_int_inv. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - generalize (compare_int_spec rs' (rs x) (Vint i) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. rewrite Q. rewrite R; eauto with asmgen. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - intros. rewrite C; auto with asmgen. + split. rewrite <- R by (eauto with asmgen). + destruct (Val.cmp_bool c0 (rs' x) (Vint i)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto. + intros. rewrite compare_int_inv by auto. auto with asmgen. - (* Ccompuimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs (rs x) (Vint i) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. apply exec_straight_one. simpl. eauto. auto. + split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto. + apply compare_int_inv. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - generalize (compare_int_spec rs' (rs x) (Vint i) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. rewrite Q. rewrite R; eauto with asmgen. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - intros. rewrite C; auto with asmgen. + split. rewrite <- R by (eauto with asmgen). + destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs' x) (Vint i)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto. + intros. rewrite compare_int_inv by auto. auto with asmgen. - (* Ccompf *) - generalize (compare_float_spec rs (rs x) (rs x0)). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. case c0; apply MATCH; assumption. - auto. + split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. + split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto. + destruct (rs x); try discriminate. destruct (rs x0); try discriminate. + simpl in CMP. inv CMP. apply cond_for_float_cmp_correct. + apply compare_float_inv. - (* Cnotcompf *) - generalize (compare_float_spec rs (rs x) (rs x0)). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1. - destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. - auto. + split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. + split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto. + destruct (rs x); try discriminate. destruct (rs x0); try discriminate. + simpl in CMP. inv CMP. +Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct. + exact I. + apply compare_float_inv. - (* Ccompfzero *) - generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. case c0; apply MATCH; assumption. - auto. -- (* Cnotcompf *) - generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). + split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. + split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto. + destruct (rs x); try discriminate. + simpl in CMP. inv CMP. apply cond_for_float_cmp_correct. + apply compare_float_inv. +- (* Cnotcompfzero *) econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1. - destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. - auto. + split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. + split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto. + destruct (rs x); try discriminate. simpl in CMP. inv CMP. +Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct. + exact I. + apply compare_float_inv. Qed. (** Translation of arithmetic operations. *) @@ -788,8 +965,7 @@ Proof. set (islt := Int.lt n Int.zero) in *. set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero) m)). assert (OTH1: forall r', data_preg r' = true -> rs1#r' = rs#r'). - generalize (compare_int_spec rs (Vint n) (Vint Int.zero) m). - fold rs1. intros [A B]. intuition. + { apply compare_int_inv; auto. } exploit (addimm_correct IR14 x0 (Int.sub (Int.shl Int.one i) Int.one)). intros [rs2 [EXEC2 [RES2 OTH2]]]. set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))). @@ -799,18 +975,19 @@ Proof. simpl. rewrite ARG1. auto. auto. eapply exec_straight_trans. eexact EXEC2. apply exec_straight_two with rs3 m. - simpl. rewrite OTH2; eauto with asmgen. - change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)). - unfold Val.cmp, Val.cmp_bool. change (Int.cmp Cge n Int.zero) with (negb islt). - rewrite OTH2; eauto with asmgen. rewrite OTH1. rewrite ARG1. - unfold rs3. case islt; reflexivity. - rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen. - auto. - unfold rs3. destruct islt; auto. auto. - split. unfold rs4; Simpl. unfold rs3. destruct islt. - Simpl. rewrite RES2. unfold rs1. Simpl. - Simpl. congruence. - intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. + unfold exec_instr. + assert (TC: eval_testcond TCge rs2 = Some (negb islt)). + { simpl. rewrite ! OTH2 by auto with asmgen. simpl. + rewrite Int.lt_sub_overflow. fold islt. destruct islt; auto. } + rewrite TC. simpl. rewrite OTH2 by eauto with asmgen. rewrite OTH1. rewrite ARG1. + unfold rs3; destruct islt; reflexivity. + rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen. + reflexivity. + unfold rs3; destruct islt; reflexivity. + reflexivity. + split. unfold rs4; Simpl. unfold rs3. destruct islt. + Simpl. rewrite RES2. unfold rs1. Simpl. Simpl. congruence. + intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. (* intoffloat *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. Transparent destroyed_by_op. @@ -848,25 +1025,22 @@ Proof. rewrite (ireg_of_eq _ _ EQ). exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. set (rs2 := nextinstr (rs1#x <- (Vint Int.zero))). - set (rs3 := nextinstr (match rs2#(crbit_for_cond cmp) with - | Vint n => if Int.eq n Int.zero then rs2 else rs2#x <- Vone - | _ => rs2#x <- Vundef - end)). + set (rs3 := nextinstr (match eval_testcond (cond_for_cond cmp) rs2 with + | Some true => rs2 # x <- (Vint Int.one) + | Some false => rs2 + | None => rs2 # x <- Vundef end)). exists rs3; split. eapply exec_straight_trans. eexact A. apply exec_straight_two with rs2 m. auto. - simpl. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto. - auto. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto. - split. unfold rs3. Simpl. - replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)). - destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *. - rewrite B. simpl. rewrite Int.eq_false. Simpl. apply Int.one_not_zero. - rewrite B. simpl. rewrite Int.eq_true. unfold rs2. Simpl. - auto. - destruct cmp; reflexivity. + simpl. unfold rs3. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; auto. + auto. unfold rs3. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; auto. + split. destruct (eval_condition cmp rs ## (preg_of ## args) m) as [b|]; simpl; auto. + unfold rs3. + change (eval_testcond (cond_for_cond cmp) rs2) with (eval_testcond (cond_for_cond cmp) rs1). rewrite B. + Simpl. destruct b. Simpl. unfold rs2. Simpl. intros. transitivity (rs2 r). - unfold rs3. destruct (rs2 (crbit_for_cond cmp)); Simpl. destruct (Int.eq i Int.zero); auto; Simpl. - unfold rs2. Simpl. + unfold rs3. Simpl. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; Simpl; auto. + unfold rs2. Simpl. Qed. (** Translation of loads and stores. *) diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 3740c1f9..d700326b 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -93,18 +93,18 @@ let preg oc = function | _ -> assert false let condition_name = function - | CReq -> "eq" - | CRne -> "ne" - | CRhs -> "hs" - | CRlo -> "lo" - | CRmi -> "mi" - | CRpl -> "pl" - | CRhi -> "hi" - | CRls -> "ls" - | CRge -> "ge" - | CRlt -> "lt" - | CRgt -> "gt" - | CRle -> "le" + | TCeq -> "eq" + | TCne -> "ne" + | TChs -> "hs" + | TClo -> "lo" + | TCmi -> "mi" + | TCpl -> "pl" + | TChi -> "hi" + | TCls -> "ls" + | TCge -> "ge" + | TClt -> "lt" + | TCgt -> "gt" + | TCle -> "le" (* Names of sections *) @@ -744,12 +744,6 @@ let rec print_instructions oc instrs = end; print_instructions oc il -(* Base-2 log of a Caml integer *) - -let rec log2 n = - assert (n > 0); - if n = 1 then 0 else 1 + log2 (n lsr 1) - let print_function oc name fn = Hashtbl.clear current_function_labels; reset_constants(); @@ -760,8 +754,8 @@ let print_function oc name fn = | _ -> Section_text in section oc text; let alignment = - match !Clflags.option_falignfunctions with Some n -> log2 n | None -> 2 in - fprintf oc " .align %d\n" alignment; + match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in + fprintf oc " .balign %d\n" alignment; if not (C2C.atom_is_static name) then fprintf oc " .global %a\n" print_symb name; fprintf oc "%a:\n" print_symb name; @@ -815,11 +809,11 @@ let print_var oc name v = | _ -> Section_data true and align = match C2C.atom_alignof name with - | Some a -> log2 a - | None -> 3 (* 8-alignment is a safe default *) + | Some a -> a + | None -> 8 (* 8-alignment is a safe default *) in section oc sec; - fprintf oc " .align %d\n" align; + fprintf oc " .balign %d\n" align; if not (C2C.atom_is_static name) then fprintf oc " .global %a\n" print_symb name; fprintf oc "%a:\n" print_symb name; diff --git a/common/Values.v b/common/Values.v index b937071c..05749b7f 100644 --- a/common/Values.v +++ b/common/Values.v @@ -262,6 +262,18 @@ Definition add_carry (v1 v2 cin: val): val := | _, _, _ => Vundef end. +Definition sub_overflow (v1 v2: val) : val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.sub_overflow n1 n2 Int.zero) + | _, _ => Vundef + end. + +Definition negative (v: val) : val := + match v with + | Vint n => Vint (Int.negative n) + | _ => Vundef + end. + Definition and (v1 v2: val): val := match v1, v2 with | Vint n1, Vint n2 => Vint(Int.and n1 n2) 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. diff --git a/lib/Floats.v b/lib/Floats.v index 7ae1705c..94c19d25 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -453,6 +453,12 @@ Proof. now apply cmp_le_lt_eq. Qed. +Theorem cmp_lt_gt_false: + forall f1 f2, cmp Clt f1 f2 = true -> cmp Cgt f1 f2 = true -> False. +Proof. + unfold cmp; intros; destruct (order_float f1 f2) as [ [] | ]; discriminate. +Qed. + (** Properties of conversions to/from in-memory representation. The double-precision conversions are bijective (one-to-one). The single-precision conversions lose precision exactly diff --git a/lib/Integers.v b/lib/Integers.v index 5eb4c82d..49fa48fa 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -257,11 +257,6 @@ Definition divu (x y: int) : int := Definition modu (x y: int) : int := repr ((unsigned x) mod (unsigned y)). -Definition add_carry (x y cin: int): int := - if zlt (unsigned x + unsigned y + unsigned cin) modulus - then zero - else one. - (** Bitwise boolean operations. *) Definition and (x y: int): int := repr (Z.land (unsigned x) (unsigned y)). @@ -291,10 +286,30 @@ Definition rolm (x a m: int): int := and (rol x a) m. Definition shrx (x y: int): int := divs x (shl one y). +(** Condition flags *) + +Definition negative (x: int): int := + if lt x zero then one else zero. + +Definition add_carry (x y cin: int): int := + if zlt (unsigned x + unsigned y + unsigned cin) modulus then zero else one. + +Definition add_overflow (x y cin: int): int := + let s := signed x + signed y + signed cin in + if zle min_signed s && zle s max_signed then zero else one. + +Definition sub_borrow (x y bin: int): int := + if zlt (unsigned x - unsigned y - unsigned bin) 0 then one else zero. + +Definition sub_overflow (x y bin: int): int := + let s := signed x - signed y - signed bin in + if zle min_signed s && zle s max_signed then zero else one. + (** [shr_carry x y] is 1 if [x] is negative and at least one 1 bit is shifted away. *) -Definition shr_carry (x y: int) := - if lt x zero && negb (eq (and x (sub (shl one y) one)) zero) then one else zero. +Definition shr_carry (x y: int) : int := + if lt x zero && negb (eq (and x (sub (shl one y) one)) zero) + then one else zero. (** Zero and sign extensions *) @@ -882,7 +897,7 @@ Proof. unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r. rewrite unsigned_repr_eq. generalize (unsigned_range x) (unsigned_range y). intros. - destruct (zlt (unsigned x + unsigned y) modulus). + destruct (zlt (unsigned x + unsigned y) modulus). rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. rewrite unsigned_one. apply Zmod_unique with 1. omega. omega. Qed. @@ -983,6 +998,21 @@ Proof. apply eqm_sub; apply eqm_sym; apply eqm_signed_unsigned. Qed. +Theorem unsigned_sub_borrow: + forall x y, + unsigned (sub x y) = unsigned x - unsigned y + unsigned (sub_borrow x y zero) * modulus. +Proof. + intros. + unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Zminus_0_r. + rewrite unsigned_repr_eq. + generalize (unsigned_range x) (unsigned_range y). intros. + destruct (zlt (unsigned x - unsigned y) 0). + rewrite unsigned_one. apply Zmod_unique with (-1). omega. omega. + rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. +Qed. + + + (** ** Properties of multiplication *) Theorem mul_commut: forall x y, mul x y = mul y x. @@ -1783,6 +1813,16 @@ Proof. bit_solve. destruct (testbit x i); auto. Qed. +Lemma unsigned_not: + forall x, unsigned (not x) = max_unsigned - unsigned x. +Proof. + intros. transitivity (unsigned (repr(-unsigned x - 1))). + f_equal. bit_solve. rewrite testbit_repr; auto. symmetry. apply Z_one_complement. omega. + rewrite unsigned_repr_eq. apply Zmod_unique with (-1). + unfold max_unsigned. omega. + generalize (unsigned_range x). unfold max_unsigned. omega. +Qed. + Theorem not_neg: forall x, not x = add (neg x) mone. Proof. @@ -1807,6 +1847,23 @@ Proof. exists (-1). ring. Qed. +Theorem sub_borrow_add_carry: + forall x y b, + b = zero \/ b = one -> + sub_borrow x y b = xor (add_carry x (not y) (xor b one)) one. +Proof. + intros. unfold sub_borrow, add_carry. rewrite unsigned_not. + replace (unsigned (xor b one)) with (1 - unsigned b). + destruct (zlt (unsigned x - unsigned y - unsigned b)). + rewrite zlt_true. rewrite xor_zero_l; auto. + unfold max_unsigned; omega. + rewrite zlt_false. rewrite xor_idem; auto. + unfold max_unsigned; omega. + destruct H; subst b. + rewrite xor_zero_l. rewrite unsigned_one, unsigned_zero; auto. + rewrite xor_idem. rewrite unsigned_one, unsigned_zero; auto. +Qed. + (** Connections between [add] and bitwise logical operations. *) Lemma Z_add_is_or: @@ -3382,6 +3439,23 @@ Proof. generalize wordsize_max_unsigned; omega. Qed. +Theorem shr_lt_zero: + forall x, + shr x (repr (zwordsize - 1)) = if lt x zero then mone else zero. +Proof. + intros. apply same_bits_eq; intros. + rewrite bits_shr; auto. + rewrite unsigned_repr. + transitivity (testbit x (zwordsize - 1)). + f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); omega. + rewrite sign_bit_of_unsigned. + unfold lt. rewrite signed_zero. unfold signed. + destruct (zlt (unsigned x) half_modulus). + rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); omega. + rewrite zlt_true. rewrite bits_mone; auto. generalize (unsigned_range x); omega. + generalize wordsize_max_unsigned; omega. +Qed. + Theorem ltu_range_test: forall x y, ltu x y = true -> unsigned y <= max_signed -> @@ -3393,6 +3467,43 @@ Proof. generalize (unsigned_range x). omega. omega. Qed. +Theorem lt_sub_overflow: + forall x y, + xor (sub_overflow x y zero) (negative (sub x y)) = if lt x y then one else zero. +Proof. + intros. unfold negative, sub_overflow, lt. rewrite sub_signed. + rewrite signed_zero. rewrite Zminus_0_r. + generalize (signed_range x) (signed_range y). + set (X := signed x); set (Y := signed y). intros RX RY. + unfold min_signed, max_signed in *. + generalize half_modulus_pos half_modulus_modulus; intros HM MM. + destruct (zle 0 (X - Y)). +- unfold proj_sumbool at 1; rewrite zle_true at 1 by omega. simpl. + rewrite (zlt_false _ X) by omega. + destruct (zlt (X - Y) half_modulus). + + unfold proj_sumbool; rewrite zle_true by omega. + rewrite signed_repr. rewrite zlt_false by omega. apply xor_idem. + unfold min_signed, max_signed; omega. + + unfold proj_sumbool; rewrite zle_false by omega. + replace (signed (repr (X - Y))) with (X - Y - modulus). + rewrite zlt_true by omega. apply xor_idem. + rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y). + rewrite zlt_false; auto. + symmetry. apply Zmod_unique with 0; omega. +- unfold proj_sumbool at 2. rewrite zle_true at 1 by omega. rewrite andb_true_r. + rewrite (zlt_true _ X) by omega. + destruct (zlt (X - Y) (-half_modulus)). + + unfold proj_sumbool; rewrite zle_false by omega. + replace (signed (repr (X - Y))) with (X - Y + modulus). + rewrite zlt_false by omega. apply xor_zero. + rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y + modulus). + rewrite zlt_true by omega; auto. + symmetry. apply Zmod_unique with (-1); omega. + + unfold proj_sumbool; rewrite zle_true by omega. + rewrite signed_repr. rewrite zlt_true by omega. apply xor_zero_l. + unfold min_signed, max_signed; omega. +Qed. + (** Non-overlapping test *) Definition no_overlap (ofs1: int) (sz1: Z) (ofs2: int) (sz2: Z) : bool := -- cgit